Proof of Theorem xlemul1
| Step | Hyp | Ref
| Expression |
| 1 | | rpxr 13044 |
. . . 4
⊢ (𝐶 ∈ ℝ+
→ 𝐶 ∈
ℝ*) |
| 2 | | rpge0 13048 |
. . . 4
⊢ (𝐶 ∈ ℝ+
→ 0 ≤ 𝐶) |
| 3 | 1, 2 | jca 511 |
. . 3
⊢ (𝐶 ∈ ℝ+
→ (𝐶 ∈
ℝ* ∧ 0 ≤ 𝐶)) |
| 4 | | xlemul1a 13330 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
| 5 | 4 | ex 412 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → (𝐴 ≤ 𝐵 → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))) |
| 6 | 3, 5 | syl3an3 1166 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → (𝐴 ≤ 𝐵 → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))) |
| 7 | | simp1 1137 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → 𝐴 ∈
ℝ*) |
| 8 | 1 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → 𝐶 ∈
ℝ*) |
| 9 | | xmulcl 13315 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐴 ·e 𝐶) ∈
ℝ*) |
| 10 | 7, 8, 9 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → (𝐴 ·e 𝐶) ∈
ℝ*) |
| 11 | | simp2 1138 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → 𝐵 ∈
ℝ*) |
| 12 | | xmulcl 13315 |
. . . . 5
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐵 ·e 𝐶) ∈
ℝ*) |
| 13 | 11, 8, 12 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → (𝐵 ·e 𝐶) ∈
ℝ*) |
| 14 | | rpreccl 13061 |
. . . . . 6
⊢ (𝐶 ∈ ℝ+
→ (1 / 𝐶) ∈
ℝ+) |
| 15 | 14 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → (1 / 𝐶) ∈
ℝ+) |
| 16 | | rpxr 13044 |
. . . . 5
⊢ ((1 /
𝐶) ∈
ℝ+ → (1 / 𝐶) ∈
ℝ*) |
| 17 | 15, 16 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → (1 / 𝐶) ∈
ℝ*) |
| 18 | | rpge0 13048 |
. . . . 5
⊢ ((1 /
𝐶) ∈
ℝ+ → 0 ≤ (1 / 𝐶)) |
| 19 | 15, 18 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → 0 ≤ (1 / 𝐶)) |
| 20 | | xlemul1a 13330 |
. . . . 5
⊢ ((((𝐴 ·e 𝐶) ∈ ℝ*
∧ (𝐵
·e 𝐶)
∈ ℝ* ∧ ((1 / 𝐶) ∈ ℝ* ∧ 0 ≤ (1
/ 𝐶))) ∧ (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) → ((𝐴 ·e 𝐶) ·e (1 / 𝐶)) ≤ ((𝐵 ·e 𝐶) ·e (1 / 𝐶))) |
| 21 | 20 | ex 412 |
. . . 4
⊢ (((𝐴 ·e 𝐶) ∈ ℝ*
∧ (𝐵
·e 𝐶)
∈ ℝ* ∧ ((1 / 𝐶) ∈ ℝ* ∧ 0 ≤ (1
/ 𝐶))) → ((𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶) → ((𝐴 ·e 𝐶) ·e (1 / 𝐶)) ≤ ((𝐵 ·e 𝐶) ·e (1 / 𝐶)))) |
| 22 | 10, 13, 17, 19, 21 | syl112anc 1376 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → ((𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶) → ((𝐴 ·e 𝐶) ·e (1 / 𝐶)) ≤ ((𝐵 ·e 𝐶) ·e (1 / 𝐶)))) |
| 23 | | xmulass 13329 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ (1 / 𝐶) ∈ ℝ*) → ((𝐴 ·e 𝐶) ·e (1 /
𝐶)) = (𝐴 ·e (𝐶 ·e (1 / 𝐶)))) |
| 24 | 7, 8, 17, 23 | syl3anc 1373 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → ((𝐴 ·e 𝐶) ·e (1 / 𝐶)) = (𝐴 ·e (𝐶 ·e (1 / 𝐶)))) |
| 25 | | rpre 13043 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℝ+
→ 𝐶 ∈
ℝ) |
| 26 | 25 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → 𝐶 ∈ ℝ) |
| 27 | 15 | rpred 13077 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → (1 / 𝐶) ∈ ℝ) |
| 28 | | rexmul 13313 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ ∧ (1 / 𝐶) ∈ ℝ) → (𝐶 ·e (1 / 𝐶)) = (𝐶 · (1 / 𝐶))) |
| 29 | 26, 27, 28 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → (𝐶 ·e (1 / 𝐶)) = (𝐶 · (1 / 𝐶))) |
| 30 | 26 | recnd 11289 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → 𝐶 ∈ ℂ) |
| 31 | | rpne0 13051 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℝ+
→ 𝐶 ≠
0) |
| 32 | 31 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → 𝐶 ≠ 0) |
| 33 | 30, 32 | recidd 12038 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → (𝐶 · (1 / 𝐶)) = 1) |
| 34 | 29, 33 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → (𝐶 ·e (1 / 𝐶)) = 1) |
| 35 | 34 | oveq2d 7447 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → (𝐴 ·e (𝐶 ·e (1 / 𝐶))) = (𝐴 ·e 1)) |
| 36 | | xmulrid 13321 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (𝐴
·e 1) = 𝐴) |
| 37 | 7, 36 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → (𝐴 ·e 1) = 𝐴) |
| 38 | 24, 35, 37 | 3eqtrd 2781 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → ((𝐴 ·e 𝐶) ·e (1 / 𝐶)) = 𝐴) |
| 39 | | xmulass 13329 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ (1 / 𝐶) ∈ ℝ*) → ((𝐵 ·e 𝐶) ·e (1 /
𝐶)) = (𝐵 ·e (𝐶 ·e (1 / 𝐶)))) |
| 40 | 11, 8, 17, 39 | syl3anc 1373 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → ((𝐵 ·e 𝐶) ·e (1 / 𝐶)) = (𝐵 ·e (𝐶 ·e (1 / 𝐶)))) |
| 41 | 34 | oveq2d 7447 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → (𝐵 ·e (𝐶 ·e (1 / 𝐶))) = (𝐵 ·e 1)) |
| 42 | | xmulrid 13321 |
. . . . . 6
⊢ (𝐵 ∈ ℝ*
→ (𝐵
·e 1) = 𝐵) |
| 43 | 11, 42 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → (𝐵 ·e 1) = 𝐵) |
| 44 | 40, 41, 43 | 3eqtrd 2781 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → ((𝐵 ·e 𝐶) ·e (1 / 𝐶)) = 𝐵) |
| 45 | 38, 44 | breq12d 5156 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → (((𝐴 ·e 𝐶) ·e (1 / 𝐶)) ≤ ((𝐵 ·e 𝐶) ·e (1 / 𝐶)) ↔ 𝐴 ≤ 𝐵)) |
| 46 | 22, 45 | sylibd 239 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → ((𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶) → 𝐴 ≤ 𝐵)) |
| 47 | 6, 46 | impbid 212 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐶
∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))) |