Metamath Proof Explorer

Theorem prmfac1

Description: The factorial of a number only contains primes less than the base. (Contributed by Mario Carneiro, 6-Mar-2014)

Ref Expression
Assertion prmfac1 
|- ( ( N e. NN0 /\ P e. Prime /\ P || ( ! ` N ) ) -> P <_ N )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( x = 0 -> ( ! ` x ) = ( ! ` 0 ) )
2 1 breq2d 
 |-  ( x = 0 -> ( P || ( ! ` x ) <-> P || ( ! ` 0 ) ) )
3 breq2 
 |-  ( x = 0 -> ( P <_ x <-> P <_ 0 ) )
4 2 3 imbi12d 
 |-  ( x = 0 -> ( ( P || ( ! ` x ) -> P <_ x ) <-> ( P || ( ! ` 0 ) -> P <_ 0 ) ) )
5 4 imbi2d 
 |-  ( x = 0 -> ( ( P e. Prime -> ( P || ( ! ` x ) -> P <_ x ) ) <-> ( P e. Prime -> ( P || ( ! ` 0 ) -> P <_ 0 ) ) ) )
6 fveq2 
 |-  ( x = k -> ( ! ` x ) = ( ! ` k ) )
7 6 breq2d 
 |-  ( x = k -> ( P || ( ! ` x ) <-> P || ( ! ` k ) ) )
8 breq2 
 |-  ( x = k -> ( P <_ x <-> P <_ k ) )
9 7 8 imbi12d 
 |-  ( x = k -> ( ( P || ( ! ` x ) -> P <_ x ) <-> ( P || ( ! ` k ) -> P <_ k ) ) )
10 9 imbi2d 
 |-  ( x = k -> ( ( P e. Prime -> ( P || ( ! ` x ) -> P <_ x ) ) <-> ( P e. Prime -> ( P || ( ! ` k ) -> P <_ k ) ) ) )
11 fveq2 
 |-  ( x = ( k + 1 ) -> ( ! ` x ) = ( ! ` ( k + 1 ) ) )
12 11 breq2d 
 |-  ( x = ( k + 1 ) -> ( P || ( ! ` x ) <-> P || ( ! ` ( k + 1 ) ) ) )
13 breq2 
 |-  ( x = ( k + 1 ) -> ( P <_ x <-> P <_ ( k + 1 ) ) )
14 12 13 imbi12d 
 |-  ( x = ( k + 1 ) -> ( ( P || ( ! ` x ) -> P <_ x ) <-> ( P || ( ! ` ( k + 1 ) ) -> P <_ ( k + 1 ) ) ) )
15 14 imbi2d 
 |-  ( x = ( k + 1 ) -> ( ( P e. Prime -> ( P || ( ! ` x ) -> P <_ x ) ) <-> ( P e. Prime -> ( P || ( ! ` ( k + 1 ) ) -> P <_ ( k + 1 ) ) ) ) )
16 fveq2 
 |-  ( x = N -> ( ! ` x ) = ( ! ` N ) )
17 16 breq2d 
 |-  ( x = N -> ( P || ( ! ` x ) <-> P || ( ! ` N ) ) )
18 breq2 
 |-  ( x = N -> ( P <_ x <-> P <_ N ) )
19 17 18 imbi12d 
 |-  ( x = N -> ( ( P || ( ! ` x ) -> P <_ x ) <-> ( P || ( ! ` N ) -> P <_ N ) ) )
20 19 imbi2d 
 |-  ( x = N -> ( ( P e. Prime -> ( P || ( ! ` x ) -> P <_ x ) ) <-> ( P e. Prime -> ( P || ( ! ` N ) -> P <_ N ) ) ) )
21 fac0 
 |-  ( ! ` 0 ) = 1
22 21 breq2i 
 |-  ( P || ( ! ` 0 ) <-> P || 1 )
23 nprmdvds1 
 |-  ( P e. Prime -> -. P || 1 )
24 23 pm2.21d 
 |-  ( P e. Prime -> ( P || 1 -> P <_ 0 ) )
25 22 24 biimtrid 
 |-  ( P e. Prime -> ( P || ( ! ` 0 ) -> P <_ 0 ) )
26 facp1 
 |-  ( k e. NN0 -> ( ! ` ( k + 1 ) ) = ( ( ! ` k ) x. ( k + 1 ) ) )
