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	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
	zdivgd.2	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
	zdivgd.3	⊢ ( 𝜑 → 𝑀 ≠ 0 )
Assertion	zdivgd	⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) )

Proof

Step	Hyp	Ref	Expression
1		zdivgd.1	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
2		zdivgd.2	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
3		zdivgd.3	⊢ ( 𝜑 → 𝑀 ≠ 0 )
4		zcn	⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℂ )
5	4	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℂ )
6	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑀 ∈ ℂ )
7	3	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑀 ≠ 0 )
8	5 6 7	divcan3d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( 𝑀 · 𝑘 ) / 𝑀 ) = 𝑘 )
9		oveq1	⊢ ( ( 𝑀 · 𝑘 ) = 𝑁 → ( ( 𝑀 · 𝑘 ) / 𝑀 ) = ( 𝑁 / 𝑀 ) )
10	8 9	sylan9req	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑀 · 𝑘 ) = 𝑁 ) → 𝑘 = ( 𝑁 / 𝑀 ) )
11		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑀 · 𝑘 ) = 𝑁 ) → 𝑘 ∈ ℤ )
12	10 11	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑀 · 𝑘 ) = 𝑁 ) → ( 𝑁 / 𝑀 ) ∈ ℤ )
13	12	rexlimdva2	⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 → ( 𝑁 / 𝑀 ) ∈ ℤ ) )
14	2 1 3	divcan2d	⊢ ( 𝜑 → ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 )
15		oveq2	⊢ ( 𝑘 = ( 𝑁 / 𝑀 ) → ( 𝑀 · 𝑘 ) = ( 𝑀 · ( 𝑁 / 𝑀 ) ) )
16	15	eqeq1d	⊢ ( 𝑘 = ( 𝑁 / 𝑀 ) → ( ( 𝑀 · 𝑘 ) = 𝑁 ↔ ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 ) )
17	16	rspcev	⊢ ( ( ( 𝑁 / 𝑀 ) ∈ ℤ ∧ ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 ) → ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 )
18	17	ex	⊢ ( ( 𝑁 / 𝑀 ) ∈ ℤ → ( ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 → ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ) )
19	14 18	syl5com	⊢ ( 𝜑 → ( ( 𝑁 / 𝑀 ) ∈ ℤ → ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ) )
20	13 19	impbid	⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) )