Metamath Proof Explorer

Theorem xaddval

Description: Value of the extended real addition operation. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xaddval ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 +𝑒 𝐵 ) = if ( 𝐴 = +∞ , if ( 𝐵 = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( 𝐵 = +∞ , 0 , -∞ ) , if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑥 = 𝐴 )
2 1 eqeq1d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 = +∞ ↔ 𝐴 = +∞ ) )
3 simpr ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
4 3 eqeq1d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑦 = -∞ ↔ 𝐵 = -∞ ) )
5 4 ifbid ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → if ( 𝑦 = -∞ , 0 , +∞ ) = if ( 𝐵 = -∞ , 0 , +∞ ) )
6 1 eqeq1d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 = -∞ ↔ 𝐴 = -∞ ) )
7 3 eqeq1d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑦 = +∞ ↔ 𝐵 = +∞ ) )
8 7 ifbid ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → if ( 𝑦 = +∞ , 0 , -∞ ) = if ( 𝐵 = +∞ , 0 , -∞ ) )
9 oveq12 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 + 𝑦 ) = ( 𝐴 + 𝐵 ) )
10 4 9 ifbieq2d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) = if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) )
11 7 10 ifbieq2d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ) = if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) )
12 6 8 11 ifbieq12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → if ( 𝑥 = -∞ , if ( 𝑦 = +∞ , 0 , -∞ ) , if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ) ) = if ( 𝐴 = -∞ , if ( 𝐵 = +∞ , 0 , -∞ ) , if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) ) )
13 2 5 12 ifbieq12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → if ( 𝑥 = +∞ , if ( 𝑦 = -∞ , 0 , +∞ ) , if ( 𝑥 = -∞ , if ( 𝑦 = +∞ , 0 , -∞ ) , if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ) ) ) = if ( 𝐴 = +∞ , if ( 𝐵 = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( 𝐵 = +∞ , 0 , -∞ ) , if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) ) ) )
14 df-xadd ⊢ +𝑒 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 = +∞ , if ( 𝑦 = -∞ , 0 , +∞ ) , if ( 𝑥 = -∞ , if ( 𝑦 = +∞ , 0 , -∞ ) , if ( 𝑦 = +∞ , +∞ , if ( 𝑦 = -∞ , -∞ , ( 𝑥 + 𝑦 ) ) ) ) ) )
15 c0ex ⊢ 0 ∈ V
16 pnfex ⊢ +∞ ∈ V
17 15 16 ifex ⊢ if ( 𝐵 = -∞ , 0 , +∞ ) ∈ V
18 mnfxr ⊢ -∞ ∈ ℝ*
19 18 elexi ⊢ -∞ ∈ V
20 15 19 ifex ⊢ if ( 𝐵 = +∞ , 0 , -∞ ) ∈ V
21 ovex ⊢ ( 𝐴 + 𝐵 ) ∈ V
22 19 21 ifex ⊢ if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ∈ V
23 16 22 ifex ⊢ if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) ∈ V
24 20 23 ifex ⊢ if ( 𝐴 = -∞ , if ( 𝐵 = +∞ , 0 , -∞ ) , if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) ) ∈ V
25 17 24 ifex ⊢ if ( 𝐴 = +∞ , if ( 𝐵 = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( 𝐵 = +∞ , 0 , -∞ ) , if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) ) ) ∈ V
26 13 14 25 ovmpoa ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 +𝑒 𝐵 ) = if ( 𝐴 = +∞ , if ( 𝐵 = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( 𝐵 = +∞ , 0 , -∞ ) , if ( 𝐵 = +∞ , +∞ , if ( 𝐵 = -∞ , -∞ , ( 𝐴 + 𝐵 ) ) ) ) ) )