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 e. NN
2 prmonn2 
 |-  ( 4 e. NN -> ( #p ` 4 ) = if ( 4 e. Prime , ( ( #p ` ( 4 - 1 ) ) x. 4 ) , ( #p ` ( 4 - 1 ) ) ) )
3 1 2 ax-mp 
 |-  ( #p ` 4 ) = if ( 4 e. Prime , ( ( #p ` ( 4 - 1 ) ) x. 4 ) , ( #p ` ( 4 - 1 ) ) )
4 4nprm 
 |-  -. 4 e. Prime
5 4 iffalsei 
 |-  if ( 4 e. Prime , ( ( #p ` ( 4 - 1 ) ) x. 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