Theorem prmo2

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

	Ref	Expression
Assertion	prmo2	⊢ ( #p ‘ 2 ) = 2

Proof

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