Proof of Theorem xaddass
| Step | Hyp | Ref
| Expression |
| 1 | | recn 11245 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
| 2 | | recn 11245 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
| 3 | | recn 11245 |
. . . . . . . . . 10
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℂ) |
| 4 | | addass 11242 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
| 5 | 1, 2, 3, 4 | syl3an 1161 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
| 6 | 5 | 3expa 1119 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
| 7 | | readdcl 11238 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) |
| 8 | | rexadd 13274 |
. . . . . . . . 9
⊢ (((𝐴 + 𝐵) ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) +𝑒 𝐶) = ((𝐴 + 𝐵) + 𝐶)) |
| 9 | 7, 8 | sylan 580 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) +𝑒 𝐶) = ((𝐴 + 𝐵) + 𝐶)) |
| 10 | | readdcl 11238 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 + 𝐶) ∈ ℝ) |
| 11 | | rexadd 13274 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 + 𝐶) ∈ ℝ) → (𝐴 +𝑒 (𝐵 + 𝐶)) = (𝐴 + (𝐵 + 𝐶))) |
| 12 | 10, 11 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐴 +𝑒 (𝐵 + 𝐶)) = (𝐴 + (𝐵 + 𝐶))) |
| 13 | 12 | anassrs 467 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 (𝐵 + 𝐶)) = (𝐴 + (𝐵 + 𝐶))) |
| 14 | 6, 9, 13 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 + 𝐶))) |
| 15 | | rexadd 13274 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵)) |
| 16 | 15 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵)) |
| 17 | 16 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = ((𝐴 + 𝐵) +𝑒 𝐶)) |
| 18 | | rexadd 13274 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶)) |
| 19 | 18 | adantll 714 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶)) |
| 20 | 19 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 (𝐵 +𝑒 𝐶)) = (𝐴 +𝑒 (𝐵 + 𝐶))) |
| 21 | 14, 17, 20 | 3eqtr4d 2787 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐶 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
| 22 | 21 | adantll 714 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐴
≠ -∞) ∧ (𝐵
∈ ℝ* ∧ 𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐶 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
| 23 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝐶 = +∞ → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = ((𝐴 +𝑒 𝐵) +𝑒
+∞)) |
| 24 | | simp1l 1198 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → 𝐴 ∈
ℝ*) |
| 25 | | simp2l 1200 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → 𝐵 ∈
ℝ*) |
| 26 | | xaddcl 13281 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 +𝑒 𝐵) ∈
ℝ*) |
| 27 | 24, 25, 26 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (𝐴 +𝑒 𝐵) ∈
ℝ*) |
| 28 | | xaddnemnf 13278 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞)) → (𝐴
+𝑒 𝐵)
≠ -∞) |
| 29 | 28 | 3adant3 1133 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (𝐴 +𝑒 𝐵) ≠ -∞) |
| 30 | | xaddpnf1 13268 |
. . . . . . . . . 10
⊢ (((𝐴 +𝑒 𝐵) ∈ ℝ*
∧ (𝐴
+𝑒 𝐵)
≠ -∞) → ((𝐴
+𝑒 𝐵)
+𝑒 +∞) = +∞) |
| 31 | 27, 29, 30 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → ((𝐴 +𝑒 𝐵) +𝑒 +∞) =
+∞) |
| 32 | 23, 31 | sylan9eqr 2799 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = +∞) |
| 33 | | xaddpnf1 13268 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
→ (𝐴
+𝑒 +∞) = +∞) |
| 34 | 33 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (𝐴 +𝑒 +∞) =
+∞) |
| 35 | 34 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → (𝐴 +𝑒 +∞) =
+∞) |
| 36 | 32, 35 | eqtr4d 2780 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒
+∞)) |
| 37 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝐶 = +∞ → (𝐵 +𝑒 𝐶) = (𝐵 +𝑒
+∞)) |
| 38 | | xaddpnf1 13268 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ (𝐵
+𝑒 +∞) = +∞) |
| 39 | 38 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (𝐵 +𝑒 +∞) =
+∞) |
| 40 | 37, 39 | sylan9eqr 2799 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → (𝐵 +𝑒 𝐶) = +∞) |
| 41 | 40 | oveq2d 7447 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → (𝐴 +𝑒 (𝐵 +𝑒 𝐶)) = (𝐴 +𝑒
+∞)) |
| 42 | 36, 41 | eqtr4d 2780 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐶 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
| 43 | 42 | adantlr 715 |
. . . . 5
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐴
≠ -∞) ∧ (𝐵
∈ ℝ* ∧ 𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) ∧ 𝐶 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
| 44 | | simp3 1139 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (𝐶 ∈ ℝ* ∧ 𝐶 ≠
-∞)) |
| 45 | | xrnemnf 13159 |
. . . . . . 7
⊢ ((𝐶 ∈ ℝ*
∧ 𝐶 ≠ -∞)
↔ (𝐶 ∈ ℝ
∨ 𝐶 =
+∞)) |
| 46 | 44, 45 | sylib 218 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞)) |
| 47 | 46 | adantr 480 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → (𝐶 ∈ ℝ ∨ 𝐶 = +∞)) |
| 48 | 22, 43, 47 | mpjaodan 961 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
| 49 | 48 | anassrs 467 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐴
≠ -∞) ∧ (𝐵
∈ ℝ* ∧ 𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
| 50 | | xaddpnf2 13269 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ*
∧ 𝐶 ≠ -∞)
→ (+∞ +𝑒 𝐶) = +∞) |
| 51 | 50 | 3ad2ant3 1136 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (+∞
+𝑒 𝐶) =
+∞) |
| 52 | 51, 34 | eqtr4d 2780 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (+∞
+𝑒 𝐶) =
(𝐴 +𝑒
+∞)) |
| 53 | 52 | adantr 480 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → (+∞
+𝑒 𝐶) =
(𝐴 +𝑒
+∞)) |
| 54 | | oveq2 7439 |
. . . . . . 7
⊢ (𝐵 = +∞ → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒
+∞)) |
| 55 | 54, 34 | sylan9eqr 2799 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐵) = +∞) |
| 56 | 55 | oveq1d 7446 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (+∞ +𝑒 𝐶)) |
| 57 | | oveq1 7438 |
. . . . . . 7
⊢ (𝐵 = +∞ → (𝐵 +𝑒 𝐶) = (+∞
+𝑒 𝐶)) |
| 58 | 57, 51 | sylan9eqr 2799 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → (𝐵 +𝑒 𝐶) = +∞) |
| 59 | 58 | oveq2d 7447 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → (𝐴 +𝑒 (𝐵 +𝑒 𝐶)) = (𝐴 +𝑒
+∞)) |
| 60 | 53, 56, 59 | 3eqtr4d 2787 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐵 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
| 61 | 60 | adantlr 715 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 𝐴
≠ -∞) ∧ (𝐵
∈ ℝ* ∧ 𝐵 ≠ -∞) ∧ (𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
| 62 | | simpl2 1193 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 ∈ ℝ) → (𝐵 ∈ ℝ* ∧ 𝐵 ≠
-∞)) |
| 63 | | xrnemnf 13159 |
. . . 4
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
↔ (𝐵 ∈ ℝ
∨ 𝐵 =
+∞)) |
| 64 | 62, 63 | sylib 218 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 ∈ ℝ) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞)) |
| 65 | 49, 61, 64 | mpjaodan 961 |
. 2
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 ∈ ℝ) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
| 66 | | simpl3 1194 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐶 ∈ ℝ* ∧ 𝐶 ≠
-∞)) |
| 67 | 66, 50 | syl 17 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (+∞
+𝑒 𝐶) =
+∞) |
| 68 | | simpl2l 1227 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → 𝐵 ∈
ℝ*) |
| 69 | | simpl3l 1229 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → 𝐶 ∈
ℝ*) |
| 70 | | xaddcl 13281 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
| 71 | 68, 69, 70 | syl2anc 584 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
| 72 | | simpl2 1193 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐵 ∈ ℝ* ∧ 𝐵 ≠
-∞)) |
| 73 | | xaddnemnf 13278 |
. . . . . 6
⊢ (((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
∧ (𝐶 ∈
ℝ* ∧ 𝐶
≠ -∞)) → (𝐵
+𝑒 𝐶)
≠ -∞) |
| 74 | 72, 66, 73 | syl2anc 584 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐵 +𝑒 𝐶) ≠ -∞) |
| 75 | | xaddpnf2 13269 |
. . . . 5
⊢ (((𝐵 +𝑒 𝐶) ∈ ℝ*
∧ (𝐵
+𝑒 𝐶)
≠ -∞) → (+∞ +𝑒 (𝐵 +𝑒 𝐶)) = +∞) |
| 76 | 71, 74, 75 | syl2anc 584 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (+∞
+𝑒 (𝐵
+𝑒 𝐶)) =
+∞) |
| 77 | 67, 76 | eqtr4d 2780 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (+∞
+𝑒 𝐶) =
(+∞ +𝑒 (𝐵 +𝑒 𝐶))) |
| 78 | | simpr 484 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → 𝐴 = +∞) |
| 79 | 78 | oveq1d 7446 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐵) = (+∞ +𝑒 𝐵)) |
| 80 | | xaddpnf2 13269 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ (+∞ +𝑒 𝐵) = +∞) |
| 81 | 72, 80 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (+∞
+𝑒 𝐵) =
+∞) |
| 82 | 79, 81 | eqtrd 2777 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐵) = +∞) |
| 83 | 82 | oveq1d 7446 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (+∞ +𝑒 𝐶)) |
| 84 | 78 | oveq1d 7446 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → (𝐴 +𝑒 (𝐵 +𝑒 𝐶)) = (+∞ +𝑒 (𝐵 +𝑒 𝐶))) |
| 85 | 77, 83, 84 | 3eqtr4d 2787 |
. 2
⊢ ((((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) ∧ 𝐴 = +∞) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |
| 86 | | simp1 1137 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (𝐴 ∈ ℝ* ∧ 𝐴 ≠
-∞)) |
| 87 | | xrnemnf 13159 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
↔ (𝐴 ∈ ℝ
∨ 𝐴 =
+∞)) |
| 88 | 86, 87 | sylib 218 |
. 2
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞)) |
| 89 | 65, 85, 88 | mpjaodan 961 |
1
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ -∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ -∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |