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	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
Assertion	nznngen	⊢ ( 𝜑 → ( ( ∥ “ { 𝑁 } ) ∩ ℕ ) ⊆ ( ℤ≥ ‘ ( abs ‘ 𝑁 ) ) )

Proof

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