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 13140

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

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

**Proof of Theorem xaddrid**
Step	Hyp	Ref	Expression
1		elxr 13015	. 2 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2		0re 11114	. . . . 5 ⊢ 0 ∈ ℝ
3		rexadd 13131	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐴 +_𝑒 0) = (𝐴 + 0))
4	2, 3	mpan2 691	. . . 4 ⊢ (𝐴 ∈ ℝ → (𝐴 +_𝑒 0) = (𝐴 + 0))
5		recn 11096	. . . . 5 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
6	5	addridd 11313	. . . 4 ⊢ (𝐴 ∈ ℝ → (𝐴 + 0) = 𝐴)
7	4, 6	eqtrd 2766	. . 3 ⊢ (𝐴 ∈ ℝ → (𝐴 +_𝑒 0) = 𝐴)
8		0xr 11159	. . . . 5 ⊢ 0 ∈ ℝ^*
9		renemnf 11161	. . . . . 6 ⊢ (0 ∈ ℝ → 0 ≠ -∞)
10	2, 9	ax-mp 5	. . . . 5 ⊢ 0 ≠ -∞
11		xaddpnf2 13126	. . . . 5 ⊢ ((0 ∈ ℝ^* ∧ 0 ≠ -∞) → (+∞ +_𝑒 0) = +∞)
12	8, 10, 11	mp2an 692	. . . 4 ⊢ (+∞ +_𝑒 0) = +∞
13		oveq1 7353	. . . 4 ⊢ (𝐴 = +∞ → (𝐴 +_𝑒 0) = (+∞ +_𝑒 0))
14		id 22	. . . 4 ⊢ (𝐴 = +∞ → 𝐴 = +∞)
15	12, 13, 14	3eqtr4a 2792	. . 3 ⊢ (𝐴 = +∞ → (𝐴 +_𝑒 0) = 𝐴)
16		renepnf 11160	. . . . . 6 ⊢ (0 ∈ ℝ → 0 ≠ +∞)
17	2, 16	ax-mp 5	. . . . 5 ⊢ 0 ≠ +∞
18		xaddmnf2 13128	. . . . 5 ⊢ ((0 ∈ ℝ^* ∧ 0 ≠ +∞) → (-∞ +_𝑒 0) = -∞)
19	8, 17, 18	mp2an 692	. . . 4 ⊢ (-∞ +_𝑒 0) = -∞
20		oveq1 7353	. . . 4 ⊢ (𝐴 = -∞ → (𝐴 +_𝑒 0) = (-∞ +_𝑒 0))
21		id 22	. . . 4 ⊢ (𝐴 = -∞ → 𝐴 = -∞)
22	19, 20, 21	3eqtr4a 2792	. . 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 1541 ∈ wcel 2111 ≠ wne 2928 (class class class)co 7346 ℝcr 11005 0cc0 11006 + caddc 11009 +∞cpnf 11143 -∞cmnf 11144 ℝ^*cxr 11145 +_𝑒 cxad 13009

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-br 5092 df-opab 5154 df-mpt 5173 df-id 5511 df-po 5524 df-so 5525 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-ov 7349 df-oprab 7350 df-mpo 7351 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-xadd 13012

This theorem is referenced by: xaddlid 13141 xaddridd 13142 xnn0xadd0 13146 xpncan 13150 xadddi 13194 xrsnsgrp 21345 imasdsf1olem 24289 vtxdlfgrval 29465 vtxdginducedm1 29523 xraddge02 32738 xlt2addrd 32740 xrs0 32985 xrge0addgt0 32996 xrge0npcan 32999 metideq 33904 metider 33905 esumpad 34066 esumpr2 34078 esumpfinvallem 34085 esumpmono 34090 ddemeas 34247 aean 34255 baselcarsg 34317 carsgclctunlem2 34330 xadd0ge 45366 sge0tsms 46424 sge0ss 46456

W3C validator