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 e. ZZ /\ M =/= 0 /\ N e. ZZ ) -> ( M || N <-> ( N / M ) e. ZZ ) )

Proof

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