Metamath Proof Explorer

Theorem xlemul1

Description: Extended real version of lemul1 . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xlemul1 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→A≤B↔A⋅𝑒C≤B⋅𝑒C

Proof

Step Hyp Ref Expression
1 rpxr ⊢C∈ℝ+→C∈ℝ*
2 rpge0 ⊢C∈ℝ+→0≤C
3 1 2 jca ⊢C∈ℝ+→C∈ℝ*∧0≤C
4 xlemul1a ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧0≤C∧A≤B→A⋅𝑒C≤B⋅𝑒C
5 4 ex ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧0≤C→A≤B→A⋅𝑒C≤B⋅𝑒C
6 3 5 syl3an3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→A≤B→A⋅𝑒C≤B⋅𝑒C
7 simp1 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→A∈ℝ*
8 1 3ad2ant3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→C∈ℝ*
9 xmulcl ⊢A∈ℝ*∧C∈ℝ*→A⋅𝑒C∈ℝ*
10 7 8 9 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→A⋅𝑒C∈ℝ*
11 simp2 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→B∈ℝ*
12 xmulcl ⊢B∈ℝ*∧C∈ℝ*→B⋅𝑒C∈ℝ*
13 11 8 12 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→B⋅𝑒C∈ℝ*
14 rpreccl ⊢C∈ℝ+→1C∈ℝ+
15 14 3ad2ant3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→1C∈ℝ+
16 rpxr ⊢1C∈ℝ+→1C∈ℝ*
17 15 16 syl ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→1C∈ℝ*
18 rpge0 ⊢1C∈ℝ+→0≤1C
19 15 18 syl ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→0≤1C
20 xlemul1a ⊢A⋅𝑒C∈ℝ*∧B⋅𝑒C∈ℝ*∧1C∈ℝ*∧0≤1C∧A⋅𝑒C≤B⋅𝑒C→A⋅𝑒C⋅𝑒1C≤B⋅𝑒C⋅𝑒1C
21 20 ex ⊢A⋅𝑒C∈ℝ*∧B⋅𝑒C∈ℝ*∧1C∈ℝ*∧0≤1C→A⋅𝑒C≤B⋅𝑒C→A⋅𝑒C⋅𝑒1C≤B⋅𝑒C⋅𝑒1C
22 10 13 17 19 21 syl112anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→A⋅𝑒C≤B⋅𝑒C→A⋅𝑒C⋅𝑒1C≤B⋅𝑒C⋅𝑒1C
23 xmulass ⊢A∈ℝ*∧C∈ℝ*∧1C∈ℝ*→A⋅𝑒C⋅𝑒1C=A⋅𝑒C⋅𝑒1C
24 7 8 17 23 syl3anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→A⋅𝑒C⋅𝑒1C=A⋅𝑒C⋅𝑒1C
25 rpre ⊢C∈ℝ+→C∈ℝ
26 25 3ad2ant3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→C∈ℝ
27 15 rpred ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→1C∈ℝ
28 rexmul ⊢C∈ℝ∧1C∈ℝ→C⋅𝑒1C=C⁢1C
29 26 27 28 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→C⋅𝑒1C=C⁢1C
30 26 recnd ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→C∈ℂ
31 rpne0 ⊢C∈ℝ+→C≠0
32 31 3ad2ant3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→C≠0
33 30 32 recidd ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→C⁢1C=1
34 29 33 eqtrd ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→C⋅𝑒1C=1
35 34 oveq2d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→A⋅𝑒C⋅𝑒1C=A⋅𝑒1
36 xmulrid ⊢A∈ℝ*→A⋅𝑒1=A
37 7 36 syl ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→A⋅𝑒1=A
38 24 35 37 3eqtrd ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→A⋅𝑒C⋅𝑒1C=A
39 xmulass ⊢B∈ℝ*∧C∈ℝ*∧1C∈ℝ*→B⋅𝑒C⋅𝑒1C=B⋅𝑒C⋅𝑒1C
40 11 8 17 39 syl3anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→B⋅𝑒C⋅𝑒1C=B⋅𝑒C⋅𝑒1C
41 34 oveq2d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→B⋅𝑒C⋅𝑒1C=B⋅𝑒1
42 xmulrid ⊢B∈ℝ*→B⋅𝑒1=B
43 11 42 syl ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→B⋅𝑒1=B
44 40 41 43 3eqtrd ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→B⋅𝑒C⋅𝑒1C=B
45 38 44 breq12d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→A⋅𝑒C⋅𝑒1C≤B⋅𝑒C⋅𝑒1C↔A≤B
46 22 45 sylibd ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→A⋅𝑒C≤B⋅𝑒C→A≤B
47 6 46 impbid ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ+→A≤B↔A⋅𝑒C≤B⋅𝑒C