Metamath Proof Explorer

Theorem prmo3

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

Ref Expression
Assertion prmo3 
|- ( #p ` 3 ) = 6

Proof

Step Hyp Ref Expression
1 3nn 
 |-  3 e. NN
2 prmonn2 
 |-  ( 3 e. NN -> ( #p ` 3 ) = if ( 3 e. Prime , ( ( #p ` ( 3 - 1 ) ) x. 3 ) , ( #p ` ( 3 - 1 ) ) ) )
3 1 2 ax-mp 
 |-  ( #p ` 3 ) = if ( 3 e. Prime , ( ( #p ` ( 3 - 1 ) ) x. 3 ) , ( #p ` ( 3 - 1 ) ) )
4 3prm 
 |-  3 e. Prime
5 4 iftruei 
 |-  if ( 3 e. Prime , ( ( #p ` ( 3 - 1 ) ) x. 3 ) , ( #p ` ( 3 - 1 ) ) ) = ( ( #p ` ( 3 - 1 ) ) x. 3 )
6 3m1e2 
 |-  ( 3 - 1 ) = 2
7 6 fveq2i 
 |-  ( #p ` ( 3 - 1 ) ) = ( #p ` 2 )
8 prmo2 
 |-  ( #p ` 2 ) = 2
9 7 8 eqtri 
 |-  ( #p ` ( 3 - 1 ) ) = 2
10 9 oveq1i 
 |-  ( ( #p ` ( 3 - 1 ) ) x. 3 ) = ( 2 x. 3 )
11 3cn 
 |-  3 e. CC
12 2cn 
 |-  2 e. CC
13 3t2e6 
 |-  ( 3 x. 2 ) = 6
14 11 12 13 mulcomli 
 |-  ( 2 x. 3 ) = 6
15 10 14 eqtri 
 |-  ( ( #p ` ( 3 - 1 ) ) x. 3 ) = 6
16 5 15 eqtri 
 |-  if ( 3 e. Prime , ( ( #p ` ( 3 - 1 ) ) x. 3 ) , ( #p ` ( 3 - 1 ) ) ) = 6
17 3 16 eqtri 
 |-  ( #p ` 3 ) = 6