Metamath Proof Explorer

Theorem facdiv

Description: A positive integer divides the factorial of an equal or larger number. (Contributed by NM, 2-May-2005)

Ref Expression
Assertion facdiv 
|- ( ( M e. NN0 /\ N e. NN /\ N <_ M ) -> ( ( ! ` M ) / N ) e. NN )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( j = 0 -> ( N <_ j <-> N <_ 0 ) )
2 fveq2 
 |-  ( j = 0 -> ( ! ` j ) = ( ! ` 0 ) )
3 2 oveq1d 
 |-  ( j = 0 -> ( ( ! ` j ) / N ) = ( ( ! ` 0 ) / N ) )
4 3 eleq1d 
 |-  ( j = 0 -> ( ( ( ! ` j ) / N ) e. NN <-> ( ( ! ` 0 ) / N ) e. NN ) )
5 1 4 imbi12d 
 |-  ( j = 0 -> ( ( N <_ j -> ( ( ! ` j ) / N ) e. NN ) <-> ( N <_ 0 -> ( ( ! ` 0 ) / N ) e. NN ) ) )
6 5 imbi2d 
 |-  ( j = 0 -> ( ( N e. NN -> ( N <_ j -> ( ( ! ` j ) / N ) e. NN ) ) <-> ( N e. NN -> ( N <_ 0 -> ( ( ! ` 0 ) / N ) e. NN ) ) ) )
7 breq2 
 |-  ( j = k -> ( N <_ j <-> N <_ k ) )
8 fveq2 
 |-  ( j = k -> ( ! ` j ) = ( ! ` k ) )
9 8 oveq1d 
 |-  ( j = k -> ( ( ! ` j ) / N ) = ( ( ! ` k ) / N ) )
10 9 eleq1d 
 |-  ( j = k -> ( ( ( ! ` j ) / N ) e. NN <-> ( ( ! ` k ) / N ) e. NN ) )
11 7 10 imbi12d 
 |-  ( j = k -> ( ( N <_ j -> ( ( ! ` j ) / N ) e. NN ) <-> ( N <_ k -> ( ( ! ` k ) / N ) e. NN ) ) )
12 11 imbi2d 
 |-  ( j = k -> ( ( N e. NN -> ( N <_ j -> ( ( ! ` j ) / N ) e. NN ) ) <-> ( N e. NN -> ( N <_ k -> ( ( ! ` k ) / N ) e. NN ) ) ) )
13 breq2 
 |-  ( j = ( k + 1 ) -> ( N <_ j <-> N <_ ( k + 1 ) ) )
14 fveq2 
 |-  ( j = ( k + 1 ) -> ( ! ` j ) = ( ! ` ( k + 1 ) ) )
15 14 oveq1d 
 |-  ( j = ( k + 1 ) -> ( ( ! ` j ) / N ) = ( ( ! ` ( k + 1 ) ) / N ) )
16 15 eleq1d 
 |-  ( j = ( k + 1 ) -> ( ( ( ! ` j ) / N ) e. NN <-> ( ( ! ` ( k + 1 ) ) / N ) e. NN ) )
17 13 16 imbi12d 
 |-  ( j = ( k + 1 ) -> ( ( N <_ j -> ( ( ! ` j ) / N ) e. NN ) <-> ( N <_ ( k + 1 ) -> ( ( ! ` ( k + 1 ) ) / N ) e. NN ) ) )
18 17 imbi2d 
 |-  ( j = ( k + 1 ) -> ( ( N e. NN -> ( N <_ j -> ( ( ! ` j ) / N ) e. NN ) ) <-> ( N e. NN -> ( N <_ ( k + 1 ) -> ( ( ! ` ( k + 1 ) ) / N ) e. NN ) ) ) )
19 breq2 
 |-  ( j = M -> ( N <_ j <-> N <_ M ) )
20 fveq2 
 |-  ( j = M -> ( ! ` j ) = ( ! ` M ) )
21 20 oveq1d 
 |-  ( j = M -> ( ( ! ` j ) / N ) = ( ( ! ` M ) / N ) )
22 21 eleq1d 
 |-  ( j = M -> ( ( ( ! ` j ) / N ) e. NN <-> ( ( ! ` M ) / N ) e. NN ) )
23 19 22 imbi12d 
 |-  ( j = M -> ( ( N <_ j -> ( ( ! ` j ) / N ) e. NN ) <-> ( N <_ M -> ( ( ! ` M ) / N ) e. NN ) ) )
24 23 imbi2d 
 |-  ( j = M -> ( ( N e. NN -> ( N <_ j -> ( ( ! ` j ) / N ) e. NN ) ) <-> ( N e. NN -> ( N <_ M -> ( ( ! ` M ) / N ) e. NN ) ) ) )
25 nnnle0 
 |-  ( N e. NN -> -. N <_ 0 )
26 25 pm2.21d 
 |-  ( N e. NN -> ( N <_ 0 -> ( ( ! ` 0 ) / N ) e. NN ) )
