Proof of Theorem xaddass
Step | Hyp | Ref
| Expression |
1 | | recn 10970 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
2 | | recn 10970 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
3 | | recn 10970 |
. . . . . . . . . 10
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℂ) |
4 | | addass 10967 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
5 | 1, 2, 3, 4 | syl3an 1159 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
6 | 5 | 3expa 1117 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
7 | | readdcl 10963 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) |
8 | | rexadd 12975 |
. . . . . . . . 9
⊢ (((𝐴 + 𝐵) ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) +𝑒 𝐶) = ((𝐴 + 𝐵) + 𝐶)) |
9 | 7, 8 | sylan 580 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) +𝑒 𝐶) = ((𝐴 + 𝐵) + 𝐶)) |
10 | | readdcl 10963 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 + 𝐶) ∈ ℝ) |
11 | | rexadd 12975 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 + 𝐶) ∈ ℝ) → (𝐴 +𝑒 (𝐵 + 𝐶)) = (𝐴 + (𝐵 + 𝐶))) |
12 | 10, 11 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐴 +𝑒 (𝐵 + 𝐶)) = (𝐴 + (𝐵 + 𝐶))) |
13 | 12 | anassrs 468 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 (𝐵 + 𝐶)) = (𝐴 + (𝐵 + 𝐶))) |
14 | 6, 9, 13 | 3eqtr4d 2789 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 + 𝐶))) |
15 | | rexadd 12975 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵)) |
16 | 15 | adantr 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵)) |
17 | 16 | oveq1d 7299 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = ((𝐴 + 𝐵) +𝑒 𝐶)) |
18 | | rexadd 12975 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶)) |
19 | 18 | adantll 711 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶)) |
20 | 19 | oveq2d 7300 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 (𝐵 +𝑒 𝐶)) = (𝐴 +𝑒 (𝐵 + 𝐶))) |
21 | 14, 17, 20 | 3eqtr4d 2789 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
22 | 21 | adantll 711 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐴
≠ -∞) ∧ (𝐵
∈ ℝ* ∧ 𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐶 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
23 | | oveq2 7292 |
. . . . . . . . 9
⊢ (𝐶 = +∞ → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = ((𝐴 +𝑒 𝐵) +𝑒
+∞)) |
24 | | simp1l 1196 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → 𝐴 ∈
ℝ*) |
25 | | simp2l 1198 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → 𝐵 ∈
ℝ*) |
26 | | xaddcl 12982 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 +𝑒 𝐵) ∈
ℝ*) |
27 | 24, 25, 26 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (𝐴 +𝑒 𝐵) ∈
ℝ*) |
28 | | xaddnemnf 12979 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞)) → (𝐴
+𝑒 𝐵)
≠ -∞) |
29 | 28 | 3adant3 1131 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (𝐴 +𝑒 𝐵) ≠ -∞) |
30 | | xaddpnf1 12969 |
. . . . . . . . . 10
⊢ (((𝐴 +𝑒 𝐵) ∈ ℝ*
∧ (𝐴
+𝑒 𝐵)
≠ -∞) → ((𝐴
+𝑒 𝐵)
+𝑒 +∞) = +∞) |
31 | 27, 29, 30 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → ((𝐴 +𝑒 𝐵) +𝑒 +∞) =
+∞) |
32 | 23, 31 | sylan9eqr 2801 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = +∞) |
33 | | xaddpnf1 12969 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
→ (𝐴
+𝑒 +∞) = +∞) |
34 | 33 | 3ad2ant1 1132 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (𝐴 +𝑒 +∞) =
+∞) |
35 | 34 | adantr 481 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → (𝐴 +𝑒 +∞) =
+∞) |
36 | 32, 35 | eqtr4d 2782 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒
+∞)) |
37 | | oveq2 7292 |
. . . . . . . . 9
⊢ (𝐶 = +∞ → (𝐵 +𝑒 𝐶) = (𝐵 +𝑒
+∞)) |
38 | | xaddpnf1 12969 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ (𝐵
+𝑒 +∞) = +∞) |
39 | 38 | 3ad2ant2 1133 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (𝐵 +𝑒 +∞) =
+∞) |
40 | 37, 39 | sylan9eqr 2801 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → (𝐵 +𝑒 𝐶) = +∞) |
41 | 40 | oveq2d 7300 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → (𝐴 +𝑒 (𝐵 +𝑒 𝐶)) = (𝐴 +𝑒
+∞)) |
42 | 36, 41 | eqtr4d 2782 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
43 | 42 | adantlr 712 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐴
≠ -∞) ∧ (𝐵
∈ ℝ* ∧ 𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐶 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
44 | | simp3 1137 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (𝐶 ∈ ℝ* ∧ 𝐶 ≠
-∞)) |
45 | | xrnemnf 12862 |
. . . . . . 7
⊢ ((𝐶 ∈ ℝ*
∧ 𝐶 ≠ -∞)
↔ (𝐶 ∈ ℝ
∨ 𝐶 =
+∞)) |
46 | 44, 45 | sylib 217 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞)) |
47 | 46 | adantr 481 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞)) |
48 | 22, 43, 47 | mpjaodan 956 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
49 | 48 | anassrs 468 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐴
≠ -∞) ∧ (𝐵
∈ ℝ* ∧ 𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
50 | | xaddpnf2 12970 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ*
∧ 𝐶 ≠ -∞)
→ (+∞ +𝑒 𝐶) = +∞) |
51 | 50 | 3ad2ant3 1134 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (+∞
+𝑒 𝐶) =
+∞) |
52 | 51, 34 | eqtr4d 2782 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (+∞
+𝑒 𝐶) =
(𝐴 +𝑒
+∞)) |
53 | 52 | adantr 481 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → (+∞
+𝑒 𝐶) =
(𝐴 +𝑒
+∞)) |
54 | | oveq2 7292 |
. . . . . . 7
⊢ (𝐵 = +∞ → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒
+∞)) |
55 | 54, 34 | sylan9eqr 2801 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐵) = +∞) |
56 | 55 | oveq1d 7299 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (+∞ +𝑒 𝐶)) |
57 | | oveq1 7291 |
. . . . . . 7
⊢ (𝐵 = +∞ → (𝐵 +𝑒 𝐶) = (+∞
+𝑒 𝐶)) |
58 | 57, 51 | sylan9eqr 2801 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → (𝐵 +𝑒 𝐶) = +∞) |
59 | 58 | oveq2d 7300 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 (𝐵 +𝑒 𝐶)) = (𝐴 +𝑒
+∞)) |
60 | 53, 56, 59 | 3eqtr4d 2789 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
61 | 60 | adantlr 712 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐴
≠ -∞) ∧ (𝐵
∈ ℝ* ∧ 𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
62 | | simpl2 1191 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 ∈ ℝ) → (𝐵 ∈ ℝ* ∧ 𝐵 ≠
-∞)) |
63 | | xrnemnf 12862 |
. . . 4
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
↔ (𝐵 ∈ ℝ
∨ 𝐵 =
+∞)) |
64 | 62, 63 | sylib 217 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 ∈ ℝ) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞)) |
65 | 49, 61, 64 | mpjaodan 956 |
. 2
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
66 | | simpl3 1192 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐶 ∈ ℝ* ∧ 𝐶 ≠
-∞)) |
67 | 66, 50 | syl 17 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (+∞
+𝑒 𝐶) =
+∞) |
68 | | simpl2l 1225 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → 𝐵 ∈
ℝ*) |
69 | | simpl3l 1227 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → 𝐶 ∈
ℝ*) |
70 | | xaddcl 12982 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
71 | 68, 69, 70 | syl2anc 584 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
72 | | simpl2 1191 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐵 ∈ ℝ* ∧ 𝐵 ≠
-∞)) |
73 | | xaddnemnf 12979 |
. . . . . 6
⊢ (((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
∧ (𝐶 ∈
ℝ* ∧ 𝐶
≠ -∞)) → (𝐵
+𝑒 𝐶)
≠ -∞) |
74 | 72, 66, 73 | syl2anc 584 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐵 +𝑒 𝐶) ≠ -∞) |
75 | | xaddpnf2 12970 |
. . . . 5
⊢ (((𝐵 +𝑒 𝐶) ∈ ℝ*
∧ (𝐵
+𝑒 𝐶)
≠ -∞) → (+∞ +𝑒 (𝐵 +𝑒 𝐶)) = +∞) |
76 | 71, 74, 75 | syl2anc 584 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (+∞
+𝑒 (𝐵
+𝑒 𝐶)) =
+∞) |
77 | 67, 76 | eqtr4d 2782 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (+∞
+𝑒 𝐶) =
(+∞ +𝑒 (𝐵 +𝑒 𝐶))) |
78 | | simpr 485 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → 𝐴 = +∞) |
79 | 78 | oveq1d 7299 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐵) = (+∞ +𝑒 𝐵)) |
80 | | xaddpnf2 12970 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ (+∞ +𝑒 𝐵) = +∞) |
81 | 72, 80 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (+∞
+𝑒 𝐵) =
+∞) |
82 | 79, 81 | eqtrd 2779 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐵) = +∞) |
83 | 82 | oveq1d 7299 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (+∞ +𝑒 𝐶)) |
84 | 78 | oveq1d 7299 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐴 +𝑒 (𝐵 +𝑒 𝐶)) = (+∞ +𝑒 (𝐵 +𝑒 𝐶))) |
85 | 77, 83, 84 | 3eqtr4d 2789 |
. 2
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
86 | | simp1 1135 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (𝐴 ∈ ℝ* ∧ 𝐴 ≠
-∞)) |
87 | | xrnemnf 12862 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
↔ (𝐴 ∈ ℝ
∨ 𝐴 =
+∞)) |
88 | 86, 87 | sylib 217 |
. 2
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞)) |
89 | 65, 85, 88 | mpjaodan 956 |
1
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |