Metamath Proof Explorer

Theorem expgt0b

Description: A real number A raised to an odd integer power is positive iff it is positive. (Contributed by SN, 4-Mar-2023) Use the more standard -. 2 || N (Revised by Thierry Arnoux, 14-Jun-2025)

Ref Expression
Hypotheses expgt0b.n ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
expgt0b.m ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
expgt0b.1 ⊢ ( 𝜑 → ¬ 2 ∥ 𝑁 )
Assertion expgt0b ( 𝜑 → ( 0 < 𝐴 ↔ 0 < ( 𝐴 ↑ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 expgt0b.n ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 expgt0b.m ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 expgt0b.1 ⊢ ( 𝜑 → ¬ 2 ∥ 𝑁 )
4 1 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝐴 ∈ ℝ )
5 2 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
6 5 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝑁 ∈ ℤ )
7 simpr ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 0 < 𝐴 )
8 expgt0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 0 < 𝐴 ) → 0 < ( 𝐴 ↑ 𝑁 ) )
9 4 6 7 8 syl3anc ⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 0 < ( 𝐴 ↑ 𝑁 ) )
10 9 ex ⊢ ( 𝜑 → ( 0 < 𝐴 → 0 < ( 𝐴 ↑ 𝑁 ) ) )
11 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
12 11 1 lttrid ⊢ ( 𝜑 → ( 0 < 𝐴 ↔ ¬ ( 0 = 𝐴 ∨ 𝐴 < 0 ) ) )
13 12 notbid ⊢ ( 𝜑 → ( ¬ 0 < 𝐴 ↔ ¬ ¬ ( 0 = 𝐴 ∨ 𝐴 < 0 ) ) )
14 notnotr ⊢ ( ¬ ¬ ( 0 = 𝐴 ∨ 𝐴 < 0 ) → ( 0 = 𝐴 ∨ 𝐴 < 0 ) )
15 0re ⊢ 0 ∈ ℝ
16 15 ltnri ⊢ ¬ 0 < 0
17 2 0expd ⊢ ( 𝜑 → ( 0 ↑ 𝑁 ) = 0 )
18 17 breq2d ⊢ ( 𝜑 → ( 0 < ( 0 ↑ 𝑁 ) ↔ 0 < 0 ) )
19 16 18 mtbiri ⊢ ( 𝜑 → ¬ 0 < ( 0 ↑ 𝑁 ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → ¬ 0 < ( 0 ↑ 𝑁 ) )
21 simpr ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → 0 = 𝐴 )
22 21 eqcomd ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → 𝐴 = 0 )
23 22 oveq1d ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → ( 𝐴 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
24 23 breq2d ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → ( 0 < ( 𝐴 ↑ 𝑁 ) ↔ 0 < ( 0 ↑ 𝑁 ) ) )
25 20 24 mtbird ⊢ ( ( 𝜑 ∧ 0 = 𝐴 ) → ¬ 0 < ( 𝐴 ↑ 𝑁 ) )
26 25 ex ⊢ ( 𝜑 → ( 0 = 𝐴 → ¬ 0 < ( 𝐴 ↑ 𝑁 ) ) )
27 1 renegcld ⊢ ( 𝜑 → - 𝐴 ∈ ℝ )
28 27 adantr ⊢ ( ( 𝜑 ∧ 0 < - 𝐴 ) → - 𝐴 ∈ ℝ )
29 5 adantr ⊢ ( ( 𝜑 ∧ 0 < - 𝐴 ) → 𝑁 ∈ ℤ )
30 simpr ⊢ ( ( 𝜑 ∧ 0 < - 𝐴 ) → 0 < - 𝐴 )
31 expgt0 ⊢ ( ( - 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 0 < - 𝐴 ) → 0 < ( - 𝐴 ↑ 𝑁 ) )
32 28 29 30 31 syl3anc ⊢ ( ( 𝜑 ∧ 0 < - 𝐴 ) → 0 < ( - 𝐴 ↑ 𝑁 ) )
33 32 ex ⊢ ( 𝜑 → ( 0 < - 𝐴 → 0 < ( - 𝐴 ↑ 𝑁 ) ) )
34 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
35 oexpneg ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( - 𝐴 ↑ 𝑁 ) = - ( 𝐴 ↑ 𝑁 ) )
36 34 2 3 35 syl3anc ⊢ ( 𝜑 → ( - 𝐴 ↑ 𝑁 ) = - ( 𝐴 ↑ 𝑁 ) )
37 36 breq2d ⊢ ( 𝜑 → ( 0 < ( - 𝐴 ↑ 𝑁 ) ↔ 0 < - ( 𝐴 ↑ 𝑁 ) ) )
38 37 biimpd ⊢ ( 𝜑 → ( 0 < ( - 𝐴 ↑ 𝑁 ) → 0 < - ( 𝐴 ↑ 𝑁 ) ) )
39 2 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
40 1 39 reexpcld ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℝ )
41 40 renegcld ⊢ ( 𝜑 → - ( 𝐴 ↑ 𝑁 ) ∈ ℝ )
42 11 41 lttrid ⊢ ( 𝜑 → ( 0 < - ( 𝐴 ↑ 𝑁 ) ↔ ¬ ( 0 = - ( 𝐴 ↑ 𝑁 ) ∨ - ( 𝐴 ↑ 𝑁 ) < 0 ) ) )
43 pm2.46 ⊢ ( ¬ ( 0 = - ( 𝐴 ↑ 𝑁 ) ∨ - ( 𝐴 ↑ 𝑁 ) < 0 ) → ¬ - ( 𝐴 ↑ 𝑁 ) < 0 )
44 42 43 biimtrdi ⊢ ( 𝜑 → ( 0 < - ( 𝐴 ↑ 𝑁 ) → ¬ - ( 𝐴 ↑ 𝑁 ) < 0 ) )
45 33 38 44 3syld ⊢ ( 𝜑 → ( 0 < - 𝐴 → ¬ - ( 𝐴 ↑ 𝑁 ) < 0 ) )
46 1 lt0neg1d ⊢ ( 𝜑 → ( 𝐴 < 0 ↔ 0 < - 𝐴 ) )
47 40 lt0neg2d ⊢ ( 𝜑 → ( 0 < ( 𝐴 ↑ 𝑁 ) ↔ - ( 𝐴 ↑ 𝑁 ) < 0 ) )
48 47 notbid ⊢ ( 𝜑 → ( ¬ 0 < ( 𝐴 ↑ 𝑁 ) ↔ ¬ - ( 𝐴 ↑ 𝑁 ) < 0 ) )
49 45 46 48 3imtr4d ⊢ ( 𝜑 → ( 𝐴 < 0 → ¬ 0 < ( 𝐴 ↑ 𝑁 ) ) )
50 26 49 jaod ⊢ ( 𝜑 → ( ( 0 = 𝐴 ∨ 𝐴 < 0 ) → ¬ 0 < ( 𝐴 ↑ 𝑁 ) ) )
51 14 50 syl5 ⊢ ( 𝜑 → ( ¬ ¬ ( 0 = 𝐴 ∨ 𝐴 < 0 ) → ¬ 0 < ( 𝐴 ↑ 𝑁 ) ) )
52 13 51 sylbid ⊢ ( 𝜑 → ( ¬ 0 < 𝐴 → ¬ 0 < ( 𝐴 ↑ 𝑁 ) ) )
53 10 52 impcon4bid ⊢ ( 𝜑 → ( 0 < 𝐴 ↔ 0 < ( 𝐴 ↑ 𝑁 ) ) )