Metamath Proof Explorer

Theorem prmolefac

Description: The primorial of a positive integer is less than or equal to the factorial of the integer. (Contributed by AV, 15-Aug-2020) (Revised by AV, 29-Aug-2020)

Ref Expression
Assertion prmolefac ${⊢}{N}\in {ℕ}_{0}\to {#}_{p}\left({N}\right)\le {N}!$

Proof

Step Hyp Ref Expression
1 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{N}\in {ℕ}_{0}$
2 fzfid ${⊢}{N}\in {ℕ}_{0}\to \left(1\dots {N}\right)\in \mathrm{Fin}$
3 elfznn ${⊢}{k}\in \left(1\dots {N}\right)\to {k}\in ℕ$
4 3 adantl ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to {k}\in ℕ$
5 1nn ${⊢}1\in ℕ$
6 5 a1i ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to 1\in ℕ$
7 4 6 ifcld ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to if\left({k}\in ℙ,{k},1\right)\in ℕ$
8 7 nnred ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to if\left({k}\in ℙ,{k},1\right)\in ℝ$
9 ifeqor ${⊢}\left(if\left({k}\in ℙ,{k},1\right)={k}\vee if\left({k}\in ℙ,{k},1\right)=1\right)$
10 nnnn0 ${⊢}{k}\in ℕ\to {k}\in {ℕ}_{0}$
11 10 nn0ge0d ${⊢}{k}\in ℕ\to 0\le {k}$
12 3 11 syl ${⊢}{k}\in \left(1\dots {N}\right)\to 0\le {k}$
13 12 adantl ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to 0\le {k}$
14 breq2 ${⊢}if\left({k}\in ℙ,{k},1\right)={k}\to \left(0\le if\left({k}\in ℙ,{k},1\right)↔0\le {k}\right)$
15 13 14 syl5ibr ${⊢}if\left({k}\in ℙ,{k},1\right)={k}\to \left(\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to 0\le if\left({k}\in ℙ,{k},1\right)\right)$
16 0le1 ${⊢}0\le 1$
17 breq2 ${⊢}if\left({k}\in ℙ,{k},1\right)=1\to \left(0\le if\left({k}\in ℙ,{k},1\right)↔0\le 1\right)$
18 17 adantr ${⊢}\left(if\left({k}\in ℙ,{k},1\right)=1\wedge \left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\right)\to \left(0\le if\left({k}\in ℙ,{k},1\right)↔0\le 1\right)$
19 16 18 mpbiri ${⊢}\left(if\left({k}\in ℙ,{k},1\right)=1\wedge \left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\right)\to 0\le if\left({k}\in ℙ,{k},1\right)$
20 19 ex ${⊢}if\left({k}\in ℙ,{k},1\right)=1\to \left(\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to 0\le if\left({k}\in ℙ,{k},1\right)\right)$
21 15 20 jaoi ${⊢}\left(if\left({k}\in ℙ,{k},1\right)={k}\vee if\left({k}\in ℙ,{k},1\right)=1\right)\to \left(\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to 0\le if\left({k}\in ℙ,{k},1\right)\right)$
22 9 21 ax-mp ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to 0\le if\left({k}\in ℙ,{k},1\right)$
23 4 nnred ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to {k}\in ℝ$
24 23 leidd ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to {k}\le {k}$
25 breq1 ${⊢}if\left({k}\in ℙ,{k},1\right)={k}\to \left(if\left({k}\in ℙ,{k},1\right)\le {k}↔{k}\le {k}\right)$
26 24 25 syl5ibr ${⊢}if\left({k}\in ℙ,{k},1\right)={k}\to \left(\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to if\left({k}\in ℙ,{k},1\right)\le {k}\right)$
27 4 nnge1d ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to 1\le {k}$
28 breq1 ${⊢}if\left({k}\in ℙ,{k},1\right)=1\to \left(if\left({k}\in ℙ,{k},1\right)\le {k}↔1\le {k}\right)$
29 27 28 syl5ibr ${⊢}if\left({k}\in ℙ,{k},1\right)=1\to \left(\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to if\left({k}\in ℙ,{k},1\right)\le {k}\right)$
30 26 29 jaoi ${⊢}\left(if\left({k}\in ℙ,{k},1\right)={k}\vee if\left({k}\in ℙ,{k},1\right)=1\right)\to \left(\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to if\left({k}\in ℙ,{k},1\right)\le {k}\right)$
31 9 30 ax-mp ${⊢}\left({N}\in {ℕ}_{0}\wedge {k}\in \left(1\dots {N}\right)\right)\to if\left({k}\in ℙ,{k},1\right)\le {k}$
32 1 2 8 22 23 31 fprodle ${⊢}{N}\in {ℕ}_{0}\to \prod _{{k}=1}^{{N}}if\left({k}\in ℙ,{k},1\right)\le \prod _{{k}=1}^{{N}}{k}$
33 prmoval ${⊢}{N}\in {ℕ}_{0}\to {#}_{p}\left({N}\right)=\prod _{{k}=1}^{{N}}if\left({k}\in ℙ,{k},1\right)$
34 fprodfac ${⊢}{N}\in {ℕ}_{0}\to {N}!=\prod _{{k}=1}^{{N}}{k}$
35 32 33 34 3brtr4d ${⊢}{N}\in {ℕ}_{0}\to {#}_{p}\left({N}\right)\le {N}!$