mod0mul

Description: If an integer is 0 modulo a positive integer, this integer must be the product of another integer and the modulus. (Contributed by AV, 7-Jun-2020)

		Ref	Expression
	Assertion	mod0mul	$⊢ (A \in ℤ \land N \in ℕ) \to (A \mod N = 0 \to \exists x \in ℤ A = x \cdot N)$

Proof

Step	Hyp	Ref	Expression
1		zre	$⊢ A \in ℤ \to A \in ℝ$
2		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
3		mod0	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to (A \mod N = 0 \leftrightarrow \frac{A}{N} \in ℤ)$
4	1 2 3	syl2an	$⊢ (A \in ℤ \land N \in ℕ) \to (A \mod N = 0 \leftrightarrow \frac{A}{N} \in ℤ)$
5		simpr	$⊢ ((A \in ℤ \land N \in ℕ) \land \frac{A}{N} \in ℤ) \to \frac{A}{N} \in ℤ$
6		oveq1	$⊢ x = \frac{A}{N} \to x \cdot N = (\frac{A}{N}) \cdot N$
7	6	eqeq2d	$⊢ x = \frac{A}{N} \to (A = x \cdot N \leftrightarrow A = (\frac{A}{N}) \cdot N)$
8	7	adantl	$⊢ (((A \in ℤ \land N \in ℕ) \land \frac{A}{N} \in ℤ) \land x = \frac{A}{N}) \to (A = x \cdot N \leftrightarrow A = (\frac{A}{N}) \cdot N)$
9		zcn	$⊢ A \in ℤ \to A \in ℂ$
10	9	adantr	$⊢ (A \in ℤ \land N \in ℕ) \to A \in ℂ$
11		nncn	$⊢ N \in ℕ \to N \in ℂ$
12	11	adantl	$⊢ (A \in ℤ \land N \in ℕ) \to N \in ℂ$
13		nnne0	$⊢ N \in ℕ \to N \neq 0$
14	13	adantl	$⊢ (A \in ℤ \land N \in ℕ) \to N \neq 0$
15	10 12 14	divcan1d	$⊢ (A \in ℤ \land N \in ℕ) \to (\frac{A}{N}) \cdot N = A$
16	15	adantr	$⊢ ((A \in ℤ \land N \in ℕ) \land \frac{A}{N} \in ℤ) \to (\frac{A}{N}) \cdot N = A$
17	16	eqcomd	$⊢ ((A \in ℤ \land N \in ℕ) \land \frac{A}{N} \in ℤ) \to A = (\frac{A}{N}) \cdot N$
18	5 8 17	rspcedvd	$⊢ ((A \in ℤ \land N \in ℕ) \land \frac{A}{N} \in ℤ) \to \exists x \in ℤ A = x \cdot N$
19	18	ex	$⊢ (A \in ℤ \land N \in ℕ) \to (\frac{A}{N} \in ℤ \to \exists x \in ℤ A = x \cdot N)$
20	4 19	sylbid	$⊢ (A \in ℤ \land N \in ℕ) \to (A \mod N = 0 \to \exists x \in ℤ A = x \cdot N)$

Metamath Proof Explorer

Theorem mod0mul

Proof