[GOAL]
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
⊢ ∑ i in range (n + 1), x ^ i = x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
simp only [mul_sum, ← pow_succ, sum_range_succ', pow_zero]
[GOAL]
α : Type u
inst✝ : Semiring α
x : α
⊢ ∑ i in range 1, x ^ i = 1
[PROOFSTEP]
simp [geom_sum_succ']
[GOAL]
α : Type u
inst✝ : Semiring α
x : α
⊢ ∑ i in range 2, x ^ i = x + 1
[PROOFSTEP]
simp [geom_sum_succ']
[GOAL]
α : Type u
inst✝ : Semiring α
⊢ ∑ i in range 0, 0 ^ i = if 0 = 0 then 0 else 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : Semiring α
⊢ ∑ i in range 1, 0 ^ i = if 1 = 0 then 0 else 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : Semiring α
n : ℕ
⊢ ∑ i in range (n + 2), 0 ^ i = if n + 2 = 0 then 0 else 1
[PROOFSTEP]
rw [geom_sum_succ']
[GOAL]
α : Type u
inst✝ : Semiring α
n : ℕ
⊢ 0 ^ (n + 1) + ∑ i in range (n + 1), 0 ^ i = if n + 2 = 0 then 0 else 1
[PROOFSTEP]
simp [zero_geom_sum]
[GOAL]
α : Type u
inst✝ : Semiring α
n : ℕ
⊢ ∑ i in range n, 1 ^ i = ↑n
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
⊢ op (∑ i in range n, x ^ i) = ∑ i in range n, op x ^ i
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : Semiring α
x y : α
n : ℕ
⊢ ∑ i in range n, op y ^ (n - 1 - i) * op x ^ i = ∑ i in range n, op y ^ i * op x ^ (n - 1 - i)
[PROOFSTEP]
rw [← sum_range_reflect]
[GOAL]
α : Type u
inst✝ : Semiring α
x y : α
n : ℕ
⊢ ∑ j in range n, op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = ∑ i in range n, op y ^ i * op x ^ (n - 1 - i)
[PROOFSTEP]
refine' sum_congr rfl fun j j_in => _
[GOAL]
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j ∈ range n
⊢ op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)
[PROOFSTEP]
rw [mem_range, Nat.lt_iff_add_one_le] at j_in 
[GOAL]
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j + 1 ≤ n
⊢ op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j + 1 ≤ n
⊢ n - 1 - (n - 1 - j) = j
[PROOFSTEP]
apply tsub_tsub_cancel_of_le
[GOAL]
case e_a.e_a.h
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j + 1 ≤ n
⊢ j ≤ n - 1
[PROOFSTEP]
exact le_tsub_of_add_le_right j_in
[GOAL]
α : Type u
inst✝ : Semiring α
x : α
n i : ℕ
x✝ : i ∈ range n
⊢ x ^ i * 1 ^ (n - 1 - i) = x ^ i
[PROOFSTEP]
rw [one_pow, mul_one]
[GOAL]
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
⊢ (∑ i in range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
[PROOFSTEP]
let f : ℕ → ℕ → α := fun m i : ℕ =>
  (x + y) ^ i *
    y ^
      (m - 1 - i)
        -- porting note: adding `hf` here, because below in two places `dsimp [f]` didn't work
[GOAL]
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i in range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
[PROOFSTEP]
have hf : ∀ m i : ℕ, f m i = (x + y) ^ i * y ^ (m - 1 - i) := by simp only [ge_iff_le, tsub_le_iff_right, forall_const]
[GOAL]
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
⊢ ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
[PROOFSTEP]
simp only [ge_iff_le, tsub_le_iff_right, forall_const]
[GOAL]
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i in range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
[PROOFSTEP]
change (∑ i in range n, (f n) i) * x + y ^ n = (x + y) ^ n
[GOAL]
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n : ℕ
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i in range Nat.zero, f Nat.zero i) * x + y ^ Nat.zero = (x + y) ^ Nat.zero
[PROOFSTEP]
rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]
[GOAL]
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ (∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ n
[PROOFSTEP]
have f_last : f (n + 1) n = (x + y) ^ n := by
  rw [hf, ← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
[GOAL]
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ f (n + 1) n = (x + y) ^ n
[PROOFSTEP]
rw [hf, ← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
[GOAL]
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
⊢ (∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ n
[PROOFSTEP]
have f_succ : ∀ i, i ∈ range n → f (n + 1) i = y * f n i := fun i hi =>
  by
  rw [hf]
  have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
  rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ y (n - 1 - i)]
  congr 2
  rw [add_tsub_cancel_right, ← tsub_add_eq_tsub_tsub, add_comm 1 i]
  have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)
  rw [add_comm (i + 1)] at this 
  rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]
[GOAL]
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
⊢ f (n + 1) i = y * f n i
[PROOFSTEP]
rw [hf]
[GOAL]
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = y * f n i
[PROOFSTEP]
have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
[GOAL]
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = y * f n i
[PROOFSTEP]
rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ y (n - 1 - i)]
[GOAL]
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = (x + y) ^ i * y ^ (n - 1 - i + 1)
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ n + 1 - 1 - i = n - 1 - i + 1
[PROOFSTEP]
rw [add_tsub_cancel_right, ← tsub_add_eq_tsub_tsub, add_comm 1 i]
[GOAL]
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ n - i = n - (i + 1) + 1
[PROOFSTEP]
have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)
[GOAL]
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this✝ : Commute y ((x + y) ^ i)
this : i + 1 + (n - (i + 1)) = n
⊢ n - i = n - (i + 1) + 1
[PROOFSTEP]
rw [add_comm (i + 1)] at this 
[GOAL]
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this✝ : Commute y ((x + y) ^ i)
this : n - (i + 1) + (i + 1) = n
⊢ n - i = n - (i + 1) + 1
[PROOFSTEP]
rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]
[GOAL]
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
⊢ (∑ i in range (Nat.succ n), f (Nat.succ n) i) * x + y ^ Nat.succ n = (x + y) ^ Nat.succ n
[PROOFSTEP]
rw [pow_succ (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc]
[GOAL]
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
⊢ (x + y) ^ n * x + ((∑ x in range n, f (Nat.succ n) x) * x + y ^ Nat.succ n) = x * (x + y) ^ n + y * (x + y) ^ n
[PROOFSTEP]
rw [(((Commute.refl x).add_right h).pow_right n).eq]
[GOAL]
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
⊢ (x + y) ^ n * x + ((∑ x in range n, f (Nat.succ n) x) * x + y ^ Nat.succ n) = (x + y) ^ n * x + y * (x + y) ^ n
[PROOFSTEP]
congr 1
[GOAL]
case succ.e_a
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
hf : ∀ (m i : ℕ), f m i = (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i in range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ (i : ℕ), i ∈ range n → f (n + 1) i = y * f n i
⊢ (∑ x in range n, f (Nat.succ n) x) * x + y ^ Nat.succ n = y * (x + y) ^ n
[PROOFSTEP]
rw [sum_congr rfl f_succ, ← mul_sum, pow_succ y, mul_assoc, ← mul_add y, ih]
[GOAL]
α : Type u
inst✝ : Ring α
n : ℕ
⊢ ∑ i in range n, (-1) ^ i = if Even n then 0 else 1
[PROOFSTEP]
induction' n with k hk
[GOAL]
case zero
α : Type u
inst✝ : Ring α
⊢ ∑ i in range Nat.zero, (-1) ^ i = if Even Nat.zero then 0 else 1
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i in range k, (-1) ^ i = if Even k then 0 else 1
⊢ ∑ i in range (Nat.succ k), (-1) ^ i = if Even (Nat.succ k) then 0 else 1
[PROOFSTEP]
simp only [geom_sum_succ', Nat.even_add_one, hk]
[GOAL]
case succ
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i in range k, (-1) ^ i = if Even k then 0 else 1
⊢ ((-1) ^ k + if Even k then 0 else 1) = if ¬Even k then 0 else 1
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i in range k, (-1) ^ i = if Even k then 0 else 1
h : Even k
⊢ (-1) ^ k + 0 = 1
[PROOFSTEP]
rw [h.neg_one_pow, add_zero]
[GOAL]
case neg
α : Type u
inst✝ : Ring α
k : ℕ
hk : ∑ i in range k, (-1) ^ i = if Even k then 0 else 1
h : ¬Even k
⊢ (-1) ^ k + 1 = 0
[PROOFSTEP]
rw [(Nat.odd_iff_not_even.2 h).neg_one_pow, neg_add_self]
[GOAL]
α✝ : Type u
α : Type u_1
inst✝ : CommRing α
x : α
n : ℕ
⊢ ∑ i in range n, x ^ i * x ^ (n - 1 - i) = ∑ i in range n, x ^ (i + (n - 1 - i))
[PROOFSTEP]
simp_rw [← pow_add]
[GOAL]
α✝ : Type u
α : Type u_1
inst✝ : CommRing α
x : α
n : ℕ
⊢ card (range n) • x ^ (n - 1) = ↑n * x ^ (n - 1)
[PROOFSTEP]
rw [Finset.card_range, nsmul_eq_mul]
[GOAL]
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
⊢ (∑ i in range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
[PROOFSTEP]
have := (Commute.one_right x).geom_sum₂_mul_add n
[GOAL]
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
this : (∑ i in range n, (x + 1) ^ i * 1 ^ (n - 1 - i)) * x + 1 ^ n = (x + 1) ^ n
⊢ (∑ i in range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
[PROOFSTEP]
rw [one_pow, geom_sum₂_with_one] at this 
[GOAL]
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
this : (∑ i in range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
⊢ (∑ i in range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
[PROOFSTEP]
exact this
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
[PROOFSTEP]
have := (h.sub_left (Commute.refl y)).geom_sum₂_mul_add n
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
this : (∑ i in range n, (x - y + y) ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = (x - y + y) ^ n
⊢ (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
[PROOFSTEP]
rw [sub_add_cancel] at this 
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
this : (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n
⊢ (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
[PROOFSTEP]
rw [← this, add_sub_cancel]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ (y - x) * ∑ i in range n, x ^ i * y ^ (n - 1 - i) = y ^ n - x ^ n
[PROOFSTEP]
apply op_injective
[GOAL]
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ MulOpposite.op ((y - x) * ∑ i in range n, x ^ i * y ^ (n - 1 - i)) = MulOpposite.op (y ^ n - x ^ n)
[PROOFSTEP]
simp only [op_mul, op_sub, op_geom_sum₂, op_pow]
[GOAL]
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ MulOpposite.op (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (MulOpposite.op y - MulOpposite.op x) =
    MulOpposite.op y ^ n - MulOpposite.op x ^ n
[PROOFSTEP]
simp [(Commute.op h.symm).geom_sum₂_mul n]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ (x - y) * ∑ i in range n, x ^ i * y ^ (n - 1 - i) = x ^ n - y ^ n
[PROOFSTEP]
rw [← neg_sub (y ^ n), ← h.mul_neg_geom_sum₂, ← neg_mul, neg_sub]
[GOAL]
α : Type u
x y n : ℕ
⊢ x - y ∣ x ^ n - y ^ n
[PROOFSTEP]
cases' le_or_lt y x with h h
[GOAL]
case inl
α : Type u
x y n : ℕ
h : y ≤ x
⊢ x - y ∣ x ^ n - y ^ n
[PROOFSTEP]
have : y ^ n ≤ x ^ n := Nat.pow_le_pow_of_le_left h _
[GOAL]
case inl
α : Type u
x y n : ℕ
h : y ≤ x
this : y ^ n ≤ x ^ n
⊢ x - y ∣ x ^ n - y ^ n
[PROOFSTEP]
exact_mod_cast sub_dvd_pow_sub_pow (x : ℤ) (↑y) n
[GOAL]
case inr
α : Type u
x y n : ℕ
h : x < y
⊢ x - y ∣ x ^ n - y ^ n
[PROOFSTEP]
have : x ^ n ≤ y ^ n := Nat.pow_le_pow_of_le_left h.le _
[GOAL]
case inr
α : Type u
x y n : ℕ
h : x < y
this : x ^ n ≤ y ^ n
⊢ x - y ∣ x ^ n - y ^ n
[PROOFSTEP]
exact (Nat.sub_eq_zero_of_le this).symm ▸ dvd_zero (x - y)
[GOAL]
α : Type u
inst✝ : CommRing α
x y : α
n : ℕ
h : Odd n
⊢ x + y ∣ x ^ n + y ^ n
[PROOFSTEP]
have h₁ := geom_sum₂_mul x (-y) n
[GOAL]
α : Type u
inst✝ : CommRing α
x y : α
n : ℕ
h : Odd n
h₁ : (∑ i in range n, x ^ i * (-y) ^ (n - 1 - i)) * (x - -y) = x ^ n - (-y) ^ n
⊢ x + y ∣ x ^ n + y ^ n
[PROOFSTEP]
rw [Odd.neg_pow h y, sub_neg_eq_add, sub_neg_eq_add] at h₁ 
[GOAL]
α : Type u
inst✝ : CommRing α
x y : α
n : ℕ
h : Odd n
h₁ : (∑ i in range n, x ^ i * (-y) ^ (n - 1 - i)) * (x + y) = x ^ n + y ^ n
⊢ x + y ∣ x ^ n + y ^ n
[PROOFSTEP]
exact Dvd.intro_left _ h₁
[GOAL]
α : Type u
x y n : ℕ
h : Odd n
⊢ x + y ∣ x ^ n + y ^ n
[PROOFSTEP]
exact_mod_cast Odd.add_dvd_pow_add_pow (x : ℤ) (↑y) h
[GOAL]
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ (∑ i in range n, x ^ i) * (x - 1) = x ^ n - 1
[PROOFSTEP]
have := (Commute.one_right x).geom_sum₂_mul n
[GOAL]
α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : (∑ i in range n, x ^ i * 1 ^ (n - 1 - i)) * (x - 1) = x ^ n - 1 ^ n
⊢ (∑ i in range n, x ^ i) * (x - 1) = x ^ n - 1
[PROOFSTEP]
rw [one_pow, geom_sum₂_with_one] at this 
[GOAL]
α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : (∑ i in range n, x ^ i) * (x - 1) = x ^ n - 1
⊢ (∑ i in range n, x ^ i) * (x - 1) = x ^ n - 1
[PROOFSTEP]
exact this
[GOAL]
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ op ((x - 1) * ∑ i in range n, x ^ i) = op (x ^ n - 1)
[PROOFSTEP]
simpa using geom_sum_mul (op x) n
[GOAL]
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ (∑ i in range n, x ^ i) * (1 - x) = 1 - x ^ n
[PROOFSTEP]
have := congr_arg Neg.neg (geom_sum_mul x n)
[GOAL]
α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : -((∑ i in range n, x ^ i) * (x - 1)) = -(x ^ n - 1)
⊢ (∑ i in range n, x ^ i) * (1 - x) = 1 - x ^ n
[PROOFSTEP]
rw [neg_sub, ← mul_neg, neg_sub] at this 
[GOAL]
α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : (∑ i in range n, x ^ i) * (1 - x) = 1 - x ^ n
⊢ (∑ i in range n, x ^ i) * (1 - x) = 1 - x ^ n
[PROOFSTEP]
exact this
[GOAL]
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ op ((1 - x) * ∑ i in range n, x ^ i) = op (1 - x ^ n)
[PROOFSTEP]
simpa using geom_sum_mul_neg (op x) n
[GOAL]
α✝ α : Type u
inst✝ : Semiring α
x y : α
n : ℕ
h : Commute x y
⊢ ∑ i in range n, x ^ i * y ^ (n - 1 - i) = ∑ i in range n, y ^ i * x ^ (n - 1 - i)
[PROOFSTEP]
cases n
[GOAL]
case zero
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
⊢ ∑ i in range Nat.zero, x ^ i * y ^ (Nat.zero - 1 - i) = ∑ i in range Nat.zero, y ^ i * x ^ (Nat.zero - 1 - i)
[PROOFSTEP]
simp
[GOAL]
case succ
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ i in range (Nat.succ n✝), x ^ i * y ^ (Nat.succ n✝ - 1 - i) =
    ∑ i in range (Nat.succ n✝), y ^ i * x ^ (Nat.succ n✝ - 1 - i)
[PROOFSTEP]
simp only [Nat.succ_eq_add_one, Nat.add_sub_cancel]
[GOAL]
case succ
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ x_1 in range (n✝ + 1), x ^ x_1 * y ^ (n✝ - x_1) = ∑ x_1 in range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)
[PROOFSTEP]
rw [← Finset.sum_flip]
[GOAL]
case succ
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ : ℕ
⊢ ∑ r in range (n✝ + 1), x ^ (n✝ - r) * y ^ (n✝ - (n✝ - r)) = ∑ x_1 in range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)
[PROOFSTEP]
refine' Finset.sum_congr rfl fun i hi => _
[GOAL]
case succ
α✝ α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
n✝ i : ℕ
hi : i ∈ range (n✝ + 1)
⊢ x ^ (n✝ - i) * y ^ (n✝ - (n✝ - i)) = y ^ i * x ^ (n✝ - i)
[PROOFSTEP]
simpa [Nat.sub_sub_self (Nat.succ_le_succ_iff.mp (Finset.mem_range.mp hi))] using h.pow_pow _ _
[GOAL]
α : Type u
inst✝ : DivisionRing α
x y : α
h' : Commute x y
h : x ≠ y
n : ℕ
⊢ ∑ i in range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
[PROOFSTEP]
have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x y : α
h' : Commute x y
h : x ≠ y
n : ℕ
⊢ x - y ≠ 0
[PROOFSTEP]
simp_all [sub_eq_iff_eq_add]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x y : α
h' : Commute x y
h : x ≠ y
n : ℕ
this : x - y ≠ 0
⊢ ∑ i in range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
[PROOFSTEP]
rw [← h'.geom_sum₂_mul, mul_div_cancel _ this]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
h : x ≠ 1
n : ℕ
⊢ ∑ i in range n, x ^ i = (x ^ n - 1) / (x - 1)
[PROOFSTEP]
have : x - 1 ≠ 0 := by simp_all [sub_eq_iff_eq_add]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
h : x ≠ 1
n : ℕ
⊢ x - 1 ≠ 0
[PROOFSTEP]
simp_all [sub_eq_iff_eq_add]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
h : x ≠ 1
n : ℕ
this : x - 1 ≠ 0
⊢ ∑ i in range n, x ^ i = (x ^ n - 1) / (x - 1)
[PROOFSTEP]
rw [← geom_sum_mul, mul_div_cancel _ this]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (x - y) * ∑ i in Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)
[PROOFSTEP]
rw [sum_Ico_eq_sub _ hmn]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ k in range m, x ^ k * y ^ (n - 1 - k)) =
    x ^ n - x ^ m * y ^ (n - m)
[PROOFSTEP]
have : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k)) :=
  by
  refine' sum_congr rfl fun j j_in => _
  rw [← pow_add]
  congr
  rw [mem_range, Nat.lt_iff_add_one_le, add_comm] at j_in 
  have h' : n - m + (m - (1 + j)) = n - (1 + j) := tsub_add_tsub_cancel hmn j_in
  rw [← tsub_add_eq_tsub_tsub m, h', ← tsub_add_eq_tsub_tsub]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
[PROOFSTEP]
refine' sum_congr rfl fun j j_in => _
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ x ^ j * y ^ (n - 1 - j) = x ^ j * (y ^ (n - m) * y ^ (m - 1 - j))
[PROOFSTEP]
rw [← pow_add]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ x ^ j * y ^ (n - 1 - j) = x ^ j * y ^ (n - m + (m - 1 - j))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ n - 1 - j = n - m + (m - 1 - j)
[PROOFSTEP]
rw [mem_range, Nat.lt_iff_add_one_le, add_comm] at j_in 
[GOAL]
case e_a.e_a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : 1 + j ≤ m
⊢ n - 1 - j = n - m + (m - 1 - j)
[PROOFSTEP]
have h' : n - m + (m - (1 + j)) = n - (1 + j) := tsub_add_tsub_cancel hmn j_in
[GOAL]
case e_a.e_a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : 1 + j ≤ m
h' : n - m + (m - (1 + j)) = n - (1 + j)
⊢ n - 1 - j = n - m + (m - 1 - j)
[PROOFSTEP]
rw [← tsub_add_eq_tsub_tsub m, h', ← tsub_add_eq_tsub_tsub]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ k in range m, x ^ k * y ^ (n - 1 - k)) =
    x ^ n - x ^ m * y ^ (n - m)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))) =
    x ^ n - x ^ m * y ^ (n - m)
[PROOFSTEP]
simp_rw [pow_mul_comm y (n - m) _]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ x_1 in range m, x ^ x_1 * (y ^ (m - 1 - x_1) * y ^ (n - m))) =
    x ^ n - x ^ m * y ^ (n - m)
[PROOFSTEP]
simp_rw [← mul_assoc]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this : ∑ k in range m, x ^ k * y ^ (n - 1 - k) = ∑ k in range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))
⊢ (x - y) * (∑ k in range n, x ^ k * y ^ (n - 1 - k) - ∑ x_1 in range m, x ^ x_1 * y ^ (m - 1 - x_1) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
[PROOFSTEP]
rw [← sum_mul, mul_sub, h.mul_geom_sum₂, ← mul_assoc, h.mul_geom_sum₂, sub_mul, ← pow_add, add_tsub_cancel_of_le hmn,
  sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ n)]
[GOAL]
α✝ α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ ∑ i in range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i in range n, x ^ i * y ^ (n - 1 - i)
[PROOFSTEP]
simp_rw [mul_sum, sum_range_succ_comm, tsub_self, pow_zero, mul_one, add_right_inj, ← mul_assoc,
  (h.symm.pow_right _).eq, mul_assoc, ← pow_succ]
[GOAL]
α✝ α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ ∑ i in range n, x ^ i * y ^ (n - i) = ∑ x_1 in range n, x ^ x_1 * y ^ (n - 1 - x_1 + 1)
[PROOFSTEP]
refine' sum_congr rfl fun i hi => _
[GOAL]
α✝ α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n i : ℕ
hi : i ∈ range n
⊢ x ^ i * y ^ (n - i) = x ^ i * y ^ (n - 1 - i + 1)
[PROOFSTEP]
suffices n - 1 - i + 1 = n - i by rw [this]
[GOAL]
α✝ α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n i : ℕ
hi : i ∈ range n
this : n - 1 - i + 1 = n - i
⊢ x ^ i * y ^ (n - i) = x ^ i * y ^ (n - 1 - i + 1)
[PROOFSTEP]
rw [this]
[GOAL]
α✝ α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n i : ℕ
hi : i ∈ range n
⊢ n - 1 - i + 1 = n - i
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
α✝ α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
i : ℕ
hi : i ∈ range Nat.zero
⊢ Nat.zero - 1 - i + 1 = Nat.zero - i
[PROOFSTEP]
exact absurd (List.mem_range.mp hi) i.not_lt_zero
[GOAL]
case succ
α✝ α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
i n : ℕ
hi : i ∈ range (Nat.succ n)
⊢ Nat.succ n - 1 - i + 1 = Nat.succ n - i
[PROOFSTEP]
rw [tsub_add_eq_add_tsub (Nat.le_pred_of_lt (List.mem_range.mp hi)),
  tsub_add_cancel_of_le (Nat.succ_le_iff.mpr n.succ_pos)]
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (∑ i in Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ (n - m) * x ^ m
[PROOFSTEP]
apply op_injective
[GOAL]
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ MulOpposite.op ((∑ i in Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y)) = MulOpposite.op (x ^ n - y ^ (n - m) * x ^ m)
[PROOFSTEP]
simp only [op_sub, op_mul, op_pow, op_sum]
[GOAL]
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (MulOpposite.op x - MulOpposite.op y) * ∑ x_1 in Ico m n, MulOpposite.op y ^ (n - 1 - x_1) * MulOpposite.op x ^ x_1 =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
[PROOFSTEP]
have :
  (∑ k in Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k) =
    ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) :=
  by
  refine' sum_congr rfl fun k _ => _
  have hp := Commute.pow_pow (Commute.op h.symm) (n - 1 - k) k
  simpa [Commute, SemiconjBy] using hp
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ ∑ k in Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k =
    ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
[PROOFSTEP]
refine' sum_congr rfl fun k _ => _
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
k : ℕ
x✝ : k ∈ Ico m n
⊢ MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
[PROOFSTEP]
have hp := Commute.pow_pow (Commute.op h.symm) (n - 1 - k) k
[GOAL]
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
k : ℕ
x✝ : k ∈ Ico m n
hp : Commute (MulOpposite.op y ^ (n - 1 - k)) (MulOpposite.op x ^ k)
⊢ MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
[PROOFSTEP]
simpa [Commute, SemiconjBy] using hp
[GOAL]
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this :
  ∑ k in Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k =
    ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
⊢ (MulOpposite.op x - MulOpposite.op y) * ∑ x_1 in Ico m n, MulOpposite.op y ^ (n - 1 - x_1) * MulOpposite.op x ^ x_1 =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
[PROOFSTEP]
simp only [this]
  -- porting note: gives deterministic timeout without this intermediate `have`
[GOAL]
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
m n : ℕ
hmn : m ≤ n
this :
  ∑ k in Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k =
    ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
⊢ (MulOpposite.op x - MulOpposite.op y) * ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
[PROOFSTEP]
convert (Commute.op h).mul_geom_sum₂_Ico hmn
[GOAL]
α : Type u
inst✝ : Ring α
x : α
m n : ℕ
hmn : m ≤ n
⊢ (∑ i in Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m
[PROOFSTEP]
rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul, geom_sum_mul, sub_sub_sub_cancel_right]
[GOAL]
α : Type u
inst✝ : Ring α
x : α
m n : ℕ
hmn : m ≤ n
⊢ (∑ i in Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n
[PROOFSTEP]
rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul_neg, geom_sum_mul_neg, sub_sub_sub_cancel_left]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x y : α
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
⊢ ∑ i in Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
[PROOFSTEP]
have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x y : α
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
⊢ x - y ≠ 0
[PROOFSTEP]
simp_all [sub_eq_iff_eq_add]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x y : α
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
this : x - y ≠ 0
⊢ ∑ i in Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
[PROOFSTEP]
rw [← h.geom_sum₂_Ico_mul hmn, mul_div_cancel _ this]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ ∑ i in Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)
[PROOFSTEP]
simp only [sum_Ico_eq_sub _ hmn, geom_sum_eq hx, div_sub_div_same, sub_sub_sub_cancel_right]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ ∑ i in Ico m n, x ^ i = (x ^ m - x ^ n) / (1 - x)
[PROOFSTEP]
simp only [geom_sum_Ico hx hmn]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ (x ^ n - x ^ m) / (x - 1) = (x ^ m - x ^ n) / (1 - x)
[PROOFSTEP]
convert neg_div_neg_eq (x ^ m - x ^ n) (1 - x) using 2
[GOAL]
case h.e'_2.h.e'_5
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ x ^ n - x ^ m = -(x ^ m - x ^ n)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ x ^ n - x ^ m = -(x ^ m - x ^ n)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ x - 1 = -(1 - x)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ x - 1 = -(1 - x)
[PROOFSTEP]
abel
[GOAL]
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
⊢ ∑ i in Ico m n, x ^ i ≤ x ^ m / (1 - x)
[PROOFSTEP]
rcases le_or_lt m n with (hmn | hmn)
[GOAL]
case inl
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : m ≤ n
⊢ ∑ i in Ico m n, x ^ i ≤ x ^ m / (1 - x)
[PROOFSTEP]
rw [geom_sum_Ico' h'x.ne hmn]
[GOAL]
case inl
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : m ≤ n
⊢ (x ^ m - x ^ n) / (1 - x) ≤ x ^ m / (1 - x)
[PROOFSTEP]
apply div_le_div (pow_nonneg hx _) _ (sub_pos.2 h'x) le_rfl
[GOAL]
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : m ≤ n
⊢ x ^ m - x ^ n ≤ x ^ m
[PROOFSTEP]
simpa using pow_nonneg hx _
[GOAL]
case inr
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : n < m
⊢ ∑ i in Ico m n, x ^ i ≤ x ^ m / (1 - x)
[PROOFSTEP]
rw [Ico_eq_empty, sum_empty]
[GOAL]
case inr
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : n < m
⊢ 0 ≤ x ^ m / (1 - x)
[PROOFSTEP]
apply div_nonneg (pow_nonneg hx _)
[GOAL]
case inr
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : n < m
⊢ 0 ≤ 1 - x
[PROOFSTEP]
simpa using h'x.le
[GOAL]
case inr
α : Type u
inst✝ : LinearOrderedField α
x : α
hx : 0 ≤ x
h'x : x < 1
m n : ℕ
hmn : n < m
⊢ ¬m < n
[PROOFSTEP]
simpa using hmn.le
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
⊢ ∑ i in range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
[PROOFSTEP]
have h₁ : x⁻¹ ≠ 1 := by rwa [inv_eq_one_div, Ne.def, div_eq_iff_mul_eq hx0, one_mul]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
⊢ x⁻¹ ≠ 1
[PROOFSTEP]
rwa [inv_eq_one_div, Ne.def, div_eq_iff_mul_eq hx0, one_mul]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
⊢ ∑ i in range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
[PROOFSTEP]
have h₂ : x⁻¹ - 1 ≠ 0 := mt sub_eq_zero.1 h₁
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
⊢ ∑ i in range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
[PROOFSTEP]
have h₃ : x - 1 ≠ 0 := mt sub_eq_zero.1 hx1
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
⊢ ∑ i in range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
[PROOFSTEP]
have h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x :=
  Nat.recOn n (by simp) fun n h => by
    rw [pow_succ, mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel hx0, mul_assoc, inv_mul_cancel hx0]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
⊢ x * (x ^ Nat.zero)⁻¹ = (x ^ Nat.zero)⁻¹ * x
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n✝ : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ x * (x ^ Nat.succ n)⁻¹ = (x ^ Nat.succ n)⁻¹ * x
[PROOFSTEP]
rw [pow_succ, mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel hx0, mul_assoc, inv_mul_cancel hx0]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ ∑ i in range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
[PROOFSTEP]
rw [geom_sum_eq h₁, div_eq_iff_mul_eq h₂, ← mul_right_inj' h₃, ← mul_assoc, ← mul_assoc, mul_inv_cancel h₃]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ 1 * (x - x⁻¹ ^ n * x) * (x⁻¹ - 1) = (x - 1) * (x⁻¹ ^ n - 1)
[PROOFSTEP]
simp [mul_add, add_mul, mul_inv_cancel hx0, mul_assoc, h₄, sub_eq_add_neg, add_comm, add_left_comm]
[GOAL]
α : Type u
inst✝ : DivisionRing α
x : α
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ (x ^ n)⁻¹ * x + -x + (-(x ^ n)⁻¹ + 1) = -x + ((x ^ n)⁻¹ * x + -(x ^ n)⁻¹ + 1)
[PROOFSTEP]
rw [add_comm _ (-x), add_assoc, add_assoc _ _ 1]
[GOAL]
α : Type u
β : Type u_1
inst✝¹ : Semiring α
inst✝ : Semiring β
x : α
n : ℕ
f : α →+* β
⊢ ↑f (∑ i in range n, x ^ i) = ∑ i in range n, ↑f x ^ i
[PROOFSTEP]
simp [f.map_sum]
[GOAL]
α : Type u
β : Type u_1
inst✝¹ : Semiring α
inst✝ : Semiring β
x y : α
n : ℕ
f : α →+* β
⊢ ↑f (∑ i in range n, x ^ i * y ^ (n - 1 - i)) = ∑ i in range n, ↑f x ^ i * ↑f y ^ (n - 1 - i)
[PROOFSTEP]
simp [f.map_sum]
[GOAL]
α : Type u
β : Type u_1
a b n : ℕ
⊢ (b - 1) * ∑ i in range (succ n), a / b ^ i =
    ∑ i in range n, a / b ^ (i + 1) * b + a * b - (∑ i in range n, a / b ^ i + a / b ^ n)
[PROOFSTEP]
rw [tsub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero, Nat.div_one]
[GOAL]
α : Type u
β : Type u_1
a b n : ℕ
⊢ ∑ i in range n, a / b ^ (i + 1) * b + a * b - (∑ i in range n, a / b ^ i + a / b ^ n) ≤
    ∑ i in range n, a / b ^ i + a * b - (∑ i in range n, a / b ^ i + a / b ^ n)
[PROOFSTEP]
refine' tsub_le_tsub_right (add_le_add_right (sum_le_sum fun i _ => _) _) _
[GOAL]
α : Type u
β : Type u_1
a b n i : ℕ
x✝ : i ∈ range n
⊢ a / b ^ (i + 1) * b ≤ a / b ^ i
[PROOFSTEP]
rw [pow_succ', mul_comm b]
[GOAL]
α : Type u
β : Type u_1
a b n i : ℕ
x✝ : i ∈ range n
⊢ a / (b ^ i * b) * b ≤ a / b ^ i
[PROOFSTEP]
rw [← Nat.div_div_eq_div_mul]
[GOAL]
α : Type u
β : Type u_1
a b n i : ℕ
x✝ : i ∈ range n
⊢ a / b ^ i / b * b ≤ a / b ^ i
[PROOFSTEP]
exact Nat.div_mul_le_self _ _
[GOAL]
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i in range n, a / b ^ i ≤ a * b / (b - 1)
[PROOFSTEP]
refine' (Nat.le_div_iff_mul_le <| tsub_pos_of_lt hb).2 _
[GOAL]
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (∑ i in range n, a / b ^ i) * (b - 1) ≤ a * b
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ (∑ i in range zero, a / b ^ i) * (b - 1) ≤ a * b
[PROOFSTEP]
rw [sum_range_zero, zero_mul]
[GOAL]
case zero
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a * b
[PROOFSTEP]
exact Nat.zero_le _
[GOAL]
case succ
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (∑ i in range (succ n), a / b ^ i) * (b - 1) ≤ a * b
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case succ
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (b - 1) * ∑ i in range (succ n), a / b ^ i ≤ a * b
[PROOFSTEP]
exact (Nat.pred_mul_geom_sum_le a b n).trans tsub_le_self
[GOAL]
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i in Ico 1 n, a / b ^ i ≤ a / (b - 1)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ ∑ i in Ico 1 zero, a / b ^ i ≤ a / (b - 1)
[PROOFSTEP]
rw [zero_eq, Ico_eq_empty_of_le (zero_le_one' ℕ), sum_empty]
[GOAL]
case zero
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a / (b - 1)
[PROOFSTEP]
exact Nat.zero_le _
[GOAL]
case succ
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i in Ico 1 (succ n), a / b ^ i ≤ a / (b - 1)
[PROOFSTEP]
rw [← add_le_add_iff_left a]
[GOAL]
case succ
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i in Ico 1 (succ n), a / b ^ i ≤ a + a / (b - 1)
[PROOFSTEP]
calc
  (a + ∑ i : ℕ in Ico 1 n.succ, a / b ^ i) = a / b ^ 0 + ∑ i : ℕ in Ico 1 n.succ, a / b ^ i := by
    rw [pow_zero, Nat.div_one]
  _ = ∑ i in range n.succ, a / b ^ i :=
    by
    rw [range_eq_Ico, ← Nat.Ico_insert_succ_left (Nat.succ_pos _), sum_insert]
    exact fun h => zero_lt_one.not_le (mem_Ico.1 h).1
  _ ≤ a * b / (b - 1) := (Nat.geom_sum_le hb a _)
  _ = (a * 1 + a * (b - 1)) / (b - 1) := by rw [← mul_add, add_tsub_cancel_of_le (one_le_two.trans hb)]
  _ = a + a / (b - 1) := by rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]
[GOAL]
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i in Ico 1 (succ n), a / b ^ i = a / b ^ 0 + ∑ i in Ico 1 (succ n), a / b ^ i
[PROOFSTEP]
rw [pow_zero, Nat.div_one]
[GOAL]
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / b ^ 0 + ∑ i in Ico 1 (succ n), a / b ^ i = ∑ i in range (succ n), a / b ^ i
[PROOFSTEP]
rw [range_eq_Ico, ← Nat.Ico_insert_succ_left (Nat.succ_pos _), sum_insert]
[GOAL]
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ¬0 ∈ Ico (succ 0) (succ n)
[PROOFSTEP]
exact fun h => zero_lt_one.not_le (mem_Ico.1 h).1
[GOAL]
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a * b / (b - 1) = (a * 1 + a * (b - 1)) / (b - 1)
[PROOFSTEP]
rw [← mul_add, add_tsub_cancel_of_le (one_le_two.trans hb)]
[GOAL]
α : Type u
β : Type u_1
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (a * 1 + a * (b - 1)) / (b - 1) = a + a / (b - 1)
[PROOFSTEP]
rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedSemiring α
hx : 0 ≤ x
hn : n ≠ 0
⊢ 0 < x ^ 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ 0 < ∑ i in range n, x ^ i ∧ ∑ i in range n, x ^ i < 1
[PROOFSTEP]
refine' Nat.le_induction _ _ n (show 2 ≤ n from hn)
[GOAL]
case refine'_1
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ 0 < ∑ i in range 2, x ^ i ∧ ∑ i in range 2, x ^ i < 1
[PROOFSTEP]
rw [geom_sum_two]
[GOAL]
case refine'_1
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ 0 < x + 1 ∧ x + 1 < 1
[PROOFSTEP]
exact ⟨hx', (add_lt_iff_neg_right _).2 hx⟩
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ ∀ (n : ℕ),
    2 ≤ n →
      0 < ∑ i in range n, x ^ i ∧ ∑ i in range n, x ^ i < 1 →
        0 < ∑ i in range (n + 1), x ^ i ∧ ∑ i in range (n + 1), x ^ i < 1
[PROOFSTEP]
clear hn
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x < 0
hx' : 0 < x + 1
⊢ ∀ (n : ℕ),
    2 ≤ n →
      0 < ∑ i in range n, x ^ i ∧ ∑ i in range n, x ^ i < 1 →
        0 < ∑ i in range (n + 1), x ^ i ∧ ∑ i in range (n + 1), x ^ i < 1
[PROOFSTEP]
intro n _ ihn
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x < 0
hx' : 0 < x + 1
n : ℕ
hn✝ : 2 ≤ n
ihn : 0 < ∑ i in range n, x ^ i ∧ ∑ i in range n, x ^ i < 1
⊢ 0 < ∑ i in range (n + 1), x ^ i ∧ ∑ i in range (n + 1), x ^ i < 1
[PROOFSTEP]
rw [geom_sum_succ, add_lt_iff_neg_right, ← neg_lt_iff_pos_add', neg_mul_eq_neg_mul]
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x < 0
hx' : 0 < x + 1
n : ℕ
hn✝ : 2 ≤ n
ihn : 0 < ∑ i in range n, x ^ i ∧ ∑ i in range n, x ^ i < 1
⊢ -x * ∑ i in range n, x ^ i < 1 ∧ x * ∑ i in range n, x ^ i < 0
[PROOFSTEP]
exact
  ⟨mul_lt_one_of_nonneg_of_lt_one_left (neg_nonneg.2 hx.le) (neg_lt_iff_pos_add'.2 hx') ihn.2.le,
    mul_neg_of_neg_of_pos hx ihn.1⟩
[GOAL]
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
n : ℕ
⊢ if Even n then ∑ i in range n, x ^ i ≤ 0 else 1 ≤ ∑ i in range n, x ^ i
[PROOFSTEP]
have hx0 : x ≤ 0 := (le_add_of_nonneg_right zero_le_one).trans hx
[GOAL]
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
n : ℕ
hx0 : x ≤ 0
⊢ if Even n then ∑ i in range n, x ^ i ≤ 0 else 1 ≤ ∑ i in range n, x ^ i
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
⊢ if Even Nat.zero then ∑ i in range Nat.zero, x ^ i ≤ 0 else 1 ≤ ∑ i in range Nat.zero, x ^ i
[PROOFSTEP]
simp only [Nat.zero_eq, range_zero, sum_empty, le_refl, ite_true]
[GOAL]
case succ
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
ih : if Even n then ∑ i in range n, x ^ i ≤ 0 else 1 ≤ ∑ i in range n, x ^ i
⊢ if Even (Nat.succ n) then ∑ i in range (Nat.succ n), x ^ i ≤ 0 else 1 ≤ ∑ i in range (Nat.succ n), x ^ i
[PROOFSTEP]
simp only [Nat.even_add_one, geom_sum_succ]
[GOAL]
case succ
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
ih : if Even n then ∑ i in range n, x ^ i ≤ 0 else 1 ≤ ∑ i in range n, x ^ i
⊢ if ¬Even n then x * ∑ i in range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
split_ifs at ih  with h
[GOAL]
case pos
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : ∑ i in range n, x ^ i ≤ 0
⊢ if ¬Even n then x * ∑ i in range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
rw [if_neg (not_not_intro h), le_add_iff_nonneg_left]
[GOAL]
case pos
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : ∑ i in range n, x ^ i ≤ 0
⊢ 0 ≤ x * ∑ i in range n, x ^ i
[PROOFSTEP]
exact mul_nonneg_of_nonpos_of_nonpos hx0 ih
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i in range n, x ^ i
⊢ if ¬Even n then x * ∑ i in range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
rw [if_pos h]
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i in range n, x ^ i
⊢ x * ∑ i in range n, x ^ i + 1 ≤ 0
[PROOFSTEP]
refine' (add_le_add_right _ _).trans hx
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i in range n, x ^ i
⊢ x * ∑ i in range n, x ^ i ≤ x
[PROOFSTEP]
simpa only [mul_one] using mul_le_mul_of_nonpos_left ih hx0
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hn : 1 < n
⊢ if Even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i
[PROOFSTEP]
have hx0 : x < 0 := ((le_add_iff_nonneg_right _).2 zero_le_one).trans_lt hx
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ if Even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i
[PROOFSTEP]
refine' Nat.le_induction _ _ n (show 2 ≤ n from hn)
[GOAL]
case refine'_1
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ if Even 2 then ∑ i in range 2, x ^ i < 0 else 1 < ∑ i in range 2, x ^ i
[PROOFSTEP]
simp only [geom_sum_two, lt_add_iff_pos_left, ite_true, gt_iff_lt, hx]
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ ∀ (n : ℕ),
    2 ≤ n →
      (if Even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i) →
        if Even (n + 1) then ∑ i in range (n + 1), x ^ i < 0 else 1 < ∑ i in range (n + 1), x ^ i
[PROOFSTEP]
clear hn
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
⊢ ∀ (n : ℕ),
    2 ≤ n →
      (if Even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i) →
        if Even (n + 1) then ∑ i in range (n + 1), x ^ i < 0 else 1 < ∑ i in range (n + 1), x ^ i
[PROOFSTEP]
intro n _ ihn
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : if Even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i
⊢ if Even (n + 1) then ∑ i in range (n + 1), x ^ i < 0 else 1 < ∑ i in range (n + 1), x ^ i
[PROOFSTEP]
simp only [Nat.even_add_one, geom_sum_succ]
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : if Even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i
⊢ if ¬Even n then x * ∑ i in range n, x ^ i + 1 < 0 else 1 < x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
by_cases hn' : Even n
[GOAL]
case pos
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : if Even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i
hn' : Even n
⊢ if ¬Even n then x * ∑ i in range n, x ^ i + 1 < 0 else 1 < x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
rw [if_pos hn'] at ihn 
[GOAL]
case pos
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : ∑ i in range n, x ^ i < 0
hn' : Even n
⊢ if ¬Even n then x * ∑ i in range n, x ^ i + 1 < 0 else 1 < x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
rw [if_neg, lt_add_iff_pos_left]
[GOAL]
case pos
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : ∑ i in range n, x ^ i < 0
hn' : Even n
⊢ 0 < x * ∑ i in range n, x ^ i
case pos.hnc
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : ∑ i in range n, x ^ i < 0
hn' : Even n
⊢ ¬¬Even n
[PROOFSTEP]
exact mul_pos_of_neg_of_neg hx0 ihn
[GOAL]
case pos.hnc
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : ∑ i in range n, x ^ i < 0
hn' : Even n
⊢ ¬¬Even n
[PROOFSTEP]
exact not_not_intro hn'
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : if Even n then ∑ i in range n, x ^ i < 0 else 1 < ∑ i in range n, x ^ i
hn' : ¬Even n
⊢ if ¬Even n then x * ∑ i in range n, x ^ i + 1 < 0 else 1 < x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
rw [if_neg hn'] at ihn 
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : 1 < ∑ i in range n, x ^ i
hn' : ¬Even n
⊢ if ¬Even n then x * ∑ i in range n, x ^ i + 1 < 0 else 1 < x * ∑ i in range n, x ^ i + 1
[PROOFSTEP]
rw [if_pos]
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : 1 < ∑ i in range n, x ^ i
hn' : ¬Even n
⊢ x * ∑ i in range n, x ^ i + 1 < 0
case neg.hc
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : 1 < ∑ i in range n, x ^ i
hn' : ¬Even n
⊢ ¬Even n
[PROOFSTEP]
swap
[GOAL]
case neg.hc
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : 1 < ∑ i in range n, x ^ i
hn' : ¬Even n
⊢ ¬Even n
[PROOFSTEP]
exact hn'
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : 1 < ∑ i in range n, x ^ i
hn' : ¬Even n
⊢ x * ∑ i in range n, x ^ i + 1 < 0
[PROOFSTEP]
have := add_lt_add_right (mul_lt_mul_of_neg_left ihn hx0) 1
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : 1 < ∑ i in range n, x ^ i
hn' : ¬Even n
this : x * ∑ i in range n, x ^ i + 1 < x * 1 + 1
⊢ x * ∑ i in range n, x ^ i + 1 < 0
[PROOFSTEP]
rw [mul_one] at this 
[GOAL]
case neg
α : Type u
β : Type u_1
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hn✝ : 2 ≤ n
ihn : 1 < ∑ i in range n, x ^ i
hn' : ¬Even n
this : x * ∑ i in range n, x ^ i + 1 < x + 1
⊢ x * ∑ i in range n, x ^ i + 1 < 0
[PROOFSTEP]
exact this.trans hx
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
hn : n ≠ 0
⊢ 0 < ∑ i in range n, x ^ i
[PROOFSTEP]
obtain _ | _ | n := n
[GOAL]
case zero
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
hn : Nat.zero ≠ 0
⊢ 0 < ∑ i in range Nat.zero, x ^ i
[PROOFSTEP]
cases hn rfl
[GOAL]
case succ.zero
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
hn : Nat.succ Nat.zero ≠ 0
⊢ 0 < ∑ i in range (Nat.succ Nat.zero), x ^ i
[PROOFSTEP]
simp only [Nat.zero_eq, ← Nat.one_eq_succ_zero, range_one, sum_singleton, pow_zero, zero_lt_one]
[GOAL]
case succ.succ
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
[PROOFSTEP]
obtain hx' | hx' := lt_or_le x 0
[GOAL]
case succ.succ.inl
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
hx' : x < 0
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
[PROOFSTEP]
exact (geom_sum_pos_and_lt_one hx' hx n.one_lt_succ_succ).1
[GOAL]
case succ.succ.inr
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
hx' : 0 ≤ x
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
[PROOFSTEP]
exact geom_sum_pos hx' (by simp only [Nat.succ_ne_zero, Ne.def, not_false_iff])
[GOAL]
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
hx' : 0 ≤ x
⊢ Nat.succ (Nat.succ n) ≠ 0
[PROOFSTEP]
simp only [Nat.succ_ne_zero, Ne.def, not_false_iff]
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
h : Odd n
⊢ 0 < ∑ i in range n, x ^ i
[PROOFSTEP]
rcases n with (_ | _ | k)
[GOAL]
case zero
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
h : Odd Nat.zero
⊢ 0 < ∑ i in range Nat.zero, x ^ i
[PROOFSTEP]
exact ((show ¬Odd 0 by decide) h).elim
[GOAL]
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
h : Odd Nat.zero
⊢ ¬Odd 0
[PROOFSTEP]
decide
[GOAL]
case succ.zero
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
h : Odd (Nat.succ Nat.zero)
⊢ 0 < ∑ i in range (Nat.succ Nat.zero), x ^ i
[PROOFSTEP]
simp only [Nat.zero_eq, ← Nat.one_eq_succ_zero, geom_sum_one, zero_lt_one]
[GOAL]
case succ.succ
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : Odd (Nat.succ (Nat.succ k))
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
[PROOFSTEP]
rw [Nat.odd_iff_not_even] at h 
[GOAL]
case succ.succ
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
[PROOFSTEP]
rcases lt_trichotomy (x + 1) 0 with (hx | hx | hx)
[GOAL]
case succ.succ.inl
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : x + 1 < 0
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
[PROOFSTEP]
have := geom_sum_alternating_of_lt_neg_one hx k.one_lt_succ_succ
[GOAL]
case succ.succ.inl
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : x + 1 < 0
this :
  if Even (Nat.succ (Nat.succ k)) then ∑ i in range (Nat.succ (Nat.succ k)), x ^ i < 0
  else 1 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
[PROOFSTEP]
simp only [h, if_false] at this 
[GOAL]
case succ.succ.inl
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : x + 1 < 0
this : 1 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
[PROOFSTEP]
exact zero_lt_one.trans this
[GOAL]
case succ.succ.inr.inl
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : x + 1 = 0
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
[PROOFSTEP]
simp only [eq_neg_of_add_eq_zero_left hx, h, neg_one_geom_sum, if_false, zero_lt_one]
[GOAL]
case succ.succ.inr.inr
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : 0 < x + 1
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
[PROOFSTEP]
exact geom_sum_pos' hx k.succ.succ_ne_zero
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
⊢ 0 < ∑ i in range n, x ^ i ↔ Odd n ∨ 0 < x + 1
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : 0 < ∑ i in range n, x ^ i
⊢ Odd n ∨ 0 < x + 1
[PROOFSTEP]
rw [or_iff_not_imp_left, ← not_le, ← Nat.even_iff_not_odd]
[GOAL]
case refine'_1
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : 0 < ∑ i in range n, x ^ i
⊢ Even n → ¬x + 1 ≤ 0
[PROOFSTEP]
refine' fun hn hx => h.not_le _
[GOAL]
case refine'_1
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn✝ : n ≠ 0
h : 0 < ∑ i in range n, x ^ i
hn : Even n
hx : x + 1 ≤ 0
⊢ ∑ i in range n, x ^ i ≤ 0
[PROOFSTEP]
simpa [if_pos hn] using geom_sum_alternating_of_le_neg_one hx n
[GOAL]
case refine'_2
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
⊢ Odd n ∨ 0 < x + 1 → 0 < ∑ i in range n, x ^ i
[PROOFSTEP]
rintro (hn | hx')
[GOAL]
case refine'_2.inl
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn✝ : n ≠ 0
hn : Odd n
⊢ 0 < ∑ i in range n, x ^ i
[PROOFSTEP]
exact hn.geom_sum_pos
[GOAL]
case refine'_2.inr
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
hx' : 0 < x + 1
⊢ 0 < ∑ i in range n, x ^ i
[PROOFSTEP]
exact geom_sum_pos' hx' hn
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
hn : n ≠ 0
⊢ ∑ i in range n, x ^ i ≠ 0
[PROOFSTEP]
obtain _ | _ | n := n
[GOAL]
case zero
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
hn : Nat.zero ≠ 0
⊢ ∑ i in range Nat.zero, x ^ i ≠ 0
[PROOFSTEP]
cases hn rfl
[GOAL]
case succ.zero
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
hn : Nat.succ Nat.zero ≠ 0
⊢ ∑ i in range (Nat.succ Nat.zero), x ^ i ≠ 0
[PROOFSTEP]
simp only [Nat.zero_eq, ← Nat.one_eq_succ_zero, range_one, sum_singleton, pow_zero, ne_eq, one_ne_zero, not_false_iff]
[GOAL]
case succ.succ
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
[PROOFSTEP]
rw [Ne.def, eq_neg_iff_add_eq_zero, ← Ne.def] at hx 
[GOAL]
case succ.succ
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
[PROOFSTEP]
obtain h | h := hx.lt_or_lt
[GOAL]
case succ.succ.inl
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : x + 1 < 0
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
[PROOFSTEP]
have := geom_sum_alternating_of_lt_neg_one h n.one_lt_succ_succ
[GOAL]
case succ.succ.inl
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : x + 1 < 0
this :
  if Even (Nat.succ (Nat.succ n)) then ∑ i in range (Nat.succ (Nat.succ n)), x ^ i < 0
  else 1 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
[PROOFSTEP]
split_ifs at this 
[GOAL]
case pos
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : x + 1 < 0
h✝ : Even (Nat.succ (Nat.succ n))
this : ∑ i in range (Nat.succ (Nat.succ n)), x ^ i < 0
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
[PROOFSTEP]
exact this.ne
[GOAL]
case neg
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : x + 1 < 0
h✝ : ¬Even (Nat.succ (Nat.succ n))
this : 1 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
[PROOFSTEP]
exact (zero_lt_one.trans this).ne'
[GOAL]
case succ.succ.inr
α : Type u
β : Type u_1
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : 0 < x + 1
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
[PROOFSTEP]
exact (geom_sum_pos' h n.succ.succ_ne_zero).ne'
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
⊢ ∑ i in range n, x ^ i = 0 ↔ x = -1 ∧ Even n
[PROOFSTEP]
refine' ⟨fun h => _, @fun ⟨h, hn⟩ => by simp only [h, hn, neg_one_geom_sum, if_true]⟩
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn✝ : n ≠ 0
x✝ : x = -1 ∧ Even n
h : x = -1
hn : Even n
⊢ ∑ i in range n, x ^ i = 0
[PROOFSTEP]
simp only [h, hn, neg_one_geom_sum, if_true]
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : ∑ i in range n, x ^ i = 0
⊢ x = -1 ∧ Even n
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
⊢ ∑ i in range n, x ^ i ≠ 0
[PROOFSTEP]
have hx := eq_or_ne x (-1)
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1 ∨ x ≠ -1
⊢ ∑ i in range n, x ^ i ≠ 0
[PROOFSTEP]
cases' hx with hx hx
[GOAL]
case inl
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ ∑ i in range n, x ^ i ≠ 0
[PROOFSTEP]
rw [hx, neg_one_geom_sum]
[GOAL]
case inl
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ (if Even n then 0 else 1) ≠ 0
[PROOFSTEP]
simp only [h hx, ne_eq, ite_eq_left_iff, one_ne_zero, not_forall, exists_prop, and_true]
[GOAL]
case inr
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x ≠ -1
⊢ ∑ i in range n, x ^ i ≠ 0
[PROOFSTEP]
exact geom_sum_ne_zero hx hn
[GOAL]
α : Type u
β : Type u_1
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
⊢ ∑ i in range n, x ^ i < 0 ↔ Even n ∧ x + 1 < 0
[PROOFSTEP]
rw [← not_iff_not, not_lt, le_iff_lt_or_eq, eq_comm, or_congr (geom_sum_pos_iff hn) (geom_sum_eq_zero_iff_neg_one hn),
  Nat.odd_iff_not_even, ← add_eq_zero_iff_eq_neg, not_and, not_lt, le_iff_lt_or_eq, eq_comm, ← imp_iff_not_or, or_comm,
  and_comm, Decidable.and_or_imp, or_comm]
