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