Metamath Proof Explorer

Theorem prmgaplcm

Description: Alternate proof of prmgap : in contrast to prmgap , where the gap starts at n! , the factorial of n, the gap starts at the least common multiple of all positive integers less than or equal to n. (Contributed by AV, 13-Aug-2020) (Revised by AV, 27-Aug-2020) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ )
2 fzssz ⊢ ( 1 ... 𝑥 ) ⊆ ℤ
3 2 a1i ⊢ ( 𝑥 ∈ ℕ → ( 1 ... 𝑥 ) ⊆ ℤ )
4 fzfi ⊢ ( 1 ... 𝑥 ) ∈ Fin
5 4 a1i ⊢ ( 𝑥 ∈ ℕ → ( 1 ... 𝑥 ) ∈ Fin )
6 0nelfz1 ⊢ 0 ∉ ( 1 ... 𝑥 )
7 6 a1i ⊢ ( 𝑥 ∈ ℕ → 0 ∉ ( 1 ... 𝑥 ) )
8 lcmfn0cl ⊢ ( ( ( 1 ... 𝑥 ) ⊆ ℤ ∧ ( 1 ... 𝑥 ) ∈ Fin ∧ 0 ∉ ( 1 ... 𝑥 ) ) → ( lcm ‘ ( 1 ... 𝑥 ) ) ∈ ℕ )
9 3 5 7 8 syl3anc ⊢ ( 𝑥 ∈ ℕ → ( lcm ‘ ( 1 ... 𝑥 ) ) ∈ ℕ )
10 9 adantl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℕ ) → ( lcm ‘ ( 1 ... 𝑥 ) ) ∈ ℕ )
11 eqid ⊢ ( 𝑥 ∈ ℕ ↦ ( lcm ‘ ( 1 ... 𝑥 ) ) ) = ( 𝑥 ∈ ℕ ↦ ( lcm ‘ ( 1 ... 𝑥 ) ) )
12 10 11 fmptd ⊢ ( 𝑛 ∈ ℕ → ( 𝑥 ∈ ℕ ↦ ( lcm ‘ ( 1 ... 𝑥 ) ) ) : ℕ ⟶ ℕ )
13 nnex ⊢ ℕ ∈ V
14 13 13 pm3.2i ⊢ ( ℕ ∈ V ∧ ℕ ∈ V )
15 elmapg ⊢ ( ( ℕ ∈ V ∧ ℕ ∈ V ) → ( ( 𝑥 ∈ ℕ ↦ ( lcm ‘ ( 1 ... 𝑥 ) ) ) ∈ ( ℕ ↑m ℕ ) ↔ ( 𝑥 ∈ ℕ ↦ ( lcm ‘ ( 1 ... 𝑥 ) ) ) : ℕ ⟶ ℕ ) )
16 14 15 mp1i ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑥 ∈ ℕ ↦ ( lcm ‘ ( 1 ... 𝑥 ) ) ) ∈ ( ℕ ↑m ℕ ) ↔ ( 𝑥 ∈ ℕ ↦ ( lcm ‘ ( 1 ... 𝑥 ) ) ) : ℕ ⟶ ℕ ) )
17 12 16 mpbird ⊢ ( 𝑛 ∈ ℕ → ( 𝑥 ∈ ℕ ↦ ( lcm ‘ ( 1 ... 𝑥 ) ) ) ∈ ( ℕ ↑m ℕ ) )
18 prmgaplcmlem2 ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) → 1 < ( ( ( lcm ‘ ( 1 ... 𝑛 ) ) + 𝑖 ) gcd 𝑖 ) )
19 eqidd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) → ( 𝑥 ∈ ℕ ↦ ( lcm ‘ ( 1 ... 𝑥 ) ) ) = ( 𝑥 ∈ ℕ ↦ ( lcm ‘ ( 1 ... 𝑥 ) ) ) )
20 oveq2 ⊢ ( 𝑥 = 𝑛 → ( 1 ... 𝑥 ) = ( 1 ... 𝑛 ) )
21 20 fveq2d ⊢ ( 𝑥 = 𝑛 → ( lcm ‘ ( 1 ... 𝑥 ) ) = ( lcm ‘ ( 1 ... 𝑛 ) ) )
22 21 adantl ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) ∧ 𝑥 = 𝑛 ) → ( lcm ‘ ( 1 ... 𝑥 ) ) = ( lcm ‘ ( 1 ... 𝑛 ) ) )
23 simpl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) → 𝑛 ∈ ℕ )
24 fzssz ⊢ ( 1 ... 𝑛 ) ⊆ ℤ
25 fzfi ⊢ ( 1 ... 𝑛 ) ∈ Fin
26 24 25 pm3.2i ⊢ ( ( 1 ... 𝑛 ) ⊆ ℤ ∧ ( 1 ... 𝑛 ) ∈ Fin )
27 lcmfcl ⊢ ( ( ( 1 ... 𝑛 ) ⊆ ℤ ∧ ( 1 ... 𝑛 ) ∈ Fin ) → ( lcm ‘ ( 1 ... 𝑛 ) ) ∈ ℕ0 )
28 26 27 mp1i ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) → ( lcm ‘ ( 1 ... 𝑛 ) ) ∈ ℕ0 )
29 19 22 23 28 fvmptd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) → ( ( 𝑥 ∈ ℕ ↦ ( lcm ‘ ( 1 ... 𝑥 ) ) ) ‘ 𝑛 ) = ( lcm ‘ ( 1 ... 𝑛 ) ) )
30 29 oveq1d ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) → ( ( ( 𝑥 ∈ ℕ ↦ ( lcm ‘ ( 1 ... 𝑥 ) ) ) ‘ 𝑛 ) + 𝑖 ) = ( ( lcm ‘ ( 1 ... 𝑛 ) ) + 𝑖 ) )
31 30 oveq1d ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) → ( ( ( ( 𝑥 ∈ ℕ ↦ ( lcm ‘ ( 1 ... 𝑥 ) ) ) ‘ 𝑛 ) + 𝑖 ) gcd 𝑖 ) = ( ( ( lcm ‘ ( 1 ... 𝑛 ) ) + 𝑖 ) gcd 𝑖 ) )
32 18 31 breqtrrd ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) → 1 < ( ( ( ( 𝑥 ∈ ℕ ↦ ( lcm ‘ ( 1 ... 𝑥 ) ) ) ‘ 𝑛 ) + 𝑖 ) gcd 𝑖 ) )
33 32 ralrimiva ⊢ ( 𝑛 ∈ ℕ → ∀ 𝑖 ∈ ( 2 ... 𝑛 ) 1 < ( ( ( ( 𝑥 ∈ ℕ ↦ ( lcm ‘ ( 1 ... 𝑥 ) ) ) ‘ 𝑛 ) + 𝑖 ) gcd 𝑖 ) )
34 1 17 33 prmgaplem8 ⊢ ( 𝑛 ∈ ℕ → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑛 ≤ ( 𝑞 − 𝑝 ) ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) )
35 34 rgen ⊢ ∀ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑛 ≤ ( 𝑞 − 𝑝 ) ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ )