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} (N) \leq N!$

Proof

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

Metamath Proof Explorer

Theorem prmolefac

Proof