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