Proof of Theorem xmulpnf1
Step | Hyp | Ref
| Expression |
1 | | pnfxr 11039 |
. . . 4
⊢ +∞
∈ ℝ* |
2 | | xmulval 12969 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝐴 ·e +∞) = if((𝐴 = 0 ∨ +∞ = 0), 0,
if((((0 < +∞ ∧ 𝐴 = +∞) ∨ (+∞ < 0 ∧
𝐴 = -∞)) ∨ ((0
< 𝐴 ∧ +∞ =
+∞) ∨ (𝐴 < 0
∧ +∞ = -∞))), +∞, if((((0 < +∞ ∧ 𝐴 = -∞) ∨ (+∞ <
0 ∧ 𝐴 = +∞)) ∨
((0 < 𝐴 ∧ +∞ =
-∞) ∨ (𝐴 < 0
∧ +∞ = +∞))), -∞, (𝐴 · +∞))))) |
3 | 1, 2 | mpan2 688 |
. . 3
⊢ (𝐴 ∈ ℝ*
→ (𝐴
·e +∞) = if((𝐴 = 0 ∨ +∞ = 0), 0, if((((0 <
+∞ ∧ 𝐴 =
+∞) ∨ (+∞ < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ +∞ = +∞) ∨
(𝐴 < 0 ∧ +∞ =
-∞))), +∞, if((((0 < +∞ ∧ 𝐴 = -∞) ∨ (+∞ < 0 ∧
𝐴 = +∞)) ∨ ((0
< 𝐴 ∧ +∞ =
-∞) ∨ (𝐴 < 0
∧ +∞ = +∞))), -∞, (𝐴 · +∞))))) |
4 | 3 | adantr 481 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) →
(𝐴 ·e
+∞) = if((𝐴 = 0 ∨
+∞ = 0), 0, if((((0 < +∞ ∧ 𝐴 = +∞) ∨ (+∞ < 0 ∧
𝐴 = -∞)) ∨ ((0
< 𝐴 ∧ +∞ =
+∞) ∨ (𝐴 < 0
∧ +∞ = -∞))), +∞, if((((0 < +∞ ∧ 𝐴 = -∞) ∨ (+∞ <
0 ∧ 𝐴 = +∞)) ∨
((0 < 𝐴 ∧ +∞ =
-∞) ∨ (𝐴 < 0
∧ +∞ = +∞))), -∞, (𝐴 · +∞))))) |
5 | | 0xr 11032 |
. . . . 5
⊢ 0 ∈
ℝ* |
6 | | xrltne 12907 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 0 <
𝐴) → 𝐴 ≠ 0) |
7 | 5, 6 | mp3an1 1447 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) →
𝐴 ≠ 0) |
8 | | 0re 10987 |
. . . . . 6
⊢ 0 ∈
ℝ |
9 | | renepnf 11033 |
. . . . . 6
⊢ (0 ∈
ℝ → 0 ≠ +∞) |
10 | 8, 9 | ax-mp 5 |
. . . . 5
⊢ 0 ≠
+∞ |
11 | 10 | necomi 2998 |
. . . 4
⊢ +∞
≠ 0 |
12 | | neanior 3037 |
. . . 4
⊢ ((𝐴 ≠ 0 ∧ +∞ ≠ 0)
↔ ¬ (𝐴 = 0 ∨
+∞ = 0)) |
13 | 7, 11, 12 | sylanblc 589 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) →
¬ (𝐴 = 0 ∨ +∞
= 0)) |
14 | 13 | iffalsed 4470 |
. 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 485 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) → 0
< 𝐴) |
16 | | eqid 2738 |
. . . . . 6
⊢ +∞
= +∞ |
17 | 15, 16 | jctir 521 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) → (0
< 𝐴 ∧ +∞ =
+∞)) |
18 | 17 | orcd 870 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) → ((0
< 𝐴 ∧ +∞ =
+∞) ∨ (𝐴 < 0
∧ +∞ = -∞))) |
19 | 18 | olcd 871 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) → (((0
< +∞ ∧ 𝐴 =
+∞) ∨ (+∞ < 0 ∧ 𝐴 = -∞)) ∨ ((0 < 𝐴 ∧ +∞ = +∞) ∨
(𝐴 < 0 ∧ +∞ =
-∞)))) |
20 | 19 | iftrued 4467 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) →
if((((0 < +∞ ∧ 𝐴 = +∞) ∨ (+∞ < 0 ∧
𝐴 = -∞)) ∨ ((0
< 𝐴 ∧ +∞ =
+∞) ∨ (𝐴 < 0
∧ +∞ = -∞))), +∞, if((((0 < +∞ ∧ 𝐴 = -∞) ∨ (+∞ <
0 ∧ 𝐴 = +∞)) ∨
((0 < 𝐴 ∧ +∞ =
-∞) ∨ (𝐴 < 0
∧ +∞ = +∞))), -∞, (𝐴 · +∞))) =
+∞) |
21 | 4, 14, 20 | 3eqtrd 2782 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) →
(𝐴 ·e
+∞) = +∞) |