Proof of Theorem xrltnr
Step | Hyp | Ref
| Expression |
1 | | elxr 12851 |
. 2
⊢ (𝐴 ∈ ℝ*
↔ (𝐴 ∈ ℝ
∨ 𝐴 = +∞ ∨
𝐴 =
-∞)) |
2 | | ltnr 11070 |
. . 3
⊢ (𝐴 ∈ ℝ → ¬
𝐴 < 𝐴) |
3 | | pnfnre 11017 |
. . . . . . . . . 10
⊢ +∞
∉ ℝ |
4 | 3 | neli 3053 |
. . . . . . . . 9
⊢ ¬
+∞ ∈ ℝ |
5 | 4 | intnan 487 |
. . . . . . . 8
⊢ ¬
(+∞ ∈ ℝ ∧ +∞ ∈ ℝ) |
6 | 5 | intnanr 488 |
. . . . . . 7
⊢ ¬
((+∞ ∈ ℝ ∧ +∞ ∈ ℝ) ∧ +∞
<ℝ +∞) |
7 | | pnfnemnf 11031 |
. . . . . . . . 9
⊢ +∞
≠ -∞ |
8 | 7 | neii 2947 |
. . . . . . . 8
⊢ ¬
+∞ = -∞ |
9 | 8 | intnanr 488 |
. . . . . . 7
⊢ ¬
(+∞ = -∞ ∧ +∞ = +∞) |
10 | 6, 9 | pm3.2ni 878 |
. . . . . 6
⊢ ¬
(((+∞ ∈ ℝ ∧ +∞ ∈ ℝ) ∧ +∞
<ℝ +∞) ∨ (+∞ = -∞ ∧ +∞ =
+∞)) |
11 | 4 | intnanr 488 |
. . . . . . 7
⊢ ¬
(+∞ ∈ ℝ ∧ +∞ = +∞) |
12 | 4 | intnan 487 |
. . . . . . 7
⊢ ¬
(+∞ = -∞ ∧ +∞ ∈ ℝ) |
13 | 11, 12 | pm3.2ni 878 |
. . . . . 6
⊢ ¬
((+∞ ∈ ℝ ∧ +∞ = +∞) ∨ (+∞ = -∞
∧ +∞ ∈ ℝ)) |
14 | 10, 13 | pm3.2ni 878 |
. . . . 5
⊢ ¬
((((+∞ ∈ ℝ ∧ +∞ ∈ ℝ) ∧ +∞
<ℝ +∞) ∨ (+∞ = -∞ ∧ +∞ =
+∞)) ∨ ((+∞ ∈ ℝ ∧ +∞ = +∞) ∨
(+∞ = -∞ ∧ +∞ ∈ ℝ))) |
15 | | pnfxr 11030 |
. . . . . 6
⊢ +∞
∈ ℝ* |
16 | | ltxr 12850 |
. . . . . 6
⊢
((+∞ ∈ ℝ* ∧ +∞ ∈
ℝ*) → (+∞ < +∞ ↔ ((((+∞ ∈
ℝ ∧ +∞ ∈ ℝ) ∧ +∞ <ℝ
+∞) ∨ (+∞ = -∞ ∧ +∞ = +∞)) ∨ ((+∞
∈ ℝ ∧ +∞ = +∞) ∨ (+∞ = -∞ ∧
+∞ ∈ ℝ))))) |
17 | 15, 15, 16 | mp2an 689 |
. . . . 5
⊢ (+∞
< +∞ ↔ ((((+∞ ∈ ℝ ∧ +∞ ∈ ℝ)
∧ +∞ <ℝ +∞) ∨ (+∞ = -∞ ∧
+∞ = +∞)) ∨ ((+∞ ∈ ℝ ∧ +∞ = +∞)
∨ (+∞ = -∞ ∧ +∞ ∈ ℝ)))) |
18 | 14, 17 | mtbir 323 |
. . . 4
⊢ ¬
+∞ < +∞ |
19 | | breq12 5084 |
. . . . 5
⊢ ((𝐴 = +∞ ∧ 𝐴 = +∞) → (𝐴 < 𝐴 ↔ +∞ <
+∞)) |
20 | 19 | anidms 567 |
. . . 4
⊢ (𝐴 = +∞ → (𝐴 < 𝐴 ↔ +∞ <
+∞)) |
21 | 18, 20 | mtbiri 327 |
. . 3
⊢ (𝐴 = +∞ → ¬ 𝐴 < 𝐴) |
22 | | mnfnre 11019 |
. . . . . . . . . 10
⊢ -∞
∉ ℝ |
23 | 22 | neli 3053 |
. . . . . . . . 9
⊢ ¬
-∞ ∈ ℝ |
24 | 23 | intnan 487 |
. . . . . . . 8
⊢ ¬
(-∞ ∈ ℝ ∧ -∞ ∈ ℝ) |
25 | 24 | intnanr 488 |
. . . . . . 7
⊢ ¬
((-∞ ∈ ℝ ∧ -∞ ∈ ℝ) ∧ -∞
<ℝ -∞) |
26 | 7 | nesymi 3003 |
. . . . . . . 8
⊢ ¬
-∞ = +∞ |
27 | 26 | intnan 487 |
. . . . . . 7
⊢ ¬
(-∞ = -∞ ∧ -∞ = +∞) |
28 | 25, 27 | pm3.2ni 878 |
. . . . . 6
⊢ ¬
(((-∞ ∈ ℝ ∧ -∞ ∈ ℝ) ∧ -∞
<ℝ -∞) ∨ (-∞ = -∞ ∧ -∞ =
+∞)) |
29 | 23 | intnanr 488 |
. . . . . . 7
⊢ ¬
(-∞ ∈ ℝ ∧ -∞ = +∞) |
30 | 23 | intnan 487 |
. . . . . . 7
⊢ ¬
(-∞ = -∞ ∧ -∞ ∈ ℝ) |
31 | 29, 30 | pm3.2ni 878 |
. . . . . 6
⊢ ¬
((-∞ ∈ ℝ ∧ -∞ = +∞) ∨ (-∞ = -∞
∧ -∞ ∈ ℝ)) |
32 | 28, 31 | pm3.2ni 878 |
. . . . 5
⊢ ¬
((((-∞ ∈ ℝ ∧ -∞ ∈ ℝ) ∧ -∞
<ℝ -∞) ∨ (-∞ = -∞ ∧ -∞ =
+∞)) ∨ ((-∞ ∈ ℝ ∧ -∞ = +∞) ∨
(-∞ = -∞ ∧ -∞ ∈ ℝ))) |
33 | | mnfxr 11033 |
. . . . . 6
⊢ -∞
∈ ℝ* |
34 | | ltxr 12850 |
. . . . . 6
⊢
((-∞ ∈ ℝ* ∧ -∞ ∈
ℝ*) → (-∞ < -∞ ↔ ((((-∞ ∈
ℝ ∧ -∞ ∈ ℝ) ∧ -∞ <ℝ
-∞) ∨ (-∞ = -∞ ∧ -∞ = +∞)) ∨ ((-∞
∈ ℝ ∧ -∞ = +∞) ∨ (-∞ = -∞ ∧
-∞ ∈ ℝ))))) |
35 | 33, 33, 34 | mp2an 689 |
. . . . 5
⊢ (-∞
< -∞ ↔ ((((-∞ ∈ ℝ ∧ -∞ ∈ ℝ)
∧ -∞ <ℝ -∞) ∨ (-∞ = -∞ ∧
-∞ = +∞)) ∨ ((-∞ ∈ ℝ ∧ -∞ = +∞)
∨ (-∞ = -∞ ∧ -∞ ∈ ℝ)))) |
36 | 32, 35 | mtbir 323 |
. . . 4
⊢ ¬
-∞ < -∞ |
37 | | breq12 5084 |
. . . . 5
⊢ ((𝐴 = -∞ ∧ 𝐴 = -∞) → (𝐴 < 𝐴 ↔ -∞ <
-∞)) |
38 | 37 | anidms 567 |
. . . 4
⊢ (𝐴 = -∞ → (𝐴 < 𝐴 ↔ -∞ <
-∞)) |
39 | 36, 38 | mtbiri 327 |
. . 3
⊢ (𝐴 = -∞ → ¬ 𝐴 < 𝐴) |
40 | 2, 21, 39 | 3jaoi 1426 |
. 2
⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → ¬ 𝐴 < 𝐴) |
41 | 1, 40 | sylbi 216 |
1
⊢ (𝐴 ∈ ℝ*
→ ¬ 𝐴 < 𝐴) |