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 ⊢ if ( 𝑦 = -∞ , 0 , +∞ ) ∈ ℝ*
4 3 a1i ⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 = +∞ ) → if ( 𝑦 = -∞ , 0 , +∞ ) ∈ ℝ* )
5 mnfxr ⊢ -∞ ∈ ℝ*
6 1 5 ifcli ⊢ if ( 𝑦 = +∞ , 0 , -∞ ) ∈ ℝ*
7 6 a1i ⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ¬ 𝑥 = +∞ ) ∧ 𝑥 = -∞ ) → if ( 𝑦 = +∞ , 0 , -∞ ) ∈ ℝ* )
8 2 a1i ⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ ( ¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞ ) ) ∧ 𝑦 ∈ ℝ* ) ∧ 𝑦 = +∞ ) → +∞ ∈ ℝ* )
9 5 a1i ⊢ ( ( ( ( ( 𝑥 ∈ ℝ* ∧ ( ¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞ ) ) ∧ 𝑦 ∈ ℝ* ) ∧ ¬ 𝑦 = +∞ ) ∧ 𝑦 = -∞ ) → -∞ ∈ ℝ* )
10 ioran ⊢ ( ¬ ( 𝑥 = +∞ ∨ 𝑥 = -∞ ) ↔ ( ¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞ ) )
11 elxr ⊢ ( 𝑥 ∈ ℝ* ↔ ( 𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞ ) )
12 3orass ⊢ ( ( 𝑥 ∈ ℝ ∨ 𝑥 = +∞ ∨ 𝑥 = -∞ ) ↔ ( 𝑥 ∈ ℝ ∨ ( 𝑥 = +∞ ∨ 𝑥 = -∞ ) ) )
13 11 12 sylbb ⊢ ( 𝑥 ∈ ℝ* → ( 𝑥 ∈ ℝ ∨ ( 𝑥 = +∞ ∨ 𝑥 = -∞ ) ) )
14 13 ord ⊢ ( 𝑥 ∈ ℝ* → ( ¬ 𝑥 ∈ ℝ → ( 𝑥 = +∞ ∨ 𝑥 = -∞ ) ) )
15 14 con1d ⊢ ( 𝑥 ∈ ℝ* → ( ¬ ( 𝑥 = +∞ ∨ 𝑥 = -∞ ) → 𝑥 ∈ ℝ ) )
16 15 imp ⊢ ( ( 𝑥 ∈ ℝ* ∧ ¬ ( 𝑥 = +∞ ∨ 𝑥 = -∞ ) ) → 𝑥 ∈ ℝ )
17 10 16 sylan2br ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( ¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞ ) ) → 𝑥 ∈ ℝ )
18 ioran ⊢ ( ¬ ( 𝑦 = +∞ ∨ 𝑦 = -∞ ) ↔ ( ¬ 𝑦 = +∞ ∧ ¬ 𝑦 = -∞ ) )
19 elxr ⊢ ( 𝑦 ∈ ℝ* ↔ ( 𝑦 ∈ ℝ ∨ 𝑦 = +∞ ∨ 𝑦 = -∞ ) )
20 3orass ⊢ ( ( 𝑦 ∈ ℝ ∨ 𝑦 = +∞ ∨ 𝑦 = -∞ ) ↔ ( 𝑦 ∈ ℝ ∨ ( 𝑦 = +∞ ∨ 𝑦 = -∞ ) ) )
21 19 20 sylbb ⊢ ( 𝑦 ∈ ℝ* → ( 𝑦 ∈ ℝ ∨ ( 𝑦 = +∞ ∨ 𝑦 = -∞ ) ) )
22 21 ord ⊢ ( 𝑦 ∈ ℝ* → ( ¬ 𝑦 ∈ ℝ → ( 𝑦 = +∞ ∨ 𝑦 = -∞ ) ) )
23 22 con1d ⊢ ( 𝑦 ∈ ℝ* → ( ¬ ( 𝑦 = +∞ ∨ 𝑦 = -∞ ) → 𝑦 ∈ ℝ ) )
24 23 imp ⊢ ( ( 𝑦 ∈ ℝ* ∧ ¬ ( 𝑦 = +∞ ∨ 𝑦 = -∞ ) ) → 𝑦 ∈ ℝ )
25 18 24 sylan2br ⊢ ( ( 𝑦 ∈ ℝ* ∧ ( ¬ 𝑦 = +∞ ∧ ¬ 𝑦 = -∞ ) ) → 𝑦 ∈ ℝ )
26 readdcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
27 17 25 26 syl2an ⊢ ( ( ( 𝑥 ∈ ℝ* ∧ ( ¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞ ) ) ∧ ( 𝑦 ∈ ℝ* ∧ ( ¬ 𝑦 = +∞ ∧ ¬ 𝑦 = -∞ ) ) ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
28 27 rexrd ⊢ ( ( ( 𝑥 ∈ ℝ* ∧ ( ¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞ ) ) ∧ ( 𝑦 ∈ ℝ* ∧ ( ¬ 𝑦 = +∞ ∧ ¬ 𝑦 = -∞ ) ) ) → ( 𝑥 + 𝑦 ) ∈ ℝ* )
29 28 anassrs ⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ ( ¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞ ) ) ∧ 𝑦 ∈ ℝ* ) ∧ ( ¬ 𝑦 = +∞ ∧ ¬ 𝑦 = -∞ ) ) → ( 𝑥 + 𝑦 ) ∈ ℝ* )
30 29 anassrs ⊢ ( ( ( ( ( 𝑥 ∈ ℝ* ∧ ( ¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞ ) ) ∧ 𝑦 ∈ ℝ* ) ∧ ¬ 𝑦 = +∞ ) ∧ ¬ 𝑦 = -∞ ) → ( 𝑥 + 𝑦 ) ∈ ℝ* )
31 9 30 ifclda ⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ ( ¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞ ) ) ∧ 𝑦 ∈ ℝ* ) ∧ ¬ 𝑦 = +∞ ) → if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ∈ ℝ* )
32 8 31 ifclda ⊢ ( ( ( 𝑥 ∈ ℝ* ∧ ( ¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞ ) ) ∧ 𝑦 ∈ ℝ* ) → if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ) ∈ ℝ* )
33 32 an32s ⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( ¬ 𝑥 = +∞ ∧ ¬ 𝑥 = -∞ ) ) → if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ) ∈ ℝ* )
34 33 anassrs ⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ¬ 𝑥 = +∞ ) ∧ ¬ 𝑥 = -∞ ) → if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ) ∈ ℝ* )
35 7 34 ifclda ⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ¬ 𝑥 = +∞ ) → if ( 𝑥 = -∞ , if ( 𝑦 = +∞ , 0 , -∞ ) , if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ) ) ∈ ℝ* )
36 4 35 ifclda ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → if ( 𝑥 = +∞ , if ( 𝑦 = -∞ , 0 , +∞ ) , if ( 𝑥 = -∞ , if ( 𝑦 = +∞ , 0 , -∞ ) , if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ) ) ) ∈ ℝ* )
37 36 rgen2 ⊢ ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* if ( 𝑥 = +∞ , if ( 𝑦 = -∞ , 0 , +∞ ) , if ( 𝑥 = -∞ , if ( 𝑦 = +∞ , 0 , -∞ ) , if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ) ) ) ∈ ℝ*
38 df-xadd ⊢ +𝑒 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 = +∞ , if ( 𝑦 = -∞ , 0 , +∞ ) , if ( 𝑥 = -∞ , if ( 𝑦 = +∞ , 0 , -∞ ) , if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ) ) ) )
39 38 fmpo ⊢ ( ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* if ( 𝑥 = +∞ , if ( 𝑦 = -∞ , 0 , +∞ ) , if ( 𝑥 = -∞ , if ( 𝑦 = +∞ , 0 , -∞ ) , if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ) ) ) ∈ ℝ* ↔ +𝑒 : ( ℝ* × ℝ* ) ⟶ ℝ* )
40 37 39 mpbi ⊢ +𝑒 : ( ℝ* × ℝ* ) ⟶ ℝ*