27 26 adantr 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( ! ` ( k + 1 ) ) = ( ( ! ` k ) x. ( k + 1 ) ) )
28 27 breq2d 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( P || ( ! ` ( k + 1 ) ) <-> P || ( ( ! ` k ) x. ( k + 1 ) ) ) )
29 simpr 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> P e. Prime )
30 faccl 
 |-  ( k e. NN0 -> ( ! ` k ) e. NN )
31 30 adantr 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( ! ` k ) e. NN )
32 31 nnzd 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( ! ` k ) e. ZZ )
33 nn0p1nn 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN )
34 33 adantr 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( k + 1 ) e. NN )
35 34 nnzd 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( k + 1 ) e. ZZ )
36 euclemma 
 |-  ( ( P e. Prime /\ ( ! ` k ) e. ZZ /\ ( k + 1 ) e. ZZ ) -> ( P || ( ( ! ` k ) x. ( k + 1 ) ) <-> ( P || ( ! ` k ) \/ P || ( k + 1 ) ) ) )
37 29 32 35 36 syl3anc 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( P || ( ( ! ` k ) x. ( k + 1 ) ) <-> ( P || ( ! ` k ) \/ P || ( k + 1 ) ) ) )
38 28 37 bitrd 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( P || ( ! ` ( k + 1 ) ) <-> ( P || ( ! ` k ) \/ P || ( k + 1 ) ) ) )
39 nn0re 
 |-  ( k e. NN0 -> k e. RR )
40 39 adantr 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> k e. RR )
41 40 lep1d 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> k <_ ( k + 1 ) )
42 prmz 
 |-  ( P e. Prime -> P e. ZZ )
43 42 adantl 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> P e. ZZ )
44 43 zred 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> P e. RR )
45 34 nnred 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( k + 1 ) e. RR )
46 letr 
 |-  ( ( P e. RR /\ k e. RR /\ ( k + 1 ) e. RR ) -> ( ( P <_ k /\ k <_ ( k + 1 ) ) -> P <_ ( k + 1 ) ) )
47 44 40 45 46 syl3anc 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( ( P <_ k /\ k <_ ( k + 1 ) ) -> P <_ ( k + 1 ) ) )
48 41 47 mpan2d 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( P <_ k -> P <_ ( k + 1 ) ) )
49 48 imim2d 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( ( P || ( ! ` k ) -> P <_ k ) -> ( P || ( ! ` k ) -> P <_ ( k + 1 ) ) ) )
50 49 com23 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( P || ( ! ` k ) -> ( ( P || ( ! ` k ) -> P <_ k ) -> P <_ ( k + 1 ) ) ) )
51 dvdsle 
 |-  ( ( P e. ZZ /\ ( k + 1 ) e. NN ) -> ( P || ( k + 1 ) -> P <_ ( k + 1 ) ) )
52 43 34 51 syl2anc 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( P || ( k + 1 ) -> P <_ ( k + 1 ) ) )
53 52 a1dd 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( P || ( k + 1 ) -> ( ( P || ( ! ` k ) -> P <_ k ) -> P <_ ( k + 1 ) ) ) )
54 50 53 jaod 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( ( P || ( ! ` k ) \/ P || ( k + 1 ) ) -> ( ( P || ( ! ` k ) -> P <_ k ) -> P <_ ( k + 1 ) ) ) )
55 38 54 sylbid 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( P || ( ! ` ( k + 1 ) ) -> ( ( P || ( ! ` k ) -> P <_ k ) -> P <_ ( k + 1 ) ) ) )
56 55 com23 
 |-  ( ( k e. NN0 /\ P e. Prime ) -> ( ( P || ( ! ` k ) -> P <_ k ) -> ( P || ( ! ` ( k + 1 ) ) -> P <_ ( k + 1 ) ) ) )
57 56 ex 
 |-  ( k e. NN0 -> ( P e. Prime -> ( ( P || ( ! ` k ) -> P <_ k ) -> ( P || ( ! ` ( k + 1 ) ) -> P <_ ( k + 1 ) ) ) ) )
58 57 a2d 
 |-  ( k e. NN0 -> ( ( P e. Prime -> ( P || ( ! ` k ) -> P <_ k ) ) -> ( P e. Prime -> ( P || ( ! ` ( k + 1 ) ) -> P <_ ( k + 1 ) ) ) ) )
59 5 10 15 20 25 58 nn0ind 
 |-  ( N e. NN0 -> ( P e. Prime -> ( P || ( ! ` N ) -> P <_ N ) ) )
60 59 3imp 
 |-  ( ( N e. NN0 /\ P e. Prime /\ P || ( ! ` N ) ) -> P <_ N )