Metamath Proof Explorer

Theorem prmdvdsprmo

Description: The primorial of a number is divisible by each prime less then or equal to the number. (Contributed by AV, 15-Aug-2020) (Revised by AV, 28-Aug-2020)

Ref Expression
Assertion prmdvdsprmo ( 𝑁 ∈ ℕ → ∀ 𝑝 ∈ ℙ ( 𝑝 ≤ 𝑁 → 𝑝 ∥ ( #p ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
2 diffi ⊢ ( ( 1 ... 𝑁 ) ∈ Fin → ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) ∈ Fin )
3 1 2 mp1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) ∈ Fin )
4 eldifi ⊢ ( 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) → 𝑘 ∈ ( 1 ... 𝑁 ) )
5 elfzelz ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℤ )
6 4 5 syl ⊢ ( 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) → 𝑘 ∈ ℤ )
7 1zzd ⊢ ( 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) → 1 ∈ ℤ )
8 6 7 ifcld ⊢ ( 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℤ )
9 8 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) ∧ 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℤ )
10 3 9 fprodzcl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → ∏ 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℤ )
11 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
12 11 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℤ )
13 12 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → 𝑝 ∈ ℤ )
14 dvdsmul2 ⊢ ( ( ∏ 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℤ ∧ 𝑝 ∈ ℤ ) → 𝑝 ∥ ( ∏ 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · 𝑝 ) )
15 10 13 14 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → 𝑝 ∥ ( ∏ 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · 𝑝 ) )
16 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
17 prmoval ⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
18 16 17 syl ⊢ ( 𝑁 ∈ ℕ → ( #p ‘ 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
19 18 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → ( #p ‘ 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
20 19 breq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → ( 𝑝 ∥ ( #p ‘ 𝑁 ) ↔ 𝑝 ∥ ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ) )
21 neldifsnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → ¬ 𝑝 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) )
22 disjsn ⊢ ( ( ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) ∩ { 𝑝 } ) = ∅ ↔ ¬ 𝑝 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) )
23 21 22 sylibr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → ( ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) ∩ { 𝑝 } ) = ∅ )
24 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
25 24 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℕ )
26 25 anim1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → ( 𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑁 ) )
27 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
28 fznn ⊢ ( 𝑁 ∈ ℤ → ( 𝑝 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑁 ) ) )
29 27 28 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝑝 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑁 ) ) )
30 29 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → ( 𝑝 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝑁 ) ) )
31 26 30 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → 𝑝 ∈ ( 1 ... 𝑁 ) )
32 difsnid ⊢ ( 𝑝 ∈ ( 1 ... 𝑁 ) → ( ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) ∪ { 𝑝 } ) = ( 1 ... 𝑁 ) )
33 32 eqcomd ⊢ ( 𝑝 ∈ ( 1 ... 𝑁 ) → ( 1 ... 𝑁 ) = ( ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) ∪ { 𝑝 } ) )
34 31 33 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → ( 1 ... 𝑁 ) = ( ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) ∪ { 𝑝 } ) )
35 fzfid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → ( 1 ... 𝑁 ) ∈ Fin )
36 1zzd ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 1 ∈ ℤ )
37 5 36 ifcld ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℤ )
38 37 zcnd ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℂ )
39 38 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℂ )
40 23 34 35 39 fprodsplit ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = ( ∏ 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · ∏ 𝑘 ∈ { 𝑝 } if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ) )
41 simplr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → 𝑝 ∈ ℙ )
42 25 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → 𝑝 ∈ ℕ )
43 42 nncnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → 𝑝 ∈ ℂ )
44 1cnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → 1 ∈ ℂ )
45 43 44 ifcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → if ( 𝑝 ∈ ℙ , 𝑝 , 1 ) ∈ ℂ )
46 eleq1w ⊢ ( 𝑘 = 𝑝 → ( 𝑘 ∈ ℙ ↔ 𝑝 ∈ ℙ ) )
47 id ⊢ ( 𝑘 = 𝑝 → 𝑘 = 𝑝 )
48 46 47 ifbieq1d ⊢ ( 𝑘 = 𝑝 → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = if ( 𝑝 ∈ ℙ , 𝑝 , 1 ) )
49 48 prodsn ⊢ ( ( 𝑝 ∈ ℙ ∧ if ( 𝑝 ∈ ℙ , 𝑝 , 1 ) ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑝 } if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = if ( 𝑝 ∈ ℙ , 𝑝 , 1 ) )
50 41 45 49 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → ∏ 𝑘 ∈ { 𝑝 } if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = if ( 𝑝 ∈ ℙ , 𝑝 , 1 ) )
51 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
52 51 iftrued ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → if ( 𝑝 ∈ ℙ , 𝑝 , 1 ) = 𝑝 )
53 52 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → if ( 𝑝 ∈ ℙ , 𝑝 , 1 ) = 𝑝 )
54 50 53 eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → ∏ 𝑘 ∈ { 𝑝 } if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 𝑝 )
55 54 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → ( ∏ 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · ∏ 𝑘 ∈ { 𝑝 } if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ) = ( ∏ 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · 𝑝 ) )
56 40 55 eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = ( ∏ 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · 𝑝 ) )
57 56 breq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → ( 𝑝 ∥ ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ↔ 𝑝 ∥ ( ∏ 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · 𝑝 ) ) )
58 20 57 bitrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → ( 𝑝 ∥ ( #p ‘ 𝑁 ) ↔ 𝑝 ∥ ( ∏ 𝑘 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑝 } ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) · 𝑝 ) ) )
59 15 58 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ 𝑁 ) → 𝑝 ∥ ( #p ‘ 𝑁 ) )
60 59 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ≤ 𝑁 → 𝑝 ∥ ( #p ‘ 𝑁 ) ) )
61 60 ralrimiva ⊢ ( 𝑁 ∈ ℕ → ∀ 𝑝 ∈ ℙ ( 𝑝 ≤ 𝑁 → 𝑝 ∥ ( #p ‘ 𝑁 ) ) )