This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ℕ_{0} \to #_{p} (N) \leq \underline{lcm} ((1 \dots N))$

Proof

Step	Hyp	Ref	Expression
1		prmocl	$⊢ N \in ℕ_{0} \to #_{p} (N) \in ℕ$
2	1	nnzd	$⊢ N \in ℕ_{0} \to #_{p} (N) \in ℤ$
3		fzssz	$⊢ (1 \dots N) \subseteq ℤ$
4		fzfid	$⊢ N \in ℕ_{0} \to (1 \dots N) \in Fin$
5		0nelfz1	$⊢ 0 \notin (1 \dots N)$
6	5	a1i	$⊢ N \in ℕ_{0} \to 0 \notin (1 \dots N)$
7		lcmfn0cl	$⊢ ((1 \dots N) \subseteq ℤ \land (1 \dots N) \in Fin \land 0 \notin (1 \dots N)) \to \underline{lcm} ((1 \dots N)) \in ℕ$
8	3 4 6 7	mp3an2i	$⊢ N \in ℕ_{0} \to \underline{lcm} ((1 \dots N)) \in ℕ$
9	2 8	jca	$⊢ N \in ℕ_{0} \to (#_{p} (N) \in ℤ \land \underline{lcm} ((1 \dots N)) \in ℕ)$
10		prmodvdslcmf	$⊢ N \in ℕ_{0} \to #_{p} (N) ∥ \underline{lcm} ((1 \dots N))$
11		dvdsle	$⊢ (#_{p} (N) \in ℤ \land \underline{lcm} ((1 \dots N)) \in ℕ) \to (#_{p} (N) ∥ \underline{lcm} ((1 \dots N)) \to #_{p} (N) \leq \underline{lcm} ((1 \dots N)))$
12	9 10 11	sylc	$⊢ N \in ℕ_{0} \to #_{p} (N) \leq \underline{lcm} ((1 \dots N))$