Theorem: Lean4Axiomatic.Rational.pow_preserves_nonzero (Lean4Axiomatic/Rational/Exponentiation.lean)

State before:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
⊢ p ^ a ≄ 0
Tactic:
intro (_ : p^a ≃ 0)
State after:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
⊢ False

State before:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
⊢ False
Tactic:
have Exists.intro (n : ℕ) (Exists.intro (m : ℕ) (_ : a ≃ n - m)) :=
  Integer.as_diff a
State after:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
⊢ False

State before:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
⊢ False
Tactic:
have : p^n / p^m ≃ 0 := calc
  _ = p^n / p^m     := rfl
  _ ≃ p^((n:ℤ) - m) := eqv_symm pow_diff
  _ ≃ p^a           := pow_substR (Rel.symm ‹a ≃ n - m›)
  _ ≃ 0             := ‹p^a ≃ 0›
State after:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
this : p ^ n / p ^ m ≃ 0
⊢ False

State before:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
this : p ^ n / p ^ m ≃ 0
⊢ False
Tactic:
have : p^n ≃ 0 := div_eqv_0.mp this
State after:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
this✝ : p ^ n / p ^ m ≃ 0
this : p ^ n ≃ 0
⊢ False

State before:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
this✝ : p ^ n / p ^ m ≃ 0
this : p ^ n ≃ 0
⊢ False
Tactic:
have : p^n ≄ 0 := Natural.pow_preserves_nonzero_base ‹AP (p ≄ 0)›.ev
State after:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
this✝¹ : p ^ n / p ^ m ≃ 0
this✝ : p ^ n ≃ 0
this : p ^ n ≄ 0
⊢ False

State before:
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : Type
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝¹ : Exponentiation ℚ
p : ℚ
a : ℤ
inst✝ : AP (p ≄ 0)
x✝ : p ^ a ≃ 0
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
this✝¹ : p ^ n / p ^ m ≃ 0
this✝ : p ^ n ≃ 0
this : p ^ n ≄ 0
⊢ False
Tactic:
exact absurd ‹p^n ≃ 0› ‹p^n ≄ 0›
State after:
no goals