Metamath Proof Explorer

Theorem nznngen

Description: All positive integers in the set of multiples ofn, nℤ, are the absolute value ofn or greater. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Hypothesis nznngen.n ⊢ φ → N ∈ ℤ
Assertion nznngen ⊢ φ → ∥ N ∩ ℕ ⊆ ℤ ≥ N

Proof

Step Hyp Ref Expression
1 nznngen.n ⊢ φ → N ∈ ℤ
2 reldvds ⊢ Rel ⁡ ∥
3 relimasn ⊢ Rel ⁡ ∥ → ∥ N = x | N ∥ x
4 2 3 ax-mp ⊢ ∥ N = x | N ∥ x
5 4 ineq1i ⊢ ∥ N ∩ ℕ = x | N ∥ x ∩ ℕ
6 dfrab2 ⊢ x ∈ ℕ | N ∥ x = x | N ∥ x ∩ ℕ
7 5 6 eqtr4i ⊢ ∥ N ∩ ℕ = x ∈ ℕ | N ∥ x
8 7 eleq2i ⊢ x ∈ ∥ N ∩ ℕ ↔ x ∈ x ∈ ℕ | N ∥ x
9 rabid ⊢ x ∈ x ∈ ℕ | N ∥ x ↔ x ∈ ℕ ∧ N ∥ x
10 nnz ⊢ x ∈ ℕ → x ∈ ℤ
11 absdvdsb ⊢ N ∈ ℤ ∧ x ∈ ℤ → N ∥ x ↔ N ∥ x
12 1 10 11 syl2an ⊢ φ ∧ x ∈ ℕ → N ∥ x ↔ N ∥ x
13 zabscl ⊢ N ∈ ℤ → N ∈ ℤ
14 1 13 syl ⊢ φ → N ∈ ℤ
15 dvdsle ⊢ N ∈ ℤ ∧ x ∈ ℕ → N ∥ x → N ≤ x
16 14 15 sylan ⊢ φ ∧ x ∈ ℕ → N ∥ x → N ≤ x
17 12 16 sylbid ⊢ φ ∧ x ∈ ℕ → N ∥ x → N ≤ x
18 17 impr ⊢ φ ∧ x ∈ ℕ ∧ N ∥ x → N ≤ x
19 9 18 sylan2b ⊢ φ ∧ x ∈ x ∈ ℕ | N ∥ x → N ≤ x
20 9 simplbi ⊢ x ∈ x ∈ ℕ | N ∥ x → x ∈ ℕ
21 20 nnzd ⊢ x ∈ x ∈ ℕ | N ∥ x → x ∈ ℤ
22 eluz ⊢ N ∈ ℤ ∧ x ∈ ℤ → x ∈ ℤ ≥ N ↔ N ≤ x
23 14 21 22 syl2an ⊢ φ ∧ x ∈ x ∈ ℕ | N ∥ x → x ∈ ℤ ≥ N ↔ N ≤ x
24 19 23 mpbird ⊢ φ ∧ x ∈ x ∈ ℕ | N ∥ x → x ∈ ℤ ≥ N
25 8 24 sylan2b ⊢ φ ∧ x ∈ ∥ N ∩ ℕ → x ∈ ℤ ≥ N
26 25 ex ⊢ φ → x ∈ ∥ N ∩ ℕ → x ∈ ℤ ≥ N
27 26 ssrdv ⊢ φ → ∥ N ∩ ℕ ⊆ ℤ ≥ N