Metamath Proof Explorer

Theorem prmo6

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

Ref Expression
Assertion prmo6 ( #p ‘ 6 ) = 3 0

Proof

Step Hyp Ref Expression
1 6nn ⊢ 6 ∈ ℕ
2 prmonn2 ⊢ ( 6 ∈ ℕ → ( #p ‘ 6 ) = if ( 6 ∈ ℙ , ( ( #p ‘ ( 6 − 1 ) ) · 6 ) , ( #p ‘ ( 6 − 1 ) ) ) )
3 1 2 ax-mp ⊢ ( #p ‘ 6 ) = if ( 6 ∈ ℙ , ( ( #p ‘ ( 6 − 1 ) ) · 6 ) , ( #p ‘ ( 6 − 1 ) ) )
4 6nprm ⊢ ¬ 6 ∈ ℙ
5 4 iffalsei ⊢ if ( 6 ∈ ℙ , ( ( #p ‘ ( 6 − 1 ) ) · 6 ) , ( #p ‘ ( 6 − 1 ) ) ) = ( #p ‘ ( 6 − 1 ) )
6 3 5 eqtri ⊢ ( #p ‘ 6 ) = ( #p ‘ ( 6 − 1 ) )
7 6m1e5 ⊢ ( 6 − 1 ) = 5
8 7 fveq2i ⊢ ( #p ‘ ( 6 − 1 ) ) = ( #p ‘ 5 )
9 prmo5 ⊢ ( #p ‘ 5 ) = 3 0
10 8 9 eqtri ⊢ ( #p ‘ ( 6 − 1 ) ) = 3 0
11 6 10 eqtri ⊢ ( #p ‘ 6 ) = 3 0