Metamath Proof Explorer

Theorem cxplea

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

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

Proof

Step Hyp Ref Expression
1 simpl3 
 |-  ( ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) /\ 1 < A ) -> B <_ C )
2 simpl1l 
 |-  ( ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) /\ 1 < A ) -> A e. RR )
3 simpr 
 |-  ( ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) /\ 1 < A ) -> 1 < A )
4 simpl2 
 |-  ( ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) /\ 1 < A ) -> ( B e. RR /\ C e. RR ) )
5 cxple 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( B <_ C <-> ( A ^c B ) <_ ( A ^c C ) ) )
6 2 3 4 5 syl21anc 
 |-  ( ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) /\ 1 < A ) -> ( B <_ C <-> ( A ^c B ) <_ ( A ^c C ) ) )
7 1 6 mpbid 
 |-  ( ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) /\ 1 < A ) -> ( A ^c B ) <_ ( A ^c C ) )
8 1le1 
 |-  1 <_ 1
9 simp2l 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) -> B e. RR )
10 9 recnd 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) -> B e. CC )
11 1cxp 
 |-  ( B e. CC -> ( 1 ^c B ) = 1 )
12 10 11 syl 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) -> ( 1 ^c B ) = 1 )
13 simp2r 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) -> C e. RR )
14 13 recnd 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) -> C e. CC )
15 1cxp 
 |-  ( C e. CC -> ( 1 ^c C ) = 1 )
16 14 15 syl 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) -> ( 1 ^c C ) = 1 )
17 12 16 breq12d 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) -> ( ( 1 ^c B ) <_ ( 1 ^c C ) <-> 1 <_ 1 ) )
18 8 17 mpbiri 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) -> ( 1 ^c B ) <_ ( 1 ^c C ) )
19 oveq1 
 |-  ( 1 = A -> ( 1 ^c B ) = ( A ^c B ) )
20 oveq1 
 |-  ( 1 = A -> ( 1 ^c C ) = ( A ^c C ) )
21 19 20 breq12d 
 |-  ( 1 = A -> ( ( 1 ^c B ) <_ ( 1 ^c C ) <-> ( A ^c B ) <_ ( A ^c C ) ) )
22 18 21 syl5ibcom 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) -> ( 1 = A -> ( A ^c B ) <_ ( A ^c C ) ) )
23 22 imp 
 |-  ( ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) /\ 1 = A ) -> ( A ^c B ) <_ ( A ^c C ) )
24 1re 
 |-  1 e. RR
25 leloe 
 |-  ( ( 1 e. RR /\ A e. RR ) -> ( 1 <_ A <-> ( 1 < A \/ 1 = A ) ) )
26 24 25 mpan 
 |-  ( A e. RR -> ( 1 <_ A <-> ( 1 < A \/ 1 = A ) ) )
27 26 biimpa 
 |-  ( ( A e. RR /\ 1 <_ A ) -> ( 1 < A \/ 1 = A ) )
28 27 3ad2ant1 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) -> ( 1 < A \/ 1 = A ) )
29 7 23 28 mpjaodan 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) -> ( A ^c B ) <_ ( A ^c C ) )