Proof of Theorem xadddi2
| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 ∈ ℝ) → 𝐴 ∈ ℝ) |
| 2 | | simp2l 1200 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → 𝐵 ∈
ℝ*) |
| 3 | 2 | ad2antrr 726 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 ∈ ℝ) → 𝐵 ∈
ℝ*) |
| 4 | | simp3l 1202 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → 𝐶 ∈
ℝ*) |
| 5 | 4 | ad2antrr 726 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 ∈ ℝ) → 𝐶 ∈
ℝ*) |
| 6 | | xadddi 13337 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
| 7 | 1, 3, 5, 6 | syl3anc 1373 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 ∈ ℝ) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
| 8 | | pnfxr 11315 |
. . . . . 6
⊢ +∞
∈ ℝ* |
| 9 | 4 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 𝐶 ∈
ℝ*) |
| 10 | | xmulcl 13315 |
. . . . . 6
⊢
((+∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ*) →
(+∞ ·e 𝐶) ∈
ℝ*) |
| 11 | 8, 9, 10 | sylancr 587 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (+∞
·e 𝐶)
∈ ℝ*) |
| 12 | | simpl3r 1230 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 0 ≤ 𝐶) |
| 13 | | 0lepnf 13175 |
. . . . . . . . 9
⊢ 0 ≤
+∞ |
| 14 | | xmulge0 13326 |
. . . . . . . . 9
⊢
(((+∞ ∈ ℝ* ∧ 0 ≤ +∞) ∧
(𝐶 ∈
ℝ* ∧ 0 ≤ 𝐶)) → 0 ≤ (+∞
·e 𝐶)) |
| 15 | 8, 13, 14 | mpanl12 702 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ*
∧ 0 ≤ 𝐶) → 0
≤ (+∞ ·e 𝐶)) |
| 16 | 4, 12, 15 | syl2an2r 685 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 0 ≤ (+∞
·e 𝐶)) |
| 17 | | ge0nemnf 13215 |
. . . . . . 7
⊢
(((+∞ ·e 𝐶) ∈ ℝ* ∧ 0 ≤
(+∞ ·e 𝐶)) → (+∞ ·e
𝐶) ≠
-∞) |
| 18 | 11, 16, 17 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (+∞
·e 𝐶)
≠ -∞) |
| 19 | 18 | adantr 480 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = +∞) → (+∞
·e 𝐶)
≠ -∞) |
| 20 | | xaddpnf2 13269 |
. . . . 5
⊢
(((+∞ ·e 𝐶) ∈ ℝ* ∧ (+∞
·e 𝐶)
≠ -∞) → (+∞ +𝑒 (+∞
·e 𝐶)) =
+∞) |
| 21 | 11, 19, 20 | syl2an2r 685 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = +∞) → (+∞
+𝑒 (+∞ ·e 𝐶)) = +∞) |
| 22 | | oveq1 7438 |
. . . . . 6
⊢ (𝐴 = +∞ → (𝐴 ·e 𝐵) = (+∞
·e 𝐵)) |
| 23 | | oveq1 7438 |
. . . . . 6
⊢ (𝐴 = +∞ → (𝐴 ·e 𝐶) = (+∞
·e 𝐶)) |
| 24 | 22, 23 | oveq12d 7449 |
. . . . 5
⊢ (𝐴 = +∞ → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = ((+∞
·e 𝐵)
+𝑒 (+∞ ·e 𝐶))) |
| 25 | | xmulpnf2 13317 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 0 < 𝐵) →
(+∞ ·e 𝐵) = +∞) |
| 26 | 2, 25 | sylan 580 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (+∞
·e 𝐵) =
+∞) |
| 27 | 26 | oveq1d 7446 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → ((+∞
·e 𝐵)
+𝑒 (+∞ ·e 𝐶)) = (+∞ +𝑒
(+∞ ·e 𝐶))) |
| 28 | 24, 27 | sylan9eqr 2799 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = +∞) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = (+∞ +𝑒
(+∞ ·e 𝐶))) |
| 29 | | oveq1 7438 |
. . . . 5
⊢ (𝐴 = +∞ → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (+∞
·e (𝐵
+𝑒 𝐶))) |
| 30 | | xaddcl 13281 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
| 31 | 2, 4, 30 | syl2anc 584 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
| 32 | | 0xr 11308 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
| 33 | 32 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 0 ∈
ℝ*) |
| 34 | 2 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 𝐵 ∈
ℝ*) |
| 35 | 31 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
| 36 | | simpr 484 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 0 < 𝐵) |
| 37 | 34 | xaddridd 13285 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (𝐵 +𝑒 0) = 𝐵) |
| 38 | | xleadd2a 13296 |
. . . . . . . . 9
⊢ (((0
∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ 0 ≤ 𝐶) →
(𝐵 +𝑒 0)
≤ (𝐵
+𝑒 𝐶)) |
| 39 | 33, 9, 34, 12, 38 | syl31anc 1375 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (𝐵 +𝑒 0) ≤ (𝐵 +𝑒 𝐶)) |
| 40 | 37, 39 | eqbrtrrd 5167 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 𝐵 ≤ (𝐵 +𝑒 𝐶)) |
| 41 | 33, 34, 35, 36, 40 | xrltletrd 13203 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 0 < (𝐵 +𝑒 𝐶)) |
| 42 | | xmulpnf2 13317 |
. . . . . 6
⊢ (((𝐵 +𝑒 𝐶) ∈ ℝ*
∧ 0 < (𝐵
+𝑒 𝐶))
→ (+∞ ·e (𝐵 +𝑒 𝐶)) = +∞) |
| 43 | 31, 41, 42 | syl2an2r 685 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (+∞
·e (𝐵
+𝑒 𝐶)) =
+∞) |
| 44 | 29, 43 | sylan9eqr 2799 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = +∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = +∞) |
| 45 | 21, 28, 44 | 3eqtr4rd 2788 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = +∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
| 46 | | mnfxr 11318 |
. . . . . . 7
⊢ -∞
∈ ℝ* |
| 47 | | xmulcl 13315 |
. . . . . . 7
⊢
((-∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ*) →
(-∞ ·e 𝐶) ∈
ℝ*) |
| 48 | 46, 9, 47 | sylancr 587 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (-∞
·e 𝐶)
∈ ℝ*) |
| 49 | | xmulneg1 13311 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ*) →
(-𝑒-∞ ·e 𝐶) = -𝑒(-∞
·e 𝐶)) |
| 50 | 46, 9, 49 | sylancr 587 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) →
(-𝑒-∞ ·e 𝐶) = -𝑒(-∞
·e 𝐶)) |
| 51 | | xnegmnf 13252 |
. . . . . . . . . . . 12
⊢
-𝑒-∞ = +∞ |
| 52 | 51 | oveq1i 7441 |
. . . . . . . . . . 11
⊢
(-𝑒-∞ ·e 𝐶) = (+∞ ·e 𝐶) |
| 53 | 50, 52 | eqtr3di 2792 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) →
-𝑒(-∞ ·e 𝐶) = (+∞ ·e 𝐶)) |
| 54 | | xnegpnf 13251 |
. . . . . . . . . . 11
⊢
-𝑒+∞ = -∞ |
| 55 | 54 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) →
-𝑒+∞ = -∞) |
| 56 | 53, 55 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) →
(-𝑒(-∞ ·e 𝐶) = -𝑒+∞ ↔
(+∞ ·e 𝐶) = -∞)) |
| 57 | | xneg11 13257 |
. . . . . . . . . 10
⊢
(((-∞ ·e 𝐶) ∈ ℝ* ∧ +∞
∈ ℝ*) → (-𝑒(-∞
·e 𝐶) =
-𝑒+∞ ↔ (-∞ ·e 𝐶) = +∞)) |
| 58 | 48, 8, 57 | sylancl 586 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) →
(-𝑒(-∞ ·e 𝐶) = -𝑒+∞ ↔
(-∞ ·e 𝐶) = +∞)) |
| 59 | 56, 58 | bitr3d 281 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → ((+∞
·e 𝐶) =
-∞ ↔ (-∞ ·e 𝐶) = +∞)) |
| 60 | 59 | necon3bid 2985 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → ((+∞
·e 𝐶)
≠ -∞ ↔ (-∞ ·e 𝐶) ≠ +∞)) |
| 61 | 18, 60 | mpbid 232 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (-∞
·e 𝐶)
≠ +∞) |
| 62 | | xaddmnf2 13271 |
. . . . . 6
⊢
(((-∞ ·e 𝐶) ∈ ℝ* ∧ (-∞
·e 𝐶)
≠ +∞) → (-∞ +𝑒 (-∞
·e 𝐶)) =
-∞) |
| 63 | 48, 61, 62 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (-∞
+𝑒 (-∞ ·e 𝐶)) = -∞) |
| 64 | 63 | adantr 480 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = -∞) → (-∞
+𝑒 (-∞ ·e 𝐶)) = -∞) |
| 65 | | oveq1 7438 |
. . . . . 6
⊢ (𝐴 = -∞ → (𝐴 ·e 𝐵) = (-∞
·e 𝐵)) |
| 66 | | oveq1 7438 |
. . . . . 6
⊢ (𝐴 = -∞ → (𝐴 ·e 𝐶) = (-∞
·e 𝐶)) |
| 67 | 65, 66 | oveq12d 7449 |
. . . . 5
⊢ (𝐴 = -∞ → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = ((-∞
·e 𝐵)
+𝑒 (-∞ ·e 𝐶))) |
| 68 | | xmulmnf2 13319 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 0 < 𝐵) →
(-∞ ·e 𝐵) = -∞) |
| 69 | 2, 68 | sylan 580 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (-∞
·e 𝐵) =
-∞) |
| 70 | 69 | oveq1d 7446 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → ((-∞
·e 𝐵)
+𝑒 (-∞ ·e 𝐶)) = (-∞ +𝑒
(-∞ ·e 𝐶))) |
| 71 | 67, 70 | sylan9eqr 2799 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = -∞) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = (-∞ +𝑒
(-∞ ·e 𝐶))) |
| 72 | | oveq1 7438 |
. . . . 5
⊢ (𝐴 = -∞ → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (-∞
·e (𝐵
+𝑒 𝐶))) |
| 73 | | xmulmnf2 13319 |
. . . . . 6
⊢ (((𝐵 +𝑒 𝐶) ∈ ℝ*
∧ 0 < (𝐵
+𝑒 𝐶))
→ (-∞ ·e (𝐵 +𝑒 𝐶)) = -∞) |
| 74 | 31, 41, 73 | syl2an2r 685 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (-∞
·e (𝐵
+𝑒 𝐶)) =
-∞) |
| 75 | 72, 74 | sylan9eqr 2799 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = -∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = -∞) |
| 76 | 64, 71, 75 | 3eqtr4rd 2788 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = -∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
| 77 | | simpl1 1192 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 𝐴 ∈
ℝ*) |
| 78 | | elxr 13158 |
. . . 4
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) |
| 79 | 77, 78 | sylib 218 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
| 80 | 7, 45, 76, 79 | mpjao3dan 1434 |
. 2
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
| 81 | | simp1 1137 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → 𝐴 ∈
ℝ*) |
| 82 | | xmulcl 13315 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐴 ·e 𝐶) ∈
ℝ*) |
| 83 | 81, 4, 82 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → (𝐴 ·e 𝐶) ∈
ℝ*) |
| 84 | 83 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 = 𝐵) → (𝐴 ·e 𝐶) ∈
ℝ*) |
| 85 | | xaddlid 13284 |
. . . 4
⊢ ((𝐴 ·e 𝐶) ∈ ℝ*
→ (0 +𝑒 (𝐴 ·e 𝐶)) = (𝐴 ·e 𝐶)) |
| 86 | 84, 85 | syl 17 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 = 𝐵) → (0
+𝑒 (𝐴
·e 𝐶)) =
(𝐴 ·e
𝐶)) |
| 87 | | oveq2 7439 |
. . . . . 6
⊢ (0 =
𝐵 → (𝐴 ·e 0) = (𝐴 ·e 𝐵)) |
| 88 | 87 | eqcomd 2743 |
. . . . 5
⊢ (0 =
𝐵 → (𝐴 ·e 𝐵) = (𝐴 ·e 0)) |
| 89 | | xmul01 13309 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (𝐴
·e 0) = 0) |
| 90 | 89 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → (𝐴 ·e 0) =
0) |
| 91 | 88, 90 | sylan9eqr 2799 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 = 𝐵) → (𝐴 ·e 𝐵) = 0) |
| 92 | 91 | oveq1d 7446 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 = 𝐵) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = (0 +𝑒 (𝐴 ·e 𝐶))) |
| 93 | | oveq1 7438 |
. . . . . 6
⊢ (0 =
𝐵 → (0
+𝑒 𝐶) =
(𝐵 +𝑒
𝐶)) |
| 94 | 93 | eqcomd 2743 |
. . . . 5
⊢ (0 =
𝐵 → (𝐵 +𝑒 𝐶) = (0 +𝑒 𝐶)) |
| 95 | | xaddlid 13284 |
. . . . . 6
⊢ (𝐶 ∈ ℝ*
→ (0 +𝑒 𝐶) = 𝐶) |
| 96 | 4, 95 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → (0
+𝑒 𝐶) =
𝐶) |
| 97 | 94, 96 | sylan9eqr 2799 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 = 𝐵) → (𝐵 +𝑒 𝐶) = 𝐶) |
| 98 | 97 | oveq2d 7447 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 = 𝐵) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (𝐴 ·e 𝐶)) |
| 99 | 86, 92, 98 | 3eqtr4rd 2788 |
. 2
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 = 𝐵) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
| 100 | | simp2r 1201 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → 0 ≤ 𝐵) |
| 101 | | xrleloe 13186 |
. . . 4
⊢ ((0
∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (0 ≤
𝐵 ↔ (0 < 𝐵 ∨ 0 = 𝐵))) |
| 102 | 32, 2, 101 | sylancr 587 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → (0 ≤ 𝐵 ↔ (0 < 𝐵 ∨ 0 = 𝐵))) |
| 103 | 100, 102 | mpbid 232 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → (0 < 𝐵 ∨ 0 = 𝐵)) |
| 104 | 80, 99, 103 | mpjaodan 961 |
1
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |