α : Type u
β : Type ?u.231983
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
α : Type u
β : Type ?u.231983
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
have hx0 : x ≤ 0 := (le_add_of_nonneg_right zero_le_one).trans hx
case zero
α : Type u
β : Type ?u.231983
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

case succ
α : Type u
β : Type ?u.231983
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
α : Type u
β : Type ?u.231983
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
induction' n with n ih
case succ
α : Type u
β : Type ?u.231983
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
case succ
α : Type u
β : Type ?u.231983
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
simp only [Nat.even_add_one, geom_sum_succ]
case succ.inl
α : Type u
β : Type ?u.231983
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

case succ.inr
α : Type u
β : Type ?u.231983
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
case succ
α : Type u
β : Type ?u.231983
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
split_ifs at ih with h
no goals
case zero
α : Type u
β : Type ?u.231983
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
simp only [Nat.zero_eq, range_zero, sum_empty, le_refl, ite_true]
case succ.inl
α : Type u
β : Type ?u.231983
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
case succ.inl
α : Type u
β : Type ?u.231983
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
rw [if_neg (not_not_intro h), le_add_iff_nonneg_left]
no goals
case succ.inl
α : Type u
β : Type ?u.231983
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
exact mul_nonneg_of_nonpos_of_nonpos hx0 ih
case succ.inr
α : Type u
β : Type ?u.231983
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
case succ.inr
α : Type u
β : Type ?u.231983
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
rw [if_pos h]
case succ.inr
α : Type u
β : Type ?u.231983
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
case succ.inr
α : Type u
β : Type ?u.231983
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
refine' (add_le_add_right _ _).trans hx
no goals
case succ.inr
α : Type u
β : Type ?u.231983
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
simpa only [mul_one] using mul_le_mul_of_nonpos_left ih hx0