Theorem cxple3

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

	Ref	Expression
Assertion	cxple3	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 ≤ 𝐶 ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐴 ↑𝑐 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cxplt3	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) → ( 𝐶 < 𝐵 ↔ ( 𝐴 ↑𝑐 𝐵 ) < ( 𝐴 ↑𝑐 𝐶 ) ) )
2	1	ancom2s	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐶 < 𝐵 ↔ ( 𝐴 ↑𝑐 𝐵 ) < ( 𝐴 ↑𝑐 𝐶 ) ) )
3	2	notbid	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( ¬ 𝐶 < 𝐵 ↔ ¬ ( 𝐴 ↑𝑐 𝐵 ) < ( 𝐴 ↑𝑐 𝐶 ) ) )
4		lenlt	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 ≤ 𝐶 ↔ ¬ 𝐶 < 𝐵 ) )
5	4	adantl	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 ≤ 𝐶 ↔ ¬ 𝐶 < 𝐵 ) )
6		rpcxpcl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ+ )
7	6	ad2ant2rl	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ+ )
8		rpcxpcl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ+ )
9	8	ad2ant2r	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ+ )
10		rpre	⊢ ( ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ+ → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ )
11		rpre	⊢ ( ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ+ → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ )
12		lenlt	⊢ ( ( ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ ∧ ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ ) → ( ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐴 ↑𝑐 𝐵 ) ↔ ¬ ( 𝐴 ↑𝑐 𝐵 ) < ( 𝐴 ↑𝑐 𝐶 ) ) )
13	10 11 12	syl2an	⊢ ( ( ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ+ ∧ ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ+ ) → ( ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐴 ↑𝑐 𝐵 ) ↔ ¬ ( 𝐴 ↑𝑐 𝐵 ) < ( 𝐴 ↑𝑐 𝐶 ) ) )
14	7 9 13	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐴 ↑𝑐 𝐵 ) ↔ ¬ ( 𝐴 ↑𝑐 𝐵 ) < ( 𝐴 ↑𝑐 𝐶 ) ) )
15	3 5 14	3bitr4d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 ≤ 𝐶 ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐴 ↑𝑐 𝐵 ) ) )