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