Metamath Proof Explorer


Theorem zdiv

Description: Two ways to express " M divides N . (Contributed by NM, 3-Oct-2008)

Ref Expression
Assertion zdiv
|- ( ( M e. NN /\ N e. ZZ ) -> ( E. k e. ZZ ( M x. k ) = N <-> ( N / M ) e. ZZ ) )

Proof

Step Hyp Ref Expression
1 nnne0
 |-  ( M e. NN -> M =/= 0 )
2 1 adantr
 |-  ( ( M e. NN /\ N e. ZZ ) -> M =/= 0 )
3 nncn
 |-  ( M e. NN -> M e. CC )
4 zcn
 |-  ( N e. ZZ -> N e. CC )
5 zcn
 |-  ( k e. ZZ -> k e. CC )
6 divcan3
 |-  ( ( k e. CC /\ M e. CC /\ M =/= 0 ) -> ( ( M x. k ) / M ) = k )
7 6 3coml
 |-  ( ( M e. CC /\ M =/= 0 /\ k e. CC ) -> ( ( M x. k ) / M ) = k )
8 7 3expa
 |-  ( ( ( M e. CC /\ M =/= 0 ) /\ k e. CC ) -> ( ( M x. k ) / M ) = k )
9 5 8 sylan2
 |-  ( ( ( M e. CC /\ M =/= 0 ) /\ k e. ZZ ) -> ( ( M x. k ) / M ) = k )
10 9 3adantl2
 |-  ( ( ( M e. CC /\ N e. CC /\ M =/= 0 ) /\ k e. ZZ ) -> ( ( M x. k ) / M ) = k )
11 oveq1
 |-  ( ( M x. k ) = N -> ( ( M x. k ) / M ) = ( N / M ) )
12 10 11 sylan9req
 |-  ( ( ( ( M e. CC /\ N e. CC /\ M =/= 0 ) /\ k e. ZZ ) /\ ( M x. k ) = N ) -> k = ( N / M ) )
13 simplr
 |-  ( ( ( ( M e. CC /\ N e. CC /\ M =/= 0 ) /\ k e. ZZ ) /\ ( M x. k ) = N ) -> k e. ZZ )
14 12 13 eqeltrrd
 |-  ( ( ( ( M e. CC /\ N e. CC /\ M =/= 0 ) /\ k e. ZZ ) /\ ( M x. k ) = N ) -> ( N / M ) e. ZZ )
15 14 rexlimdva2
 |-  ( ( M e. CC /\ N e. CC /\ M =/= 0 ) -> ( E. k e. ZZ ( M x. k ) = N -> ( N / M ) e. ZZ ) )
16 divcan2
 |-  ( ( N e. CC /\ M e. CC /\ M =/= 0 ) -> ( M x. ( N / M ) ) = N )
17 16 3com12
 |-  ( ( M e. CC /\ N e. CC /\ M =/= 0 ) -> ( M x. ( N / M ) ) = N )
18 oveq2
 |-  ( k = ( N / M ) -> ( M x. k ) = ( M x. ( N / M ) ) )
19 18 eqeq1d
 |-  ( k = ( N / M ) -> ( ( M x. k ) = N <-> ( M x. ( N / M ) ) = N ) )
20 19 rspcev
 |-  ( ( ( N / M ) e. ZZ /\ ( M x. ( N / M ) ) = N ) -> E. k e. ZZ ( M x. k ) = N )
21 20 expcom
 |-  ( ( M x. ( N / M ) ) = N -> ( ( N / M ) e. ZZ -> E. k e. ZZ ( M x. k ) = N ) )
22 17 21 syl
 |-  ( ( M e. CC /\ N e. CC /\ M =/= 0 ) -> ( ( N / M ) e. ZZ -> E. k e. ZZ ( M x. k ) = N ) )
23 15 22 impbid
 |-  ( ( M e. CC /\ N e. CC /\ M =/= 0 ) -> ( E. k e. ZZ ( M x. k ) = N <-> ( N / M ) e. ZZ ) )
24 23 3expia
 |-  ( ( M e. CC /\ N e. CC ) -> ( M =/= 0 -> ( E. k e. ZZ ( M x. k ) = N <-> ( N / M ) e. ZZ ) ) )
25 3 4 24 syl2an
 |-  ( ( M e. NN /\ N e. ZZ ) -> ( M =/= 0 -> ( E. k e. ZZ ( M x. k ) = N <-> ( N / M ) e. ZZ ) ) )
26 2 25 mpd
 |-  ( ( M e. NN /\ N e. ZZ ) -> ( E. k e. ZZ ( M x. k ) = N <-> ( N / M ) e. ZZ ) )