Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . 3
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ) |
2 | | eqid 2738 |
. . . . . 6
⊢ (𝑗 ∈ ℕ ↦
∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)) |
3 | | fzfid 13432 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ →
(1...𝑗) ∈
Fin) |
4 | | eqidd 2739 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈ (1...𝑗)) → (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1)) = (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))) |
5 | | eleq1 2820 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → (𝑚 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
6 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → 𝑚 = 𝑘) |
7 | 5, 6 | ifbieq1d 4438 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑘 → if(𝑚 ∈ ℙ, 𝑚, 1) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
8 | 7 | adantl 485 |
. . . . . . . . 9
⊢ (((𝑗 ∈ ℕ ∧ 𝑘 ∈ (1...𝑗)) ∧ 𝑚 = 𝑘) → if(𝑚 ∈ ℙ, 𝑚, 1) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
9 | | elfznn 13027 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝑗) → 𝑘 ∈ ℕ) |
10 | 9 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈ (1...𝑗)) → 𝑘 ∈ ℕ) |
11 | | 1nn 11727 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
12 | 11 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑗) → 1 ∈ ℕ) |
13 | 9, 12 | ifcld 4460 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝑗) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℕ) |
14 | 13 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈ (1...𝑗)) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℕ) |
15 | 4, 8, 10, 14 | fvmptd 6782 |
. . . . . . . 8
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈ (1...𝑗)) → ((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
16 | 15, 14 | eqeltrd 2833 |
. . . . . . 7
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈ (1...𝑗)) → ((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) ∈ ℕ) |
17 | 3, 16 | fprodnncl 15401 |
. . . . . 6
⊢ (𝑗 ∈ ℕ →
∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) ∈ ℕ) |
18 | 2, 17 | fmpti 6886 |
. . . . 5
⊢ (𝑗 ∈ ℕ ↦
∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)):ℕ⟶ℕ |
19 | | nnex 11722 |
. . . . . 6
⊢ ℕ
∈ V |
20 | 19, 19 | elmap 8481 |
. . . . 5
⊢ ((𝑗 ∈ ℕ ↦
∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)) ∈ (ℕ ↑m
ℕ) ↔ (𝑗 ∈
ℕ ↦ ∏𝑘
∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)):ℕ⟶ℕ) |
21 | 18, 20 | mpbir 234 |
. . . 4
⊢ (𝑗 ∈ ℕ ↦
∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)) ∈ (ℕ ↑m
ℕ) |
22 | 21 | a1i 11 |
. . 3
⊢ (𝑛 ∈ ℕ → (𝑗 ∈ ℕ ↦
∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)) ∈ (ℕ ↑m
ℕ)) |
23 | | prmgapprmolem 16497 |
. . . . 5
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → 1 < (((#p‘𝑛) + 𝑖) gcd 𝑖)) |
24 | | eqidd 2739 |
. . . . . . . . . . . 12
⊢ ((((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑗)) → (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1)) = (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))) |
25 | 7 | adantl 485 |
. . . . . . . . . . . 12
⊢
(((((𝑛 ∈
ℕ ∧ 𝑖 ∈
(2...𝑛)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑗)) ∧ 𝑚 = 𝑘) → if(𝑚 ∈ ℙ, 𝑚, 1) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
26 | 9 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑗)) → 𝑘 ∈ ℕ) |
27 | | elfzelz 12998 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1...𝑗) → 𝑘 ∈ ℤ) |
28 | | 1zzd 12094 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1...𝑗) → 1 ∈ ℤ) |
29 | 27, 28 | ifcld 4460 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑗) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ) |
30 | 29 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑗)) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ) |
31 | 24, 25, 26, 30 | fvmptd 6782 |
. . . . . . . . . . 11
⊢ ((((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑗)) → ((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
32 | 31 | prodeq2dv 15369 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) = ∏𝑘 ∈ (1...𝑗)if(𝑘 ∈ ℙ, 𝑘, 1)) |
33 | 32 | mpteq2dva 5125 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)if(𝑘 ∈ ℙ, 𝑘, 1))) |
34 | | oveq2 7178 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑛 → (1...𝑗) = (1...𝑛)) |
35 | 34 | prodeq1d 15367 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑛 → ∏𝑘 ∈ (1...𝑗)if(𝑘 ∈ ℙ, 𝑘, 1) = ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1)) |
36 | 35 | adantl 485 |
. . . . . . . . 9
⊢ (((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) ∧ 𝑗 = 𝑛) → ∏𝑘 ∈ (1...𝑗)if(𝑘 ∈ ℙ, 𝑘, 1) = ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1)) |
37 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → 𝑛 ∈ ℕ) |
38 | | fzfid 13432 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → (1...𝑛) ∈ Fin) |
39 | | elfznn 13027 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ) |
40 | 11 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝑛) → 1 ∈ ℕ) |
41 | 39, 40 | ifcld 4460 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑛) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℕ) |
42 | 41 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) ∧ 𝑘 ∈ (1...𝑛)) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℕ) |
43 | 38, 42 | fprodnncl 15401 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℕ) |
44 | 33, 36, 37, 43 | fvmptd 6782 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → ((𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘))‘𝑛) = ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1)) |
45 | | nnnn0 11983 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
46 | | prmoval 16469 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ (#p‘𝑛) = ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1)) |
47 | 45, 46 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(#p‘𝑛) =
∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1)) |
48 | 47 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1) = (#p‘𝑛)) |
49 | 48 | adantr 484 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1) = (#p‘𝑛)) |
50 | 44, 49 | eqtrd 2773 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → ((𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘))‘𝑛) = (#p‘𝑛)) |
51 | 50 | oveq1d 7185 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → (((𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘))‘𝑛) + 𝑖) = ((#p‘𝑛) + 𝑖)) |
52 | 51 | oveq1d 7185 |
. . . . 5
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → ((((𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘))‘𝑛) + 𝑖) gcd 𝑖) = (((#p‘𝑛) + 𝑖) gcd 𝑖)) |
53 | 23, 52 | breqtrrd 5058 |
. . . 4
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → 1 < ((((𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘))‘𝑛) + 𝑖) gcd 𝑖)) |
54 | 53 | ralrimiva 3096 |
. . 3
⊢ (𝑛 ∈ ℕ →
∀𝑖 ∈ (2...𝑛)1 < ((((𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘))‘𝑛) + 𝑖) gcd 𝑖)) |
55 | 1, 22, 54 | prmgaplem8 16494 |
. 2
⊢ (𝑛 ∈ ℕ →
∃𝑝 ∈ ℙ
∃𝑞 ∈ ℙ
(𝑛 ≤ (𝑞 − 𝑝) ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)) |
56 | 55 | rgen 3063 |
1
⊢
∀𝑛 ∈
ℕ ∃𝑝 ∈
ℙ ∃𝑞 ∈
ℙ (𝑛 ≤ (𝑞 − 𝑝) ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ) |