Metamath Proof Explorer

Theorem xaddf

Description: The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion xaddf ⊢+𝑒:ℝ*×ℝ*⟶ℝ*

Proof

Step Hyp Ref Expression
1 0xr ⊢0∈ℝ*
2 pnfxr ⊢+∞∈ℝ*
3 1 2 ifcli ⊢ify=−∞0+∞∈ℝ*
4 3 a1i ⊢x∈ℝ*∧y∈ℝ*∧x=+∞→ify=−∞0+∞∈ℝ*
5 mnfxr ⊢−∞∈ℝ*
6 1 5 ifcli ⊢ify=+∞0−∞∈ℝ*
7 6 a1i ⊢x∈ℝ*∧y∈ℝ*∧¬x=+∞∧x=−∞→ify=+∞0−∞∈ℝ*
8 2 a1i ⊢x∈ℝ*∧¬x=+∞∧¬x=−∞∧y∈ℝ*∧y=+∞→+∞∈ℝ*
9 5 a1i ⊢x∈ℝ*∧¬x=+∞∧¬x=−∞∧y∈ℝ*∧¬y=+∞∧y=−∞→−∞∈ℝ*
10 ioran ⊢¬x=+∞∨x=−∞↔¬x=+∞∧¬x=−∞
11 elxr ⊢x∈ℝ*↔x∈ℝ∨x=+∞∨x=−∞
12 3orass ⊢x∈ℝ∨x=+∞∨x=−∞↔x∈ℝ∨x=+∞∨x=−∞
13 11 12 sylbb ⊢x∈ℝ*→x∈ℝ∨x=+∞∨x=−∞
14 13 ord ⊢x∈ℝ*→¬x∈ℝ→x=+∞∨x=−∞
15 14 con1d ⊢x∈ℝ*→¬x=+∞∨x=−∞→x∈ℝ
16 15 imp ⊢x∈ℝ*∧¬x=+∞∨x=−∞→x∈ℝ
17 10 16 sylan2br ⊢x∈ℝ*∧¬x=+∞∧¬x=−∞→x∈ℝ
18 ioran ⊢¬y=+∞∨y=−∞↔¬y=+∞∧¬y=−∞
19 elxr ⊢y∈ℝ*↔y∈ℝ∨y=+∞∨y=−∞
20 3orass ⊢y∈ℝ∨y=+∞∨y=−∞↔y∈ℝ∨y=+∞∨y=−∞
21 19 20 sylbb ⊢y∈ℝ*→y∈ℝ∨y=+∞∨y=−∞
22 21 ord ⊢y∈ℝ*→¬y∈ℝ→y=+∞∨y=−∞
23 22 con1d ⊢y∈ℝ*→¬y=+∞∨y=−∞→y∈ℝ
24 23 imp ⊢y∈ℝ*∧¬y=+∞∨y=−∞→y∈ℝ
25 18 24 sylan2br ⊢y∈ℝ*∧¬y=+∞∧¬y=−∞→y∈ℝ
26 readdcl ⊢x∈ℝ∧y∈ℝ→x+y∈ℝ
27 17 25 26 syl2an ⊢x∈ℝ*∧¬x=+∞∧¬x=−∞∧y∈ℝ*∧¬y=+∞∧¬y=−∞→x+y∈ℝ
28 27 rexrd ⊢x∈ℝ*∧¬x=+∞∧¬x=−∞∧y∈ℝ*∧¬y=+∞∧¬y=−∞→x+y∈ℝ*
29 28 anassrs ⊢x∈ℝ*∧¬x=+∞∧¬x=−∞∧y∈ℝ*∧¬y=+∞∧¬y=−∞→x+y∈ℝ*
30 29 anassrs ⊢x∈ℝ*∧¬x=+∞∧¬x=−∞∧y∈ℝ*∧¬y=+∞∧¬y=−∞→x+y∈ℝ*
31 9 30 ifclda ⊢x∈ℝ*∧¬x=+∞∧¬x=−∞∧y∈ℝ*∧¬y=+∞→ify=−∞−∞x+y∈ℝ*
32 8 31 ifclda ⊢x∈ℝ*∧¬x=+∞∧¬x=−∞∧y∈ℝ*→ify=+∞+∞ify=−∞−∞x+y∈ℝ*
33 32 an32s ⊢x∈ℝ*∧y∈ℝ*∧¬x=+∞∧¬x=−∞→ify=+∞+∞ify=−∞−∞x+y∈ℝ*
34 33 anassrs ⊢x∈ℝ*∧y∈ℝ*∧¬x=+∞∧¬x=−∞→ify=+∞+∞ify=−∞−∞x+y∈ℝ*
35 7 34 ifclda ⊢x∈ℝ*∧y∈ℝ*∧¬x=+∞→ifx=−∞ify=+∞0−∞ify=+∞+∞ify=−∞−∞x+y∈ℝ*
36 4 35 ifclda ⊢x∈ℝ*∧y∈ℝ*→ifx=+∞ify=−∞0+∞ifx=−∞ify=+∞0−∞ify=+∞+∞ify=−∞−∞x+y∈ℝ*
37 36 rgen2 ⊢∀x∈ℝ*∀y∈ℝ*ifx=+∞ify=−∞0+∞ifx=−∞ify=+∞0−∞ify=+∞+∞ify=−∞−∞x+y∈ℝ*
38 df-xadd ⊢+𝑒=x∈ℝ*,y∈ℝ*⟼ifx=+∞ify=−∞0+∞ifx=−∞ify=+∞0−∞ify=+∞+∞ify=−∞−∞x+y
39 38 fmpo ⊢∀x∈ℝ*∀y∈ℝ*ifx=+∞ify=−∞0+∞ifx=−∞ify=+∞0−∞ify=+∞+∞ify=−∞−∞x+y∈ℝ*↔+𝑒:ℝ*×ℝ*⟶ℝ*
40 37 39 mpbi ⊢+𝑒:ℝ*×ℝ*⟶ℝ*