Metamath Proof Explorer

Theorem cxple2a

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

Ref Expression
Assertion cxple2a ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ A ∧ 0 ≤ C ∧ A ≤ B → A C ≤ B C

Proof

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