English
If x ≠ -1 and n ≠ 0, then the sum ∑ x^i is nonzero.
Русский
Если x ≠ −1 и n ≠ 0, сумма ∑ x^i не равна нулю.
LaTeX
$$$x \\neq -1 \\land n \\neq 0 \\Rightarrow \\sum_{i=0}^{n-1} x^i \\neq 0$$$
Lean4
theorem geom_sum_ne_zero (hx : x ≠ -1) (hn : n ≠ 0) : ∑ i ∈ range n, x ^ i ≠ 0 :=
by
obtain _ | _ | n := n
· cases hn rfl
· simp only [zero_add, range_one, sum_singleton, pow_zero, ne_eq, one_ne_zero, not_false_eq_true]
rw [Ne, eq_neg_iff_add_eq_zero, ← Ne] at hx
obtain h | h := hx.lt_or_gt
· have := geom_sum_alternating_of_lt_neg_one h n.one_lt_succ_succ
split_ifs at this
· exact this.ne
· exact (zero_lt_one.trans this).ne'
· exact (geom_sum_pos' h n.succ.succ_ne_zero).ne'
