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 12903

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 12781	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		elxr 12781	. . . 4 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
3		recn 10892	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
4		recn 10892	. . . . . . 7 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
5		addcom 11091	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
6	3, 4, 5	syl2an 595	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
7		rexadd 12895	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +_𝑒 𝐵) = (𝐴 + 𝐵))
8		rexadd 12895	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 +_𝑒 𝐴) = (𝐵 + 𝐴))
9	8	ancoms 458	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 𝐴) = (𝐵 + 𝐴))
10	6, 7, 9	3eqtr4d 2788	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
11		oveq2 7263	. . . . . . 7 ⊢ (𝐵 = +∞ → (𝐴 +_𝑒 𝐵) = (𝐴 +_𝑒 +∞))
12		rexr 10952	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
13		renemnf 10955	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
14		xaddpnf1 12889	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞) → (𝐴 +_𝑒 +∞) = +∞)
15	12, 13, 14	syl2anc 583	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (𝐴 +_𝑒 +∞) = +∞)
16	11, 15	sylan9eqr 2801	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 +_𝑒 𝐵) = +∞)
17		oveq1 7262	. . . . . . 7 ⊢ (𝐵 = +∞ → (𝐵 +_𝑒 𝐴) = (+∞ +_𝑒 𝐴))
18		xaddpnf2 12890	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞) → (+∞ +_𝑒 𝐴) = +∞)
19	12, 13, 18	syl2anc 583	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (+∞ +_𝑒 𝐴) = +∞)
20	17, 19	sylan9eqr 2801	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 𝐴) = +∞)
21	16, 20	eqtr4d 2781	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
22		oveq2 7263	. . . . . . 7 ⊢ (𝐵 = -∞ → (𝐴 +_𝑒 𝐵) = (𝐴 +_𝑒 -∞))
23		renepnf 10954	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
24		xaddmnf1 12891	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ +∞) → (𝐴 +_𝑒 -∞) = -∞)
25	12, 23, 24	syl2anc 583	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (𝐴 +_𝑒 -∞) = -∞)
26	22, 25	sylan9eqr 2801	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 +_𝑒 𝐵) = -∞)
27		oveq1 7262	. . . . . . 7 ⊢ (𝐵 = -∞ → (𝐵 +_𝑒 𝐴) = (-∞ +_𝑒 𝐴))
28		xaddmnf2 12892	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ +∞) → (-∞ +_𝑒 𝐴) = -∞)
29	12, 23, 28	syl2anc 583	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (-∞ +_𝑒 𝐴) = -∞)
30	27, 29	sylan9eqr 2801	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 𝐴) = -∞)
31	26, 30	eqtr4d 2781	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
32	10, 21, 31	3jaodan 1428	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
33	2, 32	sylan2b 593	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
34		pnfaddmnf 12893	. . . . . . . 8 ⊢ (+∞ +_𝑒 -∞) = 0
35		mnfaddpnf 12894	. . . . . . . 8 ⊢ (-∞ +_𝑒 +∞) = 0
36	34, 35	eqtr4i 2769	. . . . . . 7 ⊢ (+∞ +_𝑒 -∞) = (-∞ +_𝑒 +∞)
37		simpr 484	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = -∞) → 𝐵 = -∞)
38	37	oveq2d 7271	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = -∞) → (+∞ +_𝑒 𝐵) = (+∞ +_𝑒 -∞))
39	37	oveq1d 7270	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = -∞) → (𝐵 +_𝑒 +∞) = (-∞ +_𝑒 +∞))
40	36, 38, 39	3eqtr4a 2805	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = -∞) → (+∞ +_𝑒 𝐵) = (𝐵 +_𝑒 +∞))
41		xaddpnf2 12890	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (+∞ +_𝑒 𝐵) = +∞)
42		xaddpnf1 12889	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (𝐵 +_𝑒 +∞) = +∞)
43	41, 42	eqtr4d 2781	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (+∞ +_𝑒 𝐵) = (𝐵 +_𝑒 +∞))
44	40, 43	pm2.61dane 3031	. . . . 5 ⊢ (𝐵 ∈ ℝ^* → (+∞ +_𝑒 𝐵) = (𝐵 +_𝑒 +∞))
45	44	adantl 481	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (+∞ +_𝑒 𝐵) = (𝐵 +_𝑒 +∞))
46		simpl 482	. . . . 5 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → 𝐴 = +∞)
47	46	oveq1d 7270	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (+∞ +_𝑒 𝐵))
48	46	oveq2d 7271	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐵 +_𝑒 𝐴) = (𝐵 +_𝑒 +∞))
49	45, 47, 48	3eqtr4d 2788	. . 3 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
50	35, 34	eqtr4i 2769	. . . . . . 7 ⊢ (-∞ +_𝑒 +∞) = (+∞ +_𝑒 -∞)
51		simpr 484	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = +∞) → 𝐵 = +∞)
52	51	oveq2d 7271	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = +∞) → (-∞ +_𝑒 𝐵) = (-∞ +_𝑒 +∞))
53	51	oveq1d 7270	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -∞) = (+∞ +_𝑒 -∞))
54	50, 52, 53	3eqtr4a 2805	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = +∞) → (-∞ +_𝑒 𝐵) = (𝐵 +_𝑒 -∞))
55		xaddmnf2 12892	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (-∞ +_𝑒 𝐵) = -∞)
56		xaddmnf1 12891	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (𝐵 +_𝑒 -∞) = -∞)
57	55, 56	eqtr4d 2781	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (-∞ +_𝑒 𝐵) = (𝐵 +_𝑒 -∞))
58	54, 57	pm2.61dane 3031	. . . . 5 ⊢ (𝐵 ∈ ℝ^* → (-∞ +_𝑒 𝐵) = (𝐵 +_𝑒 -∞))
59	58	adantl 481	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (-∞ +_𝑒 𝐵) = (𝐵 +_𝑒 -∞))
60		simpl 482	. . . . 5 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → 𝐴 = -∞)
61	60	oveq1d 7270	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (-∞ +_𝑒 𝐵))
62	60	oveq2d 7271	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (𝐵 +_𝑒 𝐴) = (𝐵 +_𝑒 -∞))
63	59, 61, 62	3eqtr4d 2788	. . 3 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
64	33, 49, 63	3jaoian 1427	. 2 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
65	1, 64	sylanb 580	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ w3o 1084 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 (class class class)co 7255 ℂcc 10800 ℝcr 10801 0cc0 10802 + caddc 10805 +∞cpnf 10937 -∞cmnf 10938 ℝ^*cxr 10939 +_𝑒 cxad 12775

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-po 5494 df-so 5495 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-ov 7258 df-oprab 7259 df-mpo 7260 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-xadd 12778

This theorem is referenced by: xaddid2 12905 xleadd2a 12917 xltadd2 12920 xposdif 12925 xadd4d 12966 hashunx 14029 xrsnsgrp 20546 xrs1cmn 20550 blcld 23567 xrsxmet 23878 metdstri 23920 vtxdginducedm1 27813 xaddeq0 30978 xlt2addrd 30983 xrge0npcan 31205 esumle 31926 esumlef 31930 measun 32079 difelcarsg 32177 xaddcomd 42753

W3C validator