This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( A e. NN -> { p e. NN | p || A } C_ ( 1 ... A ) )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( p e. NN -> p e. ZZ )
2 id 
 |-  ( A e. NN -> A e. NN )
3 dvdsle 
 |-  ( ( p e. ZZ /\ A e. NN ) -> ( p || A -> p <_ A ) )
4 1 2 3 syl2anr 
 |-  ( ( A e. NN /\ p e. NN ) -> ( p || A -> p <_ A ) )
5 ibar 
 |-  ( p e. NN -> ( p <_ A <-> ( p e. NN /\ p <_ A ) ) )
6 5 adantl 
 |-  ( ( A e. NN /\ p e. NN ) -> ( p <_ A <-> ( p e. NN /\ p <_ A ) ) )
7 nnz 
 |-  ( A e. NN -> A e. ZZ )
8 7 adantr 
 |-  ( ( A e. NN /\ p e. NN ) -> A e. ZZ )
9 fznn 
 |-  ( A e. ZZ -> ( p e. ( 1 ... A ) <-> ( p e. NN /\ p <_ A ) ) )
10 8 9 syl 
 |-  ( ( A e. NN /\ p e. NN ) -> ( p e. ( 1 ... A ) <-> ( p e. NN /\ p <_ A ) ) )
11 6 10 bitr4d 
 |-  ( ( A e. NN /\ p e. NN ) -> ( p <_ A <-> p e. ( 1 ... A ) ) )
12 4 11 sylibd 
 |-  ( ( A e. NN /\ p e. NN ) -> ( p || A -> p e. ( 1 ... A ) ) )
13 12 ralrimiva 
 |-  ( A e. NN -> A. p e. NN ( p || A -> p e. ( 1 ... A ) ) )
14 rabss 
 |-  ( { p e. NN | p || A } C_ ( 1 ... A ) <-> A. p e. NN ( p || A -> p e. ( 1 ... A ) ) )
15 13 14 sylibr 
 |-  ( A e. NN -> { p e. NN | p || A } C_ ( 1 ... A ) )