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

Metamath Proof Explorer

Theorem prmo5

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

Ref Expression
Assertion prmo5 ( #p ‘ 5 ) = 3 0

Proof

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