α : Type u
β : Type ?u.222007
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (∑ i in range n, a / b ^ i) * (b - 1) ≤ a * b
α : Type u
β : Type ?u.222007
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i in range n, a / b ^ i ≤ a * b / (b - 1)
refine' (Nat.le_div_iff_mul_le <| tsub_pos_of_lt hb).2 _
case zero
α : Type u
β : Type ?u.222007
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ (∑ i in range zero, a / b ^ i) * (b - 1) ≤ a * b

case succ
α : Type u
β : Type ?u.222007
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (∑ i in range (succ n), a / b ^ i) * (b - 1) ≤ a * b
α : Type u
β : Type ?u.222007
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (∑ i in range n, a / b ^ i) * (b - 1) ≤ a * b
cases' n with n
case succ
α : Type u
β : Type ?u.222007
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (b - 1) * ∑ i in range (succ n), a / b ^ i ≤ a * b
case succ
α : Type u
β : Type ?u.222007
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (∑ i in range (succ n), a / b ^ i) * (b - 1) ≤ a * b
rw [mul_comm]
no goals
case succ
α : Type u
β : Type ?u.222007
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (b - 1) * ∑ i in range (succ n), a / b ^ i ≤ a * b
exact (Nat.pred_mul_geom_sum_le a b n).trans tsub_le_self
case zero
α : Type u
β : Type ?u.222007
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a * b
case zero
α : Type u
β : Type ?u.222007
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ (∑ i in range zero, a / b ^ i) * (b - 1) ≤ a * b
rw [sum_range_zero, zero_mul]
no goals
case zero
α : Type u
β : Type ?u.222007
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a * b
exact Nat.zero_le _