Theorem: Smt.Reconstruct.Arith.powNegEven (Smt/Reconstruct/Arith/ArithMulSign/Lemmas.lean)

State before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
⊢ ∀ {k : ℕ} {z : α}, z < 0 → Even k → z ^ k > 0
Tactic:
intros k z h₁ h₂
State after:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z < 0
h₂ : Even k
⊢ z ^ k > 0

State before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z < 0
h₂ : Even k
⊢ z ^ k > 0
Tactic:
cases k with
| zero    => simp
| succ k' =>
  have k'NotEven := Nat.even_add_one.mp h₂
  have k'Odd := Nat.odd_iff_not_even.mpr k'NotEven
  have rc := powNegOdd h₁ k'Odd
  simp [Pow.pow]
  have mulZ := arith_mul_neg_lt ⟨h₁, rc⟩
  simp at mulZ
  rw [pow_succ, mul_comm]
  exact mulZ
State after:
no goals

State before:
case zero
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
h₂ : Even 0
⊢ z ^ 0 > 0
Tactic:
simp
State after:
no goals

State before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
⊢ z ^ (k' + 1) > 0
Tactic:
have k'NotEven := Nat.even_add_one.mp h₂
State after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
⊢ z ^ (k' + 1) > 0

State before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
⊢ z ^ (k' + 1) > 0
Tactic:
have k'Odd := Nat.odd_iff_not_even.mpr k'NotEven
State after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
⊢ z ^ (k' + 1) > 0

State before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
⊢ z ^ (k' + 1) > 0
Tactic:
have rc := powNegOdd h₁ k'Odd
State after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
⊢ z ^ (k' + 1) > 0

State before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
⊢ z ^ (k' + 1) > 0
Tactic:
simp [Pow.pow]
State after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
⊢ 0 < z ^ (k' + 1)

State before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
⊢ 0 < z ^ (k' + 1)
Tactic:
have mulZ := arith_mul_neg_lt ⟨h₁, rc⟩
State after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
mulZ : z * z ^ k' > z * 0
⊢ 0 < z ^ (k' + 1)

State before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
mulZ : z * z ^ k' > z * 0
⊢ 0 < z ^ (k' + 1)
Tactic:
simp at mulZ
State after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
mulZ : 0 < z * z ^ k'
⊢ 0 < z ^ (k' + 1)

State before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
mulZ : 0 < z * z ^ k'
⊢ 0 < z ^ (k' + 1)
Tactic:
rw [pow_succ, mul_comm]
State after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
mulZ : 0 < z * z ^ k'
⊢ 0 < z * z ^ k'

State before:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : Even (k' + 1)
k'NotEven : ¬Even k'
k'Odd : Odd k'
rc : z ^ k' < 0
mulZ : 0 < z * z ^ k'
⊢ 0 < z * z ^ k'
Tactic:
exact mulZ
State after:
no goals