Metamath Proof Explorer

Theorem dvdsfac

Description: A positive integer divides any greater factorial. (Contributed by Paul Chapman, 28-Nov-2012)

Ref Expression
Assertion dvdsfac 
|- ( ( K e. NN /\ N e. ( ZZ>= ` K ) ) -> K || ( ! ` N ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( x = K -> ( ! ` x ) = ( ! ` K ) )
2 1 breq2d 
 |-  ( x = K -> ( K || ( ! ` x ) <-> K || ( ! ` K ) ) )
3 2 imbi2d 
 |-  ( x = K -> ( ( K e. NN -> K || ( ! ` x ) ) <-> ( K e. NN -> K || ( ! ` K ) ) ) )
4 fveq2 
 |-  ( x = y -> ( ! ` x ) = ( ! ` y ) )
5 4 breq2d 
 |-  ( x = y -> ( K || ( ! ` x ) <-> K || ( ! ` y ) ) )
6 5 imbi2d 
 |-  ( x = y -> ( ( K e. NN -> K || ( ! ` x ) ) <-> ( K e. NN -> K || ( ! ` y ) ) ) )
7 fveq2 
 |-  ( x = ( y + 1 ) -> ( ! ` x ) = ( ! ` ( y + 1 ) ) )
8 7 breq2d 
 |-  ( x = ( y + 1 ) -> ( K || ( ! ` x ) <-> K || ( ! ` ( y + 1 ) ) ) )
9 8 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( K e. NN -> K || ( ! ` x ) ) <-> ( K e. NN -> K || ( ! ` ( y + 1 ) ) ) ) )
10 fveq2 
 |-  ( x = N -> ( ! ` x ) = ( ! ` N ) )
11 10 breq2d 
 |-  ( x = N -> ( K || ( ! ` x ) <-> K || ( ! ` N ) ) )
12 11 imbi2d 
 |-  ( x = N -> ( ( K e. NN -> K || ( ! ` x ) ) <-> ( K e. NN -> K || ( ! ` N ) ) ) )
13 nnm1nn0 
 |-  ( K e. NN -> ( K - 1 ) e. NN0 )
14 13 faccld 
 |-  ( K e. NN -> ( ! ` ( K - 1 ) ) e. NN )
15 14 nnzd 
 |-  ( K e. NN -> ( ! ` ( K - 1 ) ) e. ZZ )
16 nnz 
 |-  ( K e. NN -> K e. ZZ )
17 dvdsmul2 
 |-  ( ( ( ! ` ( K - 1 ) ) e. ZZ /\ K e. ZZ ) -> K || ( ( ! ` ( K - 1 ) ) x. K ) )
18 15 16 17 syl2anc 
 |-  ( K e. NN -> K || ( ( ! ` ( K - 1 ) ) x. K ) )
19 facnn2 
 |-  ( K e. NN -> ( ! ` K ) = ( ( ! ` ( K - 1 ) ) x. K ) )
20 18 19 breqtrrd 
 |-  ( K e. NN -> K || ( ! ` K ) )
21 16 adantl 
 |-  ( ( y e. ( ZZ>= ` K ) /\ K e. NN ) -> K e. ZZ )
22 elnnuz 
 |-  ( K e. NN <-> K e. ( ZZ>= ` 1 ) )
23 uztrn 
 |-  ( ( y e. ( ZZ>= ` K ) /\ K e. ( ZZ>= ` 1 ) ) -> y e. ( ZZ>= ` 1 ) )
24 22 23 sylan2b 
 |-  ( ( y e. ( ZZ>= ` K ) /\ K e. NN ) -> y e. ( ZZ>= ` 1 ) )
25 elnnuz 
 |-  ( y e. NN <-> y e. ( ZZ>= ` 1 ) )
26 24 25 sylibr 
 |-  ( ( y e. ( ZZ>= ` K ) /\ K e. NN ) -> y e. NN )
27 26 nnnn0d 
 |-  ( ( y e. ( ZZ>= ` K ) /\ K e. NN ) -> y e. NN0 )
28 27 faccld 
 |-  ( ( y e. ( ZZ>= ` K ) /\ K e. NN ) -> ( ! ` y ) e. NN )
29 28 nnzd 
 |-  ( ( y e. ( ZZ>= ` K ) /\ K e. NN ) -> ( ! ` y ) e. ZZ )
30 26 nnzd 
 |-  ( ( y e. ( ZZ>= ` K ) /\ K e. NN ) -> y e. ZZ )
31 30 peano2zd 
 |-  ( ( y e. ( ZZ>= ` K ) /\ K e. NN ) -> ( y + 1 ) e. ZZ )
32 dvdsmultr1 
 |-  ( ( K e. ZZ /\ ( ! ` y ) e. ZZ /\ ( y + 1 ) e. ZZ ) -> ( K || ( ! ` y ) -> K || ( ( ! ` y ) x. ( y + 1 ) ) ) )
33 21 29 31 32 syl3anc 
 |-  ( ( y e. ( ZZ>= ` K ) /\ K e. NN ) -> ( K || ( ! ` y ) -> K || ( ( ! ` y ) x. ( y + 1 ) ) ) )
34 facp1 
 |-  ( y e. NN0 -> ( ! ` ( y + 1 ) ) = ( ( ! ` y ) x. ( y + 1 ) ) )
35 27 34 syl 
 |-  ( ( y e. ( ZZ>= ` K ) /\ K e. NN ) -> ( ! ` ( y + 1 ) ) = ( ( ! ` y ) x. ( y + 1 ) ) )
36 35 breq2d 
 |-  ( ( y e. ( ZZ>= ` K ) /\ K e. NN ) -> ( K || ( ! ` ( y + 1 ) ) <-> K || ( ( ! ` y ) x. ( y + 1 ) ) ) )
37 33 36 sylibrd 
 |-  ( ( y e. ( ZZ>= ` K ) /\ K e. NN ) -> ( K || ( ! ` y ) -> K || ( ! ` ( y + 1 ) ) ) )
38 37 ex 
 |-  ( y e. ( ZZ>= ` K ) -> ( K e. NN -> ( K || ( ! ` y ) -> K || ( ! ` ( y + 1 ) ) ) ) )
39 38 a2d 
 |-  ( y e. ( ZZ>= ` K ) -> ( ( K e. NN -> K || ( ! ` y ) ) -> ( K e. NN -> K || ( ! ` ( y + 1 ) ) ) ) )
40 3 6 9 12 20 39 uzind4i 
 |-  ( N e. ( ZZ>= ` K ) -> ( K e. NN -> K || ( ! ` N ) ) )
41 40 impcom 
 |-  ( ( K e. NN /\ N e. ( ZZ>= ` K ) ) -> K || ( ! ` N ) )