Proof of Theorem xnegdi
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elxr 13159 | . 2
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) | 
| 2 |  | elxr 13159 | . . . 4
⊢ (𝐵 ∈ ℝ*
↔ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 =
-∞)) | 
| 3 |  | recn 11246 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) | 
| 4 |  | recn 11246 | . . . . . . . 8
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) | 
| 5 |  | negdi 11567 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵)) | 
| 6 | 3, 4, 5 | syl2an 596 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵)) | 
| 7 |  | readdcl 11239 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | 
| 8 |  | rexneg 13254 | . . . . . . . 8
⊢ ((𝐴 + 𝐵) ∈ ℝ →
-𝑒(𝐴 +
𝐵) = -(𝐴 + 𝐵)) | 
| 9 | 7, 8 | syl 17 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
-𝑒(𝐴 +
𝐵) = -(𝐴 + 𝐵)) | 
| 10 |  | renegcl 11573 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → -𝐴 ∈
ℝ) | 
| 11 |  | renegcl 11573 | . . . . . . . 8
⊢ (𝐵 ∈ ℝ → -𝐵 ∈
ℝ) | 
| 12 |  | rexadd 13275 | . . . . . . . 8
⊢ ((-𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (-𝐴 +𝑒 -𝐵) = (-𝐴 + -𝐵)) | 
| 13 | 10, 11, 12 | syl2an 596 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 +𝑒 -𝐵) = (-𝐴 + -𝐵)) | 
| 14 | 6, 9, 13 | 3eqtr4d 2786 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
-𝑒(𝐴 +
𝐵) = (-𝐴 +𝑒 -𝐵)) | 
| 15 |  | rexadd 13275 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵)) | 
| 16 |  | xnegeq 13250 | . . . . . . 7
⊢ ((𝐴 +𝑒 𝐵) = (𝐴 + 𝐵) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(𝐴 + 𝐵)) | 
| 17 | 15, 16 | syl 17 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
-𝑒(𝐴
+𝑒 𝐵) =
-𝑒(𝐴 +
𝐵)) | 
| 18 |  | rexneg 13254 | . . . . . . 7
⊢ (𝐴 ∈ ℝ →
-𝑒𝐴 =
-𝐴) | 
| 19 |  | rexneg 13254 | . . . . . . 7
⊢ (𝐵 ∈ ℝ →
-𝑒𝐵 =
-𝐵) | 
| 20 | 18, 19 | oveqan12d 7451 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(-𝑒𝐴
+𝑒 -𝑒𝐵) = (-𝐴 +𝑒 -𝐵)) | 
| 21 | 14, 17, 20 | 3eqtr4d 2786 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
-𝑒(𝐴
+𝑒 𝐵) =
(-𝑒𝐴
+𝑒 -𝑒𝐵)) | 
| 22 |  | xnegpnf 13252 | . . . . . 6
⊢
-𝑒+∞ = -∞ | 
| 23 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝐵 = +∞ → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒
+∞)) | 
| 24 |  | rexr 11308 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) | 
| 25 |  | renemnf 11311 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞) | 
| 26 |  | xaddpnf1 13269 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
→ (𝐴
+𝑒 +∞) = +∞) | 
| 27 | 24, 25, 26 | syl2anc 584 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 +𝑒 +∞)
= +∞) | 
| 28 | 23, 27 | sylan9eqr 2798 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐵) = +∞) | 
| 29 |  | xnegeq 13250 | . . . . . . 7
⊢ ((𝐴 +𝑒 𝐵) = +∞ →
-𝑒(𝐴
+𝑒 𝐵) =
-𝑒+∞) | 
| 30 | 28, 29 | syl 17 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) →
-𝑒(𝐴
+𝑒 𝐵) =
-𝑒+∞) | 
| 31 |  | xnegeq 13250 | . . . . . . . . 9
⊢ (𝐵 = +∞ →
-𝑒𝐵 =
-𝑒+∞) | 
| 32 | 31, 22 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝐵 = +∞ →
-𝑒𝐵 =
-∞) | 
| 33 | 32 | oveq2d 7448 | . . . . . . 7
⊢ (𝐵 = +∞ →
(-𝑒𝐴
+𝑒 -𝑒𝐵) = (-𝑒𝐴 +𝑒
-∞)) | 
| 34 | 18, 10 | eqeltrd 2840 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ →
-𝑒𝐴
∈ ℝ) | 
| 35 |  | rexr 11308 | . . . . . . . . 9
⊢
(-𝑒𝐴 ∈ ℝ →
-𝑒𝐴
∈ ℝ*) | 
| 36 |  | renepnf 11310 | . . . . . . . . 9
⊢
(-𝑒𝐴 ∈ ℝ →
-𝑒𝐴 ≠
+∞) | 
| 37 |  | xaddmnf1 13271 | . . . . . . . . 9
⊢
((-𝑒𝐴 ∈ ℝ* ∧
-𝑒𝐴 ≠
+∞) → (-𝑒𝐴 +𝑒 -∞) =
-∞) | 
| 38 | 35, 36, 37 | syl2anc 584 | . . . . . . . 8
⊢
(-𝑒𝐴 ∈ ℝ →
(-𝑒𝐴
+𝑒 -∞) = -∞) | 
| 39 | 34, 38 | syl 17 | . . . . . . 7
⊢ (𝐴 ∈ ℝ →
(-𝑒𝐴
+𝑒 -∞) = -∞) | 
| 40 | 33, 39 | sylan9eqr 2798 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) →
(-𝑒𝐴
+𝑒 -𝑒𝐵) = -∞) | 
| 41 | 22, 30, 40 | 3eqtr4a 2802 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) →
-𝑒(𝐴
+𝑒 𝐵) =
(-𝑒𝐴
+𝑒 -𝑒𝐵)) | 
| 42 |  | xnegmnf 13253 | . . . . . 6
⊢
-𝑒-∞ = +∞ | 
| 43 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝐵 = -∞ → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒
-∞)) | 
| 44 |  | renepnf 11310 | . . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞) | 
| 45 |  | xaddmnf1 13271 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
→ (𝐴
+𝑒 -∞) = -∞) | 
| 46 | 24, 44, 45 | syl2anc 584 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 +𝑒 -∞)
= -∞) | 
| 47 | 43, 46 | sylan9eqr 2798 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐵) = -∞) | 
| 48 |  | xnegeq 13250 | . . . . . . 7
⊢ ((𝐴 +𝑒 𝐵) = -∞ →
-𝑒(𝐴
+𝑒 𝐵) =
-𝑒-∞) | 
| 49 | 47, 48 | syl 17 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) →
-𝑒(𝐴
+𝑒 𝐵) =
-𝑒-∞) | 
| 50 |  | xnegeq 13250 | . . . . . . . . 9
⊢ (𝐵 = -∞ →
-𝑒𝐵 =
-𝑒-∞) | 
| 51 | 50, 42 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝐵 = -∞ →
-𝑒𝐵 =
+∞) | 
| 52 | 51 | oveq2d 7448 | . . . . . . 7
⊢ (𝐵 = -∞ →
(-𝑒𝐴
+𝑒 -𝑒𝐵) = (-𝑒𝐴 +𝑒
+∞)) | 
| 53 |  | renemnf 11311 | . . . . . . . . 9
⊢
(-𝑒𝐴 ∈ ℝ →
-𝑒𝐴 ≠
-∞) | 
| 54 |  | xaddpnf1 13269 | . . . . . . . . 9
⊢
((-𝑒𝐴 ∈ ℝ* ∧
-𝑒𝐴 ≠
-∞) → (-𝑒𝐴 +𝑒 +∞) =
+∞) | 
| 55 | 35, 53, 54 | syl2anc 584 | . . . . . . . 8
⊢
(-𝑒𝐴 ∈ ℝ →
(-𝑒𝐴
+𝑒 +∞) = +∞) | 
| 56 | 34, 55 | syl 17 | . . . . . . 7
⊢ (𝐴 ∈ ℝ →
(-𝑒𝐴
+𝑒 +∞) = +∞) | 
| 57 | 52, 56 | sylan9eqr 2798 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) →
(-𝑒𝐴
+𝑒 -𝑒𝐵) = +∞) | 
| 58 | 42, 49, 57 | 3eqtr4a 2802 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) →
-𝑒(𝐴
+𝑒 𝐵) =
(-𝑒𝐴
+𝑒 -𝑒𝐵)) | 
| 59 | 21, 41, 58 | 3jaodan 1432 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) →
-𝑒(𝐴
+𝑒 𝐵) =
(-𝑒𝐴
+𝑒 -𝑒𝐵)) | 
| 60 | 2, 59 | sylan2b 594 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
→ -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒
-𝑒𝐵)) | 
| 61 |  | xneg0 13255 | . . . . . . 7
⊢
-𝑒0 = 0 | 
| 62 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
𝐵 =
-∞) | 
| 63 | 62 | oveq2d 7448 | . . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
(+∞ +𝑒 𝐵) = (+∞ +𝑒
-∞)) | 
| 64 |  | pnfaddmnf 13273 | . . . . . . . . 9
⊢ (+∞
+𝑒 -∞) = 0 | 
| 65 | 63, 64 | eqtrdi 2792 | . . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
(+∞ +𝑒 𝐵) = 0) | 
| 66 |  | xnegeq 13250 | . . . . . . . 8
⊢
((+∞ +𝑒 𝐵) = 0 → -𝑒(+∞
+𝑒 𝐵) =
-𝑒0) | 
| 67 | 65, 66 | syl 17 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
-𝑒(+∞ +𝑒 𝐵) = -𝑒0) | 
| 68 | 51 | adantl 481 | . . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
-𝑒𝐵 =
+∞) | 
| 69 | 68 | oveq2d 7448 | . . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
(-∞ +𝑒 -𝑒𝐵) = (-∞ +𝑒
+∞)) | 
| 70 |  | mnfaddpnf 13274 | . . . . . . . 8
⊢ (-∞
+𝑒 +∞) = 0 | 
| 71 | 69, 70 | eqtrdi 2792 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
(-∞ +𝑒 -𝑒𝐵) = 0) | 
| 72 | 61, 67, 71 | 3eqtr4a 2802 | . . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
-𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒
-𝑒𝐵)) | 
| 73 |  | xaddpnf2 13270 | . . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ (+∞ +𝑒 𝐵) = +∞) | 
| 74 |  | xnegeq 13250 | . . . . . . . 8
⊢
((+∞ +𝑒 𝐵) = +∞ →
-𝑒(+∞ +𝑒 𝐵) =
-𝑒+∞) | 
| 75 | 73, 74 | syl 17 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ -𝑒(+∞ +𝑒 𝐵) =
-𝑒+∞) | 
| 76 |  | xnegcl 13256 | . . . . . . . 8
⊢ (𝐵 ∈ ℝ*
→ -𝑒𝐵 ∈
ℝ*) | 
| 77 |  | xnegeq 13250 | . . . . . . . . . . . 12
⊢
(-𝑒𝐵 = +∞ →
-𝑒-𝑒𝐵 =
-𝑒+∞) | 
| 78 | 77, 22 | eqtrdi 2792 | . . . . . . . . . . 11
⊢
(-𝑒𝐵 = +∞ →
-𝑒-𝑒𝐵 = -∞) | 
| 79 |  | xnegneg 13257 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ*
→ -𝑒-𝑒𝐵 = 𝐵) | 
| 80 | 79 | eqeq1d 2738 | . . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ*
→ (-𝑒-𝑒𝐵 = -∞ ↔ 𝐵 = -∞)) | 
| 81 | 78, 80 | imbitrid 244 | . . . . . . . . . 10
⊢ (𝐵 ∈ ℝ*
→ (-𝑒𝐵 = +∞ → 𝐵 = -∞)) | 
| 82 | 81 | necon3d 2960 | . . . . . . . . 9
⊢ (𝐵 ∈ ℝ*
→ (𝐵 ≠ -∞
→ -𝑒𝐵 ≠ +∞)) | 
| 83 | 82 | imp 406 | . . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ -𝑒𝐵 ≠ +∞) | 
| 84 |  | xaddmnf2 13272 | . . . . . . . 8
⊢
((-𝑒𝐵 ∈ ℝ* ∧
-𝑒𝐵 ≠
+∞) → (-∞ +𝑒 -𝑒𝐵) = -∞) | 
| 85 | 76, 83, 84 | syl2an2r 685 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ (-∞ +𝑒 -𝑒𝐵) = -∞) | 
| 86 | 22, 75, 85 | 3eqtr4a 2802 | . . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒
-𝑒𝐵)) | 
| 87 | 72, 86 | pm2.61dane 3028 | . . . . 5
⊢ (𝐵 ∈ ℝ*
→ -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒
-𝑒𝐵)) | 
| 88 | 87 | adantl 481 | . . . 4
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒
-𝑒𝐵)) | 
| 89 |  | simpl 482 | . . . . . 6
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ 𝐴 =
+∞) | 
| 90 | 89 | oveq1d 7447 | . . . . 5
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ (𝐴
+𝑒 𝐵) =
(+∞ +𝑒 𝐵)) | 
| 91 |  | xnegeq 13250 | . . . . 5
⊢ ((𝐴 +𝑒 𝐵) = (+∞
+𝑒 𝐵)
→ -𝑒(𝐴 +𝑒 𝐵) = -𝑒(+∞
+𝑒 𝐵)) | 
| 92 | 90, 91 | syl 17 | . . . 4
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒(𝐴 +𝑒 𝐵) = -𝑒(+∞
+𝑒 𝐵)) | 
| 93 |  | xnegeq 13250 | . . . . . . 7
⊢ (𝐴 = +∞ →
-𝑒𝐴 =
-𝑒+∞) | 
| 94 | 93 | adantr 480 | . . . . . 6
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒𝐴 =
-𝑒+∞) | 
| 95 | 94, 22 | eqtrdi 2792 | . . . . 5
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒𝐴 = -∞) | 
| 96 | 95 | oveq1d 7447 | . . . 4
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ (-𝑒𝐴 +𝑒
-𝑒𝐵) =
(-∞ +𝑒 -𝑒𝐵)) | 
| 97 | 88, 92, 96 | 3eqtr4d 2786 | . . 3
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒
-𝑒𝐵)) | 
| 98 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
𝐵 =
+∞) | 
| 99 | 98 | oveq2d 7448 | . . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
(-∞ +𝑒 𝐵) = (-∞ +𝑒
+∞)) | 
| 100 | 99, 70 | eqtrdi 2792 | . . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
(-∞ +𝑒 𝐵) = 0) | 
| 101 |  | xnegeq 13250 | . . . . . . . 8
⊢
((-∞ +𝑒 𝐵) = 0 → -𝑒(-∞
+𝑒 𝐵) =
-𝑒0) | 
| 102 | 100, 101 | syl 17 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
-𝑒(-∞ +𝑒 𝐵) = -𝑒0) | 
| 103 | 32 | adantl 481 | . . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
-𝑒𝐵 =
-∞) | 
| 104 | 103 | oveq2d 7448 | . . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
(+∞ +𝑒 -𝑒𝐵) = (+∞ +𝑒
-∞)) | 
| 105 | 104, 64 | eqtrdi 2792 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
(+∞ +𝑒 -𝑒𝐵) = 0) | 
| 106 | 61, 102, 105 | 3eqtr4a 2802 | . . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
-𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒
-𝑒𝐵)) | 
| 107 |  | xaddmnf2 13272 | . . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
→ (-∞ +𝑒 𝐵) = -∞) | 
| 108 |  | xnegeq 13250 | . . . . . . . 8
⊢
((-∞ +𝑒 𝐵) = -∞ →
-𝑒(-∞ +𝑒 𝐵) =
-𝑒-∞) | 
| 109 | 107, 108 | syl 17 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
→ -𝑒(-∞ +𝑒 𝐵) =
-𝑒-∞) | 
| 110 |  | xnegeq 13250 | . . . . . . . . . . . 12
⊢
(-𝑒𝐵 = -∞ →
-𝑒-𝑒𝐵 =
-𝑒-∞) | 
| 111 | 110, 42 | eqtrdi 2792 | . . . . . . . . . . 11
⊢
(-𝑒𝐵 = -∞ →
-𝑒-𝑒𝐵 = +∞) | 
| 112 | 79 | eqeq1d 2738 | . . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ*
→ (-𝑒-𝑒𝐵 = +∞ ↔ 𝐵 = +∞)) | 
| 113 | 111, 112 | imbitrid 244 | . . . . . . . . . 10
⊢ (𝐵 ∈ ℝ*
→ (-𝑒𝐵 = -∞ → 𝐵 = +∞)) | 
| 114 | 113 | necon3d 2960 | . . . . . . . . 9
⊢ (𝐵 ∈ ℝ*
→ (𝐵 ≠ +∞
→ -𝑒𝐵 ≠ -∞)) | 
| 115 | 114 | imp 406 | . . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
→ -𝑒𝐵 ≠ -∞) | 
| 116 |  | xaddpnf2 13270 | . . . . . . . 8
⊢
((-𝑒𝐵 ∈ ℝ* ∧
-𝑒𝐵 ≠
-∞) → (+∞ +𝑒 -𝑒𝐵) = +∞) | 
| 117 | 76, 115, 116 | syl2an2r 685 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
→ (+∞ +𝑒 -𝑒𝐵) = +∞) | 
| 118 | 42, 109, 117 | 3eqtr4a 2802 | . . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
→ -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒
-𝑒𝐵)) | 
| 119 | 106, 118 | pm2.61dane 3028 | . . . . 5
⊢ (𝐵 ∈ ℝ*
→ -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒
-𝑒𝐵)) | 
| 120 | 119 | adantl 481 | . . . 4
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒
-𝑒𝐵)) | 
| 121 |  | simpl 482 | . . . . . 6
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ 𝐴 =
-∞) | 
| 122 | 121 | oveq1d 7447 | . . . . 5
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ (𝐴
+𝑒 𝐵) =
(-∞ +𝑒 𝐵)) | 
| 123 |  | xnegeq 13250 | . . . . 5
⊢ ((𝐴 +𝑒 𝐵) = (-∞
+𝑒 𝐵)
→ -𝑒(𝐴 +𝑒 𝐵) = -𝑒(-∞
+𝑒 𝐵)) | 
| 124 | 122, 123 | syl 17 | . . . 4
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒(𝐴 +𝑒 𝐵) = -𝑒(-∞
+𝑒 𝐵)) | 
| 125 |  | xnegeq 13250 | . . . . . . 7
⊢ (𝐴 = -∞ →
-𝑒𝐴 =
-𝑒-∞) | 
| 126 | 125 | adantr 480 | . . . . . 6
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒𝐴 =
-𝑒-∞) | 
| 127 | 126, 42 | eqtrdi 2792 | . . . . 5
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒𝐴 = +∞) | 
| 128 | 127 | oveq1d 7447 | . . . 4
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ (-𝑒𝐴 +𝑒
-𝑒𝐵) =
(+∞ +𝑒 -𝑒𝐵)) | 
| 129 | 120, 124,
128 | 3eqtr4d 2786 | . . 3
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒
-𝑒𝐵)) | 
| 130 | 60, 97, 129 | 3jaoian 1431 | . 2
⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ*)
→ -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒
-𝑒𝐵)) | 
| 131 | 1, 130 | sylanb 581 | 1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒
-𝑒𝐵)) |