Step |
Hyp |
Ref |
Expression |
1 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
2 |
|
mnfxr |
⊢ -∞ ∈ ℝ* |
3 |
|
xaddval |
⊢ ( ( +∞ ∈ ℝ* ∧ -∞ ∈ ℝ* ) → ( +∞ +𝑒 -∞ ) = if ( +∞ = +∞ , if ( -∞ = -∞ , 0 , +∞ ) , if ( +∞ = -∞ , if ( -∞ = +∞ , 0 , -∞ ) , if ( -∞ = +∞ , +∞ , if ( -∞ = -∞ , -∞ , ( +∞ + -∞ ) ) ) ) ) ) |
4 |
1 2 3
|
mp2an |
⊢ ( +∞ +𝑒 -∞ ) = if ( +∞ = +∞ , if ( -∞ = -∞ , 0 , +∞ ) , if ( +∞ = -∞ , if ( -∞ = +∞ , 0 , -∞ ) , if ( -∞ = +∞ , +∞ , if ( -∞ = -∞ , -∞ , ( +∞ + -∞ ) ) ) ) ) |
5 |
|
eqid |
⊢ +∞ = +∞ |
6 |
5
|
iftruei |
⊢ if ( +∞ = +∞ , if ( -∞ = -∞ , 0 , +∞ ) , if ( +∞ = -∞ , if ( -∞ = +∞ , 0 , -∞ ) , if ( -∞ = +∞ , +∞ , if ( -∞ = -∞ , -∞ , ( +∞ + -∞ ) ) ) ) ) = if ( -∞ = -∞ , 0 , +∞ ) |
7 |
|
eqid |
⊢ -∞ = -∞ |
8 |
7
|
iftruei |
⊢ if ( -∞ = -∞ , 0 , +∞ ) = 0 |
9 |
4 6 8
|
3eqtri |
⊢ ( +∞ +𝑒 -∞ ) = 0 |