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 ( 𝑁 ∈ ℕ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 ... 𝑁 ) ) )