Metamath Proof Explorer

Theorem oexpreposd

Description: Lemma for dffltz . TODO-SN?: This can be used to show exp11d holds for all integers when the exponent is odd. The more standard -. 2 || M should be used. (Contributed by SN, 4-Mar-2023)

Ref Expression
Hypotheses oexpreposd.n 
|- ( ph -> N e. RR )
oexpreposd.m 
|- ( ph -> M e. NN )
oexpreposd.1 
|- ( ph -> -. ( M / 2 ) e. NN )
Assertion oexpreposd 
|- ( ph -> ( 0 < N <-> 0 < ( N ^ M ) ) )

Proof

Step Hyp Ref Expression
1 oexpreposd.n 
 |-  ( ph -> N e. RR )
2 oexpreposd.m 
 |-  ( ph -> M e. NN )
3 oexpreposd.1 
 |-  ( ph -> -. ( M / 2 ) e. NN )
4 1 adantr 
 |-  ( ( ph /\ 0 < N ) -> N e. RR )
5 2 nnzd 
 |-  ( ph -> M e. ZZ )
6 5 adantr 
 |-  ( ( ph /\ 0 < N ) -> M e. ZZ )
7 simpr 
 |-  ( ( ph /\ 0 < N ) -> 0 < N )
8 expgt0 
 |-  ( ( N e. RR /\ M e. ZZ /\ 0 < N ) -> 0 < ( N ^ M ) )
9 4 6 7 8 syl3anc 
 |-  ( ( ph /\ 0 < N ) -> 0 < ( N ^ M ) )
10 9 ex 
 |-  ( ph -> ( 0 < N -> 0 < ( N ^ M ) ) )
11 0red 
 |-  ( ph -> 0 e. RR )
12 11 1 lttrid 
 |-  ( ph -> ( 0 < N <-> -. ( 0 = N \/ N < 0 ) ) )
13 12 notbid 
 |-  ( ph -> ( -. 0 < N <-> -. -. ( 0 = N \/ N < 0 ) ) )
14 notnotr 
 |-  ( -. -. ( 0 = N \/ N < 0 ) -> ( 0 = N \/ N < 0 ) )
15 0re 
 |-  0 e. RR
16 15 ltnri 
 |-  -. 0 < 0
17 2 0expd 
 |-  ( ph -> ( 0 ^ M ) = 0 )
18 17 breq2d 
 |-  ( ph -> ( 0 < ( 0 ^ M ) <-> 0 < 0 ) )
19 16 18 mtbiri 
 |-  ( ph -> -. 0 < ( 0 ^ M ) )
20 19 adantr 
 |-  ( ( ph /\ 0 = N ) -> -. 0 < ( 0 ^ M ) )
21 simpr 
 |-  ( ( ph /\ 0 = N ) -> 0 = N )
22 21 eqcomd 
 |-  ( ( ph /\ 0 = N ) -> N = 0 )
23 22 oveq1d 
 |-  ( ( ph /\ 0 = N ) -> ( N ^ M ) = ( 0 ^ M ) )
24 23 breq2d 
 |-  ( ( ph /\ 0 = N ) -> ( 0 < ( N ^ M ) <-> 0 < ( 0 ^ M ) ) )
25 20 24 mtbird 
 |-  ( ( ph /\ 0 = N ) -> -. 0 < ( N ^ M ) )
26 25 ex 
 |-  ( ph -> ( 0 = N -> -. 0 < ( N ^ M ) ) )
27 1 renegcld 
 |-  ( ph -> -u N e. RR )
28 27 adantr 
 |-  ( ( ph /\ 0 < -u N ) -> -u N e. RR )
29 5 adantr 
 |-  ( ( ph /\ 0 < -u N ) -> M e. ZZ )
30 simpr 
 |-  ( ( ph /\ 0 < -u N ) -> 0 < -u N )
31 expgt0 
 |-  ( ( -u N e. RR /\ M e. ZZ /\ 0 < -u N ) -> 0 < ( -u N ^ M ) )
32 28 29 30 31 syl3anc 
 |-  ( ( ph /\ 0 < -u N ) -> 0 < ( -u N ^ M ) )
33 32 ex 
 |-  ( ph -> ( 0 < -u N -> 0 < ( -u N ^ M ) ) )
34 1 recnd 
 |-  ( ph -> N e. CC )
35 simpr 
 |-  ( ( ph /\ ( M / 2 ) e. ZZ ) -> ( M / 2 ) e. ZZ )
36 zq 
 |-  ( ( M / 2 ) e. ZZ -> ( M / 2 ) e. QQ )
37 36 adantl 
 |-  ( ( ph /\ ( M / 2 ) e. ZZ ) -> ( M / 2 ) e. QQ )
38 qden1elz 
 |-  ( ( M / 2 ) e. QQ -> ( ( denom ` ( M / 2 ) ) = 1 <-> ( M / 2 ) e. ZZ ) )
39 37 38 syl 
 |-  ( ( ph /\ ( M / 2 ) e. ZZ ) -> ( ( denom ` ( M / 2 ) ) = 1 <-> ( M / 2 ) e. ZZ ) )
