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

Metamath Proof Explorer

Theorem zdivgd

Description: Two ways to express " N is an integer multiple of M ". Originally a subproof of zdiv . (Contributed by SN, 25-Apr-2025)

Ref Expression
Hypotheses zdivgd.1 
|- ( ph -> M e. CC )
zdivgd.2 
|- ( ph -> N e. CC )
zdivgd.3 
|- ( ph -> M =/= 0 )
Assertion zdivgd 
|- ( ph -> ( E. k e. ZZ ( M x. k ) = N <-> ( N / M ) e. ZZ ) )

Proof

Step Hyp Ref Expression
1 zdivgd.1 
 |-  ( ph -> M e. CC )
2 zdivgd.2 
 |-  ( ph -> N e. CC )
3 zdivgd.3 
 |-  ( ph -> M =/= 0 )
4 zcn 
 |-  ( k e. ZZ -> k e. CC )
5 4 adantl 
 |-  ( ( ph /\ k e. ZZ ) -> k e. CC )
6 1 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> M e. CC )
7 3 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> M =/= 0 )
8 5 6 7 divcan3d 
 |-  ( ( ph /\ k e. ZZ ) -> ( ( M x. k ) / M ) = k )
9 oveq1 
 |-  ( ( M x. k ) = N -> ( ( M x. k ) / M ) = ( N / M ) )
10 8 9 sylan9req 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( M x. k ) = N ) -> k = ( N / M ) )
11 simplr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( M x. k ) = N ) -> k e. ZZ )
12 10 11 eqeltrrd 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( M x. k ) = N ) -> ( N / M ) e. ZZ )
13 12 rexlimdva2 
 |-  ( ph -> ( E. k e. ZZ ( M x. k ) = N -> ( N / M ) e. ZZ ) )
14 2 1 3 divcan2d 
 |-  ( ph -> ( M x. ( N / M ) ) = N )
15 oveq2 
 |-  ( k = ( N / M ) -> ( M x. k ) = ( M x. ( N / M ) ) )
16 15 eqeq1d 
 |-  ( k = ( N / M ) -> ( ( M x. k ) = N <-> ( M x. ( N / M ) ) = N ) )
17 16 rspcev 
 |-  ( ( ( N / M ) e. ZZ /\ ( M x. ( N / M ) ) = N ) -> E. k e. ZZ ( M x. k ) = N )
18 17 ex 
 |-  ( ( N / M ) e. ZZ -> ( ( M x. ( N / M ) ) = N -> E. k e. ZZ ( M x. k ) = N ) )
19 14 18 syl5com 
 |-  ( ph -> ( ( N / M ) e. ZZ -> E. k e. ZZ ( M x. k ) = N ) )
20 13 19 impbid 
 |-  ( ph -> ( E. k e. ZZ ( M x. k ) = N <-> ( N / M ) e. ZZ ) )