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	$⊢ φ \to M \in ℂ$
	zdivgd.2	$⊢ φ \to N \in ℂ$
	zdivgd.3	$⊢ φ \to M \neq 0$
Assertion	zdivgd	$⊢ φ \to (\exists k \in ℤ M k = N \leftrightarrow \frac{N}{M} \in ℤ)$

Step	Hyp	Ref	Expression
1		zdivgd.1	$⊢ φ \to M \in ℂ$
2		zdivgd.2	$⊢ φ \to N \in ℂ$
3		zdivgd.3	$⊢ φ \to M \neq 0$
4		zcn	$⊢ k \in ℤ \to k \in ℂ$
5	4	adantl	$⊢ (φ \land k \in ℤ) \to k \in ℂ$
6	1	adantr	$⊢ (φ \land k \in ℤ) \to M \in ℂ$
7	3	adantr	$⊢ (φ \land k \in ℤ) \to M \neq 0$
8	5 6 7	divcan3d	$⊢ (φ \land k \in ℤ) \to \frac{M k}{M} = k$
9		oveq1	$⊢ M k = N \to \frac{M k}{M} = \frac{N}{M}$
10	8 9	sylan9req	$⊢ ((φ \land k \in ℤ) \land M k = N) \to k = \frac{N}{M}$
11		simplr	$⊢ ((φ \land k \in ℤ) \land M k = N) \to k \in ℤ$
12	10 11	eqeltrrd	$⊢ ((φ \land k \in ℤ) \land M k = N) \to \frac{N}{M} \in ℤ$
13	12	rexlimdva2	$⊢ φ \to (\exists k \in ℤ M k = N \to \frac{N}{M} \in ℤ)$
14	2 1 3	divcan2d	$⊢ φ \to M (\frac{N}{M}) = N$
15		oveq2	$⊢ k = \frac{N}{M} \to M k = M (\frac{N}{M})$
16	15	eqeq1d	$⊢ k = \frac{N}{M} \to (M k = N \leftrightarrow M (\frac{N}{M}) = N)$
17	16	rspcev	$⊢ (\frac{N}{M} \in ℤ \land M (\frac{N}{M}) = N) \to \exists k \in ℤ M k = N$
18	17	ex	$⊢ \frac{N}{M} \in ℤ \to (M (\frac{N}{M}) = N \to \exists k \in ℤ M k = N)$
19	14 18	syl5com	$⊢ φ \to (\frac{N}{M} \in ℤ \to \exists k \in ℤ M k = N)$
20	13 19	impbid	$⊢ φ \to (\exists k \in ℤ M k = N \leftrightarrow \frac{N}{M} \in ℤ)$

Metamath Proof Explorer