# 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 ${⊢}\left({A}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\to {A}\cdot {M}\mathrm{mod}{M}=0$

### Proof

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