# Metamath Proof Explorer

## Theorem prmodvdslcmf

Description: The primorial of a nonnegative integer divides the least common multiple of all positive integers less than or equal to the integer. (Contributed by AV, 19-Aug-2020) (Revised by AV, 29-Aug-2020)

Ref Expression
Assertion prmodvdslcmf ${⊢}{N}\in {ℕ}_{0}\to {#}_{p}\left({N}\right)\parallel \underset{_}{\mathrm{lcm}}\left(\left(1\dots {N}\right)\right)$

### Proof

Step Hyp Ref Expression
1 prmoval ${⊢}{N}\in {ℕ}_{0}\to {#}_{p}\left({N}\right)=\prod _{{k}=1}^{{N}}if\left({k}\in ℙ,{k},1\right)$
2 eqidd ${⊢}{k}\in \left(1\dots {N}\right)\to \left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)=\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)$
3 simpr ${⊢}\left({k}\in \left(1\dots {N}\right)\wedge {m}={k}\right)\to {m}={k}$
4 3 eleq1d ${⊢}\left({k}\in \left(1\dots {N}\right)\wedge {m}={k}\right)\to \left({m}\in ℙ↔{k}\in ℙ\right)$
5 4 3 ifbieq1d ${⊢}\left({k}\in \left(1\dots {N}\right)\wedge {m}={k}\right)\to if\left({m}\in ℙ,{m},1\right)=if\left({k}\in ℙ,{k},1\right)$
6 elfznn ${⊢}{k}\in \left(1\dots {N}\right)\to {k}\in ℕ$
7 1nn ${⊢}1\in ℕ$
8 7 a1i ${⊢}{k}\in \left(1\dots {N}\right)\to 1\in ℕ$
9 6 8 ifcld ${⊢}{k}\in \left(1\dots {N}\right)\to if\left({k}\in ℙ,{k},1\right)\in ℕ$
10 2 5 6 9 fvmptd ${⊢}{k}\in \left(1\dots {N}\right)\to \left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({k}\right)=if\left({k}\in ℙ,{k},1\right)$
11 10 eqcomd ${⊢}{k}\in \left(1\dots {N}\right)\to if\left({k}\in ℙ,{k},1\right)=\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({k}\right)$
12 11 prodeq2i ${⊢}\prod _{{k}=1}^{{N}}if\left({k}\in ℙ,{k},1\right)=\prod _{{k}=1}^{{N}}\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({k}\right)$
13 1 12 syl6eq ${⊢}{N}\in {ℕ}_{0}\to {#}_{p}\left({N}\right)=\prod _{{k}=1}^{{N}}\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({k}\right)$
14 fzfid ${⊢}{N}\in {ℕ}_{0}\to \left(1\dots {N}\right)\in \mathrm{Fin}$
15 fz1ssnn ${⊢}\left(1\dots {N}\right)\subseteq ℕ$
16 14 15 jctil ${⊢}{N}\in {ℕ}_{0}\to \left(\left(1\dots {N}\right)\subseteq ℕ\wedge \left(1\dots {N}\right)\in \mathrm{Fin}\right)$
17 fzssz ${⊢}\left(1\dots {N}\right)\subseteq ℤ$
18 17 a1i ${⊢}{N}\in {ℕ}_{0}\to \left(1\dots {N}\right)\subseteq ℤ$
19 0nelfz1 ${⊢}0\notin \left(1\dots {N}\right)$
20 19 a1i ${⊢}{N}\in {ℕ}_{0}\to 0\notin \left(1\dots {N}\right)$
21 lcmfn0cl ${⊢}\left(\left(1\dots {N}\right)\subseteq ℤ\wedge \left(1\dots {N}\right)\in \mathrm{Fin}\wedge 0\notin \left(1\dots {N}\right)\right)\to \underset{_}{\mathrm{lcm}}\left(\left(1\dots {N}\right)\right)\in ℕ$
22 18 14 20 21 syl3anc ${⊢}{N}\in {ℕ}_{0}\to \underset{_}{\mathrm{lcm}}\left(\left(1\dots {N}\right)\right)\in ℕ$
23 id ${⊢}{m}\in ℕ\to {m}\in ℕ$
24 7 a1i ${⊢}{m}\in ℕ\to 1\in ℕ$
25 23 24 ifcld ${⊢}{m}\in ℕ\to if\left({m}\in ℙ,{m},1\right)\in ℕ$
26 25 adantl ${⊢}\left({N}\in {ℕ}_{0}\wedge {m}\in ℕ\right)\to if\left({m}\in ℙ,{m},1\right)\in ℕ$
27 26 fmpttd ${⊢}{N}\in {ℕ}_{0}\to \left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right):ℕ⟶ℕ$
28 simpr ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to {k}\in \left(1\dots {N}\right)$
29 28 adantr ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\wedge {x}\in \left(\left(1\dots {N}\right)\setminus \left\{{k}\right\}\right)\right)\to {k}\in \left(1\dots {N}\right)$
30 eldifi ${⊢}{x}\in \left(\left(1\dots {N}\right)\setminus \left\{{k}\right\}\right)\to {x}\in \left(1\dots {N}\right)$
31 30 adantl ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\wedge {x}\in \left(\left(1\dots {N}\right)\setminus \left\{{k}\right\}\right)\right)\to {x}\in \left(1\dots {N}\right)$
32 eldif ${⊢}{x}\in \left(\left(1\dots {N}\right)\setminus \left\{{k}\right\}\right)↔\left({x}\in \left(1\dots {N}\right)\wedge ¬{x}\in \left\{{k}\right\}\right)$
33 velsn ${⊢}{x}\in \left\{{k}\right\}↔{x}={k}$
34 33 biimpri ${⊢}{x}={k}\to {x}\in \left\{{k}\right\}$
35 34 equcoms ${⊢}{k}={x}\to {x}\in \left\{{k}\right\}$
36 35 necon3bi ${⊢}¬{x}\in \left\{{k}\right\}\to {k}\ne {x}$
37 32 36 simplbiim ${⊢}{x}\in \left(\left(1\dots {N}\right)\setminus \left\{{k}\right\}\right)\to {k}\ne {x}$
38 37 adantl ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\wedge {x}\in \left(\left(1\dots {N}\right)\setminus \left\{{k}\right\}\right)\right)\to {k}\ne {x}$
39 eqid ${⊢}\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)=\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)$
40 39 fvprmselgcd1 ${⊢}\left({k}\in \left(1\dots {N}\right)\wedge {x}\in \left(1\dots {N}\right)\wedge {k}\ne {x}\right)\to \left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({k}\right)\mathrm{gcd}\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({x}\right)=1$
41 29 31 38 40 syl3anc ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\wedge {x}\in \left(\left(1\dots {N}\right)\setminus \left\{{k}\right\}\right)\right)\to \left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({k}\right)\mathrm{gcd}\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({x}\right)=1$
42 41 ralrimiva ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to \forall {x}\in \left(\left(1\dots {N}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({k}\right)\mathrm{gcd}\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({x}\right)=1$
43 42 ralrimiva ${⊢}{N}\in {ℕ}_{0}\to \forall {k}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in \left(\left(1\dots {N}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({k}\right)\mathrm{gcd}\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({x}\right)=1$
44 eqidd ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to \left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)=\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)$
45 simpr ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\wedge {m}={k}\right)\to {m}={k}$
46 45 eleq1d ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\wedge {m}={k}\right)\to \left({m}\in ℙ↔{k}\in ℙ\right)$
47 46 45 ifbieq1d ${⊢}\left(\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\wedge {m}={k}\right)\to if\left({m}\in ℙ,{m},1\right)=if\left({k}\in ℙ,{k},1\right)$
48 15 28 sseldi ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to {k}\in ℕ$
49 17 28 sseldi ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to {k}\in ℤ$
50 1zzd ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to 1\in ℤ$
51 49 50 ifcld ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to if\left({k}\in ℙ,{k},1\right)\in ℤ$
52 44 47 48 51 fvmptd ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to \left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({k}\right)=if\left({k}\in ℙ,{k},1\right)$
53 breq1 ${⊢}{x}=if\left({k}\in ℙ,{k},1\right)\to \left({x}\parallel \underset{_}{\mathrm{lcm}}\left(\left(1\dots {N}\right)\right)↔if\left({k}\in ℙ,{k},1\right)\parallel \underset{_}{\mathrm{lcm}}\left(\left(1\dots {N}\right)\right)\right)$
54 16 adantr ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to \left(\left(1\dots {N}\right)\subseteq ℕ\wedge \left(1\dots {N}\right)\in \mathrm{Fin}\right)$
55 17 2a1i ${⊢}\left(1\dots {N}\right)\in \mathrm{Fin}\to \left(\left(1\dots {N}\right)\subseteq ℕ\to \left(1\dots {N}\right)\subseteq ℤ\right)$
56 55 imdistanri ${⊢}\left(\left(1\dots {N}\right)\subseteq ℕ\wedge \left(1\dots {N}\right)\in \mathrm{Fin}\right)\to \left(\left(1\dots {N}\right)\subseteq ℤ\wedge \left(1\dots {N}\right)\in \mathrm{Fin}\right)$
57 dvdslcmf ${⊢}\left(\left(1\dots {N}\right)\subseteq ℤ\wedge \left(1\dots {N}\right)\in \mathrm{Fin}\right)\to \forall {x}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\parallel \underset{_}{\mathrm{lcm}}\left(\left(1\dots {N}\right)\right)$
58 54 56 57 3syl ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to \forall {x}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{x}\parallel \underset{_}{\mathrm{lcm}}\left(\left(1\dots {N}\right)\right)$
59 elfzuz2 ${⊢}{k}\in \left(1\dots {N}\right)\to {N}\in {ℤ}_{\ge 1}$
60 59 adantl ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to {N}\in {ℤ}_{\ge 1}$
61 eluzfz1 ${⊢}{N}\in {ℤ}_{\ge 1}\to 1\in \left(1\dots {N}\right)$
62 60 61 syl ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to 1\in \left(1\dots {N}\right)$
63 28 62 ifcld ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to if\left({k}\in ℙ,{k},1\right)\in \left(1\dots {N}\right)$
64 53 58 63 rspcdva ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to if\left({k}\in ℙ,{k},1\right)\parallel \underset{_}{\mathrm{lcm}}\left(\left(1\dots {N}\right)\right)$
65 52 64 eqbrtrd ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to \left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({k}\right)\parallel \underset{_}{\mathrm{lcm}}\left(\left(1\dots {N}\right)\right)$
66 65 ralrimiva ${⊢}{N}\in {ℕ}_{0}\to \forall {k}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({k}\right)\parallel \underset{_}{\mathrm{lcm}}\left(\left(1\dots {N}\right)\right)$
67 coprmproddvds ${⊢}\left(\left(\left(1\dots {N}\right)\subseteq ℕ\wedge \left(1\dots {N}\right)\in \mathrm{Fin}\right)\wedge \left(\underset{_}{\mathrm{lcm}}\left(\left(1\dots {N}\right)\right)\in ℕ\wedge \left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right):ℕ⟶ℕ\right)\wedge \left(\forall {k}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in \left(\left(1\dots {N}\right)\setminus \left\{{k}\right\}\right)\phantom{\rule{.4em}{0ex}}\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({k}\right)\mathrm{gcd}\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({x}\right)=1\wedge \forall {k}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({k}\right)\parallel \underset{_}{\mathrm{lcm}}\left(\left(1\dots {N}\right)\right)\right)\right)\to \prod _{{k}=1}^{{N}}\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({k}\right)\parallel \underset{_}{\mathrm{lcm}}\left(\left(1\dots {N}\right)\right)$
68 16 22 27 43 66 67 syl122anc ${⊢}{N}\in {ℕ}_{0}\to \prod _{{k}=1}^{{N}}\left({m}\in ℕ⟼if\left({m}\in ℙ,{m},1\right)\right)\left({k}\right)\parallel \underset{_}{\mathrm{lcm}}\left(\left(1\dots {N}\right)\right)$
69 13 68 eqbrtrd ${⊢}{N}\in {ℕ}_{0}\to {#}_{p}\left({N}\right)\parallel \underset{_}{\mathrm{lcm}}\left(\left(1\dots {N}\right)\right)$