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

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 ) )