27 nnre 
 |-  ( N e. NN -> N e. RR )
28 peano2nn0 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN0 )
29 28 nn0red 
 |-  ( k e. NN0 -> ( k + 1 ) e. RR )
30 leloe 
 |-  ( ( N e. RR /\ ( k + 1 ) e. RR ) -> ( N <_ ( k + 1 ) <-> ( N < ( k + 1 ) \/ N = ( k + 1 ) ) ) )
31 27 29 30 syl2an 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( N <_ ( k + 1 ) <-> ( N < ( k + 1 ) \/ N = ( k + 1 ) ) ) )
32 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
33 nn0leltp1 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( N <_ k <-> N < ( k + 1 ) ) )
34 32 33 sylan 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( N <_ k <-> N < ( k + 1 ) ) )
35 nn0p1nn 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN )
36 nnmulcl 
 |-  ( ( ( ( ! ` k ) / N ) e. NN /\ ( k + 1 ) e. NN ) -> ( ( ( ! ` k ) / N ) x. ( k + 1 ) ) e. NN )
37 35 36 sylan2 
 |-  ( ( ( ( ! ` k ) / N ) e. NN /\ k e. NN0 ) -> ( ( ( ! ` k ) / N ) x. ( k + 1 ) ) e. NN )
38 37 expcom 
 |-  ( k e. NN0 -> ( ( ( ! ` k ) / N ) e. NN -> ( ( ( ! ` k ) / N ) x. ( k + 1 ) ) e. NN ) )
39 38 adantl 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( ( ( ! ` k ) / N ) e. NN -> ( ( ( ! ` k ) / N ) x. ( k + 1 ) ) e. NN ) )
40 faccl 
 |-  ( k e. NN0 -> ( ! ` k ) e. NN )
41 40 nncnd 
 |-  ( k e. NN0 -> ( ! ` k ) e. CC )
42 28 nn0cnd 
 |-  ( k e. NN0 -> ( k + 1 ) e. CC )
43 nncn 
 |-  ( N e. NN -> N e. CC )
44 nnne0 
 |-  ( N e. NN -> N =/= 0 )
45 43 44 jca 
 |-  ( N e. NN -> ( N e. CC /\ N =/= 0 ) )
46 45 adantr 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( N e. CC /\ N =/= 0 ) )
47 div23 
 |-  ( ( ( ! ` k ) e. CC /\ ( k + 1 ) e. CC /\ ( N e. CC /\ N =/= 0 ) ) -> ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) = ( ( ( ! ` k ) / N ) x. ( k + 1 ) ) )
48 41 42 46 47 syl2an23an 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) = ( ( ( ! ` k ) / N ) x. ( k + 1 ) ) )
49 48 eleq1d 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) e. NN <-> ( ( ( ! ` k ) / N ) x. ( k + 1 ) ) e. NN ) )
50 39 49 sylibrd 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( ( ( ! ` k ) / N ) e. NN -> ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) e. NN ) )
51 50 imim2d 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( ( N <_ k -> ( ( ! ` k ) / N ) e. NN ) -> ( N <_ k -> ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) e. NN ) ) )
52 51 com23 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( N <_ k -> ( ( N <_ k -> ( ( ! ` k ) / N ) e. NN ) -> ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) e. NN ) ) )
53 34 52 sylbird 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( N < ( k + 1 ) -> ( ( N <_ k -> ( ( ! ` k ) / N ) e. NN ) -> ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) e. NN ) ) )
54 41 adantl 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( ! ` k ) e. CC )
55 43 adantr 
 |-  ( ( N e. NN /\ k e. NN0 ) -> N e. CC )
56 44 adantr 
 |-  ( ( N e. NN /\ k e. NN0 ) -> N =/= 0 )
57 54 55 56 divcan4d 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( ( ( ! ` k ) x. N ) / N ) = ( ! ` k ) )
58 40 adantl 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( ! ` k ) e. NN )
59 57 58 eqeltrd 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( ( ( ! ` k ) x. N ) / N ) e. NN )
60 oveq2 
 |-  ( N = ( k + 1 ) -> ( ( ! ` k ) x. N ) = ( ( ! ` k ) x. ( k + 1 ) ) )
61 60 oveq1d 
 |-  ( N = ( k + 1 ) -> ( ( ( ! ` k ) x. N ) / N ) = ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) )
