Description: The set of divisors of a number is a subset of a finite set. (Contributed by Mario Carneiro, 22-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | dvdsssfz1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnz | |
|
2 | id | |
|
3 | dvdsle | |
|
4 | 1 2 3 | syl2anr | |
5 | ibar | |
|
6 | 5 | adantl | |
7 | nnz | |
|
8 | 7 | adantr | |
9 | fznn | |
|
10 | 8 9 | syl | |
11 | 6 10 | bitr4d | |
12 | 4 11 | sylibd | |
13 | 12 | ralrimiva | |
14 | rabss | |
|
15 | 13 14 | sylibr | |