xaddrid - Metamath Proof Explorer

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

Theorem xaddrid 13364

Description: Extended real version of addrid 11483. (Contributed by Mario Carneiro, 20-Aug-2015.)

**Assertion**
Ref	Expression
xaddrid	⊢ (𝐴 ∈ ℝ^* → (𝐴 +_𝑒 0) = 𝐴)

**Proof of Theorem xaddrid**
Step	Hyp	Ref	Expression
1		elxr 13238	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		0re 11303	. . . . 5 ⊢ 0 ∈ ℝ
3		rexadd 13355	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐴 +_𝑒 0) = (𝐴 + 0))
4	2, 3	mpan2 704	. . . 4 ⊢ (𝐴 ∈ ℝ → (𝐴 +_𝑒 0) = (𝐴 + 0))
5		recn 11283	. . . . 5 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
6	5	addridd 11503	. . . 4 ⊢ (𝐴 ∈ ℝ → (𝐴 + 0) = 𝐴)
7	4, 6	eqtrd 2796	. . 3 ⊢ (𝐴 ∈ ℝ → (𝐴 +_𝑒 0) = 𝐴)
8		0xr 11349	. . . . 5 ⊢ 0 ∈ ℝ^*
9		renemnf 11351	. . . . . 6 ⊢ (0 ∈ ℝ → 0 ≠ -∞)
10	2, 9	ax-mp 5	. . . . 5 ⊢ 0 ≠ -∞
11		xaddpnf2 13350	. . . . 5 ⊢ ((0 ∈ ℝ^* ∧ 0 ≠ -∞) → (+∞ +_𝑒 0) = +∞)
12	8, 10, 11	mp2an 705	. . . 4 ⊢ (+∞ +_𝑒 0) = +∞
13		oveq1 7425	. . . 4 ⊢ (𝐴 = +∞ → (𝐴 +_𝑒 0) = (+∞ +_𝑒 0))
14		id 23	. . . 4 ⊢ (𝐴 = +∞ → 𝐴 = +∞)
15	12, 13, 14	3eqtr4a 2822	. . 3 ⊢ (𝐴 = +∞ → (𝐴 +_𝑒 0) = 𝐴)
16		renepnf 11350	. . . . . 6 ⊢ (0 ∈ ℝ → 0 ≠ +∞)
17	2, 16	ax-mp 5	. . . . 5 ⊢ 0 ≠ +∞
18		xaddmnf2 13352	. . . . 5 ⊢ ((0 ∈ ℝ^* ∧ 0 ≠ +∞) → (-∞ +_𝑒 0) = -∞)
19	8, 17, 18	mp2an 705	. . . 4 ⊢ (-∞ +_𝑒 0) = -∞
20		oveq1 7425	. . . 4 ⊢ (𝐴 = -∞ → (𝐴 +_𝑒 0) = (-∞ +_𝑒 0))
21		id 23	. . . 4 ⊢ (𝐴 = -∞ → 𝐴 = -∞)
22	19, 20, 21	3eqtr4a 2822	. . 3 ⊢ (𝐴 = -∞ → (𝐴 +_𝑒 0) = 𝐴)
23	7, 15, 22	3jaoi 1454	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐴 +_𝑒 0) = 𝐴)
24	1, 23	sylbi 220	1 ⊢ (𝐴 ∈ ℝ^* → (𝐴 +_𝑒 0) = 𝐴)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∨ w3o 1102 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 (class class class)co 7418 ℝcr 11192 0cc0 11193 + caddc 11196 +∞cpnf 11333 -∞cmnf 11334 ℝ^*cxr 11335 +_𝑒 cxad 13232

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 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269

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 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5546 df-po 5559 df-so 5560 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-ov 7421 df-oprab 7422 df-mpo 7423 df-er 8710 df-en 8967 df-dom 8968 df-sdom 8969 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-xadd 13235

This theorem is used by: xaddlid 13365 xaddridd 13366 xnn0xadd0 13370 xpncan 13374 xadddi 13418 xrsnsgrp 21707 imasdsf1olem 24685 vtxdlfgrval 30059 vtxdginducedm1 30117 xraddge02 33342 xlt2addrd 33344 xrs0 33560 xrge0addgt0 33571 xrge0npcan 33574 metideq 34518 metider 34519 esumpad 34680 esumpr2 34692 esumpfinvallem 34699 esumpmono 34704 ddemeas 34862 aean 34870 baselcarsg 34931 carsgclctunlem2 34944 xadd0ge 46303 sge0tsms 47359 sge0ss 47391

W3C validator