Metamath Proof Explorer

Theorem cxple

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

Ref Expression
Assertion cxple 
|- ( ( ( 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 cxplt 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( C e. RR /\ B e. RR ) ) -> ( C < B <-> ( A ^c C ) < ( A ^c B ) ) )
2 1 ancom2s 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( C < B <-> ( A ^c C ) < ( A ^c B ) ) )
3 2 notbid 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( -. C < B <-> -. ( A ^c C ) < ( A ^c B ) ) )
4 lenlt 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B <_ C <-> -. C < B ) )
5 4 adantl 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( B <_ C <-> -. C < B ) )
6 simpll 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> A e. RR )
7 0red 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> 0 e. RR )
8 1red 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> 1 e. RR )
9 0lt1 
 |-  0 < 1
10 9 a1i 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> 0 < 1 )
11 simplr 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> 1 < A )
12 7 8 6 10 11 lttrd 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> 0 < A )
13 7 6 12 ltled 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> 0 <_ A )
14 simprl 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> B e. RR )
15 recxpcl 
 |-  ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> ( A ^c B ) e. RR )
16 6 13 14 15 syl3anc 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( A ^c B ) e. RR )
17 simprr 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> C e. RR )
18 recxpcl 
 |-  ( ( A e. RR /\ 0 <_ A /\ C e. RR ) -> ( A ^c C ) e. RR )
19 6 13 17 18 syl3anc 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( A ^c C ) e. RR )
20 16 19 lenltd 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( ( A ^c B ) <_ ( A ^c C ) <-> -. ( A ^c C ) < ( A ^c B ) ) )
21 3 5 20 3bitr4d 
 |-  ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( B <_ C <-> ( A ^c B ) <_ ( A ^c C ) ) )