This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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