Theorem prmolelcmf

Description: The primorial of a positive integer is less than or equal to 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	prmolelcmf	$$⊢N\in {\mathbb{N}}_0\to {\#}_p\left(N\right)\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		prmocl	$$⊢N\in {\mathbb{N}}_0\to {\#}_p\left(N\right)\in \mathbb{N}$$
2	1	nnzd	$$⊢N\in {\mathbb{N}}_0\to {\#}_p\left(N\right)\in \mathbb{Z}$$
3		fzssz	$$⊢\left(1\dots N\right)\subseteq \mathbb{Z}$$
4		fzfid	$$⊢N\in {\mathbb{N}}_0\to \left(1\dots N\right)\in \mathrm{Fin}$$
5		0nelfz1	$$⊢0\notin \left(1\dots N\right)$$
6	5	a1i	$$⊢N\in {\mathbb{N}}_0\to 0\notin \left(1\dots N\right)$$
7		lcmfn0cl	$$⊢\left(\left(1\dots N\right)\subseteq \mathbb{Z}\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 \mathbb{N}$$
8	3 4 6 7	mp3an2i	$$⊢N\in {\mathbb{N}}_0\to \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\in \mathbb{N}$$
9	2 8	jca	$$⊢N\in {\mathbb{N}}_0\to \left({\#}_p\left(N\right)\in \mathbb{Z}\wedge \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\in \mathbb{N}\right)$$
10		prmodvdslcmf	$$⊢N\in {\mathbb{N}}_0\to {\#}_p\left(N\right)\parallel \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$
11		dvdsle	$$⊢\left({\#}_p\left(N\right)\in \mathbb{Z}\wedge \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\in \mathbb{N}\right)\to \left({\#}_p\left(N\right)\parallel \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\to {\#}_p\left(N\right)\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)\right)$$
12	9 10 11	sylc	$$⊢N\in {\mathbb{N}}_0\to {\#}_p\left(N\right)\le \underset{\_}{\mathrm{lcm}}\left(\left(1\dots N\right)\right)$$