| Step | Hyp | Ref
| Expression |
| 1 | | id 22 |
. . 3
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ) |
| 2 | | eqid 2737 |
. . . . . 6
⊢ (𝑗 ∈ ℕ ↦
∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)) |
| 3 | | fzfid 14014 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ →
(1...𝑗) ∈
Fin) |
| 4 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈ (1...𝑗)) → (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1)) = (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))) |
| 5 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → (𝑚 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
| 6 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → 𝑚 = 𝑘) |
| 7 | 5, 6 | ifbieq1d 4550 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑘 → if(𝑚 ∈ ℙ, 𝑚, 1) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
| 8 | 7 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑗 ∈ ℕ ∧ 𝑘 ∈ (1...𝑗)) ∧ 𝑚 = 𝑘) → if(𝑚 ∈ ℙ, 𝑚, 1) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
| 9 | | elfznn 13593 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝑗) → 𝑘 ∈ ℕ) |
| 10 | 9 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈ (1...𝑗)) → 𝑘 ∈ ℕ) |
| 11 | | 1nn 12277 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
| 12 | 11 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑗) → 1 ∈ ℕ) |
| 13 | 9, 12 | ifcld 4572 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝑗) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℕ) |
| 14 | 13 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈ (1...𝑗)) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℕ) |
| 15 | 4, 8, 10, 14 | fvmptd 7023 |
. . . . . . . 8
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈ (1...𝑗)) → ((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
| 16 | 15, 14 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈ (1...𝑗)) → ((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) ∈ ℕ) |
| 17 | 3, 16 | fprodnncl 15991 |
. . . . . 6
⊢ (𝑗 ∈ ℕ →
∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) ∈ ℕ) |
| 18 | 2, 17 | fmpti 7132 |
. . . . 5
⊢ (𝑗 ∈ ℕ ↦
∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)):ℕ⟶ℕ |
| 19 | | nnex 12272 |
. . . . . 6
⊢ ℕ
∈ V |
| 20 | 19, 19 | elmap 8911 |
. . . . 5
⊢ ((𝑗 ∈ ℕ ↦
∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)) ∈ (ℕ ↑m
ℕ) ↔ (𝑗 ∈
ℕ ↦ ∏𝑘
∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)):ℕ⟶ℕ) |
| 21 | 18, 20 | mpbir 231 |
. . . 4
⊢ (𝑗 ∈ ℕ ↦
∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)) ∈ (ℕ ↑m
ℕ) |
| 22 | 21 | a1i 11 |
. . 3
⊢ (𝑛 ∈ ℕ → (𝑗 ∈ ℕ ↦
∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)) ∈ (ℕ ↑m
ℕ)) |
| 23 | | prmgapprmolem 17099 |
. . . . 5
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → 1 < (((#p‘𝑛) + 𝑖) gcd 𝑖)) |
| 24 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ ((((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑗)) → (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1)) = (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))) |
| 25 | 7 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝑛 ∈
ℕ ∧ 𝑖 ∈
(2...𝑛)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑗)) ∧ 𝑚 = 𝑘) → if(𝑚 ∈ ℙ, 𝑚, 1) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
| 26 | 9 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑗)) → 𝑘 ∈ ℕ) |
| 27 | | elfzelz 13564 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1...𝑗) → 𝑘 ∈ ℤ) |
| 28 | | 1zzd 12648 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1...𝑗) → 1 ∈ ℤ) |
| 29 | 27, 28 | ifcld 4572 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑗) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ) |
| 30 | 29 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑗)) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℤ) |
| 31 | 24, 25, 26, 30 | fvmptd 7023 |
. . . . . . . . . . 11
⊢ ((((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑗)) → ((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
| 32 | 31 | prodeq2dv 15958 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘) = ∏𝑘 ∈ (1...𝑗)if(𝑘 ∈ ℙ, 𝑘, 1)) |
| 33 | 32 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘)) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)if(𝑘 ∈ ℙ, 𝑘, 1))) |
| 34 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑛 → (1...𝑗) = (1...𝑛)) |
| 35 | 34 | prodeq1d 15956 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑛 → ∏𝑘 ∈ (1...𝑗)if(𝑘 ∈ ℙ, 𝑘, 1) = ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1)) |
| 36 | 35 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) ∧ 𝑗 = 𝑛) → ∏𝑘 ∈ (1...𝑗)if(𝑘 ∈ ℙ, 𝑘, 1) = ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1)) |
| 37 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → 𝑛 ∈ ℕ) |
| 38 | | fzfid 14014 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → (1...𝑛) ∈ Fin) |
| 39 | | elfznn 13593 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ) |
| 40 | 11 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝑛) → 1 ∈ ℕ) |
| 41 | 39, 40 | ifcld 4572 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑛) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℕ) |
| 42 | 41 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) ∧ 𝑘 ∈ (1...𝑛)) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℕ) |
| 43 | 38, 42 | fprodnncl 15991 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℕ) |
| 44 | 33, 36, 37, 43 | fvmptd 7023 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → ((𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘))‘𝑛) = ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1)) |
| 45 | | nnnn0 12533 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
| 46 | | prmoval 17071 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ (#p‘𝑛) = ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1)) |
| 47 | 45, 46 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(#p‘𝑛) =
∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1)) |
| 48 | 47 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1) = (#p‘𝑛)) |
| 49 | 48 | adantr 480 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1) = (#p‘𝑛)) |
| 50 | 44, 49 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → ((𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘))‘𝑛) = (#p‘𝑛)) |
| 51 | 50 | oveq1d 7446 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → (((𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘))‘𝑛) + 𝑖) = ((#p‘𝑛) + 𝑖)) |
| 52 | 51 | oveq1d 7446 |
. . . . 5
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → ((((𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘))‘𝑛) + 𝑖) gcd 𝑖) = (((#p‘𝑛) + 𝑖) gcd 𝑖)) |
| 53 | 23, 52 | breqtrrd 5171 |
. . . 4
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈ (2...𝑛)) → 1 < ((((𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘))‘𝑛) + 𝑖) gcd 𝑖)) |
| 54 | 53 | ralrimiva 3146 |
. . 3
⊢ (𝑛 ∈ ℕ →
∀𝑖 ∈ (2...𝑛)1 < ((((𝑗 ∈ ℕ ↦ ∏𝑘 ∈ (1...𝑗)((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))‘𝑘))‘𝑛) + 𝑖) gcd 𝑖)) |
| 55 | 1, 22, 54 | prmgaplem8 17096 |
. 2
⊢ (𝑛 ∈ ℕ →
∃𝑝 ∈ ℙ
∃𝑞 ∈ ℙ
(𝑛 ≤ (𝑞 − 𝑝) ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)) |
| 56 | 55 | rgen 3063 |
1
⊢
∀𝑛 ∈
ℕ ∃𝑝 ∈
ℙ ∃𝑞 ∈
ℙ (𝑛 ≤ (𝑞 − 𝑝) ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ) |