Proof of Theorem xnegdi
Step | Hyp | Ref
| Expression |
1 | | elxr 9720 |
. 2
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) |
2 | | elxr 9720 |
. . . 4
⊢ (𝐵 ∈ ℝ*
↔ (𝐵 ∈ ℝ
∨ 𝐵 = +∞ ∨
𝐵 =
-∞)) |
3 | | recn 7894 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
4 | | recn 7894 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
5 | | negdi 8163 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵)) |
6 | 3, 4, 5 | syl2an 287 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵)) |
7 | | readdcl 7887 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) |
8 | | rexneg 9774 |
. . . . . . . 8
⊢ ((𝐴 + 𝐵) ∈ ℝ →
-𝑒(𝐴 +
𝐵) = -(𝐴 + 𝐵)) |
9 | 7, 8 | syl 14 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
-𝑒(𝐴 +
𝐵) = -(𝐴 + 𝐵)) |
10 | | renegcl 8167 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → -𝐴 ∈
ℝ) |
11 | | renegcl 8167 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → -𝐵 ∈
ℝ) |
12 | | rexadd 9796 |
. . . . . . . 8
⊢ ((-𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (-𝐴 +𝑒 -𝐵) = (-𝐴 + -𝐵)) |
13 | 10, 11, 12 | syl2an 287 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 +𝑒 -𝐵) = (-𝐴 + -𝐵)) |
14 | 6, 9, 13 | 3eqtr4d 2213 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
-𝑒(𝐴 +
𝐵) = (-𝐴 +𝑒 -𝐵)) |
15 | | rexadd 9796 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵)) |
16 | | xnegeq 9771 |
. . . . . . 7
⊢ ((𝐴 +𝑒 𝐵) = (𝐴 + 𝐵) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(𝐴 + 𝐵)) |
17 | 15, 16 | syl 14 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
-𝑒(𝐴
+𝑒 𝐵) =
-𝑒(𝐴 +
𝐵)) |
18 | | rexneg 9774 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
-𝑒𝐴 =
-𝐴) |
19 | | rexneg 9774 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ →
-𝑒𝐵 =
-𝐵) |
20 | 18, 19 | oveqan12d 5869 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(-𝑒𝐴
+𝑒 -𝑒𝐵) = (-𝐴 +𝑒 -𝐵)) |
21 | 14, 17, 20 | 3eqtr4d 2213 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
-𝑒(𝐴
+𝑒 𝐵) =
(-𝑒𝐴
+𝑒 -𝑒𝐵)) |
22 | | xnegpnf 9772 |
. . . . . 6
⊢
-𝑒+∞ = -∞ |
23 | | oveq2 5858 |
. . . . . . . 8
⊢ (𝐵 = +∞ → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒
+∞)) |
24 | | rexr 7952 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
25 | | renemnf 7955 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞) |
26 | | xaddpnf1 9790 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
→ (𝐴
+𝑒 +∞) = +∞) |
27 | 24, 25, 26 | syl2anc 409 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 +𝑒 +∞)
= +∞) |
28 | 23, 27 | sylan9eqr 2225 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐵) = +∞) |
29 | | xnegeq 9771 |
. . . . . . 7
⊢ ((𝐴 +𝑒 𝐵) = +∞ →
-𝑒(𝐴
+𝑒 𝐵) =
-𝑒+∞) |
30 | 28, 29 | syl 14 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) →
-𝑒(𝐴
+𝑒 𝐵) =
-𝑒+∞) |
31 | | xnegeq 9771 |
. . . . . . . . 9
⊢ (𝐵 = +∞ →
-𝑒𝐵 =
-𝑒+∞) |
32 | 31, 22 | eqtrdi 2219 |
. . . . . . . 8
⊢ (𝐵 = +∞ →
-𝑒𝐵 =
-∞) |
33 | 32 | oveq2d 5866 |
. . . . . . 7
⊢ (𝐵 = +∞ →
(-𝑒𝐴
+𝑒 -𝑒𝐵) = (-𝑒𝐴 +𝑒
-∞)) |
34 | 18, 10 | eqeltrd 2247 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ →
-𝑒𝐴
∈ ℝ) |
35 | | rexr 7952 |
. . . . . . . . 9
⊢
(-𝑒𝐴 ∈ ℝ →
-𝑒𝐴
∈ ℝ*) |
36 | | renepnf 7954 |
. . . . . . . . 9
⊢
(-𝑒𝐴 ∈ ℝ →
-𝑒𝐴 ≠
+∞) |
37 | | xaddmnf1 9792 |
. . . . . . . . 9
⊢
((-𝑒𝐴 ∈ ℝ* ∧
-𝑒𝐴 ≠
+∞) → (-𝑒𝐴 +𝑒 -∞) =
-∞) |
38 | 35, 36, 37 | syl2anc 409 |
. . . . . . . 8
⊢
(-𝑒𝐴 ∈ ℝ →
(-𝑒𝐴
+𝑒 -∞) = -∞) |
39 | 34, 38 | syl 14 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(-𝑒𝐴
+𝑒 -∞) = -∞) |
40 | 33, 39 | sylan9eqr 2225 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) →
(-𝑒𝐴
+𝑒 -𝑒𝐵) = -∞) |
41 | 22, 30, 40 | 3eqtr4a 2229 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) →
-𝑒(𝐴
+𝑒 𝐵) =
(-𝑒𝐴
+𝑒 -𝑒𝐵)) |
42 | | xnegmnf 9773 |
. . . . . 6
⊢
-𝑒-∞ = +∞ |
43 | | oveq2 5858 |
. . . . . . . 8
⊢ (𝐵 = -∞ → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒
-∞)) |
44 | | renepnf 7954 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞) |
45 | | xaddmnf1 9792 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
→ (𝐴
+𝑒 -∞) = -∞) |
46 | 24, 44, 45 | syl2anc 409 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 +𝑒 -∞)
= -∞) |
47 | 43, 46 | sylan9eqr 2225 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐵) = -∞) |
48 | | xnegeq 9771 |
. . . . . . 7
⊢ ((𝐴 +𝑒 𝐵) = -∞ →
-𝑒(𝐴
+𝑒 𝐵) =
-𝑒-∞) |
49 | 47, 48 | syl 14 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) →
-𝑒(𝐴
+𝑒 𝐵) =
-𝑒-∞) |
50 | | xnegeq 9771 |
. . . . . . . . 9
⊢ (𝐵 = -∞ →
-𝑒𝐵 =
-𝑒-∞) |
51 | 50, 42 | eqtrdi 2219 |
. . . . . . . 8
⊢ (𝐵 = -∞ →
-𝑒𝐵 =
+∞) |
52 | 51 | oveq2d 5866 |
. . . . . . 7
⊢ (𝐵 = -∞ →
(-𝑒𝐴
+𝑒 -𝑒𝐵) = (-𝑒𝐴 +𝑒
+∞)) |
53 | | renemnf 7955 |
. . . . . . . . 9
⊢
(-𝑒𝐴 ∈ ℝ →
-𝑒𝐴 ≠
-∞) |
54 | | xaddpnf1 9790 |
. . . . . . . . 9
⊢
((-𝑒𝐴 ∈ ℝ* ∧
-𝑒𝐴 ≠
-∞) → (-𝑒𝐴 +𝑒 +∞) =
+∞) |
55 | 35, 53, 54 | syl2anc 409 |
. . . . . . . 8
⊢
(-𝑒𝐴 ∈ ℝ →
(-𝑒𝐴
+𝑒 +∞) = +∞) |
56 | 34, 55 | syl 14 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(-𝑒𝐴
+𝑒 +∞) = +∞) |
57 | 52, 56 | sylan9eqr 2225 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) →
(-𝑒𝐴
+𝑒 -𝑒𝐵) = +∞) |
58 | 42, 49, 57 | 3eqtr4a 2229 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) →
-𝑒(𝐴
+𝑒 𝐵) =
(-𝑒𝐴
+𝑒 -𝑒𝐵)) |
59 | 21, 41, 58 | 3jaodan 1301 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) →
-𝑒(𝐴
+𝑒 𝐵) =
(-𝑒𝐴
+𝑒 -𝑒𝐵)) |
60 | 2, 59 | sylan2b 285 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*)
→ -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒
-𝑒𝐵)) |
61 | | xneg0 9775 |
. . . . . . 7
⊢
-𝑒0 = 0 |
62 | | simpr 109 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
𝐵 =
-∞) |
63 | 62 | oveq2d 5866 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
(+∞ +𝑒 𝐵) = (+∞ +𝑒
-∞)) |
64 | | pnfaddmnf 9794 |
. . . . . . . . 9
⊢ (+∞
+𝑒 -∞) = 0 |
65 | 63, 64 | eqtrdi 2219 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
(+∞ +𝑒 𝐵) = 0) |
66 | | xnegeq 9771 |
. . . . . . . 8
⊢
((+∞ +𝑒 𝐵) = 0 → -𝑒(+∞
+𝑒 𝐵) =
-𝑒0) |
67 | 65, 66 | syl 14 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
-𝑒(+∞ +𝑒 𝐵) = -𝑒0) |
68 | 51 | adantl 275 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
-𝑒𝐵 =
+∞) |
69 | 68 | oveq2d 5866 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
(-∞ +𝑒 -𝑒𝐵) = (-∞ +𝑒
+∞)) |
70 | | mnfaddpnf 9795 |
. . . . . . . 8
⊢ (-∞
+𝑒 +∞) = 0 |
71 | 69, 70 | eqtrdi 2219 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
(-∞ +𝑒 -𝑒𝐵) = 0) |
72 | 61, 67, 71 | 3eqtr4a 2229 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = -∞) →
-𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒
-𝑒𝐵)) |
73 | | xaddpnf2 9791 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ (+∞ +𝑒 𝐵) = +∞) |
74 | | xnegeq 9771 |
. . . . . . . 8
⊢
((+∞ +𝑒 𝐵) = +∞ →
-𝑒(+∞ +𝑒 𝐵) =
-𝑒+∞) |
75 | 73, 74 | syl 14 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ -𝑒(+∞ +𝑒 𝐵) =
-𝑒+∞) |
76 | | xnegcl 9776 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ*
→ -𝑒𝐵 ∈
ℝ*) |
77 | | xnegeq 9771 |
. . . . . . . . . . . 12
⊢
(-𝑒𝐵 = +∞ →
-𝑒-𝑒𝐵 =
-𝑒+∞) |
78 | 77, 22 | eqtrdi 2219 |
. . . . . . . . . . 11
⊢
(-𝑒𝐵 = +∞ →
-𝑒-𝑒𝐵 = -∞) |
79 | | xnegneg 9777 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ*
→ -𝑒-𝑒𝐵 = 𝐵) |
80 | 79 | eqeq1d 2179 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ*
→ (-𝑒-𝑒𝐵 = -∞ ↔ 𝐵 = -∞)) |
81 | 78, 80 | syl5ib 153 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ*
→ (-𝑒𝐵 = +∞ → 𝐵 = -∞)) |
82 | 81 | necon3d 2384 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ*
→ (𝐵 ≠ -∞
→ -𝑒𝐵 ≠ +∞)) |
83 | 82 | imp 123 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ -𝑒𝐵 ≠ +∞) |
84 | | xaddmnf2 9793 |
. . . . . . . 8
⊢
((-𝑒𝐵 ∈ ℝ* ∧
-𝑒𝐵 ≠
+∞) → (-∞ +𝑒 -𝑒𝐵) = -∞) |
85 | 76, 83, 84 | syl2an2r 590 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ (-∞ +𝑒 -𝑒𝐵) = -∞) |
86 | 22, 75, 85 | 3eqtr4a 2229 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ -∞)
→ -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒
-𝑒𝐵)) |
87 | | xrmnfdc 9787 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ*
→ DECID 𝐵 = -∞) |
88 | | exmiddc 831 |
. . . . . . . 8
⊢
(DECID 𝐵 = -∞ → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞)) |
89 | 87, 88 | syl 14 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ*
→ (𝐵 = -∞ ∨
¬ 𝐵 =
-∞)) |
90 | | df-ne 2341 |
. . . . . . . 8
⊢ (𝐵 ≠ -∞ ↔ ¬
𝐵 =
-∞) |
91 | 90 | orbi2i 757 |
. . . . . . 7
⊢ ((𝐵 = -∞ ∨ 𝐵 ≠ -∞) ↔ (𝐵 = -∞ ∨ ¬ 𝐵 = -∞)) |
92 | 89, 91 | sylibr 133 |
. . . . . 6
⊢ (𝐵 ∈ ℝ*
→ (𝐵 = -∞ ∨
𝐵 ≠
-∞)) |
93 | 72, 86, 92 | mpjaodan 793 |
. . . . 5
⊢ (𝐵 ∈ ℝ*
→ -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒
-𝑒𝐵)) |
94 | 93 | adantl 275 |
. . . 4
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒
-𝑒𝐵)) |
95 | | simpl 108 |
. . . . . 6
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ 𝐴 =
+∞) |
96 | 95 | oveq1d 5865 |
. . . . 5
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ (𝐴
+𝑒 𝐵) =
(+∞ +𝑒 𝐵)) |
97 | | xnegeq 9771 |
. . . . 5
⊢ ((𝐴 +𝑒 𝐵) = (+∞
+𝑒 𝐵)
→ -𝑒(𝐴 +𝑒 𝐵) = -𝑒(+∞
+𝑒 𝐵)) |
98 | 96, 97 | syl 14 |
. . . 4
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒(𝐴 +𝑒 𝐵) = -𝑒(+∞
+𝑒 𝐵)) |
99 | | xnegeq 9771 |
. . . . . . 7
⊢ (𝐴 = +∞ →
-𝑒𝐴 =
-𝑒+∞) |
100 | 99 | adantr 274 |
. . . . . 6
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒𝐴 =
-𝑒+∞) |
101 | 100, 22 | eqtrdi 2219 |
. . . . 5
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒𝐴 = -∞) |
102 | 101 | oveq1d 5865 |
. . . 4
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ (-𝑒𝐴 +𝑒
-𝑒𝐵) =
(-∞ +𝑒 -𝑒𝐵)) |
103 | 94, 98, 102 | 3eqtr4d 2213 |
. . 3
⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒
-𝑒𝐵)) |
104 | | simpr 109 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
𝐵 =
+∞) |
105 | 104 | oveq2d 5866 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
(-∞ +𝑒 𝐵) = (-∞ +𝑒
+∞)) |
106 | 105, 70 | eqtrdi 2219 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
(-∞ +𝑒 𝐵) = 0) |
107 | | xnegeq 9771 |
. . . . . . . 8
⊢
((-∞ +𝑒 𝐵) = 0 → -𝑒(-∞
+𝑒 𝐵) =
-𝑒0) |
108 | 106, 107 | syl 14 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
-𝑒(-∞ +𝑒 𝐵) = -𝑒0) |
109 | 32 | adantl 275 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
-𝑒𝐵 =
-∞) |
110 | 109 | oveq2d 5866 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
(+∞ +𝑒 -𝑒𝐵) = (+∞ +𝑒
-∞)) |
111 | 110, 64 | eqtrdi 2219 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
(+∞ +𝑒 -𝑒𝐵) = 0) |
112 | 61, 108, 111 | 3eqtr4a 2229 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 = +∞) →
-𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒
-𝑒𝐵)) |
113 | | xaddmnf2 9793 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
→ (-∞ +𝑒 𝐵) = -∞) |
114 | | xnegeq 9771 |
. . . . . . . 8
⊢
((-∞ +𝑒 𝐵) = -∞ →
-𝑒(-∞ +𝑒 𝐵) =
-𝑒-∞) |
115 | 113, 114 | syl 14 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
→ -𝑒(-∞ +𝑒 𝐵) =
-𝑒-∞) |
116 | | xnegeq 9771 |
. . . . . . . . . . . 12
⊢
(-𝑒𝐵 = -∞ →
-𝑒-𝑒𝐵 =
-𝑒-∞) |
117 | 116, 42 | eqtrdi 2219 |
. . . . . . . . . . 11
⊢
(-𝑒𝐵 = -∞ →
-𝑒-𝑒𝐵 = +∞) |
118 | 79 | eqeq1d 2179 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ*
→ (-𝑒-𝑒𝐵 = +∞ ↔ 𝐵 = +∞)) |
119 | 117, 118 | syl5ib 153 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ*
→ (-𝑒𝐵 = -∞ → 𝐵 = +∞)) |
120 | 119 | necon3d 2384 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ*
→ (𝐵 ≠ +∞
→ -𝑒𝐵 ≠ -∞)) |
121 | 120 | imp 123 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
→ -𝑒𝐵 ≠ -∞) |
122 | | xaddpnf2 9791 |
. . . . . . . 8
⊢
((-𝑒𝐵 ∈ ℝ* ∧
-𝑒𝐵 ≠
-∞) → (+∞ +𝑒 -𝑒𝐵) = +∞) |
123 | 76, 121, 122 | syl2an2r 590 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
→ (+∞ +𝑒 -𝑒𝐵) = +∞) |
124 | 42, 115, 123 | 3eqtr4a 2229 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
→ -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒
-𝑒𝐵)) |
125 | | xrpnfdc 9786 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ*
→ DECID 𝐵 = +∞) |
126 | | exmiddc 831 |
. . . . . . . 8
⊢
(DECID 𝐵 = +∞ → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞)) |
127 | 125, 126 | syl 14 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ*
→ (𝐵 = +∞ ∨
¬ 𝐵 =
+∞)) |
128 | | df-ne 2341 |
. . . . . . . 8
⊢ (𝐵 ≠ +∞ ↔ ¬
𝐵 =
+∞) |
129 | 128 | orbi2i 757 |
. . . . . . 7
⊢ ((𝐵 = +∞ ∨ 𝐵 ≠ +∞) ↔ (𝐵 = +∞ ∨ ¬ 𝐵 = +∞)) |
130 | 127, 129 | sylibr 133 |
. . . . . 6
⊢ (𝐵 ∈ ℝ*
→ (𝐵 = +∞ ∨
𝐵 ≠
+∞)) |
131 | 112, 124,
130 | mpjaodan 793 |
. . . . 5
⊢ (𝐵 ∈ ℝ*
→ -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒
-𝑒𝐵)) |
132 | 131 | adantl 275 |
. . . 4
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒
-𝑒𝐵)) |
133 | | simpl 108 |
. . . . . 6
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ 𝐴 =
-∞) |
134 | 133 | oveq1d 5865 |
. . . . 5
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ (𝐴
+𝑒 𝐵) =
(-∞ +𝑒 𝐵)) |
135 | | xnegeq 9771 |
. . . . 5
⊢ ((𝐴 +𝑒 𝐵) = (-∞
+𝑒 𝐵)
→ -𝑒(𝐴 +𝑒 𝐵) = -𝑒(-∞
+𝑒 𝐵)) |
136 | 134, 135 | syl 14 |
. . . 4
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒(𝐴 +𝑒 𝐵) = -𝑒(-∞
+𝑒 𝐵)) |
137 | | xnegeq 9771 |
. . . . . . 7
⊢ (𝐴 = -∞ →
-𝑒𝐴 =
-𝑒-∞) |
138 | 137 | adantr 274 |
. . . . . 6
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒𝐴 =
-𝑒-∞) |
139 | 138, 42 | eqtrdi 2219 |
. . . . 5
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒𝐴 = +∞) |
140 | 139 | oveq1d 5865 |
. . . 4
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ (-𝑒𝐴 +𝑒
-𝑒𝐵) =
(+∞ +𝑒 -𝑒𝐵)) |
141 | 132, 136,
140 | 3eqtr4d 2213 |
. . 3
⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*)
→ -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒
-𝑒𝐵)) |
142 | 60, 103, 141 | 3jaoian 1300 |
. 2
⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ*)
→ -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒
-𝑒𝐵)) |
143 | 1, 142 | sylanb 282 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒
-𝑒𝐵)) |