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→AC≤BC

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↔AC≤BC
14 3 4 6 8 12 13 syl221anc ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0≤A∧0≤C∧A≤B∧0<C→A≤B↔AC≤BC
15 1 14 mpbid ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0≤A∧0≤C∧A≤B∧0<C→AC≤BC
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∈ℂ→A0=1
20 18 19 syl ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0≤A∧0≤C∧A≤B→A0=1
21 oveq2 ⊢0=C→A0=AC
22 20 21 sylan9req ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0≤A∧0≤C∧A≤B∧0=C→1=AC
23 5 recnd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0≤A∧0≤C∧A≤B→B∈ℂ
24 cxp0 ⊢B∈ℂ→B0=1
25 23 24 syl ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0≤A∧0≤C∧A≤B→B0=1
26 oveq2 ⊢0=C→B0=BC
27 25 26 sylan9req ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0≤A∧0≤C∧A≤B∧0=C→1=BC
28 17 22 27 3brtr3d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧0≤A∧0≤C∧A≤B∧0=C→AC≤BC
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→AC≤BC