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 
|- ( ph -> N e. ZZ )
Assertion nznngen 
|- ( ph -> ( ( || " { N } ) i^i NN ) C_ ( ZZ>= ` ( abs ` N ) ) )

Proof

Step Hyp Ref Expression
1 nznngen.n 
 |-  ( ph -> N e. ZZ )
2 reldvds 
 |-  Rel ||
3 relimasn 
 |-  ( Rel || -> ( || " { N } ) = { x | N || x } )
4 2 3 ax-mp 
 |-  ( || " { N } ) = { x | N || x }
5 4 ineq1i 
 |-  ( ( || " { N } ) i^i NN ) = ( { x | N || x } i^i NN )
6 dfrab2 
 |-  { x e. NN | N || x } = ( { x | N || x } i^i NN )
7 5 6 eqtr4i 
 |-  ( ( || " { N } ) i^i NN ) = { x e. NN | N || x }
8 7 eleq2i 
 |-  ( x e. ( ( || " { N } ) i^i NN ) <-> x e. { x e. NN | N || x } )
9 rabid 
 |-  ( x e. { x e. NN | N || x } <-> ( x e. NN /\ N || x ) )
10 nnz 
 |-  ( x e. NN -> x e. ZZ )
11 absdvdsb 
 |-  ( ( N e. ZZ /\ x e. ZZ ) -> ( N || x <-> ( abs ` N ) || x ) )
12 1 10 11 syl2an 
 |-  ( ( ph /\ x e. NN ) -> ( N || x <-> ( abs ` N ) || x ) )
13 zabscl 
 |-  ( N e. ZZ -> ( abs ` N ) e. ZZ )
14 1 13 syl 
 |-  ( ph -> ( abs ` N ) e. ZZ )
15 dvdsle 
 |-  ( ( ( abs ` N ) e. ZZ /\ x e. NN ) -> ( ( abs ` N ) || x -> ( abs ` N ) <_ x ) )
16 14 15 sylan 
 |-  ( ( ph /\ x e. NN ) -> ( ( abs ` N ) || x -> ( abs ` N ) <_ x ) )
17 12 16 sylbid 
 |-  ( ( ph /\ x e. NN ) -> ( N || x -> ( abs ` N ) <_ x ) )
18 17 impr 
 |-  ( ( ph /\ ( x e. NN /\ N || x ) ) -> ( abs ` N ) <_ x )
19 9 18 sylan2b 
 |-  ( ( ph /\ x e. { x e. NN | N || x } ) -> ( abs ` N ) <_ x )
20 9 simplbi 
 |-  ( x e. { x e. NN | N || x } -> x e. NN )
21 20 nnzd 
 |-  ( x e. { x e. NN | N || x } -> x e. ZZ )
22 eluz 
 |-  ( ( ( abs ` N ) e. ZZ /\ x e. ZZ ) -> ( x e. ( ZZ>= ` ( abs ` N ) ) <-> ( abs ` N ) <_ x ) )
23 14 21 22 syl2an 
 |-  ( ( ph /\ x e. { x e. NN | N || x } ) -> ( x e. ( ZZ>= ` ( abs ` N ) ) <-> ( abs ` N ) <_ x ) )
24 19 23 mpbird 
 |-  ( ( ph /\ x e. { x e. NN | N || x } ) -> x e. ( ZZ>= ` ( abs ` N ) ) )
25 8 24 sylan2b 
 |-  ( ( ph /\ x e. ( ( || " { N } ) i^i NN ) ) -> x e. ( ZZ>= ` ( abs ` N ) ) )
26 25 ex 
 |-  ( ph -> ( x e. ( ( || " { N } ) i^i NN ) -> x e. ( ZZ>= ` ( abs ` N ) ) ) )
27 26 ssrdv 
 |-  ( ph -> ( ( || " { N } ) i^i NN ) C_ ( ZZ>= ` ( abs ` N ) ) )