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