Metamath Proof Explorer

Theorem xnegdi

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

Ref Expression
Assertion xnegdi 
|- ( ( A e. RR* /\ B e. RR* ) -> -e ( A +e B ) = ( -e A +e -e B ) )

Proof

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