Description: A positive integer divides any greater factorial. (Contributed by Paul Chapman, 28-Nov-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | dvdsfac | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 | |
|
2 | 1 | breq2d | |
3 | 2 | imbi2d | |
4 | fveq2 | |
|
5 | 4 | breq2d | |
6 | 5 | imbi2d | |
7 | fveq2 | |
|
8 | 7 | breq2d | |
9 | 8 | imbi2d | |
10 | fveq2 | |
|
11 | 10 | breq2d | |
12 | 11 | imbi2d | |
13 | nnm1nn0 | |
|
14 | 13 | faccld | |
15 | 14 | nnzd | |
16 | nnz | |
|
17 | dvdsmul2 | |
|
18 | 15 16 17 | syl2anc | |
19 | facnn2 | |
|
20 | 18 19 | breqtrrd | |
21 | 16 | adantl | |
22 | elnnuz | |
|
23 | uztrn | |
|
24 | 22 23 | sylan2b | |
25 | elnnuz | |
|
26 | 24 25 | sylibr | |
27 | 26 | nnnn0d | |
28 | 27 | faccld | |
29 | 28 | nnzd | |
30 | 26 | nnzd | |
31 | 30 | peano2zd | |
32 | dvdsmultr1 | |
|
33 | 21 29 31 32 | syl3anc | |
34 | facp1 | |
|
35 | 27 34 | syl | |
36 | 35 | breq2d | |
37 | 33 36 | sylibrd | |
38 | 37 | ex | |
39 | 38 | a2d | |
40 | 3 6 9 12 20 39 | uzind4i | |
41 | 40 | impcom | |