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

Metamath Proof Explorer

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 ... 𝑁 ) ) ≤ ( ! ‘ 𝑁 ) )