62 61 eleq1d 
 |-  ( N = ( k + 1 ) -> ( ( ( ( ! ` k ) x. N ) / N ) e. NN <-> ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) e. NN ) )
63 59 62 syl5ibcom 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( N = ( k + 1 ) -> ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) e. NN ) )
64 63 a1dd 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( N = ( k + 1 ) -> ( ( N <_ k -> ( ( ! ` k ) / N ) e. NN ) -> ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) e. NN ) ) )
65 53 64 jaod 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( ( N < ( k + 1 ) \/ N = ( k + 1 ) ) -> ( ( N <_ k -> ( ( ! ` k ) / N ) e. NN ) -> ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) e. NN ) ) )
66 31 65 sylbid 
 |-  ( ( N e. NN /\ k e. NN0 ) -> ( N <_ ( k + 1 ) -> ( ( N <_ k -> ( ( ! ` k ) / N ) e. NN ) -> ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) e. NN ) ) )
67 66 ex 
 |-  ( N e. NN -> ( k e. NN0 -> ( N <_ ( k + 1 ) -> ( ( N <_ k -> ( ( ! ` k ) / N ) e. NN ) -> ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) e. NN ) ) ) )
68 67 com34 
 |-  ( N e. NN -> ( k e. NN0 -> ( ( N <_ k -> ( ( ! ` k ) / N ) e. NN ) -> ( N <_ ( k + 1 ) -> ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) e. NN ) ) ) )
69 68 com12 
 |-  ( k e. NN0 -> ( N e. NN -> ( ( N <_ k -> ( ( ! ` k ) / N ) e. NN ) -> ( N <_ ( k + 1 ) -> ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) e. NN ) ) ) )
70 69 imp4d 
 |-  ( k e. NN0 -> ( ( N e. NN /\ ( ( N <_ k -> ( ( ! ` k ) / N ) e. NN ) /\ N <_ ( k + 1 ) ) ) -> ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) e. NN ) )
71 facp1 
 |-  ( k e. NN0 -> ( ! ` ( k + 1 ) ) = ( ( ! ` k ) x. ( k + 1 ) ) )
72 71 oveq1d 
 |-  ( k e. NN0 -> ( ( ! ` ( k + 1 ) ) / N ) = ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) )
73 72 eleq1d 
 |-  ( k e. NN0 -> ( ( ( ! ` ( k + 1 ) ) / N ) e. NN <-> ( ( ( ! ` k ) x. ( k + 1 ) ) / N ) e. NN ) )
74 70 73 sylibrd 
 |-  ( k e. NN0 -> ( ( N e. NN /\ ( ( N <_ k -> ( ( ! ` k ) / N ) e. NN ) /\ N <_ ( k + 1 ) ) ) -> ( ( ! ` ( k + 1 ) ) / N ) e. NN ) )
75 74 exp4d 
 |-  ( k e. NN0 -> ( N e. NN -> ( ( N <_ k -> ( ( ! ` k ) / N ) e. NN ) -> ( N <_ ( k + 1 ) -> ( ( ! ` ( k + 1 ) ) / N ) e. NN ) ) ) )
76 75 a2d 
 |-  ( k e. NN0 -> ( ( N e. NN -> ( N <_ k -> ( ( ! ` k ) / N ) e. NN ) ) -> ( N e. NN -> ( N <_ ( k + 1 ) -> ( ( ! ` ( k + 1 ) ) / N ) e. NN ) ) ) )
77 6 12 18 24 26 76 nn0ind 
 |-  ( M e. NN0 -> ( N e. NN -> ( N <_ M -> ( ( ! ` M ) / N ) e. NN ) ) )
78 77 3imp 
 |-  ( ( M e. NN0 /\ N e. NN /\ N <_ M ) -> ( ( ! ` M ) / N ) e. NN )