xaddcom - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > xaddcom		GIF version

Theorem xaddcom 10095

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 10010	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		elxr 10010	. . . 4 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
3		recn 8164	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
4		recn 8164	. . . . . . 7 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
5		addcom 8315	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
6	3, 4, 5	syl2an 289	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
7		rexadd 10086	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +_𝑒 𝐵) = (𝐴 + 𝐵))
8		rexadd 10086	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 +_𝑒 𝐴) = (𝐵 + 𝐴))
9	8	ancoms 268	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 𝐴) = (𝐵 + 𝐴))
10	6, 7, 9	3eqtr4d 2274	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
11		oveq2 6025	. . . . . . 7 ⊢ (𝐵 = +∞ → (𝐴 +_𝑒 𝐵) = (𝐴 +_𝑒 +∞))
12		rexr 8224	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
13		renemnf 8227	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
14		xaddpnf1 10080	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞) → (𝐴 +_𝑒 +∞) = +∞)
15	12, 13, 14	syl2anc 411	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (𝐴 +_𝑒 +∞) = +∞)
16	11, 15	sylan9eqr 2286	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 +_𝑒 𝐵) = +∞)
17		oveq1 6024	. . . . . . 7 ⊢ (𝐵 = +∞ → (𝐵 +_𝑒 𝐴) = (+∞ +_𝑒 𝐴))
18		xaddpnf2 10081	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ -∞) → (+∞ +_𝑒 𝐴) = +∞)
19	12, 13, 18	syl2anc 411	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (+∞ +_𝑒 𝐴) = +∞)
20	17, 19	sylan9eqr 2286	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 𝐴) = +∞)
21	16, 20	eqtr4d 2267	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
22		oveq2 6025	. . . . . . 7 ⊢ (𝐵 = -∞ → (𝐴 +_𝑒 𝐵) = (𝐴 +_𝑒 -∞))
23		renepnf 8226	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
24		xaddmnf1 10082	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ +∞) → (𝐴 +_𝑒 -∞) = -∞)
25	12, 23, 24	syl2anc 411	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (𝐴 +_𝑒 -∞) = -∞)
26	22, 25	sylan9eqr 2286	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 +_𝑒 𝐵) = -∞)
27		oveq1 6024	. . . . . . 7 ⊢ (𝐵 = -∞ → (𝐵 +_𝑒 𝐴) = (-∞ +_𝑒 𝐴))
28		xaddmnf2 10083	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐴 ≠ +∞) → (-∞ +_𝑒 𝐴) = -∞)
29	12, 23, 28	syl2anc 411	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (-∞ +_𝑒 𝐴) = -∞)
30	27, 29	sylan9eqr 2286	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 𝐴) = -∞)
31	26, 30	eqtr4d 2267	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
32	10, 21, 31	3jaodan 1342	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
33	2, 32	sylan2b 287	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
34		pnfaddmnf 10084	. . . . . . . 8 ⊢ (+∞ +_𝑒 -∞) = 0
35		mnfaddpnf 10085	. . . . . . . 8 ⊢ (-∞ +_𝑒 +∞) = 0
36	34, 35	eqtr4i 2255	. . . . . . 7 ⊢ (+∞ +_𝑒 -∞) = (-∞ +_𝑒 +∞)
37		simpr 110	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = -∞) → 𝐵 = -∞)
38	37	oveq2d 6033	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = -∞) → (+∞ +_𝑒 𝐵) = (+∞ +_𝑒 -∞))
39	37	oveq1d 6032	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = -∞) → (𝐵 +_𝑒 +∞) = (-∞ +_𝑒 +∞))
40	36, 38, 39	3eqtr4a 2290	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = -∞) → (+∞ +_𝑒 𝐵) = (𝐵 +_𝑒 +∞))
41		xaddpnf2 10081	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (+∞ +_𝑒 𝐵) = +∞)
42		xaddpnf1 10080	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (𝐵 +_𝑒 +∞) = +∞)
43	41, 42	eqtr4d 2267	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (+∞ +_𝑒 𝐵) = (𝐵 +_𝑒 +∞))
44		xrmnfdc 10077	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ^* → DECID 𝐵 = -∞)
45		exmiddc 843	. . . . . . . 8 ⊢ (DECID 𝐵 = -∞ → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
46	44, 45	syl 14	. . . . . . 7 ⊢ (𝐵 ∈ ℝ^* → (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
47		df-ne 2403	. . . . . . . 8 ⊢ (𝐵 ≠ -∞ ↔ ¬ 𝐵 = -∞)
48	47	orbi2i 769	. . . . . . 7 ⊢ ((𝐵 = -∞ ∨ 𝐵 ≠ -∞) ↔ (𝐵 = -∞ ∨ ¬ 𝐵 = -∞))
49	46, 48	sylibr 134	. . . . . 6 ⊢ (𝐵 ∈ ℝ^* → (𝐵 = -∞ ∨ 𝐵 ≠ -∞))
50	40, 43, 49	mpjaodan 805	. . . . 5 ⊢ (𝐵 ∈ ℝ^* → (+∞ +_𝑒 𝐵) = (𝐵 +_𝑒 +∞))
51	50	adantl 277	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (+∞ +_𝑒 𝐵) = (𝐵 +_𝑒 +∞))
52		simpl 109	. . . . 5 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → 𝐴 = +∞)
53	52	oveq1d 6032	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (+∞ +_𝑒 𝐵))
54	52	oveq2d 6033	. . . 4 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐵 +_𝑒 𝐴) = (𝐵 +_𝑒 +∞))
55	51, 53, 54	3eqtr4d 2274	. . 3 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
56	35, 34	eqtr4i 2255	. . . . . . 7 ⊢ (-∞ +_𝑒 +∞) = (+∞ +_𝑒 -∞)
57		simpr 110	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = +∞) → 𝐵 = +∞)
58	57	oveq2d 6033	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = +∞) → (-∞ +_𝑒 𝐵) = (-∞ +_𝑒 +∞))
59	57	oveq1d 6032	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -∞) = (+∞ +_𝑒 -∞))
60	56, 58, 59	3eqtr4a 2290	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 = +∞) → (-∞ +_𝑒 𝐵) = (𝐵 +_𝑒 -∞))
61		xaddmnf2 10083	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (-∞ +_𝑒 𝐵) = -∞)
62		xaddmnf1 10082	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (𝐵 +_𝑒 -∞) = -∞)
63	61, 62	eqtr4d 2267	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (-∞ +_𝑒 𝐵) = (𝐵 +_𝑒 -∞))
64		xrpnfdc 10076	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ^* → DECID 𝐵 = +∞)
65		exmiddc 843	. . . . . . . 8 ⊢ (DECID 𝐵 = +∞ → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
66	64, 65	syl 14	. . . . . . 7 ⊢ (𝐵 ∈ ℝ^* → (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
67		df-ne 2403	. . . . . . . 8 ⊢ (𝐵 ≠ +∞ ↔ ¬ 𝐵 = +∞)
68	67	orbi2i 769	. . . . . . 7 ⊢ ((𝐵 = +∞ ∨ 𝐵 ≠ +∞) ↔ (𝐵 = +∞ ∨ ¬ 𝐵 = +∞))
69	66, 68	sylibr 134	. . . . . 6 ⊢ (𝐵 ∈ ℝ^* → (𝐵 = +∞ ∨ 𝐵 ≠ +∞))
70	60, 63, 69	mpjaodan 805	. . . . 5 ⊢ (𝐵 ∈ ℝ^* → (-∞ +_𝑒 𝐵) = (𝐵 +_𝑒 -∞))
71	70	adantl 277	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (-∞ +_𝑒 𝐵) = (𝐵 +_𝑒 -∞))
72		simpl 109	. . . . 5 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → 𝐴 = -∞)
73	72	oveq1d 6032	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (-∞ +_𝑒 𝐵))
74	72	oveq2d 6033	. . . 4 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (𝐵 +_𝑒 𝐴) = (𝐵 +_𝑒 -∞))
75	71, 73, 74	3eqtr4d 2274	. . 3 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
76	33, 55, 75	3jaoian 1341	. 2 ⊢ (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))
77	1, 76	sylanb 284	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 +_𝑒 𝐵) = (𝐵 +_𝑒 𝐴))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ∨ wo 715 DECID wdc 841 ∨ w3o 1003 = wceq 1397 ∈ wcel 2202 ≠ wne 2402 (class class class)co 6017 ℂcc 8029 ℝcr 8030 0cc0 8031 + caddc 8034 +∞cpnf 8210 -∞cmnf 8211 ℝ^*cxr 8212 +_𝑒 cxad 10004

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-sep 4207 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-cnex 8122 ax-resscn 8123 ax-1re 8125 ax-addrcl 8128 ax-addcom 8131 ax-rnegex 8140

This theorem depends on definitions: df-bi 117 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-nel 2498 df-ral 2515 df-rex 2516 df-rab 2519 df-v 2804 df-sbc 3032 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-if 3606 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-br 4089 df-opab 4151 df-id 4390 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-iota 5286 df-fun 5328 df-fv 5334 df-ov 6020 df-oprab 6021 df-mpo 6022 df-pnf 8215 df-mnf 8216 df-xr 8217 df-xadd 10007

This theorem is referenced by: xaddid2 10097 xleadd2a 10108 xltadd2 10111 xadd4d 10119 xrmaxaddlem 11820

W3C validator