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	⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) ≤ ( ! ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑘 𝑁 ∈ ℕ0
2		fzfid	⊢ ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) ∈ Fin )
3		elfznn	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ )
4	3	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℕ )
5		1nn	⊢ 1 ∈ ℕ
6	5	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ℕ )
7	4 6	ifcld	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℕ )
8	7	nnred	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ∈ ℝ )
9		ifeqor	⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 𝑘 ∨ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 )
10		nnnn0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
11	10	nn0ge0d	⊢ ( 𝑘 ∈ ℕ → 0 ≤ 𝑘 )
12	3 11	syl	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 0 ≤ 𝑘 )
13	12	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 0 ≤ 𝑘 )
14		breq2	⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 𝑘 → ( 0 ≤ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ↔ 0 ≤ 𝑘 ) )
15	13 14	syl5ibr	⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 𝑘 → ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 0 ≤ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ) )
16		0le1	⊢ 0 ≤ 1
17		breq2	⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 → ( 0 ≤ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ↔ 0 ≤ 1 ) )
18	17	adantr	⊢ ( ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ) → ( 0 ≤ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ↔ 0 ≤ 1 ) )
19	16 18	mpbiri	⊢ ( ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ) → 0 ≤ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
20	19	ex	⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 → ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 0 ≤ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ) )
21	15 20	jaoi	⊢ ( ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 𝑘 ∨ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 0 ≤ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ) )
22	9 21	ax-mp	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 0 ≤ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
23	4	nnred	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℝ )
24	23	leidd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ≤ 𝑘 )
25		breq1	⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 𝑘 → ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ≤ 𝑘 ↔ 𝑘 ≤ 𝑘 ) )
26	24 25	syl5ibr	⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 𝑘 → ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ≤ 𝑘 ) )
27	4	nnge1d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 1 ≤ 𝑘 )
28		breq1	⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 → ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ≤ 𝑘 ↔ 1 ≤ 𝑘 ) )
29	27 28	syl5ibr	⊢ ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 → ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ≤ 𝑘 ) )
30	26 29	jaoi	⊢ ( ( if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 𝑘 ∨ if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) = 1 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ≤ 𝑘 ) )
31	9 30	ax-mp	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ≤ 𝑘 )
32	1 2 8 22 23 31	fprodle	⊢ ( 𝑁 ∈ ℕ0 → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) ≤ ∏ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 )
33		prmoval	⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) if ( 𝑘 ∈ ℙ , 𝑘 , 1 ) )
34		fprodfac	⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 )
35	32 33 34	3brtr4d	⊢ ( 𝑁 ∈ ℕ0 → ( #p ‘ 𝑁 ) ≤ ( ! ‘ 𝑁 ) )