Step |
Hyp |
Ref |
Expression |
1 |
|
mnfxr |
⊢ -∞ ∈ ℝ* |
2 |
|
xaddval |
⊢ ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( -∞ +𝑒 𝐴 ) = if ( -∞ = +∞ , if ( 𝐴 = -∞ , 0 , +∞ ) , if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) ) ) ) |
3 |
1 2
|
mpan |
⊢ ( 𝐴 ∈ ℝ* → ( -∞ +𝑒 𝐴 ) = if ( -∞ = +∞ , if ( 𝐴 = -∞ , 0 , +∞ ) , if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) ) ) ) |
4 |
|
mnfnepnf |
⊢ -∞ ≠ +∞ |
5 |
|
ifnefalse |
⊢ ( -∞ ≠ +∞ → if ( -∞ = +∞ , if ( 𝐴 = -∞ , 0 , +∞ ) , if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) ) ) = if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) ) ) |
6 |
4 5
|
ax-mp |
⊢ if ( -∞ = +∞ , if ( 𝐴 = -∞ , 0 , +∞ ) , if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) ) ) = if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) ) |
7 |
|
eqid |
⊢ -∞ = -∞ |
8 |
7
|
iftruei |
⊢ if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) ) = if ( 𝐴 = +∞ , 0 , -∞ ) |
9 |
6 8
|
eqtri |
⊢ if ( -∞ = +∞ , if ( 𝐴 = -∞ , 0 , +∞ ) , if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) ) ) = if ( 𝐴 = +∞ , 0 , -∞ ) |
10 |
|
ifnefalse |
⊢ ( 𝐴 ≠ +∞ → if ( 𝐴 = +∞ , 0 , -∞ ) = -∞ ) |
11 |
9 10
|
eqtrid |
⊢ ( 𝐴 ≠ +∞ → if ( -∞ = +∞ , if ( 𝐴 = -∞ , 0 , +∞ ) , if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) ) ) = -∞ ) |
12 |
3 11
|
sylan9eq |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) → ( -∞ +𝑒 𝐴 ) = -∞ ) |