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

State before:
a b c d : Int
k : Nat
z : Int
h₁ : z < 0
h₂ : k % 2 = 1
⊢ z ^ k < 0
Tactic:
cases k with
| zero    => simp at h₂
| succ k =>
  have heven : k % 2 = 0 := Classical.not_not.mp (mt Nat.even_add_one.mpr (Eq.symm h₂ ▸ nofun))
  have mulZ : z * 0 > z * z ^ k := Int.mul_lt_mul_of_neg_left (pow_neg_even h₁ heven) 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 = 1
⊢ z ^ 0 < 0
Tactic:
simp at h₂
State after:
no goals

State before:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 1
⊢ z ^ (k + 1) < 0
Tactic:
have heven : k % 2 = 0 := Classical.not_not.mp (mt Nat.even_add_one.mpr (Eq.symm h₂ ▸ nofun))
State after:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 1
heven : 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 = 1
heven : k % 2 = 0
⊢ z ^ (k + 1) < 0
Tactic:
have mulZ : z * 0 > z * z ^ k := Int.mul_lt_mul_of_neg_left (pow_neg_even h₁ heven) h₁
State after:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 1
heven : k % 2 = 0
mulZ : z * 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 = 1
heven : k % 2 = 0
mulZ : z * 0 > z * z ^ k
⊢ 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 = 1
heven : k % 2 = 0
mulZ : z * z ^ k < 0
⊢ z ^ (k + 1) < 0

State before:
case succ
a b c d z : Int
h₁ : z < 0
k : Nat
h₂ : (k + 1) % 2 = 1
heven : k % 2 = 0
mulZ : z * z ^ k < 0
⊢ 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 = 1
heven : k % 2 = 0
mulZ : z * z ^ k < 0
⊢ z * z ^ k < 0

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