Theorem lcmflefac

Description: The least common multiple of all positive integers less than or equal to an integer is less than or equal to the factorial of the integer. (Contributed by AV, 16-Aug-2020) (Revised by AV, 27-Aug-2020)

	Ref	Expression
Assertion	lcmflefac	⊢ ( 𝑁 ∈ ℕ → ( lcm ‘ ( 1 ... 𝑁 ) ) ≤ ( ! ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		fzssz	⊢ ( 1 ... 𝑁 ) ⊆ ℤ
2	1	a1i	⊢ ( 𝑁 ∈ ℕ → ( 1 ... 𝑁 ) ⊆ ℤ )
3		fzfid	⊢ ( 𝑁 ∈ ℕ → ( 1 ... 𝑁 ) ∈ Fin )
4		0nelfz1	⊢ 0 ∉ ( 1 ... 𝑁 )
5	4	a1i	⊢ ( 𝑁 ∈ ℕ → 0 ∉ ( 1 ... 𝑁 ) )
6	2 3 5	3jca	⊢ ( 𝑁 ∈ ℕ → ( ( 1 ... 𝑁 ) ⊆ ℤ ∧ ( 1 ... 𝑁 ) ∈ Fin ∧ 0 ∉ ( 1 ... 𝑁 ) ) )
7		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
8	7	faccld	⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℕ )
9		elfznn	⊢ ( 𝑚 ∈ ( 1 ... 𝑁 ) → 𝑚 ∈ ℕ )
10		elfzuz3	⊢ ( 𝑚 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑚 ) )
11	10	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑚 ) )
12		dvdsfac	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑚 ) ) → 𝑚 ∥ ( ! ‘ 𝑁 ) )
13	9 11 12	syl2an2	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → 𝑚 ∥ ( ! ‘ 𝑁 ) )
14	13	ralrimiva	⊢ ( 𝑁 ∈ ℕ → ∀ 𝑚 ∈ ( 1 ... 𝑁 ) 𝑚 ∥ ( ! ‘ 𝑁 ) )
15	8 14	jca	⊢ ( 𝑁 ∈ ℕ → ( ( ! ‘ 𝑁 ) ∈ ℕ ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) 𝑚 ∥ ( ! ‘ 𝑁 ) ) )
16		lcmfledvds	⊢ ( ( ( 1 ... 𝑁 ) ⊆ ℤ ∧ ( 1 ... 𝑁 ) ∈ Fin ∧ 0 ∉ ( 1 ... 𝑁 ) ) → ( ( ( ! ‘ 𝑁 ) ∈ ℕ ∧ ∀ 𝑚 ∈ ( 1 ... 𝑁 ) 𝑚 ∥ ( ! ‘ 𝑁 ) ) → ( lcm ‘ ( 1 ... 𝑁 ) ) ≤ ( ! ‘ 𝑁 ) ) )
17	6 15 16	sylc	⊢ ( 𝑁 ∈ ℕ → ( lcm ‘ ( 1 ... 𝑁 ) ) ≤ ( ! ‘ 𝑁 ) )