xnegdi

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

		Ref	Expression
	Assertion	xnegdi	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to - (A +_{𝑒} B) = (- A) +_{𝑒} (- B)$

Proof

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

Metamath Proof Explorer

Theorem xnegdi

Proof