Metamath Proof Explorer


Theorem dvdsssfz1

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 Ap|pA1A

Proof

Step Hyp Ref Expression
1 nnz pp
2 id AA
3 dvdsle pApApA
4 1 2 3 syl2anr AppApA
5 ibar ppAppA
6 5 adantl AppAppA
7 nnz AA
8 7 adantr ApA
9 fznn Ap1AppA
10 8 9 syl App1AppA
11 6 10 bitr4d AppAp1A
12 4 11 sylibd AppAp1A
13 12 ralrimiva AppAp1A
14 rabss p|pA1AppAp1A
15 13 14 sylibr Ap|pA1A