Step |
Hyp |
Ref |
Expression |
1 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
2 |
|
xmulval |
⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐴 ·e +∞ ) = if ( ( 𝐴 = 0 ∨ +∞ = 0 ) , 0 , if ( ( ( ( 0 < +∞ ∧ 𝐴 = +∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = +∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < +∞ ∧ 𝐴 = -∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = -∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = +∞ ) ) ) , -∞ , ( 𝐴 · +∞ ) ) ) ) ) |
3 |
1 2
|
mpan2 |
⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ·e +∞ ) = if ( ( 𝐴 = 0 ∨ +∞ = 0 ) , 0 , if ( ( ( ( 0 < +∞ ∧ 𝐴 = +∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = +∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < +∞ ∧ 𝐴 = -∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = -∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = +∞ ) ) ) , -∞ , ( 𝐴 · +∞ ) ) ) ) ) |
4 |
3
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 𝐴 ·e +∞ ) = if ( ( 𝐴 = 0 ∨ +∞ = 0 ) , 0 , if ( ( ( ( 0 < +∞ ∧ 𝐴 = +∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = +∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < +∞ ∧ 𝐴 = -∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = -∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = +∞ ) ) ) , -∞ , ( 𝐴 · +∞ ) ) ) ) ) |
5 |
|
0xr |
⊢ 0 ∈ ℝ* |
6 |
|
xrltne |
⊢ ( ( 0 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 ) |
7 |
5 6
|
mp3an1 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 ) |
8 |
|
0re |
⊢ 0 ∈ ℝ |
9 |
|
renepnf |
⊢ ( 0 ∈ ℝ → 0 ≠ +∞ ) |
10 |
8 9
|
ax-mp |
⊢ 0 ≠ +∞ |
11 |
10
|
necomi |
⊢ +∞ ≠ 0 |
12 |
|
neanior |
⊢ ( ( 𝐴 ≠ 0 ∧ +∞ ≠ 0 ) ↔ ¬ ( 𝐴 = 0 ∨ +∞ = 0 ) ) |
13 |
7 11 12
|
sylanblc |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ¬ ( 𝐴 = 0 ∨ +∞ = 0 ) ) |
14 |
13
|
iffalsed |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → if ( ( 𝐴 = 0 ∨ +∞ = 0 ) , 0 , if ( ( ( ( 0 < +∞ ∧ 𝐴 = +∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = +∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < +∞ ∧ 𝐴 = -∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = -∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = +∞ ) ) ) , -∞ , ( 𝐴 · +∞ ) ) ) ) = if ( ( ( ( 0 < +∞ ∧ 𝐴 = +∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = +∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < +∞ ∧ 𝐴 = -∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = -∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = +∞ ) ) ) , -∞ , ( 𝐴 · +∞ ) ) ) ) |
15 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → 0 < 𝐴 ) |
16 |
|
eqid |
⊢ +∞ = +∞ |
17 |
15 16
|
jctir |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 0 < 𝐴 ∧ +∞ = +∞ ) ) |
18 |
17
|
orcd |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( ( 0 < 𝐴 ∧ +∞ = +∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = -∞ ) ) ) |
19 |
18
|
olcd |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( ( ( 0 < +∞ ∧ 𝐴 = +∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = +∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = -∞ ) ) ) ) |
20 |
19
|
iftrued |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → if ( ( ( ( 0 < +∞ ∧ 𝐴 = +∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = +∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = -∞ ) ) ) , +∞ , if ( ( ( ( 0 < +∞ ∧ 𝐴 = -∞ ) ∨ ( +∞ < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ +∞ = -∞ ) ∨ ( 𝐴 < 0 ∧ +∞ = +∞ ) ) ) , -∞ , ( 𝐴 · +∞ ) ) ) = +∞ ) |
21 |
4 14 20
|
3eqtrd |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 𝐴 ·e +∞ ) = +∞ ) |