Theorem prmo5

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

	Ref	Expression
Assertion	prmo5	⊢ ( #p ‘ 5 ) = ; 3 0

Proof

Step	Hyp	Ref	Expression
1		5nn	⊢ 5 ∈ ℕ
2		prmonn2	⊢ ( 5 ∈ ℕ → ( #p ‘ 5 ) = if ( 5 ∈ ℙ , ( ( #p ‘ ( 5 − 1 ) ) · 5 ) , ( #p ‘ ( 5 − 1 ) ) ) )
3	1 2	ax-mp	⊢ ( #p ‘ 5 ) = if ( 5 ∈ ℙ , ( ( #p ‘ ( 5 − 1 ) ) · 5 ) , ( #p ‘ ( 5 − 1 ) ) )
4		5prm	⊢ 5 ∈ ℙ
5	4	iftruei	⊢ if ( 5 ∈ ℙ , ( ( #p ‘ ( 5 − 1 ) ) · 5 ) , ( #p ‘ ( 5 − 1 ) ) ) = ( ( #p ‘ ( 5 − 1 ) ) · 5 )
6		5m1e4	⊢ ( 5 − 1 ) = 4
7	6	fveq2i	⊢ ( #p ‘ ( 5 − 1 ) ) = ( #p ‘ 4 )
8		prmo4	⊢ ( #p ‘ 4 ) = 6
9	7 8	eqtri	⊢ ( #p ‘ ( 5 − 1 ) ) = 6
10	9	oveq1i	⊢ ( ( #p ‘ ( 5 − 1 ) ) · 5 ) = ( 6 · 5 )
11		6t5e30	⊢ ( 6 · 5 ) = ; 3 0
12	10 11	eqtri	⊢ ( ( #p ‘ ( 5 − 1 ) ) · 5 ) = ; 3 0
13	5 12	eqtri	⊢ if ( 5 ∈ ℙ , ( ( #p ‘ ( 5 − 1 ) ) · 5 ) , ( #p ‘ ( 5 − 1 ) ) ) = ; 3 0
14	3 13	eqtri	⊢ ( #p ‘ 5 ) = ; 3 0