xaddcom

Description: The extended real addition operation is commutative. (Contributed by NM, 26-Dec-2011)

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

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		addcom	$⊢ (A \in ℂ \land B \in ℂ) \to A + B = B + A$
6	3 4 5	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to A + B = B + A$
7		rexadd	$⊢ (A \in ℝ \land B \in ℝ) \to A +_{𝑒} B = A + B$
8		rexadd	$⊢ (B \in ℝ \land A \in ℝ) \to B +_{𝑒} A = B + A$
9	8	ancoms	$⊢ (A \in ℝ \land B \in ℝ) \to B +_{𝑒} A = B + A$
10	6 7 9	3eqtr4d	$⊢ (A \in ℝ \land B \in ℝ) \to A +_{𝑒} B = B +_{𝑒} A$
11		oveq2	$⊢ B = +∞ \to A +_{𝑒} B = A +_{𝑒} +∞$
12		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
13		renemnf	$⊢ A \in ℝ \to A \neq −∞$
14		xaddpnf1	$⊢ (A \in ℝ^{*} \land A \neq −∞) \to A +_{𝑒} +∞ = +∞$
15	12 13 14	syl2anc	$⊢ A \in ℝ \to A +_{𝑒} +∞ = +∞$
16	11 15	sylan9eqr	$⊢ (A \in ℝ \land B = +∞) \to A +_{𝑒} B = +∞$
17		oveq1	$⊢ B = +∞ \to B +_{𝑒} A = +∞ +_{𝑒} A$
18		xaddpnf2	$⊢ (A \in ℝ^{*} \land A \neq −∞) \to +∞ +_{𝑒} A = +∞$
19	12 13 18	syl2anc	$⊢ A \in ℝ \to +∞ +_{𝑒} A = +∞$
20	17 19	sylan9eqr	$⊢ (A \in ℝ \land B = +∞) \to B +_{𝑒} A = +∞$
21	16 20	eqtr4d	$⊢ (A \in ℝ \land B = +∞) \to A +_{𝑒} B = B +_{𝑒} A$
22		oveq2	$⊢ B = −∞ \to A +_{𝑒} B = A +_{𝑒} −∞$
23		renepnf	$⊢ A \in ℝ \to A \neq +∞$
24		xaddmnf1	$⊢ (A \in ℝ^{*} \land A \neq +∞) \to A +_{𝑒} −∞ = −∞$
25	12 23 24	syl2anc	$⊢ A \in ℝ \to A +_{𝑒} −∞ = −∞$
26	22 25	sylan9eqr	$⊢ (A \in ℝ \land B = −∞) \to A +_{𝑒} B = −∞$
27		oveq1	$⊢ B = −∞ \to B +_{𝑒} A = −∞ +_{𝑒} A$
28		xaddmnf2	$⊢ (A \in ℝ^{*} \land A \neq +∞) \to −∞ +_{𝑒} A = −∞$
29	12 23 28	syl2anc	$⊢ A \in ℝ \to −∞ +_{𝑒} A = −∞$
30	27 29	sylan9eqr	$⊢ (A \in ℝ \land B = −∞) \to B +_{𝑒} A = −∞$
31	26 30	eqtr4d	$⊢ (A \in ℝ \land B = −∞) \to A +_{𝑒} B = B +_{𝑒} A$
32	10 21 31	3jaodan	$⊢ (A \in ℝ \land (B \in ℝ \lor B = +∞ \lor B = −∞)) \to A +_{𝑒} B = B +_{𝑒} A$
33	2 32	sylan2b	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to A +_{𝑒} B = B +_{𝑒} A$
34		pnfaddmnf	$⊢ +∞ +_{𝑒} −∞ = 0$
35		mnfaddpnf	$⊢ −∞ +_{𝑒} +∞ = 0$
36	34 35	eqtr4i	$⊢ +∞ +_{𝑒} −∞ = −∞ +_{𝑒} +∞$
37		simpr	$⊢ (B \in ℝ^{*} \land B = −∞) \to B = −∞$
38	37	oveq2d	$⊢ (B \in ℝ^{*} \land B = −∞) \to +∞ +_{𝑒} B = +∞ +_{𝑒} −∞$
39	37	oveq1d	$⊢ (B \in ℝ^{*} \land B = −∞) \to B +_{𝑒} +∞ = −∞ +_{𝑒} +∞$
40	36 38 39	3eqtr4a	$⊢ (B \in ℝ^{*} \land B = −∞) \to +∞ +_{𝑒} B = B +_{𝑒} +∞$
41		xaddpnf2	$⊢ (B \in ℝ^{*} \land B \neq −∞) \to +∞ +_{𝑒} B = +∞$
42		xaddpnf1	$⊢ (B \in ℝ^{*} \land B \neq −∞) \to B +_{𝑒} +∞ = +∞$
43	41 42	eqtr4d	$⊢ (B \in ℝ^{*} \land B \neq −∞) \to +∞ +_{𝑒} B = B +_{𝑒} +∞$
44	40 43	pm2.61dane	$⊢ B \in ℝ^{*} \to +∞ +_{𝑒} B = B +_{𝑒} +∞$
45	44	adantl	$⊢ (A = +∞ \land B \in ℝ^{*}) \to +∞ +_{𝑒} B = B +_{𝑒} +∞$
46		simpl	$⊢ (A = +∞ \land B \in ℝ^{*}) \to A = +∞$
47	46	oveq1d	$⊢ (A = +∞ \land B \in ℝ^{*}) \to A +_{𝑒} B = +∞ +_{𝑒} B$
48	46	oveq2d	$⊢ (A = +∞ \land B \in ℝ^{*}) \to B +_{𝑒} A = B +_{𝑒} +∞$
49	45 47 48	3eqtr4d	$⊢ (A = +∞ \land B \in ℝ^{*}) \to A +_{𝑒} B = B +_{𝑒} A$
50	35 34	eqtr4i	$⊢ −∞ +_{𝑒} +∞ = +∞ +_{𝑒} −∞$
51		simpr	$⊢ (B \in ℝ^{*} \land B = +∞) \to B = +∞$
52	51	oveq2d	$⊢ (B \in ℝ^{*} \land B = +∞) \to −∞ +_{𝑒} B = −∞ +_{𝑒} +∞$
53	51	oveq1d	$⊢ (B \in ℝ^{*} \land B = +∞) \to B +_{𝑒} −∞ = +∞ +_{𝑒} −∞$
54	50 52 53	3eqtr4a	$⊢ (B \in ℝ^{*} \land B = +∞) \to −∞ +_{𝑒} B = B +_{𝑒} −∞$
55		xaddmnf2	$⊢ (B \in ℝ^{*} \land B \neq +∞) \to −∞ +_{𝑒} B = −∞$
56		xaddmnf1	$⊢ (B \in ℝ^{*} \land B \neq +∞) \to B +_{𝑒} −∞ = −∞$
57	55 56	eqtr4d	$⊢ (B \in ℝ^{*} \land B \neq +∞) \to −∞ +_{𝑒} B = B +_{𝑒} −∞$
58	54 57	pm2.61dane	$⊢ B \in ℝ^{*} \to −∞ +_{𝑒} B = B +_{𝑒} −∞$
59	58	adantl	$⊢ (A = −∞ \land B \in ℝ^{*}) \to −∞ +_{𝑒} B = B +_{𝑒} −∞$
60		simpl	$⊢ (A = −∞ \land B \in ℝ^{*}) \to A = −∞$
61	60	oveq1d	$⊢ (A = −∞ \land B \in ℝ^{*}) \to A +_{𝑒} B = −∞ +_{𝑒} B$
62	60	oveq2d	$⊢ (A = −∞ \land B \in ℝ^{*}) \to B +_{𝑒} A = B +_{𝑒} −∞$
63	59 61 62	3eqtr4d	$⊢ (A = −∞ \land B \in ℝ^{*}) \to A +_{𝑒} B = B +_{𝑒} A$
64	33 49 63	3jaoian	$⊢ ((A \in ℝ \lor A = +∞ \lor A = −∞) \land B \in ℝ^{*}) \to A +_{𝑒} B = B +_{𝑒} A$
65	1 64	sylanb	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A +_{𝑒} B = B +_{𝑒} A$

Metamath Proof Explorer

Theorem xaddcom

Proof