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 MNN0MNMN

Proof

Step Hyp Ref Expression
1 zabscl MM
2 1 3anim1i MNN0MNN0
3 2 adantr MNN0MNMNN0
4 absdvdsb MNMNMN
5 4 3adant3 MNN0MNMN
6 5 biimpa MNN0MNMN
7 dvdsleabs MNN0MNMN
8 3 6 7 sylc MNN0MNMN
9 8 ex MNN0MNMN