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

Metamath Proof Explorer

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