Proof of Theorem xlemul1a
| Step | Hyp | Ref
| Expression |
| 1 | | 0xr 11308 |
. . . . . 6
⊢ 0 ∈
ℝ* |
| 2 | | simpr 484 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → 𝐶 ∈
ℝ*) |
| 3 | | xrleloe 13186 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (0 ≤
𝐶 ↔ (0 < 𝐶 ∨ 0 = 𝐶))) |
| 4 | 1, 2, 3 | sylancr 587 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (0 ≤
𝐶 ↔ (0 < 𝐶 ∨ 0 = 𝐶))) |
| 5 | | simpllr 776 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → 𝐶 ∈
ℝ*) |
| 6 | | elxr 13158 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ ℝ*
↔ (𝐶 ∈ ℝ
∨ 𝐶 = +∞ ∨
𝐶 =
-∞)) |
| 7 | 5, 6 | sylib 218 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) |
| 8 | | simplrr 778 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → 𝐴 ≤ 𝐵) |
| 9 | | simprll 779 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → 𝐴 ∈ ℝ) |
| 10 | | simprlr 780 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → 𝐵 ∈ ℝ) |
| 11 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → 𝐶 ∈ ℝ) |
| 12 | | simplrl 777 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → 0 < 𝐶) |
| 13 | | lemul1 12119 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))) |
| 14 | 9, 10, 11, 12, 13 | syl112anc 1376 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))) |
| 15 | 8, 14 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐶)) |
| 16 | | rexmul 13313 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ·e 𝐶) = (𝐴 · 𝐶)) |
| 17 | 9, 11, 16 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → (𝐴 ·e 𝐶) = (𝐴 · 𝐶)) |
| 18 | | rexmul 13313 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ·e 𝐶) = (𝐵 · 𝐶)) |
| 19 | 10, 11, 18 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → (𝐵 ·e 𝐶) = (𝐵 · 𝐶)) |
| 20 | 15, 17, 19 | 3brtr4d 5175 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
| 21 | 20 | expr 456 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐶 ∈ ℝ → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))) |
| 22 | | simprl 771 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → 𝐴 ∈ ℝ) |
| 23 | | 0re 11263 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
| 24 | | lttri4 11345 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ 0 ∈
ℝ) → (𝐴 < 0
∨ 𝐴 = 0 ∨ 0 <
𝐴)) |
| 25 | 22, 23, 24 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐴 < 0 ∨ 𝐴 = 0 ∨ 0 < 𝐴)) |
| 26 | | simplll 775 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈
ℝ*) |
| 27 | 26 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → 𝐴 ∈
ℝ*) |
| 28 | | xmulpnf1n 13320 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 < 0) →
(𝐴 ·e
+∞) = -∞) |
| 29 | 27, 28 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 < 0) → (𝐴 ·e +∞) =
-∞) |
| 30 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) → 𝐵 ∈
ℝ*) |
| 31 | 30 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → 𝐵 ∈
ℝ*) |
| 32 | 31 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 < 0) → 𝐵 ∈
ℝ*) |
| 33 | | pnfxr 11315 |
. . . . . . . . . . . . . . . . . . 19
⊢ +∞
∈ ℝ* |
| 34 | | xmulcl 13315 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝐵 ·e +∞) ∈
ℝ*) |
| 35 | 32, 33, 34 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 < 0) → (𝐵 ·e +∞) ∈
ℝ*) |
| 36 | | mnfle 13177 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ·e +∞)
∈ ℝ* → -∞ ≤ (𝐵 ·e
+∞)) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 < 0) → -∞ ≤ (𝐵 ·e
+∞)) |
| 38 | 29, 37 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 < 0) → (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞)) |
| 39 | 38 | ex 412 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐴 < 0 → (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞))) |
| 40 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 = 0 → (𝐴 ·e +∞) = (0
·e +∞)) |
| 41 | | xmul02 13310 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (+∞
∈ ℝ* → (0 ·e +∞) =
0) |
| 42 | 33, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0
·e +∞) = 0 |
| 43 | 40, 42 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 = 0 → (𝐴 ·e +∞) =
0) |
| 44 | 43 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 = 0) → (𝐴 ·e +∞) =
0) |
| 45 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → 𝐴 ≤ 𝐵) |
| 46 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 = 0 → (𝐴 ≤ 𝐵 ↔ 0 ≤ 𝐵)) |
| 47 | 45, 46 | syl5ibcom 245 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐴 = 0 → 0 ≤ 𝐵)) |
| 48 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → 𝐵 ∈ ℝ) |
| 49 | | leloe 11347 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ) → (0 ≤ 𝐵 ↔ (0 < 𝐵 ∨ 0 = 𝐵))) |
| 50 | 23, 48, 49 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (0 ≤ 𝐵 ↔ (0 < 𝐵 ∨ 0 = 𝐵))) |
| 51 | 47, 50 | sylibd 239 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐴 = 0 → (0 < 𝐵 ∨ 0 = 𝐵))) |
| 52 | 51 | imp 406 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 = 0) → (0 < 𝐵 ∨ 0 = 𝐵)) |
| 53 | | pnfge 13172 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 ∈
ℝ* → 0 ≤ +∞) |
| 54 | 1, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ≤
+∞ |
| 55 | | xmulpnf1 13316 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐵 ∈ ℝ*
∧ 0 < 𝐵) →
(𝐵 ·e
+∞) = +∞) |
| 56 | 31, 55 | sylan 580 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 0 < 𝐵) → (𝐵 ·e +∞) =
+∞) |
| 57 | 54, 56 | breqtrrid 5181 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 0 < 𝐵) → 0 ≤ (𝐵 ·e
+∞)) |
| 58 | | xrleid 13193 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ∈
ℝ* → 0 ≤ 0) |
| 59 | 1, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ≤
0 |
| 60 | 59, 42 | breqtrri 5170 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ≤ (0
·e +∞) |
| 61 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 0 = 𝐵) → 0 = 𝐵) |
| 62 | 61 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 0 = 𝐵) → (0 ·e
+∞) = (𝐵
·e +∞)) |
| 63 | 60, 62 | breqtrid 5180 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 0 = 𝐵) → 0 ≤ (𝐵 ·e
+∞)) |
| 64 | 57, 63 | jaodan 960 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (0 < 𝐵 ∨ 0 = 𝐵)) → 0 ≤ (𝐵 ·e
+∞)) |
| 65 | 52, 64 | syldan 591 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 = 0) → 0 ≤ (𝐵 ·e
+∞)) |
| 66 | 44, 65 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 = 0) → (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞)) |
| 67 | 66 | ex 412 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐴 = 0 → (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞))) |
| 68 | | pnfge 13172 |
. . . . . . . . . . . . . . . . . 18
⊢ (+∞
∈ ℝ* → +∞ ≤ +∞) |
| 69 | 33, 68 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ +∞
≤ +∞ |
| 70 | 26 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < 𝐴)) → 𝐴 ∈
ℝ*) |
| 71 | | simprr 773 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < 𝐴)) → 0 < 𝐴) |
| 72 | | xmulpnf1 13316 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) →
(𝐴 ·e
+∞) = +∞) |
| 73 | 70, 71, 72 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < 𝐴)) → (𝐴 ·e +∞) =
+∞) |
| 74 | 30 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < 𝐴)) → 𝐵 ∈
ℝ*) |
| 75 | | ltletr 11353 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ ∧ 𝐵
∈ ℝ) → ((0 < 𝐴 ∧ 𝐴 ≤ 𝐵) → 0 < 𝐵)) |
| 76 | 23, 75 | mp3an1 1450 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <
𝐴 ∧ 𝐴 ≤ 𝐵) → 0 < 𝐵)) |
| 77 | 76 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → ((0 < 𝐴 ∧ 𝐴 ≤ 𝐵) → 0 < 𝐵)) |
| 78 | 45, 77 | mpan2d 694 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (0 < 𝐴 → 0 < 𝐵)) |
| 79 | 78 | impr 454 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < 𝐴)) → 0 < 𝐵) |
| 80 | 74, 79, 55 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < 𝐴)) → (𝐵 ·e +∞) =
+∞) |
| 81 | 73, 80 | breq12d 5156 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < 𝐴)) → ((𝐴 ·e +∞) ≤ (𝐵 ·e +∞)
↔ +∞ ≤ +∞)) |
| 82 | 69, 81 | mpbiri 258 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < 𝐴)) → (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞)) |
| 83 | 82 | expr 456 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (0 < 𝐴 → (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞))) |
| 84 | 39, 67, 83 | 3jaod 1431 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → ((𝐴 < 0 ∨ 𝐴 = 0 ∨ 0 < 𝐴) → (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞))) |
| 85 | 25, 84 | mpd 15 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞)) |
| 86 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝐶 = +∞ → (𝐴 ·e 𝐶) = (𝐴 ·e
+∞)) |
| 87 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝐶 = +∞ → (𝐵 ·e 𝐶) = (𝐵 ·e
+∞)) |
| 88 | 86, 87 | breq12d 5156 |
. . . . . . . . . . . . 13
⊢ (𝐶 = +∞ → ((𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶) ↔ (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞))) |
| 89 | 85, 88 | syl5ibrcom 247 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐶 = +∞ → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))) |
| 90 | | nltmnf 13171 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
ℝ* → ¬ 0 < -∞) |
| 91 | 1, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ¬ 0
< -∞ |
| 92 | | breq2 5147 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 = -∞ → (0 < 𝐶 ↔ 0 <
-∞)) |
| 93 | 91, 92 | mtbiri 327 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 = -∞ → ¬ 0 <
𝐶) |
| 94 | 93 | con2i 139 |
. . . . . . . . . . . . . . 15
⊢ (0 <
𝐶 → ¬ 𝐶 = -∞) |
| 95 | 94 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) → ¬ 𝐶 = -∞) |
| 96 | 95 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → ¬ 𝐶 = -∞) |
| 97 | 96 | pm2.21d 121 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐶 = -∞ → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))) |
| 98 | 21, 89, 97 | 3jaod 1431 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → ((𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))) |
| 99 | 7, 98 | mpd 15 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
| 100 | 99 | anassrs 467 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 ∈ ℝ) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
| 101 | | xmulcl 13315 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐴 ·e 𝐶) ∈
ℝ*) |
| 102 | 101 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (𝐴 ·e 𝐶) ∈
ℝ*) |
| 103 | 102 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = +∞) → (𝐴 ·e 𝐶) ∈
ℝ*) |
| 104 | | pnfge 13172 |
. . . . . . . . . . . 12
⊢ ((𝐴 ·e 𝐶) ∈ ℝ*
→ (𝐴
·e 𝐶)
≤ +∞) |
| 105 | 103, 104 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = +∞) → (𝐴 ·e 𝐶) ≤ +∞) |
| 106 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝐵 = +∞ → (𝐵 ·e 𝐶) = (+∞
·e 𝐶)) |
| 107 | | xmulpnf2 13317 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℝ*
∧ 0 < 𝐶) →
(+∞ ·e 𝐶) = +∞) |
| 108 | 107 | ad2ant2lr 748 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) → (+∞ ·e
𝐶) =
+∞) |
| 109 | 106, 108 | sylan9eqr 2799 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = +∞) → (𝐵 ·e 𝐶) = +∞) |
| 110 | 105, 109 | breqtrrd 5171 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = +∞) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
| 111 | 110 | adantlr 715 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
| 112 | | simplrr 778 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → 𝐴 ≤ 𝐵) |
| 113 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → 𝐵 = -∞) |
| 114 | 26 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → 𝐴 ∈
ℝ*) |
| 115 | | mnfle 13177 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ*
→ -∞ ≤ 𝐴) |
| 116 | 114, 115 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → -∞ ≤ 𝐴) |
| 117 | 113, 116 | eqbrtrd 5165 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → 𝐵 ≤ 𝐴) |
| 118 | | xrletri3 13196 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
| 119 | 118 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
| 120 | 112, 117,
119 | mpbir2and 713 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → 𝐴 = 𝐵) |
| 121 | 120 | oveq1d 7446 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → (𝐴 ·e 𝐶) = (𝐵 ·e 𝐶)) |
| 122 | | xmulcl 13315 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐵 ·e 𝐶) ∈
ℝ*) |
| 123 | 122 | adantll 714 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (𝐵 ·e 𝐶) ∈
ℝ*) |
| 124 | 123 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → (𝐵 ·e 𝐶) ∈
ℝ*) |
| 125 | | xrleid 13193 |
. . . . . . . . . . . 12
⊢ ((𝐵 ·e 𝐶) ∈ ℝ*
→ (𝐵
·e 𝐶)
≤ (𝐵
·e 𝐶)) |
| 126 | 124, 125 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → (𝐵 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
| 127 | 121, 126 | eqbrtrd 5165 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
| 128 | 127 | adantlr 715 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
| 129 | | elxr 13158 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ*
↔ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 =
-∞)) |
| 130 | 30, 129 | sylib 218 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) |
| 131 | 130 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 ∈ ℝ) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) |
| 132 | 100, 111,
128, 131 | mpjao3dan 1434 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 ∈ ℝ) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
| 133 | | simplrr 778 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → 𝐴 ≤ 𝐵) |
| 134 | 30 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → 𝐵 ∈
ℝ*) |
| 135 | | pnfge 13172 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℝ*
→ 𝐵 ≤
+∞) |
| 136 | 134, 135 | syl 17 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → 𝐵 ≤ +∞) |
| 137 | | simpr 484 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → 𝐴 = +∞) |
| 138 | 136, 137 | breqtrrd 5171 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → 𝐵 ≤ 𝐴) |
| 139 | 118 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
| 140 | 133, 138,
139 | mpbir2and 713 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → 𝐴 = 𝐵) |
| 141 | 140 | oveq1d 7446 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → (𝐴 ·e 𝐶) = (𝐵 ·e 𝐶)) |
| 142 | 123, 125 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (𝐵 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
| 143 | 142 | ad2antrr 726 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → (𝐵 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
| 144 | 141, 143 | eqbrtrd 5165 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
| 145 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝐴 = -∞ → (𝐴 ·e 𝐶) = (-∞
·e 𝐶)) |
| 146 | | xmulmnf2 13319 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℝ*
∧ 0 < 𝐶) →
(-∞ ·e 𝐶) = -∞) |
| 147 | 146 | ad2ant2lr 748 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) → (-∞ ·e
𝐶) =
-∞) |
| 148 | 145, 147 | sylan9eqr 2799 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = -∞) → (𝐴 ·e 𝐶) = -∞) |
| 149 | 123 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = -∞) → (𝐵 ·e 𝐶) ∈
ℝ*) |
| 150 | | mnfle 13177 |
. . . . . . . . . 10
⊢ ((𝐵 ·e 𝐶) ∈ ℝ*
→ -∞ ≤ (𝐵
·e 𝐶)) |
| 151 | 149, 150 | syl 17 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = -∞) → -∞ ≤ (𝐵 ·e 𝐶)) |
| 152 | 148, 151 | eqbrtrd 5165 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = -∞) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
| 153 | | elxr 13158 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) |
| 154 | 26, 153 | sylib 218 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
| 155 | 132, 144,
152, 154 | mpjao3dan 1434 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
| 156 | 155 | exp32 420 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (0 <
𝐶 → (𝐴 ≤ 𝐵 → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)))) |
| 157 | | xmul01 13309 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ*
→ (𝐴
·e 0) = 0) |
| 158 | 157 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (𝐴 ·e 0) =
0) |
| 159 | | xmul01 13309 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ*
→ (𝐵
·e 0) = 0) |
| 160 | 159 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (𝐵 ·e 0) =
0) |
| 161 | 158, 160 | breq12d 5156 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → ((𝐴 ·e 0) ≤
(𝐵 ·e 0)
↔ 0 ≤ 0)) |
| 162 | 59, 161 | mpbiri 258 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (𝐴 ·e 0) ≤
(𝐵 ·e
0)) |
| 163 | | oveq2 7439 |
. . . . . . . . 9
⊢ (0 =
𝐶 → (𝐴 ·e 0) = (𝐴 ·e 𝐶)) |
| 164 | | oveq2 7439 |
. . . . . . . . 9
⊢ (0 =
𝐶 → (𝐵 ·e 0) = (𝐵 ·e 𝐶)) |
| 165 | 163, 164 | breq12d 5156 |
. . . . . . . 8
⊢ (0 =
𝐶 → ((𝐴 ·e 0) ≤
(𝐵 ·e 0)
↔ (𝐴
·e 𝐶)
≤ (𝐵
·e 𝐶))) |
| 166 | 162, 165 | syl5ibcom 245 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (0 =
𝐶 → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))) |
| 167 | 166 | a1dd 50 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (0 =
𝐶 → (𝐴 ≤ 𝐵 → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)))) |
| 168 | 156, 167 | jaod 860 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → ((0 <
𝐶 ∨ 0 = 𝐶) → (𝐴 ≤ 𝐵 → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)))) |
| 169 | 4, 168 | sylbid 240 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (0 ≤
𝐶 → (𝐴 ≤ 𝐵 → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)))) |
| 170 | 169 | expimpd 453 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐶 ∈ ℝ* ∧ 0 ≤
𝐶) → (𝐴 ≤ 𝐵 → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)))) |
| 171 | 170 | 3impia 1118 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → (𝐴 ≤ 𝐵 → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))) |
| 172 | 171 | imp 406 |
1
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |