Metamath Proof Explorer

Theorem cxple2a

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

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

Proof

Step Hyp Ref Expression
1 simpl3 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) /\ 0 < C ) -> A <_ B )
2 simp11 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) -> A e. RR )
3 2 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) /\ 0 < C ) -> A e. RR )
4 simpl2l 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) /\ 0 < C ) -> 0 <_ A )
5 simp12 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) -> B e. RR )
6 5 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) /\ 0 < C ) -> B e. RR )
7 0red 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) /\ 0 < C ) -> 0 e. RR )
8 7 3 6 4 1 letrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) /\ 0 < C ) -> 0 <_ B )
9 simp13 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) -> C e. RR )
10 9 anim1i 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) /\ 0 < C ) -> ( C e. RR /\ 0 < C ) )
11 elrp 
 |-  ( C e. RR+ <-> ( C e. RR /\ 0 < C ) )
12 10 11 sylibr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) /\ 0 < C ) -> C e. RR+ )
13 cxple2 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( A <_ B <-> ( A ^c C ) <_ ( B ^c C ) ) )
14 3 4 6 8 12 13 syl221anc 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) /\ 0 < C ) -> ( A <_ B <-> ( A ^c C ) <_ ( B ^c C ) ) )
15 1 14 mpbid 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) /\ 0 < C ) -> ( A ^c C ) <_ ( B ^c C ) )
16 1le1 
 |-  1 <_ 1
17 16 a1i 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) /\ 0 = C ) -> 1 <_ 1 )
18 2 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) -> A e. CC )
19 cxp0 
 |-  ( A e. CC -> ( A ^c 0 ) = 1 )
20 18 19 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) -> ( A ^c 0 ) = 1 )
21 oveq2 
 |-  ( 0 = C -> ( A ^c 0 ) = ( A ^c C ) )
22 20 21 sylan9req 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) /\ 0 = C ) -> 1 = ( A ^c C ) )
23 5 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) -> B e. CC )
24 cxp0 
 |-  ( B e. CC -> ( B ^c 0 ) = 1 )
25 23 24 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) -> ( B ^c 0 ) = 1 )
26 oveq2 
 |-  ( 0 = C -> ( B ^c 0 ) = ( B ^c C ) )
27 25 26 sylan9req 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) /\ 0 = C ) -> 1 = ( B ^c C ) )
28 17 22 27 3brtr3d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) /\ 0 = C ) -> ( A ^c C ) <_ ( B ^c C ) )
29 simp2r 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) -> 0 <_ C )
30 0re 
 |-  0 e. RR
31 leloe 
 |-  ( ( 0 e. RR /\ C e. RR ) -> ( 0 <_ C <-> ( 0 < C \/ 0 = C ) ) )
32 30 9 31 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) -> ( 0 <_ C <-> ( 0 < C \/ 0 = C ) ) )
33 29 32 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) -> ( 0 < C \/ 0 = C ) )
34 15 28 33 mpjaodan 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) -> ( A ^c C ) <_ ( B ^c C ) )