Step | Hyp | Ref
| Expression |
1 | | infpn2.1 |
. . 3
⊢ 𝑆 = {𝑛 ∈ ℕ ∣ (1 < 𝑛 ∧ ∀𝑚 ∈ ℕ ((𝑛 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑛)))} |
2 | | ssrab2 3650 |
. . 3
⊢ {𝑛 ∈ ℕ ∣ (1 <
𝑛 ∧ ∀𝑚 ∈ ℕ ((𝑛 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑛)))} ⊆ ℕ |
3 | 1, 2 | eqsstri 3598 |
. 2
⊢ 𝑆 ⊆
ℕ |
4 | | infpn 15454 |
. . . . 5
⊢ (𝑗 ∈ ℕ →
∃𝑘 ∈ ℕ
(𝑗 < 𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘)))) |
5 | | nnge1 10923 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → 1 ≤
𝑗) |
6 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ) → 1 ≤
𝑗) |
7 | | nnre 10904 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ) |
8 | | nnre 10904 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
9 | | 1re 9918 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
10 | | lelttr 10007 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 𝑗
∈ ℝ ∧ 𝑘
∈ ℝ) → ((1 ≤ 𝑗 ∧ 𝑗 < 𝑘) → 1 < 𝑘)) |
11 | 9, 10 | mp3an1 1403 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ ℝ ∧ 𝑘 ∈ ℝ) → ((1 ≤
𝑗 ∧ 𝑗 < 𝑘) → 1 < 𝑘)) |
12 | 7, 8, 11 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ) → ((1 ≤
𝑗 ∧ 𝑗 < 𝑘) → 1 < 𝑘)) |
13 | 6, 12 | mpand 707 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑗 < 𝑘 → 1 < 𝑘)) |
14 | 13 | ancld 574 |
. . . . . . . 8
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (𝑗 < 𝑘 → (𝑗 < 𝑘 ∧ 1 < 𝑘))) |
15 | 14 | anim1d 586 |
. . . . . . 7
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ) → ((𝑗 < 𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘))) → ((𝑗 < 𝑘 ∧ 1 < 𝑘) ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘))))) |
16 | | anass 679 |
. . . . . . 7
⊢ (((𝑗 < 𝑘 ∧ 1 < 𝑘) ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘))) ↔ (𝑗 < 𝑘 ∧ (1 < 𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘))))) |
17 | 15, 16 | syl6ib 240 |
. . . . . 6
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ) → ((𝑗 < 𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘))) → (𝑗 < 𝑘 ∧ (1 < 𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘)))))) |
18 | 17 | reximdva 3000 |
. . . . 5
⊢ (𝑗 ∈ ℕ →
(∃𝑘 ∈ ℕ
(𝑗 < 𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘))) → ∃𝑘 ∈ ℕ (𝑗 < 𝑘 ∧ (1 < 𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘)))))) |
19 | 4, 18 | mpd 15 |
. . . 4
⊢ (𝑗 ∈ ℕ →
∃𝑘 ∈ ℕ
(𝑗 < 𝑘 ∧ (1 < 𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘))))) |
20 | | breq2 4587 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (1 < 𝑛 ↔ 1 < 𝑘)) |
21 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (𝑛 / 𝑚) = (𝑘 / 𝑚)) |
22 | 21 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → ((𝑛 / 𝑚) ∈ ℕ ↔ (𝑘 / 𝑚) ∈ ℕ)) |
23 | | equequ2 1940 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (𝑚 = 𝑛 ↔ 𝑚 = 𝑘)) |
24 | 23 | orbi2d 734 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → ((𝑚 = 1 ∨ 𝑚 = 𝑛) ↔ (𝑚 = 1 ∨ 𝑚 = 𝑘))) |
25 | 22, 24 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (((𝑛 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑛)) ↔ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘)))) |
26 | 25 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (∀𝑚 ∈ ℕ ((𝑛 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑛)) ↔ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘)))) |
27 | 20, 26 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → ((1 < 𝑛 ∧ ∀𝑚 ∈ ℕ ((𝑛 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑛))) ↔ (1 < 𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘))))) |
28 | 27, 1 | elrab2 3333 |
. . . . . . 7
⊢ (𝑘 ∈ 𝑆 ↔ (𝑘 ∈ ℕ ∧ (1 < 𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘))))) |
29 | 28 | anbi1i 727 |
. . . . . 6
⊢ ((𝑘 ∈ 𝑆 ∧ 𝑗 < 𝑘) ↔ ((𝑘 ∈ ℕ ∧ (1 < 𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘)))) ∧ 𝑗 < 𝑘)) |
30 | | anass 679 |
. . . . . 6
⊢ (((𝑘 ∈ ℕ ∧ (1 <
𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘)))) ∧ 𝑗 < 𝑘) ↔ (𝑘 ∈ ℕ ∧ ((1 < 𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘))) ∧ 𝑗 < 𝑘))) |
31 | | ancom 465 |
. . . . . . 7
⊢ (((1 <
𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘))) ∧ 𝑗 < 𝑘) ↔ (𝑗 < 𝑘 ∧ (1 < 𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘))))) |
32 | 31 | anbi2i 726 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ ∧ ((1 <
𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘))) ∧ 𝑗 < 𝑘)) ↔ (𝑘 ∈ ℕ ∧ (𝑗 < 𝑘 ∧ (1 < 𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘)))))) |
33 | 29, 30, 32 | 3bitri 285 |
. . . . 5
⊢ ((𝑘 ∈ 𝑆 ∧ 𝑗 < 𝑘) ↔ (𝑘 ∈ ℕ ∧ (𝑗 < 𝑘 ∧ (1 < 𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘)))))) |
34 | 33 | rexbii2 3021 |
. . . 4
⊢
(∃𝑘 ∈
𝑆 𝑗 < 𝑘 ↔ ∃𝑘 ∈ ℕ (𝑗 < 𝑘 ∧ (1 < 𝑘 ∧ ∀𝑚 ∈ ℕ ((𝑘 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑘))))) |
35 | 19, 34 | sylibr 223 |
. . 3
⊢ (𝑗 ∈ ℕ →
∃𝑘 ∈ 𝑆 𝑗 < 𝑘) |
36 | 35 | rgen 2906 |
. 2
⊢
∀𝑗 ∈
ℕ ∃𝑘 ∈
𝑆 𝑗 < 𝑘 |
37 | | unben 15451 |
. 2
⊢ ((𝑆 ⊆ ℕ ∧
∀𝑗 ∈ ℕ
∃𝑘 ∈ 𝑆 𝑗 < 𝑘) → 𝑆 ≈ ℕ) |
38 | 3, 36, 37 | mp2an 704 |
1
⊢ 𝑆 ≈
ℕ |