This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvdsleabs2

Description: Transfer divisibility to an order constraint on absolute values. (Contributed by Stefan O'Rear, 24-Sep-2014)

Ref Expression
Assertion dvdsleabs2 
|- ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( M || N -> ( abs ` M ) <_ ( abs ` N ) ) )

Proof

Step Hyp Ref Expression
1 zabscl 
 |-  ( M e. ZZ -> ( abs ` M ) e. ZZ )
2 1 3anim1i 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( ( abs ` M ) e. ZZ /\ N e. ZZ /\ N =/= 0 ) )
3 2 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ M || N ) -> ( ( abs ` M ) e. ZZ /\ N e. ZZ /\ N =/= 0 ) )
4 absdvdsb 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> ( abs ` M ) || N ) )
5 4 3adant3 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( M || N <-> ( abs ` M ) || N ) )
6 5 biimpa 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ M || N ) -> ( abs ` M ) || N )
7 dvdsleabs 
 |-  ( ( ( abs ` M ) e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( ( abs ` M ) || N -> ( abs ` M ) <_ ( abs ` N ) ) )
8 3 6 7 sylc 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ M || N ) -> ( abs ` M ) <_ ( abs ` N ) )
9 8 ex 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( M || N -> ( abs ` M ) <_ ( abs ` N ) ) )