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	⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		prmocl	⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) ∈ ℕ )
2	1	nnzd	⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) ∈ ℤ )
3		fzssz	⊢ ( 1 ... 𝑁 ) ⊆ ℤ
4		fzfid	⊢ ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) ∈ Fin )
5		0nelfz1	⊢ 0 ∉ ( 1 ... 𝑁 )
6	5	a1i	⊢ ( 𝑁 ∈ ℕ0 → 0 ∉ ( 1 ... 𝑁 ) )
7		lcmfn0cl	⊢ ( ( ( 1 ... 𝑁 ) ⊆ ℤ ∧ ( 1 ... 𝑁 ) ∈ Fin ∧ 0 ∉ ( 1 ... 𝑁 ) ) → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ )
8	3 4 6 7	mp3an2i	⊢ ( 𝑁 ∈ ℕ0 → ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ )
9	2 8	jca	⊢ ( 𝑁 ∈ ℕ0 → ( ( #p ‘ 𝑁 ) ∈ ℤ ∧ ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ ) )
10		prmodvdslcmf	⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) )
11		dvdsle	⊢ ( ( ( #p ‘ 𝑁 ) ∈ ℤ ∧ ( lcm ‘ ( 1 ... 𝑁 ) ) ∈ ℕ ) → ( ( #p ‘ 𝑁 ) ∥ ( lcm ‘ ( 1 ... 𝑁 ) ) → ( #p ‘ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) ) )
12	9 10 11	sylc	⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) ≤ ( lcm ‘ ( 1 ... 𝑁 ) ) )