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 ∈ ℝ + → 1 C ∈ ℝ +
15 14 3ad2ant3 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → 1 C ∈ ℝ +
16 rpxr ⊢ 1 C ∈ ℝ + → 1 C ∈ ℝ *
17 15 16 syl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → 1 C ∈ ℝ *
18 rpge0 ⊢ 1 C ∈ ℝ + → 0 ≤ 1 C
19 15 18 syl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → 0 ≤ 1 C
20 xlemul1a ⊢ A ⋅ 𝑒 C ∈ ℝ * ∧ B ⋅ 𝑒 C ∈ ℝ * ∧ 1 C ∈ ℝ * ∧ 0 ≤ 1 C ∧ A ⋅ 𝑒 C ≤ B ⋅ 𝑒 C → A ⋅ 𝑒 C ⋅ 𝑒 1 C ≤ B ⋅ 𝑒 C ⋅ 𝑒 1 C
21 20 ex ⊢ A ⋅ 𝑒 C ∈ ℝ * ∧ B ⋅ 𝑒 C ∈ ℝ * ∧ 1 C ∈ ℝ * ∧ 0 ≤ 1 C → A ⋅ 𝑒 C ≤ B ⋅ 𝑒 C → A ⋅ 𝑒 C ⋅ 𝑒 1 C ≤ B ⋅ 𝑒 C ⋅ 𝑒 1 C
22 10 13 17 19 21 syl112anc ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → A ⋅ 𝑒 C ≤ B ⋅ 𝑒 C → A ⋅ 𝑒 C ⋅ 𝑒 1 C ≤ B ⋅ 𝑒 C ⋅ 𝑒 1 C
23 xmulass ⊢ A ∈ ℝ * ∧ C ∈ ℝ * ∧ 1 C ∈ ℝ * → A ⋅ 𝑒 C ⋅ 𝑒 1 C = A ⋅ 𝑒 C ⋅ 𝑒 1 C
24 7 8 17 23 syl3anc ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → A ⋅ 𝑒 C ⋅ 𝑒 1 C = A ⋅ 𝑒 C ⋅ 𝑒 1 C
25 rpre ⊢ C ∈ ℝ + → C ∈ ℝ
26 25 3ad2ant3 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → C ∈ ℝ
27 15 rpred ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → 1 C ∈ ℝ
28 rexmul ⊢ C ∈ ℝ ∧ 1 C ∈ ℝ → C ⋅ 𝑒 1 C = C ⁢ 1 C
29 26 27 28 syl2anc ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → C ⋅ 𝑒 1 C = C ⁢ 1 C
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 ⁢ 1 C = 1
34 29 33 eqtrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → C ⋅ 𝑒 1 C = 1
35 34 oveq2d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → A ⋅ 𝑒 C ⋅ 𝑒 1 C = A ⋅ 𝑒 1
36 xmulid1 ⊢ A ∈ ℝ * → A ⋅ 𝑒 1 = A
37 7 36 syl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → A ⋅ 𝑒 1 = A
38 24 35 37 3eqtrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → A ⋅ 𝑒 C ⋅ 𝑒 1 C = A
39 xmulass ⊢ B ∈ ℝ * ∧ C ∈ ℝ * ∧ 1 C ∈ ℝ * → B ⋅ 𝑒 C ⋅ 𝑒 1 C = B ⋅ 𝑒 C ⋅ 𝑒 1 C
40 11 8 17 39 syl3anc ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → B ⋅ 𝑒 C ⋅ 𝑒 1 C = B ⋅ 𝑒 C ⋅ 𝑒 1 C
41 34 oveq2d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → B ⋅ 𝑒 C ⋅ 𝑒 1 C = B ⋅ 𝑒 1
42 xmulid1 ⊢ B ∈ ℝ * → B ⋅ 𝑒 1 = B
43 11 42 syl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → B ⋅ 𝑒 1 = B
44 40 41 43 3eqtrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → B ⋅ 𝑒 C ⋅ 𝑒 1 C = B
45 38 44 breq12d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ + → A ⋅ 𝑒 C ⋅ 𝑒 1 C ≤ B ⋅ 𝑒 C ⋅ 𝑒 1 C ↔ 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