40 35 39 mpbird 
 |-  ( ( ph /\ ( M / 2 ) e. ZZ ) -> ( denom ` ( M / 2 ) ) = 1 )
41 40 oveq2d 
 |-  ( ( ph /\ ( M / 2 ) e. ZZ ) -> ( ( M / 2 ) x. ( denom ` ( M / 2 ) ) ) = ( ( M / 2 ) x. 1 ) )
42 qmuldeneqnum 
 |-  ( ( M / 2 ) e. QQ -> ( ( M / 2 ) x. ( denom ` ( M / 2 ) ) ) = ( numer ` ( M / 2 ) ) )
43 37 42 syl 
 |-  ( ( ph /\ ( M / 2 ) e. ZZ ) -> ( ( M / 2 ) x. ( denom ` ( M / 2 ) ) ) = ( numer ` ( M / 2 ) ) )
44 35 zcnd 
 |-  ( ( ph /\ ( M / 2 ) e. ZZ ) -> ( M / 2 ) e. CC )
45 44 mulid1d 
 |-  ( ( ph /\ ( M / 2 ) e. ZZ ) -> ( ( M / 2 ) x. 1 ) = ( M / 2 ) )
46 41 43 45 3eqtr3rd 
 |-  ( ( ph /\ ( M / 2 ) e. ZZ ) -> ( M / 2 ) = ( numer ` ( M / 2 ) ) )
47 2 nnred 
 |-  ( ph -> M e. RR )
48 2re 
 |-  2 e. RR
49 48 a1i 
 |-  ( ph -> 2 e. RR )
50 2 nngt0d 
 |-  ( ph -> 0 < M )
51 2pos 
 |-  0 < 2
52 51 a1i 
 |-  ( ph -> 0 < 2 )
53 47 49 50 52 divgt0d 
 |-  ( ph -> 0 < ( M / 2 ) )
54 qgt0numnn 
 |-  ( ( ( M / 2 ) e. QQ /\ 0 < ( M / 2 ) ) -> ( numer ` ( M / 2 ) ) e. NN )
55 36 53 54 syl2anr 
 |-  ( ( ph /\ ( M / 2 ) e. ZZ ) -> ( numer ` ( M / 2 ) ) e. NN )
56 46 55 eqeltrd 
 |-  ( ( ph /\ ( M / 2 ) e. ZZ ) -> ( M / 2 ) e. NN )
57 3 56 mtand 
 |-  ( ph -> -. ( M / 2 ) e. ZZ )
58 evend2 
 |-  ( M e. ZZ -> ( 2 || M <-> ( M / 2 ) e. ZZ ) )
59 5 58 syl 
 |-  ( ph -> ( 2 || M <-> ( M / 2 ) e. ZZ ) )
60 57 59 mtbird 
 |-  ( ph -> -. 2 || M )
61 oexpneg 
 |-  ( ( N e. CC /\ M e. NN /\ -. 2 || M ) -> ( -u N ^ M ) = -u ( N ^ M ) )
62 34 2 60 61 syl3anc 
 |-  ( ph -> ( -u N ^ M ) = -u ( N ^ M ) )
63 62 breq2d 
 |-  ( ph -> ( 0 < ( -u N ^ M ) <-> 0 < -u ( N ^ M ) ) )
64 63 biimpd 
 |-  ( ph -> ( 0 < ( -u N ^ M ) -> 0 < -u ( N ^ M ) ) )
65 2 nnnn0d 
 |-  ( ph -> M e. NN0 )
66 1 65 reexpcld 
 |-  ( ph -> ( N ^ M ) e. RR )
67 66 renegcld 
 |-  ( ph -> -u ( N ^ M ) e. RR )
68 11 67 lttrid 
 |-  ( ph -> ( 0 < -u ( N ^ M ) <-> -. ( 0 = -u ( N ^ M ) \/ -u ( N ^ M ) < 0 ) ) )
69 pm2.46 
 |-  ( -. ( 0 = -u ( N ^ M ) \/ -u ( N ^ M ) < 0 ) -> -. -u ( N ^ M ) < 0 )
70 68 69 syl6bi 
 |-  ( ph -> ( 0 < -u ( N ^ M ) -> -. -u ( N ^ M ) < 0 ) )
71 33 64 70 3syld 
 |-  ( ph -> ( 0 < -u N -> -. -u ( N ^ M ) < 0 ) )
72 1 lt0neg1d 
 |-  ( ph -> ( N < 0 <-> 0 < -u N ) )
73 66 lt0neg2d 
 |-  ( ph -> ( 0 < ( N ^ M ) <-> -u ( N ^ M ) < 0 ) )
74 73 notbid 
 |-  ( ph -> ( -. 0 < ( N ^ M ) <-> -. -u ( N ^ M ) < 0 ) )
75 71 72 74 3imtr4d 
 |-  ( ph -> ( N < 0 -> -. 0 < ( N ^ M ) ) )
76 26 75 jaod 
 |-  ( ph -> ( ( 0 = N \/ N < 0 ) -> -. 0 < ( N ^ M ) ) )
77 14 76 syl5 
 |-  ( ph -> ( -. -. ( 0 = N \/ N < 0 ) -> -. 0 < ( N ^ M ) ) )
78 13 77 sylbid 
 |-  ( ph -> ( -. 0 < N -> -. 0 < ( N ^ M ) ) )
79 10 78 impcon4bid 
 |-  ( ph -> ( 0 < N <-> 0 < ( N ^ M ) ) )