Metamath Proof Explorer


Theorem dvdsfac

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

Ref Expression
Assertion dvdsfac KNKKN!

Proof

Step Hyp Ref Expression
1 fveq2 x=Kx!=K!
2 1 breq2d x=KKx!KK!
3 2 imbi2d x=KKKx!KKK!
4 fveq2 x=yx!=y!
5 4 breq2d x=yKx!Ky!
6 5 imbi2d x=yKKx!KKy!
7 fveq2 x=y+1x!=y+1!
8 7 breq2d x=y+1Kx!Ky+1!
9 8 imbi2d x=y+1KKx!KKy+1!
10 fveq2 x=Nx!=N!
11 10 breq2d x=NKx!KN!
12 11 imbi2d x=NKKx!KKN!
13 nnm1nn0 KK10
14 13 faccld KK1!
15 14 nnzd KK1!
16 nnz KK
17 dvdsmul2 K1!KKK1!K
18 15 16 17 syl2anc KKK1!K
19 facnn2 KK!=K1!K
20 18 19 breqtrrd KKK!
21 16 adantl yKKK
22 elnnuz KK1
23 uztrn yKK1y1
24 22 23 sylan2b yKKy1
25 elnnuz yy1
26 24 25 sylibr yKKy
27 26 nnnn0d yKKy0
28 27 faccld yKKy!
29 28 nnzd yKKy!
30 26 nnzd yKKy
31 30 peano2zd yKKy+1
32 dvdsmultr1 Ky!y+1Ky!Ky!y+1
33 21 29 31 32 syl3anc yKKKy!Ky!y+1
34 facp1 y0y+1!=y!y+1
35 27 34 syl yKKy+1!=y!y+1
36 35 breq2d yKKKy+1!Ky!y+1
37 33 36 sylibrd yKKKy!Ky+1!
38 37 ex yKKKy!Ky+1!
39 38 a2d yKKKy!KKy+1!
40 3 6 9 12 20 39 uzind4i NKKKN!
41 40 impcom KNKKN!