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 e. NN
2 prmonn2 
 |-  ( 5 e. NN -> ( #p ` 5 ) = if ( 5 e. Prime , ( ( #p ` ( 5 - 1 ) ) x. 5 ) , ( #p ` ( 5 - 1 ) ) ) )
3 1 2 ax-mp 
 |-  ( #p ` 5 ) = if ( 5 e. Prime , ( ( #p ` ( 5 - 1 ) ) x. 5 ) , ( #p ` ( 5 - 1 ) ) )
4 5prm 
 |-  5 e. Prime
5 4 iftruei 
 |-  if ( 5 e. Prime , ( ( #p ` ( 5 - 1 ) ) x. 5 ) , ( #p ` ( 5 - 1 ) ) ) = ( ( #p ` ( 5 - 1 ) ) x. 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 ) ) x. 5 ) = ( 6 x. 5 )
11 6t5e30 
 |-  ( 6 x. 5 ) = ; 3 0
12 10 11 eqtri 
 |-  ( ( #p ` ( 5 - 1 ) ) x. 5 ) = ; 3 0
13 5 12 eqtri 
 |-  if ( 5 e. Prime , ( ( #p ` ( 5 - 1 ) ) x. 5 ) , ( #p ` ( 5 - 1 ) ) ) = ; 3 0
14 3 13 eqtri 
 |-  ( #p ` 5 ) = ; 3 0