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