Metamath Proof Explorer

Theorem prmolefac

Description: The primorial of a positive integer is less than or equal to the factorial of the integer. (Contributed by AV, 15-Aug-2020) (Revised by AV, 29-Aug-2020)

Ref Expression
Assertion prmolefac 
|- ( N e. NN0 -> ( #p ` N ) <_ ( ! ` N ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ k N e. NN0
2 fzfid 
 |-  ( N e. NN0 -> ( 1 ... N ) e. Fin )
3 elfznn 
 |-  ( k e. ( 1 ... N ) -> k e. NN )
4 3 adantl 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> k e. NN )
5 1nn 
 |-  1 e. NN
6 5 a1i 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> 1 e. NN )
7 4 6 ifcld 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> if ( k e. Prime , k , 1 ) e. NN )
8 7 nnred 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> if ( k e. Prime , k , 1 ) e. RR )
9 ifeqor 
 |-  ( if ( k e. Prime , k , 1 ) = k \/ if ( k e. Prime , k , 1 ) = 1 )
10 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
11 10 nn0ge0d 
 |-  ( k e. NN -> 0 <_ k )
12 3 11 syl 
 |-  ( k e. ( 1 ... N ) -> 0 <_ k )
13 12 adantl 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> 0 <_ k )
14 breq2 
 |-  ( if ( k e. Prime , k , 1 ) = k -> ( 0 <_ if ( k e. Prime , k , 1 ) <-> 0 <_ k ) )
15 13 14 syl5ibr 
 |-  ( if ( k e. Prime , k , 1 ) = k -> ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> 0 <_ if ( k e. Prime , k , 1 ) ) )
16 0le1 
 |-  0 <_ 1
17 breq2 
 |-  ( if ( k e. Prime , k , 1 ) = 1 -> ( 0 <_ if ( k e. Prime , k , 1 ) <-> 0 <_ 1 ) )
18 17 adantr 
 |-  ( ( if ( k e. Prime , k , 1 ) = 1 /\ ( N e. NN0 /\ k e. ( 1 ... N ) ) ) -> ( 0 <_ if ( k e. Prime , k , 1 ) <-> 0 <_ 1 ) )
19 16 18 mpbiri 
 |-  ( ( if ( k e. Prime , k , 1 ) = 1 /\ ( N e. NN0 /\ k e. ( 1 ... N ) ) ) -> 0 <_ if ( k e. Prime , k , 1 ) )
20 19 ex 
 |-  ( if ( k e. Prime , k , 1 ) = 1 -> ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> 0 <_ if ( k e. Prime , k , 1 ) ) )
21 15 20 jaoi 
 |-  ( ( if ( k e. Prime , k , 1 ) = k \/ if ( k e. Prime , k , 1 ) = 1 ) -> ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> 0 <_ if ( k e. Prime , k , 1 ) ) )
22 9 21 ax-mp 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> 0 <_ if ( k e. Prime , k , 1 ) )
23 4 nnred 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> k e. RR )
24 23 leidd 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> k <_ k )
25 breq1 
 |-  ( if ( k e. Prime , k , 1 ) = k -> ( if ( k e. Prime , k , 1 ) <_ k <-> k <_ k ) )
26 24 25 syl5ibr 
 |-  ( if ( k e. Prime , k , 1 ) = k -> ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> if ( k e. Prime , k , 1 ) <_ k ) )
27 4 nnge1d 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> 1 <_ k )
28 breq1 
 |-  ( if ( k e. Prime , k , 1 ) = 1 -> ( if ( k e. Prime , k , 1 ) <_ k <-> 1 <_ k ) )
29 27 28 syl5ibr 
 |-  ( if ( k e. Prime , k , 1 ) = 1 -> ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> if ( k e. Prime , k , 1 ) <_ k ) )
30 26 29 jaoi 
 |-  ( ( if ( k e. Prime , k , 1 ) = k \/ if ( k e. Prime , k , 1 ) = 1 ) -> ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> if ( k e. Prime , k , 1 ) <_ k ) )
31 9 30 ax-mp 
 |-  ( ( N e. NN0 /\ k e. ( 1 ... N ) ) -> if ( k e. Prime , k , 1 ) <_ k )
32 1 2 8 22 23 31 fprodle 
 |-  ( N e. NN0 -> prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) <_ prod_ k e. ( 1 ... N ) k )
33 prmoval 
 |-  ( N e. NN0 -> ( #p ` N ) = prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) )
34 fprodfac 
 |-  ( N e. NN0 -> ( ! ` N ) = prod_ k e. ( 1 ... N ) k )
35 32 33 34 3brtr4d 
 |-  ( N e. NN0 -> ( #p ` N ) <_ ( ! ` N ) )