xaddcom - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > xaddcom		Structured version Visualization version GIF version

Theorem xaddcom 13282

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

**Assertion**
Ref	Expression
xaddcom	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))

**Proof of Theorem xaddcom**
Step	Hyp	Ref	Expression
1		elxr 13157	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		elxr 13157	. . . 4 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
3		recn 11205	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
4		recn 11205	. . . . . . 7 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
5		addcom 11411	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
6	3, 4, 5	syl2an 608	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
7		rexadd 13274	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +_𝑒 𝐵) = (𝐴 + 𝐵))
8		rexadd 13274	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 +_𝑒 𝐴) = (𝐵 + 𝐴))
9	8	ancoms 464	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 𝐴) = (𝐵 + 𝐴))
10	6, 7, 9	3eqtr4d 2810	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
11		oveq2 7427	. . . . . . 7 ⊢ (𝐵 = +∞ → (𝐴 +_𝑒 𝐵) = (𝐴 +_𝑒 +∞))
12		rexr 11270	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
13		renemnf 11273	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
14		xaddpnf1 13268	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞) → (𝐴 +_𝑒 +∞) = +∞)
15	12, 13, 14	syl2anc 596	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (𝐴 +_𝑒 +∞) = +∞)
16	11, 15	sylan9eqr 2822	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 +_𝑒 𝐵) = +∞)
17		oveq1 7426	. . . . . . 7 ⊢ (𝐵 = +∞ → (𝐵 +_𝑒 𝐴) = (+∞ +_𝑒 𝐴))
18		xaddpnf2 13269	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞) → (+∞ +_𝑒 𝐴) = +∞)
19	12, 13, 18	syl2anc 596	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (+∞ +_𝑒 𝐴) = +∞)
20	17, 19	sylan9eqr 2822	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 𝐴) = +∞)
21	16, 20	eqtr4d 2803	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
22		oveq2 7427	. . . . . . 7 ⊢ (𝐵 = -∞ → (𝐴 +_𝑒 𝐵) = (𝐴 +_𝑒 -∞))
23		renepnf 11272	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
24		xaddmnf1 13270	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ +∞) → (𝐴 +_𝑒 -∞) = -∞)
25	12, 23, 24	syl2anc 596	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (𝐴 +_𝑒 -∞) = -∞)
26	22, 25	sylan9eqr 2822	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 +_𝑒 𝐵) = -∞)
27		oveq1 7426	. . . . . . 7 ⊢ (𝐵 = -∞ → (𝐵 +_𝑒 𝐴) = (-∞ +_𝑒 𝐴))
28		xaddmnf2 13271	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ +∞) → (-∞ +_𝑒 𝐴) = -∞)
29	12, 23, 28	syl2anc 596	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (-∞ +_𝑒 𝐴) = -∞)
30	27, 29	sylan9eqr 2822	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 𝐴) = -∞)
31	26, 30	eqtr4d 2803	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
32	10, 21, 31	3jaodan 1458	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
33	2, 32	sylan2b 606	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
34		pnfaddmnf 13272	. . . . . . . 8 ⊢ (+∞ +_𝑒 -∞) = 0
35		mnfaddpnf 13273	. . . . . . . 8 ⊢ (-∞ +_𝑒 +∞) = 0
36	34, 35	eqtr4i 2791	. . . . . . 7 ⊢ (+∞ +_𝑒 -∞) = (-∞ +_𝑒 +∞)
37		simpr 490	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = -∞) → 𝐵 = -∞)
38	37	oveq2d 7435	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = -∞) → (+∞ +_𝑒 𝐵) = (+∞ +_𝑒 -∞))
39	37	oveq1d 7434	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = -∞) → (𝐵 +_𝑒 +∞) = (-∞ +_𝑒 +∞))
40	36, 38, 39	3eqtr4a 2826	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = -∞) → (+∞ +_𝑒 𝐵) = (𝐵 +_𝑒 +∞))
41		xaddpnf2 13269	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (+∞ +_𝑒 𝐵) = +∞)
42		xaddpnf1 13268	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (𝐵 +_𝑒 +∞) = +∞)
43	41, 42	eqtr4d 2803	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (+∞ +_𝑒 𝐵) = (𝐵 +_𝑒 +∞))
44	40, 43	pm2.61dane 3047	. . . . 5 ⊢ (𝐵 ∈ ℝ^* → (+∞ +_𝑒 𝐵) = (𝐵 +_𝑒 +∞))
45	44	adantl 487	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (+∞ +_𝑒 𝐵) = (𝐵 +_𝑒 +∞))
46		simpl 488	. . . . 5 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → 𝐴 = +∞)
47	46	oveq1d 7434	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (+∞ +_𝑒 𝐵))
48	46	oveq2d 7435	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐵 +_𝑒 𝐴) = (𝐵 +_𝑒 +∞))
49	45, 47, 48	3eqtr4d 2810	. . 3 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
50	35, 34	eqtr4i 2791	. . . . . . 7 ⊢ (-∞ +_𝑒 +∞) = (+∞ +_𝑒 -∞)
51		simpr 490	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = +∞) → 𝐵 = +∞)
52	51	oveq2d 7435	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = +∞) → (-∞ +_𝑒 𝐵) = (-∞ +_𝑒 +∞))
53	51	oveq1d 7434	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -∞) = (+∞ +_𝑒 -∞))
54	50, 52, 53	3eqtr4a 2826	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = +∞) → (-∞ +_𝑒 𝐵) = (𝐵 +_𝑒 -∞))
55		xaddmnf2 13271	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (-∞ +_𝑒 𝐵) = -∞)
56		xaddmnf1 13270	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (𝐵 +_𝑒 -∞) = -∞)
57	55, 56	eqtr4d 2803	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (-∞ +_𝑒 𝐵) = (𝐵 +_𝑒 -∞))
58	54, 57	pm2.61dane 3047	. . . . 5 ⊢ (𝐵 ∈ ℝ^* → (-∞ +_𝑒 𝐵) = (𝐵 +_𝑒 -∞))
59	58	adantl 487	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (-∞ +_𝑒 𝐵) = (𝐵 +_𝑒 -∞))
60		simpl 488	. . . . 5 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → 𝐴 = -∞)
61	60	oveq1d 7434	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (-∞ +_𝑒 𝐵))
62	60	oveq2d 7435	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (𝐵 +_𝑒 𝐴) = (𝐵 +_𝑒 -∞))
63	59, 61, 62	3eqtr4d 2810	. . 3 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
64	33, 49, 63	3jaoian 1457	. 2 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
65	1, 64	sylanb 593	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∨ w3o 1102 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 (class class class)co 7419 ℂcc 11113 ℝcr 11114 0cc0 11115 + caddc 11118 +∞cpnf 11255 -∞cmnf 11256 ℝ^*cxr 11257 +_𝑒 cxad 13151

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-cnex 11171 ax-resscn 11172 ax-1cn 11173 ax-icn 11174 ax-addcl 11175 ax-addrcl 11176 ax-mulcl 11177 ax-mulrcl 11178 ax-mulcom 11179 ax-addass 11180 ax-mulass 11181 ax-distr 11182 ax-i2m1 11183 ax-1ne0 11184 ax-1rid 11185 ax-rnegex 11186 ax-rrecex 11187 ax-cnre 11188 ax-pre-lttri 11189 ax-pre-lttrn 11190 ax-pre-ltadd 11191

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5558 df-po 5571 df-so 5572 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-ov 7422 df-oprab 7423 df-mpo 7424 df-er 8700 df-en 8950 df-dom 8951 df-sdom 8952 df-pnf 11260 df-mnf 11261 df-xr 11262 df-ltxr 11263 df-xadd 13154

This theorem is used by: xaddlid 13284 xleadd2a 13296 xltadd2 13299 xposdif 13304 xadd4d 13345 hashunx 14440 xrsnsgrp 21608 xrs1cmn 21642 blcld 24713 xrsxmet 25018 metdstri 25060 vtxdginducedm1 29951 xaddeq0 33168 xlt2addrd 33174 xrge0npcan 33404 esumle 34512 esumlef 34516 measun 34666 difelcarsg 34765 xaddcomd 46098

W3C validator