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 ) ) )