Metamath Proof Explorer

Theorem mulmod0

Description: The product of an integer and a positive real number is 0 modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018) (Revised by AV, 5-Jul-2020)

		Ref	Expression
	Assertion	mulmod0	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to A \cdot M \mod M = 0$

Proof

Step	Hyp	Ref	Expression
1		zcn	$⊢ A \in ℤ \to A \in ℂ$
2	1	adantr	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to A \in ℂ$
3		rpcn	$⊢ M \in ℝ^{+} \to M \in ℂ$
4	3	adantl	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to M \in ℂ$
5		rpne0	$⊢ M \in ℝ^{+} \to M \neq 0$
6	5	adantl	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to M \neq 0$
7	2 4 6	divcan4d	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to \frac{A \cdot M}{M} = A$
8		simpl	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to A \in ℤ$
9	7 8	eqeltrd	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to \frac{A \cdot M}{M} \in ℤ$
10		zre	$⊢ A \in ℤ \to A \in ℝ$
11		rpre	$⊢ M \in ℝ^{+} \to M \in ℝ$
12		remulcl	$⊢ (A \in ℝ \land M \in ℝ) \to A \cdot M \in ℝ$
13	10 11 12	syl2an	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to A \cdot M \in ℝ$
14		mod0	$⊢ (A \cdot M \in ℝ \land M \in ℝ^{+}) \to (A \cdot M \mod M = 0 \leftrightarrow \frac{A \cdot M}{M} \in ℤ)$
15	13 14	sylancom	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to (A \cdot M \mod M = 0 \leftrightarrow \frac{A \cdot M}{M} \in ℤ)$
16	9 15	mpbird	$⊢ (A \in ℤ \land M \in ℝ^{+}) \to A \cdot M \mod M = 0$