Proof of Theorem xrpnf
Step | Hyp | Ref
| Expression |
1 | | rexr 10879 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
2 | 1 | adantl 485 |
. . . . 5
⊢ ((𝐴 = +∞ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈
ℝ*) |
3 | | id 22 |
. . . . . . 7
⊢ (𝐴 = +∞ → 𝐴 = +∞) |
4 | | pnfxr 10887 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
5 | 4 | a1i 11 |
. . . . . . 7
⊢ (𝐴 = +∞ → +∞
∈ ℝ*) |
6 | 3, 5 | eqeltrd 2838 |
. . . . . 6
⊢ (𝐴 = +∞ → 𝐴 ∈
ℝ*) |
7 | 6 | adantr 484 |
. . . . 5
⊢ ((𝐴 = +∞ ∧ 𝑥 ∈ ℝ) → 𝐴 ∈
ℝ*) |
8 | | ltpnf 12712 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → 𝑥 < +∞) |
9 | 8 | adantl 485 |
. . . . . 6
⊢ ((𝐴 = +∞ ∧ 𝑥 ∈ ℝ) → 𝑥 < +∞) |
10 | | simpl 486 |
. . . . . 6
⊢ ((𝐴 = +∞ ∧ 𝑥 ∈ ℝ) → 𝐴 = +∞) |
11 | 9, 10 | breqtrrd 5081 |
. . . . 5
⊢ ((𝐴 = +∞ ∧ 𝑥 ∈ ℝ) → 𝑥 < 𝐴) |
12 | 2, 7, 11 | xrltled 12740 |
. . . 4
⊢ ((𝐴 = +∞ ∧ 𝑥 ∈ ℝ) → 𝑥 ≤ 𝐴) |
13 | 12 | ralrimiva 3105 |
. . 3
⊢ (𝐴 = +∞ → ∀𝑥 ∈ ℝ 𝑥 ≤ 𝐴) |
14 | 13 | adantl 485 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 = +∞) →
∀𝑥 ∈ ℝ
𝑥 ≤ 𝐴) |
15 | | simpll 767 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ ∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴) ∧ 𝐴 < +∞) → 𝐴 ∈
ℝ*) |
16 | | 0red 10836 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴 → 0 ∈
ℝ) |
17 | | id 22 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴 → ∀𝑥 ∈ ℝ 𝑥 ≤ 𝐴) |
18 | | breq1 5056 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → (𝑥 ≤ 𝐴 ↔ 0 ≤ 𝐴)) |
19 | 18 | rspcva 3535 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ ∀𝑥 ∈ ℝ 𝑥 ≤ 𝐴) → 0 ≤ 𝐴) |
20 | 16, 17, 19 | syl2anc 587 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴 → 0 ≤ 𝐴) |
21 | 20 | adantr 484 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴 ∧ 𝐴 = -∞) → 0 ≤ 𝐴) |
22 | | simpr 488 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴 ∧ 𝐴 = -∞) → 𝐴 = -∞) |
23 | 21, 22 | breqtrd 5079 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴 ∧ 𝐴 = -∞) → 0 ≤
-∞) |
24 | 23 | adantll 714 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ ∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴) ∧ 𝐴 = -∞) → 0 ≤
-∞) |
25 | | mnflt0 12717 |
. . . . . . . . . 10
⊢ -∞
< 0 |
26 | | mnfxr 10890 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
27 | | 0xr 10880 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
28 | | xrltnle 10900 |
. . . . . . . . . . 11
⊢
((-∞ ∈ ℝ* ∧ 0 ∈
ℝ*) → (-∞ < 0 ↔ ¬ 0 ≤
-∞)) |
29 | 26, 27, 28 | mp2an 692 |
. . . . . . . . . 10
⊢ (-∞
< 0 ↔ ¬ 0 ≤ -∞) |
30 | 25, 29 | mpbi 233 |
. . . . . . . . 9
⊢ ¬ 0
≤ -∞ |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ ∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴) ∧ 𝐴 = -∞) → ¬ 0 ≤
-∞) |
32 | 24, 31 | pm2.65da 817 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ ∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴) → ¬ 𝐴 = -∞) |
33 | 32 | neqned 2947 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ ∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴) → 𝐴 ≠ -∞) |
34 | 33 | adantr 484 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ ∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴) ∧ 𝐴 < +∞) → 𝐴 ≠ -∞) |
35 | | simpl 486 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 < +∞)
→ 𝐴 ∈
ℝ*) |
36 | 4 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 < +∞)
→ +∞ ∈ ℝ*) |
37 | | simpr 488 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 < +∞)
→ 𝐴 <
+∞) |
38 | 35, 36, 37 | xrltned 42569 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 < +∞)
→ 𝐴 ≠
+∞) |
39 | 38 | adantlr 715 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ ∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴) ∧ 𝐴 < +∞) → 𝐴 ≠ +∞) |
40 | 15, 34, 39 | xrred 42577 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ ∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴) ∧ 𝐴 < +∞) → 𝐴 ∈ ℝ) |
41 | | peano2re 11005 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈
ℝ) |
42 | 41 | adantl 485 |
. . . . . . 7
⊢
((∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) → (𝐴 + 1) ∈ ℝ) |
43 | | simpl 486 |
. . . . . . 7
⊢
((∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) → ∀𝑥 ∈ ℝ 𝑥 ≤ 𝐴) |
44 | | breq1 5056 |
. . . . . . . 8
⊢ (𝑥 = (𝐴 + 1) → (𝑥 ≤ 𝐴 ↔ (𝐴 + 1) ≤ 𝐴)) |
45 | 44 | rspcva 3535 |
. . . . . . 7
⊢ (((𝐴 + 1) ∈ ℝ ∧
∀𝑥 ∈ ℝ
𝑥 ≤ 𝐴) → (𝐴 + 1) ≤ 𝐴) |
46 | 42, 43, 45 | syl2anc 587 |
. . . . . 6
⊢
((∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) → (𝐴 + 1) ≤ 𝐴) |
47 | | ltp1 11672 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1)) |
48 | | id 22 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ) |
49 | 48, 41 | ltnled 10979 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 < (𝐴 + 1) ↔ ¬ (𝐴 + 1) ≤ 𝐴)) |
50 | 47, 49 | mpbid 235 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → ¬
(𝐴 + 1) ≤ 𝐴) |
51 | 50 | adantl 485 |
. . . . . 6
⊢
((∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) → ¬ (𝐴 + 1) ≤ 𝐴) |
52 | 46, 51 | pm2.65da 817 |
. . . . 5
⊢
(∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴 → ¬ 𝐴 ∈ ℝ) |
53 | 52 | ad2antlr 727 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ ∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴) ∧ 𝐴 < +∞) → ¬ 𝐴 ∈
ℝ) |
54 | 40, 53 | pm2.65da 817 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ ∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴) → ¬ 𝐴 < +∞) |
55 | | nltpnft 12754 |
. . . 4
⊢ (𝐴 ∈ ℝ*
→ (𝐴 = +∞ ↔
¬ 𝐴 <
+∞)) |
56 | 55 | adantr 484 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ ∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴) → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞)) |
57 | 54, 56 | mpbird 260 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ ∀𝑥 ∈
ℝ 𝑥 ≤ 𝐴) → 𝐴 = +∞) |
58 | 14, 57 | impbida 801 |
1
⊢ (𝐴 ∈ ℝ*
→ (𝐴 = +∞ ↔
∀𝑥 ∈ ℝ
𝑥 ≤ 𝐴)) |