Metamath Proof Explorer

Definition df-xadd

Description: Define addition over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion df-xadd +𝑒 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 = +∞ , if ( 𝑦 = -∞ , 0 , +∞ ) , if ( 𝑥 = -∞ , if ( 𝑦 = +∞ , 0 , -∞ ) , if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxad ⊢ +𝑒
1 vx ⊢ 𝑥
2 cxr ⊢ ℝ*
3 vy ⊢ 𝑦
4 1 cv ⊢ 𝑥
5 cpnf ⊢ +∞
6 4 5 wceq ⊢ 𝑥 = +∞
7 3 cv ⊢ 𝑦
8 cmnf ⊢ -∞
9 7 8 wceq ⊢ 𝑦 = -∞
10 cc0 ⊢ 0
11 9 10 5 cif ⊢ if ( 𝑦 = -∞ , 0 , +∞ )
12 4 8 wceq ⊢ 𝑥 = -∞
13 7 5 wceq ⊢ 𝑦 = +∞
14 13 10 8 cif ⊢ if ( 𝑦 = +∞ , 0 , -∞ )
15 caddc ⊢ +
16 4 7 15 co ⊢ ( 𝑥 + 𝑦 )
17 9 8 16 cif ⊢ if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) )
18 13 5 17 cif ⊢ if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) )
19 12 14 18 cif ⊢ if ( 𝑥 = -∞ , if ( 𝑦 = +∞ , 0 , -∞ ) , if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ) )
20 6 11 19 cif ⊢ if ( 𝑥 = +∞ , if ( 𝑦 = -∞ , 0 , +∞ ) , if ( 𝑥 = -∞ , if ( 𝑦 = +∞ , 0 , -∞ ) , if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ) ) )
21 1 3 2 2 20 cmpo ⊢ ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 = +∞ , if ( 𝑦 = -∞ , 0 , +∞ ) , if ( 𝑥 = -∞ , if ( 𝑦 = +∞ , 0 , -∞ ) , if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ) ) ) )
22 0 21 wceq ⊢ +𝑒 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 = +∞ , if ( 𝑦 = -∞ , 0 , +∞ ) , if ( 𝑥 = -∞ , if ( 𝑦 = +∞ , 0 , -∞ ) , if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ) ) ) )