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 13161

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

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

**Proof of Theorem xaddrid**
Step	Hyp	Ref	Expression
1		elxr 13036	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		0re 11136	. . . . 5 ⊢ 0 ∈ ℝ
3		rexadd 13152	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐴 +_𝑒 0) = (𝐴 + 0))
4	2, 3	mpan2 691	. . . 4 ⊢ (𝐴 ∈ ℝ → (𝐴 +_𝑒 0) = (𝐴 + 0))
5		recn 11118	. . . . 5 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
6	5	addridd 11334	. . . 4 ⊢ (𝐴 ∈ ℝ → (𝐴 + 0) = 𝐴)
7	4, 6	eqtrd 2764	. . 3 ⊢ (𝐴 ∈ ℝ → (𝐴 +_𝑒 0) = 𝐴)
8		0xr 11181	. . . . 5 ⊢ 0 ∈ ℝ^*
9		renemnf 11183	. . . . . 6 ⊢ (0 ∈ ℝ → 0 ≠ -∞)
10	2, 9	ax-mp 5	. . . . 5 ⊢ 0 ≠ -∞
11		xaddpnf2 13147	. . . . 5 ⊢ ((0 ∈ ℝ^* ∧ 0 ≠ -∞) → (+∞ +_𝑒 0) = +∞)
12	8, 10, 11	mp2an 692	. . . 4 ⊢ (+∞ +_𝑒 0) = +∞
13		oveq1 7360	. . . 4 ⊢ (𝐴 = +∞ → (𝐴 +_𝑒 0) = (+∞ +_𝑒 0))
14		id 22	. . . 4 ⊢ (𝐴 = +∞ → 𝐴 = +∞)
15	12, 13, 14	3eqtr4a 2790	. . 3 ⊢ (𝐴 = +∞ → (𝐴 +_𝑒 0) = 𝐴)
16		renepnf 11182	. . . . . 6 ⊢ (0 ∈ ℝ → 0 ≠ +∞)
17	2, 16	ax-mp 5	. . . . 5 ⊢ 0 ≠ +∞
18		xaddmnf2 13149	. . . . 5 ⊢ ((0 ∈ ℝ^* ∧ 0 ≠ +∞) → (-∞ +_𝑒 0) = -∞)
19	8, 17, 18	mp2an 692	. . . 4 ⊢ (-∞ +_𝑒 0) = -∞
20		oveq1 7360	. . . 4 ⊢ (𝐴 = -∞ → (𝐴 +_𝑒 0) = (-∞ +_𝑒 0))
21		id 22	. . . 4 ⊢ (𝐴 = -∞ → 𝐴 = -∞)
22	19, 20, 21	3eqtr4a 2790	. . 3 ⊢ (𝐴 = -∞ → (𝐴 +_𝑒 0) = 𝐴)
23	7, 15, 22	3jaoi 1430	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐴 +_𝑒 0) = 𝐴)
24	1, 23	sylbi 217	1 ⊢ (𝐴 ∈ ℝ^* → (𝐴 +_𝑒 0) = 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∨ w3o 1085 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 (class class class)co 7353 ℝcr 11027 0cc0 11028 + caddc 11031 +∞cpnf 11165 -∞cmnf 11166 ℝ^*cxr 11167 +_𝑒 cxad 13030

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5518 df-po 5531 df-so 5532 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-ov 7356 df-oprab 7357 df-mpo 7358 df-er 8632 df-en 8880 df-dom 8881 df-sdom 8882 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-xadd 13033

This theorem is referenced by: xaddlid 13162 xaddridd 13163 xnn0xadd0 13167 xpncan 13171 xadddi 13215 xrsnsgrp 21332 imasdsf1olem 24277 vtxdlfgrval 29449 vtxdginducedm1 29507 xraddge02 32713 xlt2addrd 32715 xrs0 32973 xrge0addgt0 32984 xrge0npcan 32987 metideq 33862 metider 33863 esumpad 34024 esumpr2 34036 esumpfinvallem 34043 esumpmono 34048 ddemeas 34205 aean 34213 baselcarsg 34276 carsgclctunlem2 34289 xadd0ge 45304 sge0tsms 46365 sge0ss 46397

W3C validator