Metamath Proof Explorer

Theorem xlemul1

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

Ref Expression
Assertion xlemul1 ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ·e 𝐶 ) ≤ ( 𝐵 ·e 𝐶 ) ) )

Proof

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