Metamath Proof Explorer


Theorem dvdsval2

Description: One nonzero integer divides another integer if and only if their quotient is an integer. (Contributed by Jeff Hankins, 29-Sep-2013)

Ref Expression
Assertion dvdsval2 M M 0 N M N N M

Proof

Step Hyp Ref Expression
1 divides M N M N k k M = N
2 1 3adant2 M M 0 N M N k k M = N
3 zcn N N
4 3 3ad2ant3 M M 0 N N
5 4 adantr M M 0 N k N
6 zcn k k
7 6 adantl M M 0 N k k
8 zcn M M
9 8 3ad2ant1 M M 0 N M
10 9 adantr M M 0 N k M
11 simpl2 M M 0 N k M 0
12 5 7 10 11 divmul3d M M 0 N k N M = k N = k M
13 eqcom N = k M k M = N
14 12 13 bitrdi M M 0 N k N M = k k M = N
15 14 biimprd M M 0 N k k M = N N M = k
16 15 impr M M 0 N k k M = N N M = k
17 simprl M M 0 N k k M = N k
18 16 17 eqeltrd M M 0 N k k M = N N M
19 18 rexlimdvaa M M 0 N k k M = N N M
20 simpr M M 0 N N M N M
21 simp2 M M 0 N M 0
22 4 9 21 divcan1d M M 0 N N M M = N
23 22 adantr M M 0 N N M N M M = N
24 oveq1 k = N M k M = N M M
25 24 eqeq1d k = N M k M = N N M M = N
26 25 rspcev N M N M M = N k k M = N
27 20 23 26 syl2anc M M 0 N N M k k M = N
28 27 ex M M 0 N N M k k M = N
29 19 28 impbid M M 0 N k k M = N N M
30 2 29 bitrd M M 0 N M N N M