Metamath Proof Explorer


Theorem cxplt3d

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

Ref Expression
Hypotheses rpcxpcld.1 φ A +
rpcxpcld.2 φ B
cxplt3d.3 φ A < 1
cxplt3d.4 φ C
Assertion cxplt3d φ B < C A C < A B

Proof

Step Hyp Ref Expression
1 rpcxpcld.1 φ A +
2 rpcxpcld.2 φ B
3 cxplt3d.3 φ A < 1
4 cxplt3d.4 φ C
5 cxplt3 A + A < 1 B C B < C A C < A B
6 1 3 2 4 5 syl22anc φ B < C A C < A B