Proof of Theorem xmulpnf1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pnfxr 11316 | . . . 4
⊢ +∞
∈ ℝ* | 
| 2 |  | xmulval 13268 | . . . 4
⊢ ((𝐴 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝐴 ·e +∞) = if((𝐴 = 0 ∨ +∞ = 0), 0,
if((((0 < +∞ ∧ 𝐴 = +∞) ∨ (+∞ < 0 ∧
𝐴 = -∞)) ∨ ((0
< 𝐴 ∧ +∞ =
+∞) ∨ (𝐴 < 0
∧ +∞ = -∞))), +∞, if((((0 < +∞ ∧ 𝐴 = -∞) ∨ (+∞ <
0 ∧ 𝐴 = +∞)) ∨
((0 < 𝐴 ∧ +∞ =
-∞) ∨ (𝐴 < 0
∧ +∞ = +∞))), -∞, (𝐴 · +∞))))) | 
| 3 | 1, 2 | mpan2 691 | . . 3
⊢ (𝐴 ∈ ℝ*
→ (𝐴
·e +∞) = if((𝐴 = 0 ∨ +∞ = 0), 0, if((((0 <
+∞ ∧ 𝐴 =
+∞) ∨ (+∞ < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ +∞ = +∞) ∨
(𝐴 < 0 ∧ +∞ =
-∞))), +∞, if((((0 < +∞ ∧ 𝐴 = -∞) ∨ (+∞ < 0 ∧
𝐴 = +∞)) ∨ ((0
< 𝐴 ∧ +∞ =
-∞) ∨ (𝐴 < 0
∧ +∞ = +∞))), -∞, (𝐴 · +∞))))) | 
| 4 | 3 | adantr 480 | . 2
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) →
(𝐴 ·e
+∞) = if((𝐴 = 0 ∨
+∞ = 0), 0, if((((0 < +∞ ∧ 𝐴 = +∞) ∨ (+∞ < 0 ∧
𝐴 = -∞)) ∨ ((0
< 𝐴 ∧ +∞ =
+∞) ∨ (𝐴 < 0
∧ +∞ = -∞))), +∞, if((((0 < +∞ ∧ 𝐴 = -∞) ∨ (+∞ <
0 ∧ 𝐴 = +∞)) ∨
((0 < 𝐴 ∧ +∞ =
-∞) ∨ (𝐴 < 0
∧ +∞ = +∞))), -∞, (𝐴 · +∞))))) | 
| 5 |  | 0xr 11309 | . . . . 5
⊢ 0 ∈
ℝ* | 
| 6 |  | xrltne 13206 | . . . . 5
⊢ ((0
∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 0 <
𝐴) → 𝐴 ≠ 0) | 
| 7 | 5, 6 | mp3an1 1449 | . . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) →
𝐴 ≠ 0) | 
| 8 |  | 0re 11264 | . . . . . 6
⊢ 0 ∈
ℝ | 
| 9 |  | renepnf 11310 | . . . . . 6
⊢ (0 ∈
ℝ → 0 ≠ +∞) | 
| 10 | 8, 9 | ax-mp 5 | . . . . 5
⊢ 0 ≠
+∞ | 
| 11 | 10 | necomi 2994 | . . . 4
⊢ +∞
≠ 0 | 
| 12 |  | neanior 3034 | . . . 4
⊢ ((𝐴 ≠ 0 ∧ +∞ ≠ 0)
↔ ¬ (𝐴 = 0 ∨
+∞ = 0)) | 
| 13 | 7, 11, 12 | sylanblc 589 | . . 3
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) →
¬ (𝐴 = 0 ∨ +∞
= 0)) | 
| 14 | 13 | iffalsed 4535 | . 2
⊢ ((𝐴 ∈ ℝ*
∧ 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 484 | . . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) → 0
< 𝐴) | 
| 16 |  | eqid 2736 | . . . . . 6
⊢ +∞
= +∞ | 
| 17 | 15, 16 | jctir 520 | . . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) → (0
< 𝐴 ∧ +∞ =
+∞)) | 
| 18 | 17 | orcd 873 | . . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) → ((0
< 𝐴 ∧ +∞ =
+∞) ∨ (𝐴 < 0
∧ +∞ = -∞))) | 
| 19 | 18 | olcd 874 | . . 3
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) → (((0
< +∞ ∧ 𝐴 =
+∞) ∨ (+∞ < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ +∞ = +∞) ∨
(𝐴 < 0 ∧ +∞ =
-∞)))) | 
| 20 | 19 | iftrued 4532 | . 2
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) →
if((((0 < +∞ ∧ 𝐴 = +∞) ∨ (+∞ < 0 ∧
𝐴 = -∞)) ∨ ((0
< 𝐴 ∧ +∞ =
+∞) ∨ (𝐴 < 0
∧ +∞ = -∞))), +∞, if((((0 < +∞ ∧ 𝐴 = -∞) ∨ (+∞ <
0 ∧ 𝐴 = +∞)) ∨
((0 < 𝐴 ∧ +∞ =
-∞) ∨ (𝐴 < 0
∧ +∞ = +∞))), -∞, (𝐴 · +∞))) =
+∞) | 
| 21 | 4, 14, 20 | 3eqtrd 2780 | 1
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) →
(𝐴 ·e
+∞) = +∞) |