Theorem prmo3

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

	Ref	Expression
Assertion	prmo3	⊢ ( #p ‘ 3 ) = 6

Proof

Step	Hyp	Ref	Expression
1		3nn	⊢ 3 ∈ ℕ
2		prmonn2	⊢ ( 3 ∈ ℕ → ( #p ‘ 3 ) = if ( 3 ∈ ℙ , ( ( #p ‘ ( 3 − 1 ) ) · 3 ) , ( #p ‘ ( 3 − 1 ) ) ) )
3	1 2	ax-mp	⊢ ( #p ‘ 3 ) = if ( 3 ∈ ℙ , ( ( #p ‘ ( 3 − 1 ) ) · 3 ) , ( #p ‘ ( 3 − 1 ) ) )
4		3prm	⊢ 3 ∈ ℙ
5	4	iftruei	⊢ if ( 3 ∈ ℙ , ( ( #p ‘ ( 3 − 1 ) ) · 3 ) , ( #p ‘ ( 3 − 1 ) ) ) = ( ( #p ‘ ( 3 − 1 ) ) · 3 )
6		3m1e2	⊢ ( 3 − 1 ) = 2
7	6	fveq2i	⊢ ( #p ‘ ( 3 − 1 ) ) = ( #p ‘ 2 )
8		prmo2	⊢ ( #p ‘ 2 ) = 2
9	7 8	eqtri	⊢ ( #p ‘ ( 3 − 1 ) ) = 2
10	9	oveq1i	⊢ ( ( #p ‘ ( 3 − 1 ) ) · 3 ) = ( 2 · 3 )
11		3cn	⊢ 3 ∈ ℂ
12		2cn	⊢ 2 ∈ ℂ
13		3t2e6	⊢ ( 3 · 2 ) = 6
14	11 12 13	mulcomli	⊢ ( 2 · 3 ) = 6
15	10 14	eqtri	⊢ ( ( #p ‘ ( 3 − 1 ) ) · 3 ) = 6
16	5 15	eqtri	⊢ if ( 3 ∈ ℙ , ( ( #p ‘ ( 3 − 1 ) ) · 3 ) , ( #p ‘ ( 3 − 1 ) ) ) = 6
17	3 16	eqtri	⊢ ( #p ‘ 3 ) = 6