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 ) )