Metamath Proof Explorer

Theorem cxple2

Description: Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Assertion cxple2 
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( A <_ B <-> ( A ^c C ) <_ ( B ^c C ) ) )

Proof

Step Hyp Ref Expression
1 simpl1l 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) -> A e. RR )
2 simpr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) -> 0 < A )
3 1 2 elrpd 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) -> A e. RR+ )
4 3 adantr 
 |-  ( ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) /\ 0 < B ) -> A e. RR+ )
5 simp2l 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> B e. RR )
6 5 ad2antrr 
 |-  ( ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) /\ 0 < B ) -> B e. RR )
7 simpr 
 |-  ( ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) /\ 0 < B ) -> 0 < B )
8 6 7 elrpd 
 |-  ( ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) /\ 0 < B ) -> B e. RR+ )
9 simp3 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> C e. RR+ )
10 9 ad2antrr 
 |-  ( ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) /\ 0 < B ) -> C e. RR+ )
11 simp3 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> C e. RR+ )
12 11 rpred 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> C e. RR )
13 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
14 13 3ad2ant1 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> ( log ` A ) e. RR )
15 12 14 remulcld 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> ( C x. ( log ` A ) ) e. RR )
16 relogcl 
 |-  ( B e. RR+ -> ( log ` B ) e. RR )
17 16 3ad2ant2 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> ( log ` B ) e. RR )
18 12 17 remulcld 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> ( C x. ( log ` B ) ) e. RR )
19 efle 
 |-  ( ( ( C x. ( log ` A ) ) e. RR /\ ( C x. ( log ` B ) ) e. RR ) -> ( ( C x. ( log ` A ) ) <_ ( C x. ( log ` B ) ) <-> ( exp ` ( C x. ( log ` A ) ) ) <_ ( exp ` ( C x. ( log ` B ) ) ) ) )
20 15 18 19 syl2anc 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> ( ( C x. ( log ` A ) ) <_ ( C x. ( log ` B ) ) <-> ( exp ` ( C x. ( log ` A ) ) ) <_ ( exp ` ( C x. ( log ` B ) ) ) ) )
21 efle 
 |-  ( ( ( log ` A ) e. RR /\ ( log ` B ) e. RR ) -> ( ( log ` A ) <_ ( log ` B ) <-> ( exp ` ( log ` A ) ) <_ ( exp ` ( log ` B ) ) ) )
22 14 17 21 syl2anc 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> ( ( log ` A ) <_ ( log ` B ) <-> ( exp ` ( log ` A ) ) <_ ( exp ` ( log ` B ) ) ) )
23 14 17 11 lemul2d 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> ( ( log ` A ) <_ ( log ` B ) <-> ( C x. ( log ` A ) ) <_ ( C x. ( log ` B ) ) ) )
24 reeflog 
 |-  ( A e. RR+ -> ( exp ` ( log ` A ) ) = A )
25 24 3ad2ant1 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> ( exp ` ( log ` A ) ) = A )
26 reeflog 
 |-  ( B e. RR+ -> ( exp ` ( log ` B ) ) = B )
27 26 3ad2ant2 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> ( exp ` ( log ` B ) ) = B )
28 25 27 breq12d 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> ( ( exp ` ( log ` A ) ) <_ ( exp ` ( log ` B ) ) <-> A <_ B ) )
29 22 23 28 3bitr3rd 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> ( A <_ B <-> ( C x. ( log ` A ) ) <_ ( C x. ( log ` B ) ) ) )
30 rpre 
 |-  ( A e. RR+ -> A e. RR )
31 30 3ad2ant1 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> A e. RR )
32 31 recnd 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> A e. CC )
33 rpne0 
 |-  ( A e. RR+ -> A =/= 0 )
34 33 3ad2ant1 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> A =/= 0 )
35 12 recnd 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> C e. CC )
36 cxpef 
 |-  ( ( A e. CC /\ A =/= 0 /\ C e. CC ) -> ( A ^c C ) = ( exp ` ( C x. ( log ` A ) ) ) )
37 32 34 35 36 syl3anc 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> ( A ^c C ) = ( exp ` ( C x. ( log ` A ) ) ) )
38 rpre 
 |-  ( B e. RR+ -> B e. RR )
39 38 3ad2ant2 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> B e. RR )
40 39 recnd 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> B e. CC )
41 rpne0 
 |-  ( B e. RR+ -> B =/= 0 )
42 41 3ad2ant2 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> B =/= 0 )
43 cxpef 
 |-  ( ( B e. CC /\ B =/= 0 /\ C e. CC ) -> ( B ^c C ) = ( exp ` ( C x. ( log ` B ) ) ) )
44 40 42 35 43 syl3anc 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> ( B ^c C ) = ( exp ` ( C x. ( log ` B ) ) ) )
45 37 44 breq12d 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> ( ( A ^c C ) <_ ( B ^c C ) <-> ( exp ` ( C x. ( log ` A ) ) ) <_ ( exp ` ( C x. ( log ` B ) ) ) ) )
46 20 29 45 3bitr4d 
 |-  ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> ( A <_ B <-> ( A ^c C ) <_ ( B ^c C ) ) )
47 4 8 10 46 syl3anc 
 |-  ( ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) /\ 0 < B ) -> ( A <_ B <-> ( A ^c C ) <_ ( B ^c C ) ) )
48 0re 
 |-  0 e. RR
49 simp1l 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> A e. RR )
50 ltnle 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A <-> -. A <_ 0 ) )
51 48 49 50 sylancr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( 0 < A <-> -. A <_ 0 ) )
52 51 biimpa 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) -> -. A <_ 0 )
53 9 rpred 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> C e. RR )
54 53 adantr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) -> C e. RR )
55 rpcxpcl 
 |-  ( ( A e. RR+ /\ C e. RR ) -> ( A ^c C ) e. RR+ )
56 3 54 55 syl2anc 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) -> ( A ^c C ) e. RR+ )
57 rpgt0 
 |-  ( ( A ^c C ) e. RR+ -> 0 < ( A ^c C ) )
58 rpre 
 |-  ( ( A ^c C ) e. RR+ -> ( A ^c C ) e. RR )
59 ltnle 
 |-  ( ( 0 e. RR /\ ( A ^c C ) e. RR ) -> ( 0 < ( A ^c C ) <-> -. ( A ^c C ) <_ 0 ) )
60 48 58 59 sylancr 
 |-  ( ( A ^c C ) e. RR+ -> ( 0 < ( A ^c C ) <-> -. ( A ^c C ) <_ 0 ) )
61 57 60 mpbid 
 |-  ( ( A ^c C ) e. RR+ -> -. ( A ^c C ) <_ 0 )
62 56 61 syl 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) -> -. ( A ^c C ) <_ 0 )
63 53 recnd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> C e. CC )
64 9 rpne0d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> C =/= 0 )
65 0cxp 
 |-  ( ( C e. CC /\ C =/= 0 ) -> ( 0 ^c C ) = 0 )
66 63 64 65 syl2anc 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( 0 ^c C ) = 0 )
67 66 adantr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) -> ( 0 ^c C ) = 0 )
68 67 breq2d 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) -> ( ( A ^c C ) <_ ( 0 ^c C ) <-> ( A ^c C ) <_ 0 ) )
69 62 68 mtbird 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) -> -. ( A ^c C ) <_ ( 0 ^c C ) )
70 52 69 2falsed 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) -> ( A <_ 0 <-> ( A ^c C ) <_ ( 0 ^c C ) ) )
71 breq2 
 |-  ( 0 = B -> ( A <_ 0 <-> A <_ B ) )
72 oveq1 
 |-  ( 0 = B -> ( 0 ^c C ) = ( B ^c C ) )
73 72 breq2d 
 |-  ( 0 = B -> ( ( A ^c C ) <_ ( 0 ^c C ) <-> ( A ^c C ) <_ ( B ^c C ) ) )
74 71 73 bibi12d 
 |-  ( 0 = B -> ( ( A <_ 0 <-> ( A ^c C ) <_ ( 0 ^c C ) ) <-> ( A <_ B <-> ( A ^c C ) <_ ( B ^c C ) ) ) )
75 70 74 syl5ibcom 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) -> ( 0 = B -> ( A <_ B <-> ( A ^c C ) <_ ( B ^c C ) ) ) )
76 75 imp 
 |-  ( ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) /\ 0 = B ) -> ( A <_ B <-> ( A ^c C ) <_ ( B ^c C ) ) )
77 simp2r 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> 0 <_ B )
78 leloe 
 |-  ( ( 0 e. RR /\ B e. RR ) -> ( 0 <_ B <-> ( 0 < B \/ 0 = B ) ) )
79 48 5 78 sylancr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( 0 <_ B <-> ( 0 < B \/ 0 = B ) ) )
80 77 79 mpbid 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( 0 < B \/ 0 = B ) )
81 80 adantr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) -> ( 0 < B \/ 0 = B ) )
82 47 76 81 mpjaodan 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 < A ) -> ( A <_ B <-> ( A ^c C ) <_ ( B ^c C ) ) )
83 simpr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 = A ) -> 0 = A )
84 simpl2r 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 = A ) -> 0 <_ B )
85 83 84 eqbrtrrd 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 = A ) -> A <_ B )
86 66 adantr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 = A ) -> ( 0 ^c C ) = 0 )
87 83 oveq1d 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 = A ) -> ( 0 ^c C ) = ( A ^c C ) )
88 86 87 eqtr3d 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 = A ) -> 0 = ( A ^c C ) )
89 simpl2l 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 = A ) -> B e. RR )
90 53 adantr 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 = A ) -> C e. RR )
91 cxpge0 
 |-  ( ( B e. RR /\ 0 <_ B /\ C e. RR ) -> 0 <_ ( B ^c C ) )
92 89 84 90 91 syl3anc 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 = A ) -> 0 <_ ( B ^c C ) )
93 88 92 eqbrtrrd 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 = A ) -> ( A ^c C ) <_ ( B ^c C ) )
94 85 93 2thd 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) /\ 0 = A ) -> ( A <_ B <-> ( A ^c C ) <_ ( B ^c C ) ) )
95 simp1r 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> 0 <_ A )
96 leloe 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
97 48 49 96 sylancr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
98 95 97 mpbid 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( 0 < A \/ 0 = A ) )
99 82 94 98 mpjaodan 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( A <_ B <-> ( A ^c C ) <_ ( B ^c C ) ) )