Theorem: Nat.log_mul_add (Lib.lean)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply add_le_add _ (zero_le _)
State after:
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ b ≤ b * n

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

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

State before:
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ b ≤ b * n

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

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

case h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ?b ≤ b * n

case b
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ℕ

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

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

State before:
case h₁
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ b = ?b

case h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ?b ≤ b * n

case b
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ℕ

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

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

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

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

State before:
case h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ b * 1 ≤ b * n

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

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

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

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

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

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

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

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

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

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

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

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

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

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply Eq.trans
State after:
case a.h₂.a.h.a.h₁
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ (b * n + c) / b = ?a.h₂.a.h.a.b✝

case a.h₂.a.h.a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ?a.h₂.a.h.a.b✝ = n

case a.h₂.a.h.a.b
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ℕ

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

State before:
case a.h₂.a.h.a.h₁
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ (b * n + c) / b = ?a.h₂.a.h.a.b✝

case a.h₂.a.h.a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ?a.h₂.a.h.a.b✝ = n

case a.h₂.a.h.a.b
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ℕ

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply Nat.mul_add_div (lt_trans zero_lt_one hb)
State after:
case a.h₂.a.h.a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ n + c / b = n

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

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

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply congrArg _ (Nat.div_eq_of_lt hc)
State after:
case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)

State before:
case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply le_trans
State after:
case a.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ ?a.b✝

case a.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ?a.b✝ ≤ log b (b * n + c)

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

State before:
case a.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ ?a.b✝

case a.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ?a.b✝ ≤ log b (b * n + c)

case a.b
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ℕ
Tactic:
rw [← Nat.log_mul hb hn]
State after:
case a.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b (b * n) ≤ log b (b * n + c)

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

State before:
case a.a.h
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ b * n ≤ b * n + c
Tactic:
apply le_add_right
State after:
no goals