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 13167

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 13042	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		elxr 13042	. . . 4 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
3		recn 11128	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
4		recn 11128	. . . . . . 7 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
5		addcom 11331	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
6	3, 4, 5	syl2an 597	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
7		rexadd 13159	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +_𝑒 𝐵) = (𝐴 + 𝐵))
8		rexadd 13159	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 +_𝑒 𝐴) = (𝐵 + 𝐴))
9	8	ancoms 458	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 𝐴) = (𝐵 + 𝐴))
10	6, 7, 9	3eqtr4d 2782	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
11		oveq2 7376	. . . . . . 7 ⊢ (𝐵 = +∞ → (𝐴 +_𝑒 𝐵) = (𝐴 +_𝑒 +∞))
12		rexr 11190	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
13		renemnf 11193	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
14		xaddpnf1 13153	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞) → (𝐴 +_𝑒 +∞) = +∞)
15	12, 13, 14	syl2anc 585	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (𝐴 +_𝑒 +∞) = +∞)
16	11, 15	sylan9eqr 2794	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 +_𝑒 𝐵) = +∞)
17		oveq1 7375	. . . . . . 7 ⊢ (𝐵 = +∞ → (𝐵 +_𝑒 𝐴) = (+∞ +_𝑒 𝐴))
18		xaddpnf2 13154	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞) → (+∞ +_𝑒 𝐴) = +∞)
19	12, 13, 18	syl2anc 585	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (+∞ +_𝑒 𝐴) = +∞)
20	17, 19	sylan9eqr 2794	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 𝐴) = +∞)
21	16, 20	eqtr4d 2775	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
22		oveq2 7376	. . . . . . 7 ⊢ (𝐵 = -∞ → (𝐴 +_𝑒 𝐵) = (𝐴 +_𝑒 -∞))
23		renepnf 11192	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
24		xaddmnf1 13155	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ +∞) → (𝐴 +_𝑒 -∞) = -∞)
25	12, 23, 24	syl2anc 585	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (𝐴 +_𝑒 -∞) = -∞)
26	22, 25	sylan9eqr 2794	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 +_𝑒 𝐵) = -∞)
27		oveq1 7375	. . . . . . 7 ⊢ (𝐵 = -∞ → (𝐵 +_𝑒 𝐴) = (-∞ +_𝑒 𝐴))
28		xaddmnf2 13156	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ +∞) → (-∞ +_𝑒 𝐴) = -∞)
29	12, 23, 28	syl2anc 585	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (-∞ +_𝑒 𝐴) = -∞)
30	27, 29	sylan9eqr 2794	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 𝐴) = -∞)
31	26, 30	eqtr4d 2775	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
32	10, 21, 31	3jaodan 1434	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
33	2, 32	sylan2b 595	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
34		pnfaddmnf 13157	. . . . . . . 8 ⊢ (+∞ +_𝑒 -∞) = 0
35		mnfaddpnf 13158	. . . . . . . 8 ⊢ (-∞ +_𝑒 +∞) = 0
36	34, 35	eqtr4i 2763	. . . . . . 7 ⊢ (+∞ +_𝑒 -∞) = (-∞ +_𝑒 +∞)
37		simpr 484	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = -∞) → 𝐵 = -∞)
38	37	oveq2d 7384	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = -∞) → (+∞ +_𝑒 𝐵) = (+∞ +_𝑒 -∞))
39	37	oveq1d 7383	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = -∞) → (𝐵 +_𝑒 +∞) = (-∞ +_𝑒 +∞))
40	36, 38, 39	3eqtr4a 2798	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = -∞) → (+∞ +_𝑒 𝐵) = (𝐵 +_𝑒 +∞))
41		xaddpnf2 13154	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (+∞ +_𝑒 𝐵) = +∞)
42		xaddpnf1 13153	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (𝐵 +_𝑒 +∞) = +∞)
43	41, 42	eqtr4d 2775	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (+∞ +_𝑒 𝐵) = (𝐵 +_𝑒 +∞))
44	40, 43	pm2.61dane 3020	. . . . 5 ⊢ (𝐵 ∈ ℝ^* → (+∞ +_𝑒 𝐵) = (𝐵 +_𝑒 +∞))
45	44	adantl 481	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (+∞ +_𝑒 𝐵) = (𝐵 +_𝑒 +∞))
46		simpl 482	. . . . 5 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → 𝐴 = +∞)
47	46	oveq1d 7383	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (+∞ +_𝑒 𝐵))
48	46	oveq2d 7384	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐵 +_𝑒 𝐴) = (𝐵 +_𝑒 +∞))
49	45, 47, 48	3eqtr4d 2782	. . 3 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
50	35, 34	eqtr4i 2763	. . . . . . 7 ⊢ (-∞ +_𝑒 +∞) = (+∞ +_𝑒 -∞)
51		simpr 484	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = +∞) → 𝐵 = +∞)
52	51	oveq2d 7384	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = +∞) → (-∞ +_𝑒 𝐵) = (-∞ +_𝑒 +∞))
53	51	oveq1d 7383	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -∞) = (+∞ +_𝑒 -∞))
54	50, 52, 53	3eqtr4a 2798	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = +∞) → (-∞ +_𝑒 𝐵) = (𝐵 +_𝑒 -∞))
55		xaddmnf2 13156	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (-∞ +_𝑒 𝐵) = -∞)
56		xaddmnf1 13155	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (𝐵 +_𝑒 -∞) = -∞)
57	55, 56	eqtr4d 2775	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (-∞ +_𝑒 𝐵) = (𝐵 +_𝑒 -∞))
58	54, 57	pm2.61dane 3020	. . . . 5 ⊢ (𝐵 ∈ ℝ^* → (-∞ +_𝑒 𝐵) = (𝐵 +_𝑒 -∞))
59	58	adantl 481	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (-∞ +_𝑒 𝐵) = (𝐵 +_𝑒 -∞))
60		simpl 482	. . . . 5 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → 𝐴 = -∞)
61	60	oveq1d 7383	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (-∞ +_𝑒 𝐵))
62	60	oveq2d 7384	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (𝐵 +_𝑒 𝐴) = (𝐵 +_𝑒 -∞))
63	59, 61, 62	3eqtr4d 2782	. . 3 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
64	33, 49, 63	3jaoian 1433	. 2 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
65	1, 64	sylanb 582	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ w3o 1086 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 (class class class)co 7368 ℂcc 11036 ℝcr 11037 0cc0 11038 + caddc 11041 +∞cpnf 11175 -∞cmnf 11176 ℝ^*cxr 11177 +_𝑒 cxad 13036

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5527 df-po 5540 df-so 5541 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-ov 7371 df-oprab 7372 df-mpo 7373 df-er 8645 df-en 8896 df-dom 8897 df-sdom 8898 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-xadd 13039

This theorem is referenced by: xaddlid 13169 xleadd2a 13181 xltadd2 13184 xposdif 13189 xadd4d 13230 hashunx 14321 xrsnsgrp 21374 xrs1cmn 21409 blcld 24461 xrsxmet 24766 metdstri 24808 vtxdginducedm1 29629 xaddeq0 32844 xlt2addrd 32850 xrge0npcan 33113 esumle 34236 esumlef 34240 measun 34389 difelcarsg 34488 xaddcomd 45683

W3C validator