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