Metamath Proof Explorer


Theorem cxplt2d

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

Ref Expression
Hypotheses recxpcld.1
|- ( ph -> A e. RR )
recxpcld.2
|- ( ph -> 0 <_ A )
recxpcld.3
|- ( ph -> B e. RR )
mulcxpd.4
|- ( ph -> 0 <_ B )
cxple2d.5
|- ( ph -> C e. RR+ )
Assertion cxplt2d
|- ( ph -> ( A < B <-> ( A ^c C ) < ( B ^c C ) ) )

Proof

Step Hyp Ref Expression
1 recxpcld.1
 |-  ( ph -> A e. RR )
2 recxpcld.2
 |-  ( ph -> 0 <_ A )
3 recxpcld.3
 |-  ( ph -> B e. RR )
4 mulcxpd.4
 |-  ( ph -> 0 <_ B )
5 cxple2d.5
 |-  ( ph -> C e. RR+ )
6 cxplt2
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( A < B <-> ( A ^c C ) < ( B ^c C ) ) )
7 1 2 3 4 5 6 syl221anc
 |-  ( ph -> ( A < B <-> ( A ^c C ) < ( B ^c C ) ) )