Proof of Theorem xadddi2
Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 ∈ ℝ) → 𝐴 ∈ ℝ) |
2 | | simp2l 1080 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → 𝐵 ∈
ℝ*) |
3 | 2 | ad2antrr 758 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 ∈ ℝ) → 𝐵 ∈
ℝ*) |
4 | | simp3l 1082 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → 𝐶 ∈
ℝ*) |
5 | 4 | ad2antrr 758 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 ∈ ℝ) → 𝐶 ∈
ℝ*) |
6 | | xadddi 11997 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
7 | 1, 3, 5, 6 | syl3anc 1318 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 ∈ ℝ) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
8 | | pnfxr 9971 |
. . . . . 6
⊢ +∞
∈ ℝ* |
9 | 4 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 𝐶 ∈
ℝ*) |
10 | 9 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = +∞) → 𝐶 ∈
ℝ*) |
11 | | xmulcl 11975 |
. . . . . 6
⊢
((+∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ*) →
(+∞ ·e 𝐶) ∈
ℝ*) |
12 | 8, 10, 11 | sylancr 694 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = +∞) → (+∞
·e 𝐶)
∈ ℝ*) |
13 | 8, 9, 11 | sylancr 694 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (+∞
·e 𝐶)
∈ ℝ*) |
14 | | simpl3r 1110 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 0 ≤ 𝐶) |
15 | | 0lepnf 11842 |
. . . . . . . . 9
⊢ 0 ≤
+∞ |
16 | | xmulge0 11986 |
. . . . . . . . 9
⊢
(((+∞ ∈ ℝ* ∧ 0 ≤ +∞) ∧
(𝐶 ∈
ℝ* ∧ 0 ≤ 𝐶)) → 0 ≤ (+∞
·e 𝐶)) |
17 | 8, 15, 16 | mpanl12 714 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ*
∧ 0 ≤ 𝐶) → 0
≤ (+∞ ·e 𝐶)) |
18 | 9, 14, 17 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 0 ≤ (+∞
·e 𝐶)) |
19 | | ge0nemnf 11878 |
. . . . . . 7
⊢
(((+∞ ·e 𝐶) ∈ ℝ* ∧ 0 ≤
(+∞ ·e 𝐶)) → (+∞ ·e
𝐶) ≠
-∞) |
20 | 13, 18, 19 | syl2anc 691 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (+∞
·e 𝐶)
≠ -∞) |
21 | 20 | adantr 480 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = +∞) → (+∞
·e 𝐶)
≠ -∞) |
22 | | xaddpnf2 11932 |
. . . . 5
⊢
(((+∞ ·e 𝐶) ∈ ℝ* ∧ (+∞
·e 𝐶)
≠ -∞) → (+∞ +𝑒 (+∞
·e 𝐶)) =
+∞) |
23 | 12, 21, 22 | syl2anc 691 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = +∞) → (+∞
+𝑒 (+∞ ·e 𝐶)) = +∞) |
24 | | oveq1 6556 |
. . . . . 6
⊢ (𝐴 = +∞ → (𝐴 ·e 𝐵) = (+∞
·e 𝐵)) |
25 | | oveq1 6556 |
. . . . . 6
⊢ (𝐴 = +∞ → (𝐴 ·e 𝐶) = (+∞
·e 𝐶)) |
26 | 24, 25 | oveq12d 6567 |
. . . . 5
⊢ (𝐴 = +∞ → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = ((+∞
·e 𝐵)
+𝑒 (+∞ ·e 𝐶))) |
27 | | xmulpnf2 11977 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 0 < 𝐵) →
(+∞ ·e 𝐵) = +∞) |
28 | 2, 27 | sylan 487 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (+∞
·e 𝐵) =
+∞) |
29 | 28 | oveq1d 6564 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → ((+∞
·e 𝐵)
+𝑒 (+∞ ·e 𝐶)) = (+∞ +𝑒
(+∞ ·e 𝐶))) |
30 | 26, 29 | sylan9eqr 2666 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = +∞) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = (+∞ +𝑒
(+∞ ·e 𝐶))) |
31 | | oveq1 6556 |
. . . . 5
⊢ (𝐴 = +∞ → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (+∞
·e (𝐵
+𝑒 𝐶))) |
32 | | xaddcl 11944 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
33 | 2, 4, 32 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
34 | 33 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
35 | | 0xr 9965 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
36 | 35 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 0 ∈
ℝ*) |
37 | 2 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 𝐵 ∈
ℝ*) |
38 | | simpr 476 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 0 < 𝐵) |
39 | | xaddid1 11946 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ*
→ (𝐵
+𝑒 0) = 𝐵) |
40 | 37, 39 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (𝐵 +𝑒 0) = 𝐵) |
41 | | xleadd2a 11956 |
. . . . . . . . 9
⊢ (((0
∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
∧ 0 ≤ 𝐶) →
(𝐵 +𝑒 0)
≤ (𝐵
+𝑒 𝐶)) |
42 | 36, 9, 37, 14, 41 | syl31anc 1321 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (𝐵 +𝑒 0) ≤ (𝐵 +𝑒 𝐶)) |
43 | 40, 42 | eqbrtrrd 4607 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 𝐵 ≤ (𝐵 +𝑒 𝐶)) |
44 | 36, 37, 34, 38, 43 | xrltletrd 11868 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 0 < (𝐵 +𝑒 𝐶)) |
45 | | xmulpnf2 11977 |
. . . . . 6
⊢ (((𝐵 +𝑒 𝐶) ∈ ℝ*
∧ 0 < (𝐵
+𝑒 𝐶))
→ (+∞ ·e (𝐵 +𝑒 𝐶)) = +∞) |
46 | 34, 44, 45 | syl2anc 691 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (+∞
·e (𝐵
+𝑒 𝐶)) =
+∞) |
47 | 31, 46 | sylan9eqr 2666 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = +∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = +∞) |
48 | 23, 30, 47 | 3eqtr4rd 2655 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = +∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
49 | | mnfxr 9975 |
. . . . . . 7
⊢ -∞
∈ ℝ* |
50 | | xmulcl 11975 |
. . . . . . 7
⊢
((-∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ*) →
(-∞ ·e 𝐶) ∈
ℝ*) |
51 | 49, 9, 50 | sylancr 694 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (-∞
·e 𝐶)
∈ ℝ*) |
52 | | xnegmnf 11915 |
. . . . . . . . . . . 12
⊢
-𝑒-∞ = +∞ |
53 | 52 | oveq1i 6559 |
. . . . . . . . . . 11
⊢
(-𝑒-∞ ·e 𝐶) = (+∞ ·e 𝐶) |
54 | | xmulneg1 11971 |
. . . . . . . . . . . 12
⊢
((-∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ*) →
(-𝑒-∞ ·e 𝐶) = -𝑒(-∞
·e 𝐶)) |
55 | 49, 9, 54 | sylancr 694 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) →
(-𝑒-∞ ·e 𝐶) = -𝑒(-∞
·e 𝐶)) |
56 | 53, 55 | syl5reqr 2659 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) →
-𝑒(-∞ ·e 𝐶) = (+∞ ·e 𝐶)) |
57 | | xnegpnf 11914 |
. . . . . . . . . . 11
⊢
-𝑒+∞ = -∞ |
58 | 57 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) →
-𝑒+∞ = -∞) |
59 | 56, 58 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) →
(-𝑒(-∞ ·e 𝐶) = -𝑒+∞ ↔
(+∞ ·e 𝐶) = -∞)) |
60 | | xneg11 11920 |
. . . . . . . . . 10
⊢
(((-∞ ·e 𝐶) ∈ ℝ* ∧ +∞
∈ ℝ*) → (-𝑒(-∞
·e 𝐶) =
-𝑒+∞ ↔ (-∞ ·e 𝐶) = +∞)) |
61 | 51, 8, 60 | sylancl 693 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) →
(-𝑒(-∞ ·e 𝐶) = -𝑒+∞ ↔
(-∞ ·e 𝐶) = +∞)) |
62 | 59, 61 | bitr3d 269 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → ((+∞
·e 𝐶) =
-∞ ↔ (-∞ ·e 𝐶) = +∞)) |
63 | 62 | necon3bid 2826 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → ((+∞
·e 𝐶)
≠ -∞ ↔ (-∞ ·e 𝐶) ≠ +∞)) |
64 | 20, 63 | mpbid 221 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (-∞
·e 𝐶)
≠ +∞) |
65 | | xaddmnf2 11934 |
. . . . . 6
⊢
(((-∞ ·e 𝐶) ∈ ℝ* ∧ (-∞
·e 𝐶)
≠ +∞) → (-∞ +𝑒 (-∞
·e 𝐶)) =
-∞) |
66 | 51, 64, 65 | syl2anc 691 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (-∞
+𝑒 (-∞ ·e 𝐶)) = -∞) |
67 | 66 | adantr 480 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = -∞) → (-∞
+𝑒 (-∞ ·e 𝐶)) = -∞) |
68 | | oveq1 6556 |
. . . . . 6
⊢ (𝐴 = -∞ → (𝐴 ·e 𝐵) = (-∞
·e 𝐵)) |
69 | | oveq1 6556 |
. . . . . 6
⊢ (𝐴 = -∞ → (𝐴 ·e 𝐶) = (-∞
·e 𝐶)) |
70 | 68, 69 | oveq12d 6567 |
. . . . 5
⊢ (𝐴 = -∞ → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = ((-∞
·e 𝐵)
+𝑒 (-∞ ·e 𝐶))) |
71 | | xmulmnf2 11979 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 0 < 𝐵) →
(-∞ ·e 𝐵) = -∞) |
72 | 2, 71 | sylan 487 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (-∞
·e 𝐵) =
-∞) |
73 | 72 | oveq1d 6564 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → ((-∞
·e 𝐵)
+𝑒 (-∞ ·e 𝐶)) = (-∞ +𝑒
(-∞ ·e 𝐶))) |
74 | 70, 73 | sylan9eqr 2666 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = -∞) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = (-∞ +𝑒
(-∞ ·e 𝐶))) |
75 | | oveq1 6556 |
. . . . 5
⊢ (𝐴 = -∞ → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (-∞
·e (𝐵
+𝑒 𝐶))) |
76 | | xmulmnf2 11979 |
. . . . . 6
⊢ (((𝐵 +𝑒 𝐶) ∈ ℝ*
∧ 0 < (𝐵
+𝑒 𝐶))
→ (-∞ ·e (𝐵 +𝑒 𝐶)) = -∞) |
77 | 34, 44, 76 | syl2anc 691 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (-∞
·e (𝐵
+𝑒 𝐶)) =
-∞) |
78 | 75, 77 | sylan9eqr 2666 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = -∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = -∞) |
79 | 67, 74, 78 | 3eqtr4rd 2655 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) ∧ 𝐴 = -∞) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
80 | | simpl1 1057 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → 𝐴 ∈
ℝ*) |
81 | | elxr 11826 |
. . . 4
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) |
82 | 80, 81 | sylib 207 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞)) |
83 | 7, 48, 79, 82 | mpjao3dan 1387 |
. 2
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 < 𝐵) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
84 | | simp1 1054 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → 𝐴 ∈
ℝ*) |
85 | | xmulcl 11975 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐴 ·e 𝐶) ∈
ℝ*) |
86 | 84, 4, 85 | syl2anc 691 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → (𝐴 ·e 𝐶) ∈
ℝ*) |
87 | 86 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 = 𝐵) → (𝐴 ·e 𝐶) ∈
ℝ*) |
88 | | xaddid2 11947 |
. . . 4
⊢ ((𝐴 ·e 𝐶) ∈ ℝ*
→ (0 +𝑒 (𝐴 ·e 𝐶)) = (𝐴 ·e 𝐶)) |
89 | 87, 88 | syl 17 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 = 𝐵) → (0
+𝑒 (𝐴
·e 𝐶)) =
(𝐴 ·e
𝐶)) |
90 | | oveq2 6557 |
. . . . . 6
⊢ (0 =
𝐵 → (𝐴 ·e 0) = (𝐴 ·e 𝐵)) |
91 | 90 | eqcomd 2616 |
. . . . 5
⊢ (0 =
𝐵 → (𝐴 ·e 𝐵) = (𝐴 ·e 0)) |
92 | | xmul01 11969 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (𝐴
·e 0) = 0) |
93 | 92 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → (𝐴 ·e 0) =
0) |
94 | 91, 93 | sylan9eqr 2666 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 = 𝐵) → (𝐴 ·e 𝐵) = 0) |
95 | 94 | oveq1d 6564 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 = 𝐵) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = (0 +𝑒 (𝐴 ·e 𝐶))) |
96 | | oveq1 6556 |
. . . . . 6
⊢ (0 =
𝐵 → (0
+𝑒 𝐶) =
(𝐵 +𝑒
𝐶)) |
97 | 96 | eqcomd 2616 |
. . . . 5
⊢ (0 =
𝐵 → (𝐵 +𝑒 𝐶) = (0 +𝑒 𝐶)) |
98 | | xaddid2 11947 |
. . . . . 6
⊢ (𝐶 ∈ ℝ*
→ (0 +𝑒 𝐶) = 𝐶) |
99 | 4, 98 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → (0
+𝑒 𝐶) =
𝐶) |
100 | 97, 99 | sylan9eqr 2666 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 = 𝐵) → (𝐵 +𝑒 𝐶) = 𝐶) |
101 | 100 | oveq2d 6565 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 = 𝐵) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = (𝐴 ·e 𝐶)) |
102 | 89, 95, 101 | 3eqtr4rd 2655 |
. 2
⊢ (((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) ∧ 0 = 𝐵) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
103 | | simp2r 1081 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → 0 ≤ 𝐵) |
104 | | xrleloe 11853 |
. . . 4
⊢ ((0
∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (0 ≤
𝐵 ↔ (0 < 𝐵 ∨ 0 = 𝐵))) |
105 | 35, 2, 104 | sylancr 694 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → (0 ≤ 𝐵 ↔ (0 < 𝐵 ∨ 0 = 𝐵))) |
106 | 103, 105 | mpbid 221 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → (0 < 𝐵 ∨ 0 = 𝐵)) |
107 | 83, 102, 106 | mpjaodan 823 |
1
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵) ∧ (𝐶 ∈ ℝ* ∧ 0 ≤
𝐶)) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |