Theorem: Smt.Reconstruct.Int.pow_neg_even (Smt/Reconstruct/Int/Lemmas.lean)

State before:
a b c d : Int
k : Nat
z : Int
h₁ : z < 0
h₂ : k % 2 = 0
⊢ z ^ k > 0
Tactic:
cases k with
| zero    => simp [Int.pow_zero]
| succ k =>
  have hodd := Nat.even_add_one.mp h₂
  have mulZ : z * z ^ k > z * 0 := Int.mul_lt_mul_of_neg_left (pow_neg_odd h₁ (Nat.mod_two_ne_zero.mp hodd)) h₁
  simp at mulZ
  rw [Int.pow_succ, Int.mul_comm]
  exact mulZ
State after:
no goals

State before:
case zero
a b c d z : Int
h₁ : z < 0
h₂ : 0 % 2 = 0
⊢ z ^ 0 > 0
Tactic:
simp [Int.pow_zero]
State after:
no goals

State before:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
⊢ z ^ (k + 1) > 0
Tactic:
have hodd := Nat.even_add_one.mp h₂
State after:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
⊢ z ^ (k + 1) > 0

State before:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
⊢ z ^ (k + 1) > 0
Tactic:
have mulZ : z * z ^ k > z * 0 := Int.mul_lt_mul_of_neg_left (pow_neg_odd h₁ (Nat.mod_two_ne_zero.mp hodd)) h₁
State after:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
mulZ : z * z ^ k > z * 0
⊢ z ^ (k + 1) > 0

State before:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
mulZ : z * z ^ k > z * 0
⊢ z ^ (k + 1) > 0
Tactic:
simp at mulZ
State after:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
mulZ : 0 < z * z ^ k
⊢ z ^ (k + 1) > 0

State before:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
mulZ : 0 < z * z ^ k
⊢ z ^ (k + 1) > 0
Tactic:
rw [Int.pow_succ, Int.mul_comm]
State after:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
mulZ : 0 < z * z ^ k
⊢ z * z ^ k > 0

State before:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 0
hodd : k % 2 ≠ 0
mulZ : 0 < z * z ^ k
⊢ z * z ^ k > 0
Tactic:
exact mulZ
State after:
no goals