Metamath Proof Explorer


Theorem prmgapprmo

Description: Alternate proof of prmgap : in contrast to prmgap , where the gap starts at n! , the factorial of n, the gap starts at n#, the primorial of n. (Contributed by AV, 15-Aug-2020) (Revised by AV, 29-Aug-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion prmgapprmo 𝑛 ∈ ℕ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑛 ≤ ( 𝑞𝑝 ) ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ )

Proof

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 ) ..^ 𝑞 ) 𝑧 ∉ ℙ )