This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> A e. RR )
expgt0b.m 
|- ( ph -> N e. NN )
expgt0b.1 
|- ( ph -> -. 2 || N )
Assertion expgt0b 
|- ( ph -> ( 0 < A <-> 0 < ( A ^ N ) ) )

Proof

Step Hyp Ref Expression
1 expgt0b.n 
 |-  ( ph -> A e. RR )
2 expgt0b.m 
 |-  ( ph -> N e. NN )
3 expgt0b.1 
 |-  ( ph -> -. 2 || N )
4 1 adantr 
 |-  ( ( ph /\ 0 < A ) -> A e. RR )
5 2 nnzd 
 |-  ( ph -> N e. ZZ )
6 5 adantr 
 |-  ( ( ph /\ 0 < A ) -> N e. ZZ )
7 simpr 
 |-  ( ( ph /\ 0 < A ) -> 0 < A )
8 expgt0 
 |-  ( ( A e. RR /\ N e. ZZ /\ 0 < A ) -> 0 < ( A ^ N ) )
9 4 6 7 8 syl3anc 
 |-  ( ( ph /\ 0 < A ) -> 0 < ( A ^ N ) )
10 9 ex 
 |-  ( ph -> ( 0 < A -> 0 < ( A ^ N ) ) )
11 0red 
 |-  ( ph -> 0 e. RR )
12 11 1 lttrid 
 |-  ( ph -> ( 0 < A <-> -. ( 0 = A \/ A < 0 ) ) )
13 12 notbid 
 |-  ( ph -> ( -. 0 < A <-> -. -. ( 0 = A \/ A < 0 ) ) )
14 notnotr 
 |-  ( -. -. ( 0 = A \/ A < 0 ) -> ( 0 = A \/ A < 0 ) )
15 0re 
 |-  0 e. RR
16 15 ltnri 
 |-  -. 0 < 0
17 2 0expd 
 |-  ( ph -> ( 0 ^ N ) = 0 )
18 17 breq2d 
 |-  ( ph -> ( 0 < ( 0 ^ N ) <-> 0 < 0 ) )
19 16 18 mtbiri 
 |-  ( ph -> -. 0 < ( 0 ^ N ) )
20 19 adantr 
 |-  ( ( ph /\ 0 = A ) -> -. 0 < ( 0 ^ N ) )
21 simpr 
 |-  ( ( ph /\ 0 = A ) -> 0 = A )
22 21 eqcomd 
 |-  ( ( ph /\ 0 = A ) -> A = 0 )
23 22 oveq1d 
 |-  ( ( ph /\ 0 = A ) -> ( A ^ N ) = ( 0 ^ N ) )
24 23 breq2d 
 |-  ( ( ph /\ 0 = A ) -> ( 0 < ( A ^ N ) <-> 0 < ( 0 ^ N ) ) )
25 20 24 mtbird 
 |-  ( ( ph /\ 0 = A ) -> -. 0 < ( A ^ N ) )
26 25 ex 
 |-  ( ph -> ( 0 = A -> -. 0 < ( A ^ N ) ) )
27 1 renegcld 
 |-  ( ph -> -u A e. RR )
28 27 adantr 
 |-  ( ( ph /\ 0 < -u A ) -> -u A e. RR )
29 5 adantr 
 |-  ( ( ph /\ 0 < -u A ) -> N e. ZZ )
30 simpr 
 |-  ( ( ph /\ 0 < -u A ) -> 0 < -u A )
31 expgt0 
 |-  ( ( -u A e. RR /\ N e. ZZ /\ 0 < -u A ) -> 0 < ( -u A ^ N ) )
32 28 29 30 31 syl3anc 
 |-  ( ( ph /\ 0 < -u A ) -> 0 < ( -u A ^ N ) )
33 32 ex 
 |-  ( ph -> ( 0 < -u A -> 0 < ( -u A ^ N ) ) )
34 1 recnd 
 |-  ( ph -> A e. CC )
35 oexpneg 
 |-  ( ( A e. CC /\ N e. NN /\ -. 2 || N ) -> ( -u A ^ N ) = -u ( A ^ N ) )
36 34 2 3 35 syl3anc 
 |-  ( ph -> ( -u A ^ N ) = -u ( A ^ N ) )
37 36 breq2d 
 |-  ( ph -> ( 0 < ( -u A ^ N ) <-> 0 < -u ( A ^ N ) ) )
38 37 biimpd 
 |-  ( ph -> ( 0 < ( -u A ^ N ) -> 0 < -u ( A ^ N ) ) )
39 2 nnnn0d 
 |-  ( ph -> N e. NN0 )
40 1 39 reexpcld 
 |-  ( ph -> ( A ^ N ) e. RR )
41 40 renegcld 
 |-  ( ph -> -u ( A ^ N ) e. RR )
42 11 41 lttrid 
 |-  ( ph -> ( 0 < -u ( A ^ N ) <-> -. ( 0 = -u ( A ^ N ) \/ -u ( A ^ N ) < 0 ) ) )
43 pm2.46 
 |-  ( -. ( 0 = -u ( A ^ N ) \/ -u ( A ^ N ) < 0 ) -> -. -u ( A ^ N ) < 0 )
44 42 43 biimtrdi 
 |-  ( ph -> ( 0 < -u ( A ^ N ) -> -. -u ( A ^ N ) < 0 ) )
45 33 38 44 3syld 
 |-  ( ph -> ( 0 < -u A -> -. -u ( A ^ N ) < 0 ) )
46 1 lt0neg1d 
 |-  ( ph -> ( A < 0 <-> 0 < -u A ) )
47 40 lt0neg2d 
 |-  ( ph -> ( 0 < ( A ^ N ) <-> -u ( A ^ N ) < 0 ) )
48 47 notbid 
 |-  ( ph -> ( -. 0 < ( A ^ N ) <-> -. -u ( A ^ N ) < 0 ) )
49 45 46 48 3imtr4d 
 |-  ( ph -> ( A < 0 -> -. 0 < ( A ^ N ) ) )
50 26 49 jaod 
 |-  ( ph -> ( ( 0 = A \/ A < 0 ) -> -. 0 < ( A ^ N ) ) )
51 14 50 syl5 
 |-  ( ph -> ( -. -. ( 0 = A \/ A < 0 ) -> -. 0 < ( A ^ N ) ) )
52 13 51 sylbid 
 |-  ( ph -> ( -. 0 < A -> -. 0 < ( A ^ N ) ) )
53 10 52 impcon4bid 
 |-  ( ph -> ( 0 < A <-> 0 < ( A ^ N ) ) )