Step | Hyp | Ref
| Expression |
1 | | pm3.24 922 |
. . . 4
⊢ ¬
(∀𝑦 ∈ ℕ
¬ 𝑥 < 𝑦 ∧ ¬ ∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦) |
2 | | peano2rem 10227 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → (𝑥 − 1) ∈
ℝ) |
3 | | ltm1 10742 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → (𝑥 − 1) < 𝑥) |
4 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (𝑥 − 1) ∈
V |
5 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 − 1) → (𝑦 ∈ ℝ ↔ (𝑥 − 1) ∈ ℝ)) |
6 | | breq1 4586 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 − 1) → (𝑦 < 𝑥 ↔ (𝑥 − 1) < 𝑥)) |
7 | | breq1 4586 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑥 − 1) → (𝑦 < 𝑧 ↔ (𝑥 − 1) < 𝑧)) |
8 | 7 | rexbidv 3034 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 − 1) → (∃𝑧 ∈ ℕ 𝑦 < 𝑧 ↔ ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧)) |
9 | 6, 8 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 − 1) → ((𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧) ↔ ((𝑥 − 1) < 𝑥 → ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧))) |
10 | 5, 9 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑥 − 1) → ((𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) ↔ ((𝑥 − 1) ∈ ℝ → ((𝑥 − 1) < 𝑥 → ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧)))) |
11 | 4, 10 | spcv 3272 |
. . . . . . . . . . . 12
⊢
(∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → ((𝑥 − 1) ∈ ℝ → ((𝑥 − 1) < 𝑥 → ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧))) |
12 | 3, 11 | syl7 72 |
. . . . . . . . . . 11
⊢
(∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → ((𝑥 − 1) ∈ ℝ → (𝑥 ∈ ℝ →
∃𝑧 ∈ ℕ
(𝑥 − 1) < 𝑧))) |
13 | 2, 12 | syl5 33 |
. . . . . . . . . 10
⊢
(∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → (𝑥 ∈ ℝ → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧))) |
14 | 13 | pm2.43d 51 |
. . . . . . . . 9
⊢
(∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℕ (𝑥 − 1) < 𝑧)) |
15 | | df-rex 2902 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
ℕ (𝑥 − 1) <
𝑧 ↔ ∃𝑧(𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧)) |
16 | 14, 15 | syl6ib 240 |
. . . . . . . 8
⊢
(∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → (𝑥 ∈ ℝ → ∃𝑧(𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧))) |
17 | 16 | com12 32 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ →
(∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → ∃𝑧(𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧))) |
18 | | nnre 10904 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℝ) |
19 | | 1re 9918 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
20 | | ltsubadd 10377 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 1 ∈
ℝ ∧ 𝑧 ∈
ℝ) → ((𝑥 −
1) < 𝑧 ↔ 𝑥 < (𝑧 + 1))) |
21 | 19, 20 | mp3an2 1404 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 − 1) < 𝑧 ↔ 𝑥 < (𝑧 + 1))) |
22 | 18, 21 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℕ) → ((𝑥 − 1) < 𝑧 ↔ 𝑥 < (𝑧 + 1))) |
23 | 22 | pm5.32da 671 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → ((𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧) ↔ (𝑧 ∈ ℕ ∧ 𝑥 < (𝑧 + 1)))) |
24 | 23 | exbidv 1837 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ →
(∃𝑧(𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧) ↔ ∃𝑧(𝑧 ∈ ℕ ∧ 𝑥 < (𝑧 + 1)))) |
25 | | peano2nn 10909 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℕ → (𝑧 + 1) ∈
ℕ) |
26 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑧 + 1) ∈ V |
27 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑧 + 1) → (𝑦 ∈ ℕ ↔ (𝑧 + 1) ∈ ℕ)) |
28 | | breq2 4587 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑧 + 1) → (𝑥 < 𝑦 ↔ 𝑥 < (𝑧 + 1))) |
29 | 27, 28 | anbi12d 743 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑧 + 1) → ((𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) ↔ ((𝑧 + 1) ∈ ℕ ∧ 𝑥 < (𝑧 + 1)))) |
30 | 26, 29 | spcev 3273 |
. . . . . . . . . 10
⊢ (((𝑧 + 1) ∈ ℕ ∧ 𝑥 < (𝑧 + 1)) → ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦)) |
31 | 25, 30 | sylan 487 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℕ ∧ 𝑥 < (𝑧 + 1)) → ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦)) |
32 | 31 | exlimiv 1845 |
. . . . . . . 8
⊢
(∃𝑧(𝑧 ∈ ℕ ∧ 𝑥 < (𝑧 + 1)) → ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦)) |
33 | 24, 32 | syl6bi 242 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ →
(∃𝑧(𝑧 ∈ ℕ ∧ (𝑥 − 1) < 𝑧) → ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦))) |
34 | 17, 33 | syld 46 |
. . . . . 6
⊢ (𝑥 ∈ ℝ →
(∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦))) |
35 | | df-ral 2901 |
. . . . . 6
⊢
(∀𝑦 ∈
ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧) ↔ ∀𝑦(𝑦 ∈ ℝ → (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧))) |
36 | | df-ral 2901 |
. . . . . . . 8
⊢
(∀𝑦 ∈
ℕ ¬ 𝑥 < 𝑦 ↔ ∀𝑦(𝑦 ∈ ℕ → ¬ 𝑥 < 𝑦)) |
37 | | alinexa 1759 |
. . . . . . . 8
⊢
(∀𝑦(𝑦 ∈ ℕ → ¬
𝑥 < 𝑦) ↔ ¬ ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦)) |
38 | 36, 37 | bitr2i 264 |
. . . . . . 7
⊢ (¬
∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦) ↔ ∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦) |
39 | 38 | con1bii 345 |
. . . . . 6
⊢ (¬
∀𝑦 ∈ ℕ
¬ 𝑥 < 𝑦 ↔ ∃𝑦(𝑦 ∈ ℕ ∧ 𝑥 < 𝑦)) |
40 | 34, 35, 39 | 3imtr4g 284 |
. . . . 5
⊢ (𝑥 ∈ ℝ →
(∀𝑦 ∈ ℝ
(𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧) → ¬ ∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦)) |
41 | 40 | anim2d 587 |
. . . 4
⊢ (𝑥 ∈ ℝ →
((∀𝑦 ∈ ℕ
¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) → (∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦 ∧ ¬ ∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦))) |
42 | 1, 41 | mtoi 189 |
. . 3
⊢ (𝑥 ∈ ℝ → ¬
(∀𝑦 ∈ ℕ
¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧))) |
43 | 42 | nrex 2983 |
. 2
⊢ ¬
∃𝑥 ∈ ℝ
(∀𝑦 ∈ ℕ
¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧)) |
44 | | nnssre 10901 |
. . 3
⊢ ℕ
⊆ ℝ |
45 | | 1nn 10908 |
. . . . 5
⊢ 1 ∈
ℕ |
46 | 45 | n0ii 3881 |
. . . 4
⊢ ¬
ℕ = ∅ |
47 | 46 | neir 2785 |
. . 3
⊢ ℕ
≠ ∅ |
48 | | sup2 10858 |
. . 3
⊢ ((ℕ
⊆ ℝ ∧ ℕ ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℕ (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧))) |
49 | 44, 47, 48 | mp3an12 1406 |
. 2
⊢
(∃𝑥 ∈
ℝ ∀𝑦 ∈
ℕ (𝑦 < 𝑥 ∨ 𝑦 = 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ ℕ ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ ℕ 𝑦 < 𝑧))) |
50 | 43, 49 | mto 187 |
1
⊢ ¬
∃𝑥 ∈ ℝ
∀𝑦 ∈ ℕ
(𝑦 < 𝑥 ∨ 𝑦 = 𝑥) |