Proof of Theorem xaddcom
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elxr 13159 | . 2
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) | 
| 2 |  | elxr 13159 | . . . 4
⊢ (𝐵 ∈ ℝ*
↔ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 =
-∞)) | 
| 3 |  | recn 11246 | . . . . . . 7
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) | 
| 4 |  | recn 11246 | . . . . . . 7
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) | 
| 5 |  | addcom 11448 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | 
| 6 | 3, 4, 5 | syl2an 596 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | 
| 7 |  | rexadd 13275 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵)) | 
| 8 |  | rexadd 13275 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 +𝑒 𝐴) = (𝐵 + 𝐴)) | 
| 9 | 8 | ancoms 458 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 +𝑒 𝐴) = (𝐵 + 𝐴)) | 
| 10 | 6, 7, 9 | 3eqtr4d 2786 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐵 +𝑒 𝐴)) | 
| 11 |  | oveq2 7440 | . . . . . . 7
⊢ (𝐵 = +∞ → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒
+∞)) | 
| 12 |  | rexr 11308 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) | 
| 13 |  | renemnf 11311 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞) | 
| 14 |  | xaddpnf1 13269 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
→ (𝐴
+𝑒 +∞) = +∞) | 
| 15 | 12, 13, 14 | syl2anc 584 | . . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 +𝑒 +∞)
= +∞) | 
| 16 | 11, 15 | sylan9eqr 2798 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐵) = +∞) | 
| 17 |  | oveq1 7439 | . . . . . . 7
⊢ (𝐵 = +∞ → (𝐵 +𝑒 𝐴) = (+∞
+𝑒 𝐴)) | 
| 18 |  | xaddpnf2 13270 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
→ (+∞ +𝑒 𝐴) = +∞) | 
| 19 | 12, 13, 18 | syl2anc 584 | . . . . . . 7
⊢ (𝐴 ∈ ℝ → (+∞
+𝑒 𝐴) =
+∞) | 
| 20 | 17, 19 | sylan9eqr 2798 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 +𝑒 𝐴) = +∞) | 
| 21 | 16, 20 | eqtr4d 2779 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐵) = (𝐵 +𝑒 𝐴)) | 
| 22 |  | oveq2 7440 | . . . . . . 7
⊢ (𝐵 = -∞ → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒
-∞)) | 
| 23 |  | renepnf 11310 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞) | 
| 24 |  | xaddmnf1 13271 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
→ (𝐴
+𝑒 -∞) = -∞) | 
| 25 | 12, 23, 24 | syl2anc 584 | . . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 +𝑒 -∞)
= -∞) | 
| 26 | 22, 25 | sylan9eqr 2798 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐵) = -∞) | 
| 27 |  | oveq1 7439 | . . . . . . 7
⊢ (𝐵 = -∞ → (𝐵 +𝑒 𝐴) = (-∞
+𝑒 𝐴)) | 
| 28 |  | xaddmnf2 13272 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
→ (-∞ +𝑒 𝐴) = -∞) | 
| 29 | 12, 23, 28 | syl2anc 584 | . . . . . . 7
⊢ (𝐴 ∈ ℝ → (-∞
+𝑒 𝐴) =
-∞) | 
| 30 | 27, 29 | sylan9eqr 2798 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 +𝑒 𝐴) = -∞) | 
| 31 | 26, 30 | eqtr4d 2779 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐵) = (𝐵 +𝑒 𝐴)) | 
| 32 | 10, 21, 31 | 3jaodan 1432 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 +𝑒 𝐵) = (𝐵 +𝑒 𝐴)) | 
| 33 | 2, 32 | sylan2b 594 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
→ (𝐴
+𝑒 𝐵) =
(𝐵 +𝑒
𝐴)) | 
| 34 |  | pnfaddmnf 13273 | . . . . . . . 8
⊢ (+∞
+𝑒 -∞) = 0 | 
| 35 |  | mnfaddpnf 13274 | . . . . . . . 8
⊢ (-∞
+𝑒 +∞) = 0 | 
| 36 | 34, 35 | eqtr4i 2767 | . . . . . . 7
⊢ (+∞
+𝑒 -∞) = (-∞ +𝑒
+∞) | 
| 37 |  | simpr 484 | . . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
𝐵 =
-∞) | 
| 38 | 37 | oveq2d 7448 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
(+∞ +𝑒 𝐵) = (+∞ +𝑒
-∞)) | 
| 39 | 37 | oveq1d 7447 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
(𝐵 +𝑒
+∞) = (-∞ +𝑒 +∞)) | 
| 40 | 36, 38, 39 | 3eqtr4a 2802 | . . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
(+∞ +𝑒 𝐵) = (𝐵 +𝑒
+∞)) | 
| 41 |  | xaddpnf2 13270 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ (+∞ +𝑒 𝐵) = +∞) | 
| 42 |  | xaddpnf1 13269 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ (𝐵
+𝑒 +∞) = +∞) | 
| 43 | 41, 42 | eqtr4d 2779 | . . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ (+∞ +𝑒 𝐵) = (𝐵 +𝑒
+∞)) | 
| 44 | 40, 43 | pm2.61dane 3028 | . . . . 5
⊢ (𝐵 ∈ ℝ*
→ (+∞ +𝑒 𝐵) = (𝐵 +𝑒
+∞)) | 
| 45 | 44 | adantl 481 | . . . 4
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ (+∞ +𝑒 𝐵) = (𝐵 +𝑒
+∞)) | 
| 46 |  | simpl 482 | . . . . 5
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ 𝐴 =
+∞) | 
| 47 | 46 | oveq1d 7447 | . . . 4
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ (𝐴
+𝑒 𝐵) =
(+∞ +𝑒 𝐵)) | 
| 48 | 46 | oveq2d 7448 | . . . 4
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ (𝐵
+𝑒 𝐴) =
(𝐵 +𝑒
+∞)) | 
| 49 | 45, 47, 48 | 3eqtr4d 2786 | . . 3
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ (𝐴
+𝑒 𝐵) =
(𝐵 +𝑒
𝐴)) | 
| 50 | 35, 34 | eqtr4i 2767 | . . . . . . 7
⊢ (-∞
+𝑒 +∞) = (+∞ +𝑒
-∞) | 
| 51 |  | simpr 484 | . . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
𝐵 =
+∞) | 
| 52 | 51 | oveq2d 7448 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
(-∞ +𝑒 𝐵) = (-∞ +𝑒
+∞)) | 
| 53 | 51 | oveq1d 7447 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
(𝐵 +𝑒
-∞) = (+∞ +𝑒 -∞)) | 
| 54 | 50, 52, 53 | 3eqtr4a 2802 | . . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
(-∞ +𝑒 𝐵) = (𝐵 +𝑒
-∞)) | 
| 55 |  | xaddmnf2 13272 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
→ (-∞ +𝑒 𝐵) = -∞) | 
| 56 |  | xaddmnf1 13271 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
→ (𝐵
+𝑒 -∞) = -∞) | 
| 57 | 55, 56 | eqtr4d 2779 | . . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
→ (-∞ +𝑒 𝐵) = (𝐵 +𝑒
-∞)) | 
| 58 | 54, 57 | pm2.61dane 3028 | . . . . 5
⊢ (𝐵 ∈ ℝ*
→ (-∞ +𝑒 𝐵) = (𝐵 +𝑒
-∞)) | 
| 59 | 58 | adantl 481 | . . . 4
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ (-∞ +𝑒 𝐵) = (𝐵 +𝑒
-∞)) | 
| 60 |  | simpl 482 | . . . . 5
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ 𝐴 =
-∞) | 
| 61 | 60 | oveq1d 7447 | . . . 4
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ (𝐴
+𝑒 𝐵) =
(-∞ +𝑒 𝐵)) | 
| 62 | 60 | oveq2d 7448 | . . . 4
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ (𝐵
+𝑒 𝐴) =
(𝐵 +𝑒
-∞)) | 
| 63 | 59, 61, 62 | 3eqtr4d 2786 | . . 3
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ (𝐴
+𝑒 𝐵) =
(𝐵 +𝑒
𝐴)) | 
| 64 | 33, 49, 63 | 3jaoian 1431 | . 2
⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ*)
→ (𝐴
+𝑒 𝐵) =
(𝐵 +𝑒
𝐴)) | 
| 65 | 1, 64 | sylanb 581 | 1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 +𝑒 𝐵) = (𝐵 +𝑒 𝐴)) |