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

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

State before:
α : Type
inst✝ : LinearOrderedCommRing α
a b : α
k : ℕ
z : α
h₁ : z < 0
h₂ : Odd k
⊢ z ^ k < 0
Tactic:
cases k with
| zero    => simp at h₂
| succ k' =>
  simp at h₂
  have k'Even := of_not_not (mt Nat.even_add_one.mpr h₂)
  have rc := powNegEven h₁ k'Even
  simp [Int.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₂ : Odd 0
⊢ z ^ 0 < 0
Tactic:
simp at h₂
State after:
no goals

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

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'Even := of_not_not (mt Nat.even_add_one.mpr h₂)
State after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : ¬Even (k' + 1)
k'Even : 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'Even : Even k'
⊢ z ^ (k' + 1) < 0
Tactic:
have rc := powNegEven h₁ k'Even
State after:
case succ
α : Type
inst✝ : LinearOrderedCommRing α
a b z : α
h₁ : z < 0
k' : ℕ
h₂ : ¬Even (k' + 1)
k'Even : Even 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'Even : Even k'
rc : z ^ k' > 0
⊢ z ^ (k' + 1) < 0
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'Even : Even k'
rc : z ^ k' > 0
mulZ : z * 0 > z * z ^ k'
⊢ z ^ (k' + 1) < 0

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

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