This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xnegdi

Description: Extended real version of negdi . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xnegdi ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) )

Proof

Step Hyp Ref Expression
1 elxr ⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
2 elxr ⊢ ( 𝐵 ∈ ℝ* ↔ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) )
3 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
4 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
5 negdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐴 + 𝐵 ) = ( - 𝐴 + - 𝐵 ) )
6 3 4 5 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → - ( 𝐴 + 𝐵 ) = ( - 𝐴 + - 𝐵 ) )
7 readdcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
8 rexneg ⊢ ( ( 𝐴 + 𝐵 ) ∈ ℝ → -𝑒 ( 𝐴 + 𝐵 ) = - ( 𝐴 + 𝐵 ) )
9 7 8 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → -𝑒 ( 𝐴 + 𝐵 ) = - ( 𝐴 + 𝐵 ) )
10 renegcl ⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
11 renegcl ⊢ ( 𝐵 ∈ ℝ → - 𝐵 ∈ ℝ )
12 rexadd ⊢ ( ( - 𝐴 ∈ ℝ ∧ - 𝐵 ∈ ℝ ) → ( - 𝐴 +𝑒 - 𝐵 ) = ( - 𝐴 + - 𝐵 ) )
13 10 11 12 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - 𝐴 +𝑒 - 𝐵 ) = ( - 𝐴 + - 𝐵 ) )
14 6 9 13 3eqtr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → -𝑒 ( 𝐴 + 𝐵 ) = ( - 𝐴 +𝑒 - 𝐵 ) )
15 rexadd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +𝑒 𝐵 ) = ( 𝐴 + 𝐵 ) )
16 xnegeq ⊢ ( ( 𝐴 +𝑒 𝐵 ) = ( 𝐴 + 𝐵 ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = -𝑒 ( 𝐴 + 𝐵 ) )
17 15 16 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = -𝑒 ( 𝐴 + 𝐵 ) )
18 rexneg ⊢ ( 𝐴 ∈ ℝ → -𝑒 𝐴 = - 𝐴 )
19 rexneg ⊢ ( 𝐵 ∈ ℝ → -𝑒 𝐵 = - 𝐵 )
20 18 19 oveqan12d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) = ( - 𝐴 +𝑒 - 𝐵 ) )
21 14 17 20 3eqtr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) )
22 xnegpnf ⊢ -𝑒 +∞ = -∞
23 oveq2 ⊢ ( 𝐵 = +∞ → ( 𝐴 +𝑒 𝐵 ) = ( 𝐴 +𝑒 +∞ ) )
24 rexr ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
25 renemnf ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≠ -∞ )
26 xaddpnf1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) → ( 𝐴 +𝑒 +∞ ) = +∞ )
27 24 25 26 syl2anc ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 +𝑒 +∞ ) = +∞ )
28 23 27 sylan9eqr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → ( 𝐴 +𝑒 𝐵 ) = +∞ )
29 xnegeq ⊢ ( ( 𝐴 +𝑒 𝐵 ) = +∞ → -𝑒 ( 𝐴 +𝑒 𝐵 ) = -𝑒 +∞ )
30 28 29 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = -𝑒 +∞ )
31 xnegeq ⊢ ( 𝐵 = +∞ → -𝑒 𝐵 = -𝑒 +∞ )
32 31 22 eqtrdi ⊢ ( 𝐵 = +∞ → -𝑒 𝐵 = -∞ )
33 32 oveq2d ⊢ ( 𝐵 = +∞ → ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) = ( -𝑒 𝐴 +𝑒 -∞ ) )
34 18 10 eqeltrd ⊢ ( 𝐴 ∈ ℝ → -𝑒 𝐴 ∈ ℝ )
35 rexr ⊢ ( -𝑒 𝐴 ∈ ℝ → -𝑒 𝐴 ∈ ℝ* )
36 renepnf ⊢ ( -𝑒 𝐴 ∈ ℝ → -𝑒 𝐴 ≠ +∞ )
37 xaddmnf1 ⊢ ( ( -𝑒 𝐴 ∈ ℝ* ∧ -𝑒 𝐴 ≠ +∞ ) → ( -𝑒 𝐴 +𝑒 -∞ ) = -∞ )
38 35 36 37 syl2anc ⊢ ( -𝑒 𝐴 ∈ ℝ → ( -𝑒 𝐴 +𝑒 -∞ ) = -∞ )
39 34 38 syl ⊢ ( 𝐴 ∈ ℝ → ( -𝑒 𝐴 +𝑒 -∞ ) = -∞ )
40 33 39 sylan9eqr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) = -∞ )
41 22 30 40 3eqtr4a ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) )
42 xnegmnf ⊢ -𝑒 -∞ = +∞
43 oveq2 ⊢ ( 𝐵 = -∞ → ( 𝐴 +𝑒 𝐵 ) = ( 𝐴 +𝑒 -∞ ) )
44 renepnf ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≠ +∞ )
45 xaddmnf1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) → ( 𝐴 +𝑒 -∞ ) = -∞ )
46 24 44 45 syl2anc ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 +𝑒 -∞ ) = -∞ )
47 43 46 sylan9eqr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = -∞ ) → ( 𝐴 +𝑒 𝐵 ) = -∞ )
48 xnegeq ⊢ ( ( 𝐴 +𝑒 𝐵 ) = -∞ → -𝑒 ( 𝐴 +𝑒 𝐵 ) = -𝑒 -∞ )
49 47 48 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = -∞ ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = -𝑒 -∞ )
50 xnegeq ⊢ ( 𝐵 = -∞ → -𝑒 𝐵 = -𝑒 -∞ )
51 50 42 eqtrdi ⊢ ( 𝐵 = -∞ → -𝑒 𝐵 = +∞ )
52 51 oveq2d ⊢ ( 𝐵 = -∞ → ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) = ( -𝑒 𝐴 +𝑒 +∞ ) )
53 renemnf ⊢ ( -𝑒 𝐴 ∈ ℝ → -𝑒 𝐴 ≠ -∞ )
54 xaddpnf1 ⊢ ( ( -𝑒 𝐴 ∈ ℝ* ∧ -𝑒 𝐴 ≠ -∞ ) → ( -𝑒 𝐴 +𝑒 +∞ ) = +∞ )
55 35 53 54 syl2anc ⊢ ( -𝑒 𝐴 ∈ ℝ → ( -𝑒 𝐴 +𝑒 +∞ ) = +∞ )
56 34 55 syl ⊢ ( 𝐴 ∈ ℝ → ( -𝑒 𝐴 +𝑒 +∞ ) = +∞ )
57 52 56 sylan9eqr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = -∞ ) → ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) = +∞ )
58 42 49 57 3eqtr4a ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = -∞ ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) )
59 21 41 58 3jaodan ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) )
60 2 59 sylan2b ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) )
61 xneg0 ⊢ -𝑒 0 = 0
62 simpr ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 = -∞ ) → 𝐵 = -∞ )
63 62 oveq2d ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 = -∞ ) → ( +∞ +𝑒 𝐵 ) = ( +∞ +𝑒 -∞ ) )
64 pnfaddmnf ⊢ ( +∞ +𝑒 -∞ ) = 0
65 63 64 eqtrdi ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 = -∞ ) → ( +∞ +𝑒 𝐵 ) = 0 )
66 xnegeq ⊢ ( ( +∞ +𝑒 𝐵 ) = 0 → -𝑒 ( +∞ +𝑒 𝐵 ) = -𝑒 0 )
67 65 66 syl ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 = -∞ ) → -𝑒 ( +∞ +𝑒 𝐵 ) = -𝑒 0 )
68 51 adantl ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 = -∞ ) → -𝑒 𝐵 = +∞ )
69 68 oveq2d ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 = -∞ ) → ( -∞ +𝑒 -𝑒 𝐵 ) = ( -∞ +𝑒 +∞ ) )
70 mnfaddpnf ⊢ ( -∞ +𝑒 +∞ ) = 0
71 69 70 eqtrdi ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 = -∞ ) → ( -∞ +𝑒 -𝑒 𝐵 ) = 0 )
72 61 67 71 3eqtr4a ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 = -∞ ) → -𝑒 ( +∞ +𝑒 𝐵 ) = ( -∞ +𝑒 -𝑒 𝐵 ) )
73 xaddpnf2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) → ( +∞ +𝑒 𝐵 ) = +∞ )
74 xnegeq ⊢ ( ( +∞ +𝑒 𝐵 ) = +∞ → -𝑒 ( +∞ +𝑒 𝐵 ) = -𝑒 +∞ )
75 73 74 syl ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) → -𝑒 ( +∞ +𝑒 𝐵 ) = -𝑒 +∞ )
76 xnegcl ⊢ ( 𝐵 ∈ ℝ* → -𝑒 𝐵 ∈ ℝ* )
77 xnegeq ⊢ ( -𝑒 𝐵 = +∞ → -𝑒 -𝑒 𝐵 = -𝑒 +∞ )
78 77 22 eqtrdi ⊢ ( -𝑒 𝐵 = +∞ → -𝑒 -𝑒 𝐵 = -∞ )
79 xnegneg ⊢ ( 𝐵 ∈ ℝ* → -𝑒 -𝑒 𝐵 = 𝐵 )
80 79 eqeq1d ⊢ ( 𝐵 ∈ ℝ* → ( -𝑒 -𝑒 𝐵 = -∞ ↔ 𝐵 = -∞ ) )
81 78 80 imbitrid ⊢ ( 𝐵 ∈ ℝ* → ( -𝑒 𝐵 = +∞ → 𝐵 = -∞ ) )
82 81 necon3d ⊢ ( 𝐵 ∈ ℝ* → ( 𝐵 ≠ -∞ → -𝑒 𝐵 ≠ +∞ ) )
83 82 imp ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) → -𝑒 𝐵 ≠ +∞ )
84 xaddmnf2 ⊢ ( ( -𝑒 𝐵 ∈ ℝ* ∧ -𝑒 𝐵 ≠ +∞ ) → ( -∞ +𝑒 -𝑒 𝐵 ) = -∞ )
85 76 83 84 syl2an2r ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) → ( -∞ +𝑒 -𝑒 𝐵 ) = -∞ )
86 22 75 85 3eqtr4a ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) → -𝑒 ( +∞ +𝑒 𝐵 ) = ( -∞ +𝑒 -𝑒 𝐵 ) )
87 72 86 pm2.61dane ⊢ ( 𝐵 ∈ ℝ* → -𝑒 ( +∞ +𝑒 𝐵 ) = ( -∞ +𝑒 -𝑒 𝐵 ) )
88 87 adantl ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → -𝑒 ( +∞ +𝑒 𝐵 ) = ( -∞ +𝑒 -𝑒 𝐵 ) )
89 simpl ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → 𝐴 = +∞ )
90 89 oveq1d ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 +𝑒 𝐵 ) = ( +∞ +𝑒 𝐵 ) )
91 xnegeq ⊢ ( ( 𝐴 +𝑒 𝐵 ) = ( +∞ +𝑒 𝐵 ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = -𝑒 ( +∞ +𝑒 𝐵 ) )
92 90 91 syl ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = -𝑒 ( +∞ +𝑒 𝐵 ) )
93 xnegeq ⊢ ( 𝐴 = +∞ → -𝑒 𝐴 = -𝑒 +∞ )
94 93 adantr ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → -𝑒 𝐴 = -𝑒 +∞ )
95 94 22 eqtrdi ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → -𝑒 𝐴 = -∞ )
96 95 oveq1d ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) = ( -∞ +𝑒 -𝑒 𝐵 ) )
97 88 92 96 3eqtr4d ⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) )
98 simpr ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 = +∞ ) → 𝐵 = +∞ )
99 98 oveq2d ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 = +∞ ) → ( -∞ +𝑒 𝐵 ) = ( -∞ +𝑒 +∞ ) )
100 99 70 eqtrdi ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 = +∞ ) → ( -∞ +𝑒 𝐵 ) = 0 )
101 xnegeq ⊢ ( ( -∞ +𝑒 𝐵 ) = 0 → -𝑒 ( -∞ +𝑒 𝐵 ) = -𝑒 0 )
102 100 101 syl ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 = +∞ ) → -𝑒 ( -∞ +𝑒 𝐵 ) = -𝑒 0 )
103 32 adantl ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 = +∞ ) → -𝑒 𝐵 = -∞ )
104 103 oveq2d ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 = +∞ ) → ( +∞ +𝑒 -𝑒 𝐵 ) = ( +∞ +𝑒 -∞ ) )
105 104 64 eqtrdi ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 = +∞ ) → ( +∞ +𝑒 -𝑒 𝐵 ) = 0 )
106 61 102 105 3eqtr4a ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 = +∞ ) → -𝑒 ( -∞ +𝑒 𝐵 ) = ( +∞ +𝑒 -𝑒 𝐵 ) )
107 xaddmnf2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) → ( -∞ +𝑒 𝐵 ) = -∞ )
108 xnegeq ⊢ ( ( -∞ +𝑒 𝐵 ) = -∞ → -𝑒 ( -∞ +𝑒 𝐵 ) = -𝑒 -∞ )
109 107 108 syl ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) → -𝑒 ( -∞ +𝑒 𝐵 ) = -𝑒 -∞ )
110 xnegeq ⊢ ( -𝑒 𝐵 = -∞ → -𝑒 -𝑒 𝐵 = -𝑒 -∞ )
111 110 42 eqtrdi ⊢ ( -𝑒 𝐵 = -∞ → -𝑒 -𝑒 𝐵 = +∞ )
112 79 eqeq1d ⊢ ( 𝐵 ∈ ℝ* → ( -𝑒 -𝑒 𝐵 = +∞ ↔ 𝐵 = +∞ ) )
113 111 112 imbitrid ⊢ ( 𝐵 ∈ ℝ* → ( -𝑒 𝐵 = -∞ → 𝐵 = +∞ ) )
114 113 necon3d ⊢ ( 𝐵 ∈ ℝ* → ( 𝐵 ≠ +∞ → -𝑒 𝐵 ≠ -∞ ) )
115 114 imp ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) → -𝑒 𝐵 ≠ -∞ )
116 xaddpnf2 ⊢ ( ( -𝑒 𝐵 ∈ ℝ* ∧ -𝑒 𝐵 ≠ -∞ ) → ( +∞ +𝑒 -𝑒 𝐵 ) = +∞ )
117 76 115 116 syl2an2r ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) → ( +∞ +𝑒 -𝑒 𝐵 ) = +∞ )
118 42 109 117 3eqtr4a ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) → -𝑒 ( -∞ +𝑒 𝐵 ) = ( +∞ +𝑒 -𝑒 𝐵 ) )
119 106 118 pm2.61dane ⊢ ( 𝐵 ∈ ℝ* → -𝑒 ( -∞ +𝑒 𝐵 ) = ( +∞ +𝑒 -𝑒 𝐵 ) )
120 119 adantl ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ* ) → -𝑒 ( -∞ +𝑒 𝐵 ) = ( +∞ +𝑒 -𝑒 𝐵 ) )
121 simpl ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ* ) → 𝐴 = -∞ )
122 121 oveq1d ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 +𝑒 𝐵 ) = ( -∞ +𝑒 𝐵 ) )
123 xnegeq ⊢ ( ( 𝐴 +𝑒 𝐵 ) = ( -∞ +𝑒 𝐵 ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = -𝑒 ( -∞ +𝑒 𝐵 ) )
124 122 123 syl ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ* ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = -𝑒 ( -∞ +𝑒 𝐵 ) )
125 xnegeq ⊢ ( 𝐴 = -∞ → -𝑒 𝐴 = -𝑒 -∞ )
126 125 adantr ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ* ) → -𝑒 𝐴 = -𝑒 -∞ )
127 126 42 eqtrdi ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ* ) → -𝑒 𝐴 = +∞ )
128 127 oveq1d ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ* ) → ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) = ( +∞ +𝑒 -𝑒 𝐵 ) )
129 120 124 128 3eqtr4d ⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ* ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) )
130 60 97 129 3jaoian ⊢ ( ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) ∧ 𝐵 ∈ ℝ* ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) )
131 1 130 sylanb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → -𝑒 ( 𝐴 +𝑒 𝐵 ) = ( -𝑒 𝐴 +𝑒 -𝑒 𝐵 ) )