Metamath Proof Explorer

Theorem cxplea

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

Ref Expression
Assertion cxplea ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) → ( 𝐴 ↑𝑐 𝐵 ) ≤ ( 𝐴 ↑𝑐 𝐶 ) )

Proof

Step Hyp Ref Expression
1 simpl3 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) ∧ 1 < 𝐴 ) → 𝐵 ≤ 𝐶 )
2 simpl1l ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ )
3 simpr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) ∧ 1 < 𝐴 ) → 1 < 𝐴 )
4 simpl2 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) ∧ 1 < 𝐴 ) → ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) )
5 cxple ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 ≤ 𝐶 ↔ ( 𝐴 ↑𝑐 𝐵 ) ≤ ( 𝐴 ↑𝑐 𝐶 ) ) )
6 2 3 4 5 syl21anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) ∧ 1 < 𝐴 ) → ( 𝐵 ≤ 𝐶 ↔ ( 𝐴 ↑𝑐 𝐵 ) ≤ ( 𝐴 ↑𝑐 𝐶 ) ) )
7 1 6 mpbid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) ∧ 1 < 𝐴 ) → ( 𝐴 ↑𝑐 𝐵 ) ≤ ( 𝐴 ↑𝑐 𝐶 ) )
8 1le1 ⊢ 1 ≤ 1
9 simp2l ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) → 𝐵 ∈ ℝ )
10 9 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) → 𝐵 ∈ ℂ )
11 1cxp ⊢ ( 𝐵 ∈ ℂ → ( 1 ↑𝑐 𝐵 ) = 1 )
12 10 11 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) → ( 1 ↑𝑐 𝐵 ) = 1 )
13 simp2r ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) → 𝐶 ∈ ℝ )
14 13 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) → 𝐶 ∈ ℂ )
15 1cxp ⊢ ( 𝐶 ∈ ℂ → ( 1 ↑𝑐 𝐶 ) = 1 )
16 14 15 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) → ( 1 ↑𝑐 𝐶 ) = 1 )
17 12 16 breq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) → ( ( 1 ↑𝑐 𝐵 ) ≤ ( 1 ↑𝑐 𝐶 ) ↔ 1 ≤ 1 ) )
18 8 17 mpbiri ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) → ( 1 ↑𝑐 𝐵 ) ≤ ( 1 ↑𝑐 𝐶 ) )
19 oveq1 ⊢ ( 1 = 𝐴 → ( 1 ↑𝑐 𝐵 ) = ( 𝐴 ↑𝑐 𝐵 ) )
20 oveq1 ⊢ ( 1 = 𝐴 → ( 1 ↑𝑐 𝐶 ) = ( 𝐴 ↑𝑐 𝐶 ) )
21 19 20 breq12d ⊢ ( 1 = 𝐴 → ( ( 1 ↑𝑐 𝐵 ) ≤ ( 1 ↑𝑐 𝐶 ) ↔ ( 𝐴 ↑𝑐 𝐵 ) ≤ ( 𝐴 ↑𝑐 𝐶 ) ) )
22 18 21 syl5ibcom ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) → ( 1 = 𝐴 → ( 𝐴 ↑𝑐 𝐵 ) ≤ ( 𝐴 ↑𝑐 𝐶 ) ) )
23 22 imp ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) ∧ 1 = 𝐴 ) → ( 𝐴 ↑𝑐 𝐵 ) ≤ ( 𝐴 ↑𝑐 𝐶 ) )
24 1re ⊢ 1 ∈ ℝ
25 leloe ⊢ ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 1 ≤ 𝐴 ↔ ( 1 < 𝐴 ∨ 1 = 𝐴 ) ) )
26 24 25 mpan ⊢ ( 𝐴 ∈ ℝ → ( 1 ≤ 𝐴 ↔ ( 1 < 𝐴 ∨ 1 = 𝐴 ) ) )
27 26 biimpa ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 1 < 𝐴 ∨ 1 = 𝐴 ) )
28 27 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) → ( 1 < 𝐴 ∨ 1 = 𝐴 ) )
29 7 23 28 mpjaodan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐵 ≤ 𝐶 ) → ( 𝐴 ↑𝑐 𝐵 ) ≤ ( 𝐴 ↑𝑐 𝐶 ) )