Metamath Proof Explorer

Theorem cxple3

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

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

Proof

Step Hyp Ref Expression
1 cxplt3 
 |-  ( ( ( A e. RR+ /\ A < 1 ) /\ ( C e. RR /\ B e. RR ) ) -> ( C < B <-> ( A ^c B ) < ( A ^c C ) ) )
2 1 ancom2s 
 |-  ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( C < B <-> ( A ^c B ) < ( A ^c C ) ) )
3 2 notbid 
 |-  ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( -. C < B <-> -. ( A ^c B ) < ( A ^c C ) ) )
4 lenlt 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B <_ C <-> -. C < B ) )
5 4 adantl 
 |-  ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( B <_ C <-> -. C < B ) )
6 rpcxpcl 
 |-  ( ( A e. RR+ /\ C e. RR ) -> ( A ^c C ) e. RR+ )
7 6 ad2ant2rl 
 |-  ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( A ^c C ) e. RR+ )
8 rpcxpcl 
 |-  ( ( A e. RR+ /\ B e. RR ) -> ( A ^c B ) e. RR+ )
9 8 ad2ant2r 
 |-  ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( A ^c B ) e. RR+ )
10 rpre 
 |-  ( ( A ^c C ) e. RR+ -> ( A ^c C ) e. RR )
11 rpre 
 |-  ( ( A ^c B ) e. RR+ -> ( A ^c B ) e. RR )
12 lenlt 
 |-  ( ( ( A ^c C ) e. RR /\ ( A ^c B ) e. RR ) -> ( ( A ^c C ) <_ ( A ^c B ) <-> -. ( A ^c B ) < ( A ^c C ) ) )
13 10 11 12 syl2an 
 |-  ( ( ( A ^c C ) e. RR+ /\ ( A ^c B ) e. RR+ ) -> ( ( A ^c C ) <_ ( A ^c B ) <-> -. ( A ^c B ) < ( A ^c C ) ) )
14 7 9 13 syl2anc 
 |-  ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( ( A ^c C ) <_ ( A ^c B ) <-> -. ( A ^c B ) < ( A ^c C ) ) )
15 3 5 14 3bitr4d 
 |-  ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( B <_ C <-> ( A ^c C ) <_ ( A ^c B ) ) )