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	⊢ ( 𝐴 ∈ ℕ → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ⊆ ( 1 ... 𝐴 ) )

Proof

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	⊢ ( 𝐴 ∈ ℤ → ( 𝑝 ∈ ( 1 ... 𝐴 ) ↔ ( 𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝐴 ) ) )
10	8 9	syl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℕ ) → ( 𝑝 ∈ ( 1 ... 𝐴 ) ↔ ( 𝑝 ∈ ℕ ∧ 𝑝 ≤ 𝐴 ) ) )
11	6 10	bitr4d	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℕ ) → ( 𝑝 ≤ 𝐴 ↔ 𝑝 ∈ ( 1 ... 𝐴 ) ) )
12	4 11	sylibd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ℕ ) → ( 𝑝 ∥ 𝐴 → 𝑝 ∈ ( 1 ... 𝐴 ) ) )
13	12	ralrimiva	⊢ ( 𝐴 ∈ ℕ → ∀ 𝑝 ∈ ℕ ( 𝑝 ∥ 𝐴 → 𝑝 ∈ ( 1 ... 𝐴 ) ) )
14		rabss	⊢ ( { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ⊆ ( 1 ... 𝐴 ) ↔ ∀ 𝑝 ∈ ℕ ( 𝑝 ∥ 𝐴 → 𝑝 ∈ ( 1 ... 𝐴 ) ) )
15	13 14	sylibr	⊢ ( 𝐴 ∈ ℕ → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴 } ⊆ ( 1 ... 𝐴 ) )