Metamath Proof Explorer

Theorem cxplt2

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

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

Proof

Step Hyp Ref Expression
1 cxple2 
 |-  ( ( ( B e. RR /\ 0 <_ B ) /\ ( A e. RR /\ 0 <_ A ) /\ C e. RR+ ) -> ( B <_ A <-> ( B ^c C ) <_ ( A ^c C ) ) )
2 1 3com12 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( B <_ A <-> ( B ^c C ) <_ ( A ^c C ) ) )
3 2 notbid 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( -. B <_ A <-> -. ( B ^c C ) <_ ( A ^c C ) ) )
4 simp1l 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> A e. RR )
5 simp2l 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> B e. RR )
6 4 5 ltnled 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( A < B <-> -. B <_ A ) )
7 simp1r 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> 0 <_ A )
8 rpre 
 |-  ( C e. RR+ -> C e. RR )
9 8 3ad2ant3 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> C e. RR )
10 recxpcl 
 |-  ( ( A e. RR /\ 0 <_ A /\ C e. RR ) -> ( A ^c C ) e. RR )
11 4 7 9 10 syl3anc 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( A ^c C ) e. RR )
12 simp2r 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> 0 <_ B )
13 recxpcl 
 |-  ( ( B e. RR /\ 0 <_ B /\ C e. RR ) -> ( B ^c C ) e. RR )
14 5 12 9 13 syl3anc 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( B ^c C ) e. RR )
15 11 14 ltnled 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( ( A ^c C ) < ( B ^c C ) <-> -. ( B ^c C ) <_ ( A ^c C ) ) )
16 3 6 15 3bitr4d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( A < B <-> ( A ^c C ) < ( B ^c C ) ) )