Theorem prmo4

Description: The primorial of 4. (Contributed by AV, 28-Aug-2020)

	Ref	Expression
Assertion	prmo4	⊢ ( #p ‘ 4 ) = 6

Proof

Step	Hyp	Ref	Expression
1		4nn	⊢ 4 ∈ ℕ
2		prmonn2	⊢ ( 4 ∈ ℕ → ( #p ‘ 4 ) = if ( 4 ∈ ℙ , ( ( #p ‘ ( 4 − 1 ) ) · 4 ) , ( #p ‘ ( 4 − 1 ) ) ) )
3	1 2	ax-mp	⊢ ( #p ‘ 4 ) = if ( 4 ∈ ℙ , ( ( #p ‘ ( 4 − 1 ) ) · 4 ) , ( #p ‘ ( 4 − 1 ) ) )
4		4nprm	⊢ ¬ 4 ∈ ℙ
5	4	iffalsei	⊢ if ( 4 ∈ ℙ , ( ( #p ‘ ( 4 − 1 ) ) · 4 ) , ( #p ‘ ( 4 − 1 ) ) ) = ( #p ‘ ( 4 − 1 ) )
6	3 5	eqtri	⊢ ( #p ‘ 4 ) = ( #p ‘ ( 4 − 1 ) )
7		4m1e3	⊢ ( 4 − 1 ) = 3
8	7	fveq2i	⊢ ( #p ‘ ( 4 − 1 ) ) = ( #p ‘ 3 )
9		prmo3	⊢ ( #p ‘ 3 ) = 6
10	8 9	eqtri	⊢ ( #p ‘ ( 4 − 1 ) ) = 6
11	6 10	eqtri	⊢ ( #p ‘ 4 ) = 6