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 ∈ ℕ → p ∈ ℕ | p ∥ A ⊆ 1 … A

Proof

Step Hyp Ref Expression
1 nnz ⊢ p ∈ ℕ → p ∈ ℤ
2 id ⊢ A ∈ ℕ → A ∈ ℕ
3 dvdsle ⊢ p ∈ ℤ ∧ A ∈ ℕ → p ∥ A → p ≤ A
4 1 2 3 syl2anr ⊢ A ∈ ℕ ∧ p ∈ ℕ → p ∥ A → p ≤ A
5 ibar ⊢ p ∈ ℕ → p ≤ A ↔ p ∈ ℕ ∧ p ≤ A
6 5 adantl ⊢ A ∈ ℕ ∧ p ∈ ℕ → p ≤ A ↔ p ∈ ℕ ∧ p ≤ A
7 nnz ⊢ A ∈ ℕ → A ∈ ℤ
8 7 adantr ⊢ A ∈ ℕ ∧ p ∈ ℕ → A ∈ ℤ
9 fznn ⊢ A ∈ ℤ → p ∈ 1 … A ↔ p ∈ ℕ ∧ p ≤ A
10 8 9 syl ⊢ A ∈ ℕ ∧ p ∈ ℕ → p ∈ 1 … A ↔ p ∈ ℕ ∧ p ≤ A
11 6 10 bitr4d ⊢ A ∈ ℕ ∧ p ∈ ℕ → p ≤ A ↔ p ∈ 1 … A
12 4 11 sylibd ⊢ A ∈ ℕ ∧ p ∈ ℕ → p ∥ A → p ∈ 1 … A
13 12 ralrimiva ⊢ A ∈ ℕ → ∀ p ∈ ℕ p ∥ A → p ∈ 1 … A
14 rabss ⊢ p ∈ ℕ | p ∥ A ⊆ 1 … A ↔ ∀ p ∈ ℕ p ∥ A → p ∈ 1 … A
15 13 14 sylibr ⊢ A ∈ ℕ → p ∈ ℕ | p ∥ A ⊆ 1 … A