Metamath Proof Explorer

Theorem prmo1

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

Ref Expression
Assertion prmo1 
|- ( #p ` 1 ) = 1

Proof

Step Hyp Ref Expression
1 1nn0 
 |-  1 e. NN0
2 prmoval 
 |-  ( 1 e. NN0 -> ( #p ` 1 ) = prod_ k e. ( 1 ... 1 ) if ( k e. Prime , k , 1 ) )
3 1 2 ax-mp 
 |-  ( #p ` 1 ) = prod_ k e. ( 1 ... 1 ) if ( k e. Prime , k , 1 )
4 1z 
 |-  1 e. ZZ
5 ax-1cn 
 |-  1 e. CC
6 1nprm 
 |-  -. 1 e. Prime
7 eleq1 
 |-  ( k = 1 -> ( k e. Prime <-> 1 e. Prime ) )
8 6 7 mtbiri 
 |-  ( k = 1 -> -. k e. Prime )
9 8 iffalsed 
 |-  ( k = 1 -> if ( k e. Prime , k , 1 ) = 1 )
10 9 fprod1 
 |-  ( ( 1 e. ZZ /\ 1 e. CC ) -> prod_ k e. ( 1 ... 1 ) if ( k e. Prime , k , 1 ) = 1 )
11 4 5 10 mp2an 
 |-  prod_ k e. ( 1 ... 1 ) if ( k e. Prime , k , 1 ) = 1
12 3 11 eqtri 
 |-  ( #p ` 1 ) = 1