Theorem: Nat.log_mul (Lib.lean)

State before:
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n) = log b n + 1
Tactic:
apply le_antisymm
State after:
case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n) ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)

State before:
case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n) ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply le_of_eq_of_le
State after:
case a.h₁
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n) = ?a.b✝

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ ?a.b✝ ≤ log b n + 1

case a.b
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ ℕ

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)

State before:
case a.h₁
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n) = ?a.b✝

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ ?a.b✝ ≤ log b n + 1

case a.b
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ ℕ

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply Nat.log_of_one_lt_of_le hb
State after:
case a.h₁
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ≤ b * n

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) + 1 ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)

State before:
case a.h₁
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ≤ b * n

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) + 1 ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply le_of_eq_of_le
State after:
case a.h₁.h₁
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b = ?a.h₁.b✝

case a.h₁.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ ?a.h₁.b✝ ≤ b * n

case a.h₁.b
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ ℕ

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) + 1 ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)

State before:
case a.h₁.h₁
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b = ?a.h₁.b✝

case a.h₁.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ ?a.h₁.b✝ ≤ b * n

case a.h₁.b
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ ℕ

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) + 1 ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply (mul_one _).symm
State after:
case a.h₁.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b * 1 ≤ b * n

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) + 1 ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)

State before:
case a.h₁.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b * 1 ≤ b * n

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) + 1 ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply mul_le_mul (le_refl _) hn (zero_le _) (zero_le _)
State after:
case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) + 1 ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)

State before:
case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) + 1 ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply Nat.succ_le_succ
State after:
case a.h₂.a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) ≤ log b n

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)

State before:
case a.h₂.a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) ≤ log b n

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply Nat.log_mono_right
State after:
case a.h₂.a.h
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b * n / b ≤ n

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)

State before:
case a.h₂.a.h
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b * n / b ≤ n

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply le_of_eq
State after:
case a.h₂.a.h.a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b * n / b = n

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)

State before:
case a.h₂.a.h.a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b * n / b = n

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
rw [Nat.mul_div_right _ (lt_trans zero_lt_one hb)]
State after:
case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)

State before:
case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply Nat.le_log_of_pow_le hb
State after:
case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ^ (log b n + 1) ≤ b * n

State before:
case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ^ (log b n + 1) ≤ b * n
Tactic:
rw [Nat.pow_succ, mul_comm]
State after:
case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b * b ^ log b n ≤ b * n

State before:
case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b * b ^ log b n ≤ b * n
Tactic:
apply mul_le_mul
State after:
case a.h₁
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ≤ b

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ^ log b n ≤ n

case a.c0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b ^ log b n

case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b

State before:
case a.h₁
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ≤ b

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ^ log b n ≤ n

case a.c0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b ^ log b n

case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b
Tactic:
apply le_refl
State after:
case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ^ log b n ≤ n

case a.c0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b ^ log b n

case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b

State before:
case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ^ log b n ≤ n

case a.c0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b ^ log b n

case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b
Tactic:
apply Nat.pow_log_le_self
State after:
case a.h₂.hx
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ n ≠ 0

case a.c0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b ^ log b n

case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b

State before:
case a.h₂.hx
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ n ≠ 0

case a.c0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b ^ log b n

case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b
Tactic:
apply ne_of_lt' (Nat.lt_of_succ_le hn)
State after:
case a.c0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b ^ log b n

case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b

State before:
case a.c0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b ^ log b n

case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b
Tactic:
apply zero_le
State after:
case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b

State before:
case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b
Tactic:
apply zero_le
State after:
no goals