Metamath Proof Explorer

Theorem prmo2

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

Ref Expression
Assertion prmo2 
|- ( #p ` 2 ) = 2

Proof

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