| Step | Hyp | Ref
| Expression |
| 1 | | vdwnn.1 |
. . 3
⊢ (𝜑 → 𝑅 ∈ Fin) |
| 2 | | vdwnn.3 |
. . . . . . 7
⊢ 𝑆 = {𝑘 ∈ ℕ ∣ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})} |
| 3 | 2 | ssrab3 4082 |
. . . . . 6
⊢ 𝑆 ⊆
ℕ |
| 4 | | nnuz 12921 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
| 5 | 3, 4 | sseqtri 4032 |
. . . . . . 7
⊢ 𝑆 ⊆
(ℤ≥‘1) |
| 6 | | vdwnn.4 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑐 ∈ 𝑅 𝑆 ≠ ∅) |
| 7 | 6 | r19.21bi 3251 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑅) → 𝑆 ≠ ∅) |
| 8 | | infssuzcl 12974 |
. . . . . . 7
⊢ ((𝑆 ⊆
(ℤ≥‘1) ∧ 𝑆 ≠ ∅) → inf(𝑆, ℝ, < ) ∈ 𝑆) |
| 9 | 5, 7, 8 | sylancr 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑅) → inf(𝑆, ℝ, < ) ∈ 𝑆) |
| 10 | 3, 9 | sselid 3981 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑅) → inf(𝑆, ℝ, < ) ∈
ℕ) |
| 11 | 10 | nnred 12281 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑅) → inf(𝑆, ℝ, < ) ∈
ℝ) |
| 12 | 11 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑐 ∈ 𝑅 inf(𝑆, ℝ, < ) ∈
ℝ) |
| 13 | | fimaxre3 12214 |
. . 3
⊢ ((𝑅 ∈ Fin ∧ ∀𝑐 ∈ 𝑅 inf(𝑆, ℝ, < ) ∈ ℝ) →
∃𝑥 ∈ ℝ
∀𝑐 ∈ 𝑅 inf(𝑆, ℝ, < ) ≤ 𝑥) |
| 14 | 1, 12, 13 | syl2anc 584 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑐 ∈ 𝑅 inf(𝑆, ℝ, < ) ≤ 𝑥) |
| 15 | | vdwnn.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:ℕ⟶𝑅) |
| 16 | | 1nn 12277 |
. . . . . . . . 9
⊢ 1 ∈
ℕ |
| 17 | | ffvelcdm 7101 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶𝑅 ∧ 1 ∈ ℕ) →
(𝐹‘1) ∈ 𝑅) |
| 18 | 15, 16, 17 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘1) ∈ 𝑅) |
| 19 | 18 | ne0d 4342 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ≠ ∅) |
| 20 | 19 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑅 ≠ ∅) |
| 21 | | r19.2z 4495 |
. . . . . . 7
⊢ ((𝑅 ≠ ∅ ∧
∀𝑐 ∈ 𝑅 inf(𝑆, ℝ, < ) ≤ 𝑥) → ∃𝑐 ∈ 𝑅 inf(𝑆, ℝ, < ) ≤ 𝑥) |
| 22 | 21 | ex 412 |
. . . . . 6
⊢ (𝑅 ≠ ∅ →
(∀𝑐 ∈ 𝑅 inf(𝑆, ℝ, < ) ≤ 𝑥 → ∃𝑐 ∈ 𝑅 inf(𝑆, ℝ, < ) ≤ 𝑥)) |
| 23 | 20, 22 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑐 ∈ 𝑅 inf(𝑆, ℝ, < ) ≤ 𝑥 → ∃𝑐 ∈ 𝑅 inf(𝑆, ℝ, < ) ≤ 𝑥)) |
| 24 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → 𝑥 ∈ ℝ) |
| 25 | | fllep1 13841 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → 𝑥 ≤ ((⌊‘𝑥) + 1)) |
| 26 | 24, 25 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → 𝑥 ≤ ((⌊‘𝑥) + 1)) |
| 27 | 11 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → inf(𝑆, ℝ, < ) ∈
ℝ) |
| 28 | 24 | flcld 13838 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → (⌊‘𝑥) ∈ ℤ) |
| 29 | 28 | peano2zd 12725 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → ((⌊‘𝑥) + 1) ∈ ℤ) |
| 30 | 29 | zred 12722 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → ((⌊‘𝑥) + 1) ∈ ℝ) |
| 31 | | letr 11355 |
. . . . . . . . . 10
⊢
((inf(𝑆, ℝ,
< ) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ((⌊‘𝑥) + 1) ∈ ℝ) →
((inf(𝑆, ℝ, < )
≤ 𝑥 ∧ 𝑥 ≤ ((⌊‘𝑥) + 1)) → inf(𝑆, ℝ, < ) ≤
((⌊‘𝑥) +
1))) |
| 32 | 27, 24, 30, 31 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → ((inf(𝑆, ℝ, < ) ≤ 𝑥 ∧ 𝑥 ≤ ((⌊‘𝑥) + 1)) → inf(𝑆, ℝ, < ) ≤ ((⌊‘𝑥) + 1))) |
| 33 | 26, 32 | mpan2d 694 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → (inf(𝑆, ℝ, < ) ≤ 𝑥 → inf(𝑆, ℝ, < ) ≤ ((⌊‘𝑥) + 1))) |
| 34 | 10 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → inf(𝑆, ℝ, < ) ∈
ℕ) |
| 35 | 34 | nnzd 12640 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → inf(𝑆, ℝ, < ) ∈
ℤ) |
| 36 | | eluz 12892 |
. . . . . . . . . 10
⊢
((inf(𝑆, ℝ,
< ) ∈ ℤ ∧ ((⌊‘𝑥) + 1) ∈ ℤ) →
(((⌊‘𝑥) + 1)
∈ (ℤ≥‘inf(𝑆, ℝ, < )) ↔ inf(𝑆, ℝ, < ) ≤
((⌊‘𝑥) +
1))) |
| 37 | 35, 29, 36 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → (((⌊‘𝑥) + 1) ∈
(ℤ≥‘inf(𝑆, ℝ, < )) ↔ inf(𝑆, ℝ, < ) ≤
((⌊‘𝑥) +
1))) |
| 38 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → 𝜑) |
| 39 | 9 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → inf(𝑆, ℝ, < ) ∈ 𝑆) |
| 40 | 1, 15, 2 | vdwnnlem2 17034 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((⌊‘𝑥) + 1) ∈
(ℤ≥‘inf(𝑆, ℝ, < ))) → (inf(𝑆, ℝ, < ) ∈ 𝑆 → ((⌊‘𝑥) + 1) ∈ 𝑆)) |
| 41 | 40 | impancom 451 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ inf(𝑆, ℝ, < ) ∈ 𝑆) → (((⌊‘𝑥) + 1) ∈
(ℤ≥‘inf(𝑆, ℝ, < )) →
((⌊‘𝑥) + 1)
∈ 𝑆)) |
| 42 | 38, 39, 41 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → (((⌊‘𝑥) + 1) ∈
(ℤ≥‘inf(𝑆, ℝ, < )) →
((⌊‘𝑥) + 1)
∈ 𝑆)) |
| 43 | 37, 42 | sylbird 260 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → (inf(𝑆, ℝ, < ) ≤ ((⌊‘𝑥) + 1) →
((⌊‘𝑥) + 1)
∈ 𝑆)) |
| 44 | 33, 43 | syld 47 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → (inf(𝑆, ℝ, < ) ≤ 𝑥 → ((⌊‘𝑥) + 1) ∈ 𝑆)) |
| 45 | 3 | sseli 3979 |
. . . . . . . 8
⊢
(((⌊‘𝑥)
+ 1) ∈ 𝑆 →
((⌊‘𝑥) + 1)
∈ ℕ) |
| 46 | 45 | nnnn0d 12587 |
. . . . . . 7
⊢
(((⌊‘𝑥)
+ 1) ∈ 𝑆 →
((⌊‘𝑥) + 1)
∈ ℕ0) |
| 47 | 44, 46 | syl6 35 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → (inf(𝑆, ℝ, < ) ≤ 𝑥 → ((⌊‘𝑥) + 1) ∈
ℕ0)) |
| 48 | 47 | rexlimdva 3155 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑐 ∈ 𝑅 inf(𝑆, ℝ, < ) ≤ 𝑥 → ((⌊‘𝑥) + 1) ∈
ℕ0)) |
| 49 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((⌊‘𝑥) + 1) ∈
ℕ0) → 𝑅 ∈ Fin) |
| 50 | 15 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((⌊‘𝑥) + 1) ∈
ℕ0) → 𝐹:ℕ⟶𝑅) |
| 51 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((⌊‘𝑥) + 1) ∈
ℕ0) → ((⌊‘𝑥) + 1) ∈
ℕ0) |
| 52 | | vdwnnlem1 17033 |
. . . . . . . 8
⊢ ((𝑅 ∈ Fin ∧ 𝐹:ℕ⟶𝑅 ∧ ((⌊‘𝑥) + 1) ∈
ℕ0) → ∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(((⌊‘𝑥) + 1) − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})) |
| 53 | 49, 50, 51, 52 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ ((⌊‘𝑥) + 1) ∈
ℕ0) → ∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(((⌊‘𝑥) + 1) − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})) |
| 54 | 53 | ex 412 |
. . . . . 6
⊢ (𝜑 → (((⌊‘𝑥) + 1) ∈
ℕ0 → ∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(((⌊‘𝑥) + 1) − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 55 | 54 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(((⌊‘𝑥) + 1)
∈ ℕ0 → ∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(((⌊‘𝑥) + 1) − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 56 | 23, 48, 55 | 3syld 60 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑐 ∈ 𝑅 inf(𝑆, ℝ, < ) ≤ 𝑥 → ∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(((⌊‘𝑥) + 1) − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 57 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝑘 = ((⌊‘𝑥) + 1) → (𝑘 − 1) =
(((⌊‘𝑥) + 1)
− 1)) |
| 58 | 57 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑘 = ((⌊‘𝑥) + 1) → (0...(𝑘 − 1)) =
(0...(((⌊‘𝑥) +
1) − 1))) |
| 59 | 58 | raleqdv 3326 |
. . . . . . . . . . 11
⊢ (𝑘 = ((⌊‘𝑥) + 1) → (∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) ↔ ∀𝑚 ∈ (0...(((⌊‘𝑥) + 1) − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 60 | 59 | 2rexbidv 3222 |
. . . . . . . . . 10
⊢ (𝑘 = ((⌊‘𝑥) + 1) → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(((⌊‘𝑥) + 1) − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 61 | 60 | notbid 318 |
. . . . . . . . 9
⊢ (𝑘 = ((⌊‘𝑥) + 1) → (¬
∃𝑎 ∈ ℕ
∃𝑑 ∈ ℕ
∀𝑚 ∈
(0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) ↔ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(((⌊‘𝑥) + 1) − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 62 | 61, 2 | elrab2 3695 |
. . . . . . . 8
⊢
(((⌊‘𝑥)
+ 1) ∈ 𝑆 ↔
(((⌊‘𝑥) + 1)
∈ ℕ ∧ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(((⌊‘𝑥) + 1) − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 63 | 62 | simprbi 496 |
. . . . . . 7
⊢
(((⌊‘𝑥)
+ 1) ∈ 𝑆 → ¬
∃𝑎 ∈ ℕ
∃𝑑 ∈ ℕ
∀𝑚 ∈
(0...(((⌊‘𝑥) +
1) − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})) |
| 64 | 44, 63 | syl6 35 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ 𝑅) → (inf(𝑆, ℝ, < ) ≤ 𝑥 → ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(((⌊‘𝑥) + 1) − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 65 | 64 | ralimdva 3167 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑐 ∈ 𝑅 inf(𝑆, ℝ, < ) ≤ 𝑥 → ∀𝑐 ∈ 𝑅 ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(((⌊‘𝑥) + 1) − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 66 | | ralnex 3072 |
. . . . 5
⊢
(∀𝑐 ∈
𝑅 ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈
(0...(((⌊‘𝑥) +
1) − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}) ↔ ¬ ∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(((⌊‘𝑥) + 1) − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})) |
| 67 | 65, 66 | imbitrdi 251 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑐 ∈ 𝑅 inf(𝑆, ℝ, < ) ≤ 𝑥 → ¬ ∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(((⌊‘𝑥) + 1) − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) |
| 68 | 56, 67 | pm2.65d 196 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ¬ ∀𝑐 ∈ 𝑅 inf(𝑆, ℝ, < ) ≤ 𝑥) |
| 69 | 68 | nrexdv 3149 |
. 2
⊢ (𝜑 → ¬ ∃𝑥 ∈ ℝ ∀𝑐 ∈ 𝑅 inf(𝑆, ℝ, < ) ≤ 𝑥) |
| 70 | 14, 69 | pm2.65i 194 |
1
⊢ ¬
𝜑 |