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 ) )

Metamath Proof Explorer

Theorem xnegdi

Proof