Metamath Proof Explorer

Theorem cxple2a

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

Ref Expression
Assertion cxple2a ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) )

Proof

Step Hyp Ref Expression
1 simpl3 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) ∧ 0 < 𝐶 ) → 𝐴 ≤ 𝐵 )
2 simp11 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ℝ )
3 2 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) ∧ 0 < 𝐶 ) → 𝐴 ∈ ℝ )
4 simpl2l ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) ∧ 0 < 𝐶 ) → 0 ≤ 𝐴 )
5 simp12 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ )
6 5 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) ∧ 0 < 𝐶 ) → 𝐵 ∈ ℝ )
7 0red ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) ∧ 0 < 𝐶 ) → 0 ∈ ℝ )
8 7 3 6 4 1 letrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) ∧ 0 < 𝐶 ) → 0 ≤ 𝐵 )
9 simp13 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) → 𝐶 ∈ ℝ )
10 9 anim1i ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) ∧ 0 < 𝐶 ) → ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) )
11 elrp ⊢ ( 𝐶 ∈ ℝ+ ↔ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) )
12 10 11 sylibr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) ∧ 0 < 𝐶 ) → 𝐶 ∈ ℝ+ )
13 cxple2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) ) )
14 3 4 6 8 12 13 syl221anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) ∧ 0 < 𝐶 ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) ) )
15 1 14 mpbid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) ∧ 0 < 𝐶 ) → ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) )
16 1le1 ⊢ 1 ≤ 1
17 16 a1i ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) ∧ 0 = 𝐶 ) → 1 ≤ 1 )
18 2 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ℂ )
19 cxp0 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑𝑐 0 ) = 1 )
20 18 19 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 ↑𝑐 0 ) = 1 )
21 oveq2 ⊢ ( 0 = 𝐶 → ( 𝐴 ↑𝑐 0 ) = ( 𝐴 ↑𝑐 𝐶 ) )
22 20 21 sylan9req ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) ∧ 0 = 𝐶 ) → 1 = ( 𝐴 ↑𝑐 𝐶 ) )
23 5 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℂ )
24 cxp0 ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ↑𝑐 0 ) = 1 )
25 23 24 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐵 ↑𝑐 0 ) = 1 )
26 oveq2 ⊢ ( 0 = 𝐶 → ( 𝐵 ↑𝑐 0 ) = ( 𝐵 ↑𝑐 𝐶 ) )
27 25 26 sylan9req ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) ∧ 0 = 𝐶 ) → 1 = ( 𝐵 ↑𝑐 𝐶 ) )
28 17 22 27 3brtr3d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) ∧ 0 = 𝐶 ) → ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) )
29 simp2r ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) → 0 ≤ 𝐶 )
30 0re ⊢ 0 ∈ ℝ
31 leloe ⊢ ( ( 0 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 0 ≤ 𝐶 ↔ ( 0 < 𝐶 ∨ 0 = 𝐶 ) ) )
32 30 9 31 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) → ( 0 ≤ 𝐶 ↔ ( 0 < 𝐶 ∨ 0 = 𝐶 ) ) )
33 29 32 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) → ( 0 < 𝐶 ∨ 0 = 𝐶 ) )
34 15 28 33 mpjaodan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) )