Metamath Proof Explorer


Theorem xnegdi

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

Ref Expression
Assertion xnegdi A * B * A + 𝑒 B = A + 𝑒 B

Proof

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