Proof of Theorem xlemul1a
Step | Hyp | Ref
| Expression |
1 | | 0xr 11020 |
. . . . . 6
⊢ 0 ∈
ℝ* |
2 | | simpr 485 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → 𝐶 ∈
ℝ*) |
3 | | xrleloe 12876 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ 𝐶 ∈ ℝ*) → (0 ≤
𝐶 ↔ (0 < 𝐶 ∨ 0 = 𝐶))) |
4 | 1, 2, 3 | sylancr 587 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (0 ≤
𝐶 ↔ (0 < 𝐶 ∨ 0 = 𝐶))) |
5 | | simpllr 773 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → 𝐶 ∈
ℝ*) |
6 | | elxr 12850 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ ℝ*
↔ (𝐶 ∈ ℝ
∨ 𝐶 = +∞ ∨
𝐶 =
-∞)) |
7 | 5, 6 | sylib 217 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞)) |
8 | | simplrr 775 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → 𝐴 ≤ 𝐵) |
9 | | simprll 776 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → 𝐴 ∈ ℝ) |
10 | | simprlr 777 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → 𝐵 ∈ ℝ) |
11 | | simprr 770 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → 𝐶 ∈ ℝ) |
12 | | simplrl 774 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → 0 < 𝐶) |
13 | | lemul1 11825 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))) |
14 | 9, 10, 11, 12, 13 | syl112anc 1373 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))) |
15 | 8, 14 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐶)) |
16 | | rexmul 13003 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ·e 𝐶) = (𝐴 · 𝐶)) |
17 | 9, 11, 16 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → (𝐴 ·e 𝐶) = (𝐴 · 𝐶)) |
18 | | rexmul 13003 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ·e 𝐶) = (𝐵 · 𝐶)) |
19 | 10, 11, 18 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → (𝐵 ·e 𝐶) = (𝐵 · 𝐶)) |
20 | 15, 17, 19 | 3brtr4d 5108 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ)) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
21 | 20 | expr 457 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐶 ∈ ℝ → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))) |
22 | | simprl 768 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → 𝐴 ∈ ℝ) |
23 | | 0re 10975 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
24 | | lttri4 11057 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ 0 ∈
ℝ) → (𝐴 < 0
∨ 𝐴 = 0 ∨ 0 <
𝐴)) |
25 | 22, 23, 24 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐴 < 0 ∨ 𝐴 = 0 ∨ 0 < 𝐴)) |
26 | | simplll 772 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈
ℝ*) |
27 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → 𝐴 ∈
ℝ*) |
28 | | xmulpnf1n 13010 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 < 0) →
(𝐴 ·e
+∞) = -∞) |
29 | 27, 28 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 < 0) → (𝐴 ·e +∞) =
-∞) |
30 | | simpllr 773 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) → 𝐵 ∈
ℝ*) |
31 | 30 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → 𝐵 ∈
ℝ*) |
32 | 31 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 < 0) → 𝐵 ∈
ℝ*) |
33 | | pnfxr 11027 |
. . . . . . . . . . . . . . . . . . 19
⊢ +∞
∈ ℝ* |
34 | | xmulcl 13005 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝐵 ·e +∞) ∈
ℝ*) |
35 | 32, 33, 34 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 < 0) → (𝐵 ·e +∞) ∈
ℝ*) |
36 | | mnfle 12868 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ·e +∞)
∈ ℝ* → -∞ ≤ (𝐵 ·e
+∞)) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 < 0) → -∞ ≤ (𝐵 ·e
+∞)) |
38 | 29, 37 | eqbrtrd 5098 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 < 0) → (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞)) |
39 | 38 | ex 413 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐴 < 0 → (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞))) |
40 | | oveq1 7284 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 = 0 → (𝐴 ·e +∞) = (0
·e +∞)) |
41 | | xmul02 13000 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (+∞
∈ ℝ* → (0 ·e +∞) =
0) |
42 | 33, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0
·e +∞) = 0 |
43 | 40, 42 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 = 0 → (𝐴 ·e +∞) =
0) |
44 | 43 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 = 0) → (𝐴 ·e +∞) =
0) |
45 | | simplrr 775 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → 𝐴 ≤ 𝐵) |
46 | | breq1 5079 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 = 0 → (𝐴 ≤ 𝐵 ↔ 0 ≤ 𝐵)) |
47 | 45, 46 | syl5ibcom 244 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐴 = 0 → 0 ≤ 𝐵)) |
48 | | simprr 770 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → 𝐵 ∈ ℝ) |
49 | | leloe 11059 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ) → (0 ≤ 𝐵 ↔ (0 < 𝐵 ∨ 0 = 𝐵))) |
50 | 23, 48, 49 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (0 ≤ 𝐵 ↔ (0 < 𝐵 ∨ 0 = 𝐵))) |
51 | 47, 50 | sylibd 238 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐴 = 0 → (0 < 𝐵 ∨ 0 = 𝐵))) |
52 | 51 | imp 407 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 = 0) → (0 < 𝐵 ∨ 0 = 𝐵)) |
53 | | pnfge 12864 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 ∈
ℝ* → 0 ≤ +∞) |
54 | 1, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ≤
+∞ |
55 | | xmulpnf1 13006 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐵 ∈ ℝ*
∧ 0 < 𝐵) →
(𝐵 ·e
+∞) = +∞) |
56 | 31, 55 | sylan 580 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 0 < 𝐵) → (𝐵 ·e +∞) =
+∞) |
57 | 54, 56 | breqtrrid 5114 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 0 < 𝐵) → 0 ≤ (𝐵 ·e
+∞)) |
58 | | xrleid 12883 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ∈
ℝ* → 0 ≤ 0) |
59 | 1, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ≤
0 |
60 | 59, 42 | breqtrri 5103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ≤ (0
·e +∞) |
61 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 0 = 𝐵) → 0 = 𝐵) |
62 | 61 | oveq1d 7292 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 0 = 𝐵) → (0 ·e
+∞) = (𝐵
·e +∞)) |
63 | 60, 62 | breqtrid 5113 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 0 = 𝐵) → 0 ≤ (𝐵 ·e
+∞)) |
64 | 57, 63 | jaodan 955 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ (0 < 𝐵 ∨ 0 = 𝐵)) → 0 ≤ (𝐵 ·e
+∞)) |
65 | 52, 64 | syldan 591 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 = 0) → 0 ≤ (𝐵 ·e
+∞)) |
66 | 44, 65 | eqbrtrd 5098 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐴 = 0) → (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞)) |
67 | 66 | ex 413 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐴 = 0 → (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞))) |
68 | | pnfge 12864 |
. . . . . . . . . . . . . . . . . 18
⊢ (+∞
∈ ℝ* → +∞ ≤ +∞) |
69 | 33, 68 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ +∞
≤ +∞ |
70 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < 𝐴)) → 𝐴 ∈
ℝ*) |
71 | | simprr 770 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < 𝐴)) → 0 < 𝐴) |
72 | | xmulpnf1 13006 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) →
(𝐴 ·e
+∞) = +∞) |
73 | 70, 71, 72 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < 𝐴)) → (𝐴 ·e +∞) =
+∞) |
74 | 30 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < 𝐴)) → 𝐵 ∈
ℝ*) |
75 | | ltletr 11065 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ ∧ 𝐵
∈ ℝ) → ((0 < 𝐴 ∧ 𝐴 ≤ 𝐵) → 0 < 𝐵)) |
76 | 23, 75 | mp3an1 1447 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <
𝐴 ∧ 𝐴 ≤ 𝐵) → 0 < 𝐵)) |
77 | 76 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → ((0 < 𝐴 ∧ 𝐴 ≤ 𝐵) → 0 < 𝐵)) |
78 | 45, 77 | mpan2d 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (0 < 𝐴 → 0 < 𝐵)) |
79 | 78 | impr 455 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < 𝐴)) → 0 < 𝐵) |
80 | 74, 79, 55 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < 𝐴)) → (𝐵 ·e +∞) =
+∞) |
81 | 73, 80 | breq12d 5089 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < 𝐴)) → ((𝐴 ·e +∞) ≤ (𝐵 ·e +∞)
↔ +∞ ≤ +∞)) |
82 | 69, 81 | mpbiri 257 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < 𝐴)) → (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞)) |
83 | 82 | expr 457 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (0 < 𝐴 → (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞))) |
84 | 39, 67, 83 | 3jaod 1427 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → ((𝐴 < 0 ∨ 𝐴 = 0 ∨ 0 < 𝐴) → (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞))) |
85 | 25, 84 | mpd 15 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞)) |
86 | | oveq2 7285 |
. . . . . . . . . . . . . 14
⊢ (𝐶 = +∞ → (𝐴 ·e 𝐶) = (𝐴 ·e
+∞)) |
87 | | oveq2 7285 |
. . . . . . . . . . . . . 14
⊢ (𝐶 = +∞ → (𝐵 ·e 𝐶) = (𝐵 ·e
+∞)) |
88 | 86, 87 | breq12d 5089 |
. . . . . . . . . . . . 13
⊢ (𝐶 = +∞ → ((𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶) ↔ (𝐴 ·e +∞) ≤ (𝐵 ·e
+∞))) |
89 | 85, 88 | syl5ibrcom 246 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐶 = +∞ → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))) |
90 | | nltmnf 12863 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
ℝ* → ¬ 0 < -∞) |
91 | 1, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ¬ 0
< -∞ |
92 | | breq2 5080 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 = -∞ → (0 < 𝐶 ↔ 0 <
-∞)) |
93 | 91, 92 | mtbiri 327 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 = -∞ → ¬ 0 <
𝐶) |
94 | 93 | con2i 139 |
. . . . . . . . . . . . . . 15
⊢ (0 <
𝐶 → ¬ 𝐶 = -∞) |
95 | 94 | ad2antrl 725 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) → ¬ 𝐶 = -∞) |
96 | 95 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → ¬ 𝐶 = -∞) |
97 | 96 | pm2.21d 121 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐶 = -∞ → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))) |
98 | 21, 89, 97 | 3jaod 1427 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → ((𝐶 ∈ ℝ ∨ 𝐶 = +∞ ∨ 𝐶 = -∞) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))) |
99 | 7, 98 | mpd 15 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
100 | 99 | anassrs 468 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 ∈ ℝ) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
101 | | xmulcl 13005 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐴 ·e 𝐶) ∈
ℝ*) |
102 | 101 | adantlr 712 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (𝐴 ·e 𝐶) ∈
ℝ*) |
103 | 102 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = +∞) → (𝐴 ·e 𝐶) ∈
ℝ*) |
104 | | pnfge 12864 |
. . . . . . . . . . . 12
⊢ ((𝐴 ·e 𝐶) ∈ ℝ*
→ (𝐴
·e 𝐶)
≤ +∞) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = +∞) → (𝐴 ·e 𝐶) ≤ +∞) |
106 | | oveq1 7284 |
. . . . . . . . . . . 12
⊢ (𝐵 = +∞ → (𝐵 ·e 𝐶) = (+∞
·e 𝐶)) |
107 | | xmulpnf2 13007 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℝ*
∧ 0 < 𝐶) →
(+∞ ·e 𝐶) = +∞) |
108 | 107 | ad2ant2lr 745 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) → (+∞ ·e
𝐶) =
+∞) |
109 | 106, 108 | sylan9eqr 2800 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = +∞) → (𝐵 ·e 𝐶) = +∞) |
110 | 105, 109 | breqtrrd 5104 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = +∞) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
111 | 110 | adantlr 712 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
112 | | simplrr 775 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → 𝐴 ≤ 𝐵) |
113 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → 𝐵 = -∞) |
114 | 26 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → 𝐴 ∈
ℝ*) |
115 | | mnfle 12868 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ*
→ -∞ ≤ 𝐴) |
116 | 114, 115 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → -∞ ≤ 𝐴) |
117 | 113, 116 | eqbrtrd 5098 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → 𝐵 ≤ 𝐴) |
118 | | xrletri3 12886 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
119 | 118 | ad3antrrr 727 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
120 | 112, 117,
119 | mpbir2and 710 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → 𝐴 = 𝐵) |
121 | 120 | oveq1d 7292 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → (𝐴 ·e 𝐶) = (𝐵 ·e 𝐶)) |
122 | | xmulcl 13005 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐵 ·e 𝐶) ∈
ℝ*) |
123 | 122 | adantll 711 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (𝐵 ·e 𝐶) ∈
ℝ*) |
124 | 123 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → (𝐵 ·e 𝐶) ∈
ℝ*) |
125 | | xrleid 12883 |
. . . . . . . . . . . 12
⊢ ((𝐵 ·e 𝐶) ∈ ℝ*
→ (𝐵
·e 𝐶)
≤ (𝐵
·e 𝐶)) |
126 | 124, 125 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → (𝐵 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
127 | 121, 126 | eqbrtrd 5098 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐵 = -∞) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
128 | 127 | adantlr 712 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
129 | | elxr 12850 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ*
↔ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 =
-∞)) |
130 | 30, 129 | sylib 217 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) |
131 | 130 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 ∈ ℝ) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) |
132 | 100, 111,
128, 131 | mpjao3dan 1430 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 ∈ ℝ) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
133 | | simplrr 775 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → 𝐴 ≤ 𝐵) |
134 | 30 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → 𝐵 ∈
ℝ*) |
135 | | pnfge 12864 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℝ*
→ 𝐵 ≤
+∞) |
136 | 134, 135 | syl 17 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → 𝐵 ≤ +∞) |
137 | | simpr 485 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → 𝐴 = +∞) |
138 | 136, 137 | breqtrrd 5104 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → 𝐵 ≤ 𝐴) |
139 | 118 | ad3antrrr 727 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
140 | 133, 138,
139 | mpbir2and 710 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → 𝐴 = 𝐵) |
141 | 140 | oveq1d 7292 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → (𝐴 ·e 𝐶) = (𝐵 ·e 𝐶)) |
142 | 123, 125 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (𝐵 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
143 | 142 | ad2antrr 723 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → (𝐵 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
144 | 141, 143 | eqbrtrd 5098 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = +∞) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
145 | | oveq1 7284 |
. . . . . . . . . 10
⊢ (𝐴 = -∞ → (𝐴 ·e 𝐶) = (-∞
·e 𝐶)) |
146 | | xmulmnf2 13009 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℝ*
∧ 0 < 𝐶) →
(-∞ ·e 𝐶) = -∞) |
147 | 146 | ad2ant2lr 745 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) → (-∞ ·e
𝐶) =
-∞) |
148 | 145, 147 | sylan9eqr 2800 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = -∞) → (𝐴 ·e 𝐶) = -∞) |
149 | 123 | ad2antrr 723 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = -∞) → (𝐵 ·e 𝐶) ∈
ℝ*) |
150 | | mnfle 12868 |
. . . . . . . . . 10
⊢ ((𝐵 ·e 𝐶) ∈ ℝ*
→ -∞ ≤ (𝐵
·e 𝐶)) |
151 | 149, 150 | syl 17 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = -∞) → -∞ ≤ (𝐵 ·e 𝐶)) |
152 | 148, 151 | eqbrtrd 5098 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐵
∈ ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) ∧ 𝐴 = -∞) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
153 | | elxr 12850 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) |
154 | 26, 153 | sylib 217 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
155 | 132, 144,
152, 154 | mpjao3dan 1430 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) ∧ (0 <
𝐶 ∧ 𝐴 ≤ 𝐵)) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |
156 | 155 | exp32 421 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (0 <
𝐶 → (𝐴 ≤ 𝐵 → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)))) |
157 | | xmul01 12999 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ*
→ (𝐴
·e 0) = 0) |
158 | 157 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (𝐴 ·e 0) =
0) |
159 | | xmul01 12999 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ*
→ (𝐵
·e 0) = 0) |
160 | 159 | ad2antlr 724 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (𝐵 ·e 0) =
0) |
161 | 158, 160 | breq12d 5089 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → ((𝐴 ·e 0) ≤
(𝐵 ·e 0)
↔ 0 ≤ 0)) |
162 | 59, 161 | mpbiri 257 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (𝐴 ·e 0) ≤
(𝐵 ·e
0)) |
163 | | oveq2 7285 |
. . . . . . . . 9
⊢ (0 =
𝐶 → (𝐴 ·e 0) = (𝐴 ·e 𝐶)) |
164 | | oveq2 7285 |
. . . . . . . . 9
⊢ (0 =
𝐶 → (𝐵 ·e 0) = (𝐵 ·e 𝐶)) |
165 | 163, 164 | breq12d 5089 |
. . . . . . . 8
⊢ (0 =
𝐶 → ((𝐴 ·e 0) ≤
(𝐵 ·e 0)
↔ (𝐴
·e 𝐶)
≤ (𝐵
·e 𝐶))) |
166 | 162, 165 | syl5ibcom 244 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (0 =
𝐶 → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))) |
167 | 166 | a1dd 50 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (0 =
𝐶 → (𝐴 ≤ 𝐵 → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)))) |
168 | 156, 167 | jaod 856 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → ((0 <
𝐶 ∨ 0 = 𝐶) → (𝐴 ≤ 𝐵 → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)))) |
169 | 4, 168 | sylbid 239 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ 𝐶 ∈ ℝ*) → (0 ≤
𝐶 → (𝐴 ≤ 𝐵 → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)))) |
170 | 169 | expimpd 454 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐶 ∈ ℝ* ∧ 0 ≤
𝐶) → (𝐴 ≤ 𝐵 → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)))) |
171 | 170 | 3impia 1116 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → (𝐴 ≤ 𝐵 → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶))) |
172 | 171 | imp 407 |
1
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 ·e 𝐶) ≤ (𝐵 ·e 𝐶)) |