Theorem cxple

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

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

Proof

Step	Hyp	Ref	Expression
1		cxplt	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) → ( 𝐶 < 𝐵 ↔ ( 𝐴 ↑𝑐 𝐶 ) < ( 𝐴 ↑𝑐 𝐵 ) ) )
2	1	ancom2s	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐶 < 𝐵 ↔ ( 𝐴 ↑𝑐 𝐶 ) < ( 𝐴 ↑𝑐 𝐵 ) ) )
3	2	notbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( ¬ 𝐶 < 𝐵 ↔ ¬ ( 𝐴 ↑𝑐 𝐶 ) < ( 𝐴 ↑𝑐 𝐵 ) ) )
4		lenlt	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 ≤ 𝐶 ↔ ¬ 𝐶 < 𝐵 ) )
5	4	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 ≤ 𝐶 ↔ ¬ 𝐶 < 𝐵 ) )
6		simpll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐴 ∈ ℝ )
7		0red	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 0 ∈ ℝ )
8		1red	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 1 ∈ ℝ )
9		0lt1	⊢ 0 < 1
10	9	a1i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 0 < 1 )
11		simplr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 1 < 𝐴 )
12	7 8 6 10 11	lttrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 0 < 𝐴 )
13	7 6 12	ltled	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 0 ≤ 𝐴 )
14		simprl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐵 ∈ ℝ )
15		recxpcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ )
16	6 13 14 15	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ )
17		simprr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐶 ∈ ℝ )
18		recxpcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ )
19	6 13 17 18	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ )
20	16 19	lenltd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( ( 𝐴 ↑𝑐 𝐵 ) ≤ ( 𝐴 ↑𝑐 𝐶 ) ↔ ¬ ( 𝐴 ↑𝑐 𝐶 ) < ( 𝐴 ↑𝑐 𝐵 ) ) )
21	3 5 20	3bitr4d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 ≤ 𝐶 ↔ ( 𝐴 ↑𝑐 𝐵 ) ≤ ( 𝐴 ↑𝑐 𝐶 ) ) )