# Metamath Proof Explorer

Description: The sum of a positive real number less than an upper bound and the product of an integer and the upper bound is the positive real number modulo the upper bound. (Contributed by AV, 5-Jul-2020)

Ref Expression
Assertion muladdmodid ${⊢}\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\wedge {A}\in \left[0,{M}\right)\right)\to \left({N}\cdot {M}+{A}\right)\mathrm{mod}{M}={A}$

### Proof

Step Hyp Ref Expression
1 0red ${⊢}{M}\in {ℝ}^{+}\to 0\in ℝ$
2 rpxr ${⊢}{M}\in {ℝ}^{+}\to {M}\in {ℝ}^{*}$
3 elico2 ${⊢}\left(0\in ℝ\wedge {M}\in {ℝ}^{*}\right)\to \left({A}\in \left[0,{M}\right)↔\left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\right)$
4 1 2 3 syl2anc ${⊢}{M}\in {ℝ}^{+}\to \left({A}\in \left[0,{M}\right)↔\left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\right)$
5 4 adantl ${⊢}\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\in \left[0,{M}\right)↔\left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\right)$
6 zcn ${⊢}{N}\in ℤ\to {N}\in ℂ$
7 rpcn ${⊢}{M}\in {ℝ}^{+}\to {M}\in ℂ$
8 mulcl ${⊢}\left({N}\in ℂ\wedge {M}\in ℂ\right)\to {N}\cdot {M}\in ℂ$
9 6 7 8 syl2an ${⊢}\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\to {N}\cdot {M}\in ℂ$
10 9 adantr ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\wedge \left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\right)\to {N}\cdot {M}\in ℂ$
11 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
12 11 3ad2ant1 ${⊢}\left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\to {A}\in ℂ$
13 12 adantl ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\wedge \left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\right)\to {A}\in ℂ$
14 10 13 addcomd ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\wedge \left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\right)\to {N}\cdot {M}+{A}={A}+{N}\cdot {M}$
15 14 oveq1d ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\wedge \left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\right)\to \left({N}\cdot {M}+{A}\right)\mathrm{mod}{M}=\left({A}+{N}\cdot {M}\right)\mathrm{mod}{M}$
16 simp1 ${⊢}\left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\to {A}\in ℝ$
17 16 adantl ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\wedge \left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\right)\to {A}\in ℝ$
18 simpr ${⊢}\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\to {M}\in {ℝ}^{+}$
19 18 adantr ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\wedge \left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\right)\to {M}\in {ℝ}^{+}$
20 simpll ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\wedge \left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\right)\to {N}\in ℤ$
21 modcyc ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\wedge {N}\in ℤ\right)\to \left({A}+{N}\cdot {M}\right)\mathrm{mod}{M}={A}\mathrm{mod}{M}$
22 17 19 20 21 syl3anc ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\wedge \left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\right)\to \left({A}+{N}\cdot {M}\right)\mathrm{mod}{M}={A}\mathrm{mod}{M}$
23 18 16 anim12ci ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\wedge \left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\right)\to \left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)$
24 3simpc ${⊢}\left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\to \left(0\le {A}\wedge {A}<{M}\right)$
25 24 adantl ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\wedge \left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\right)\to \left(0\le {A}\wedge {A}<{M}\right)$
26 modid ${⊢}\left(\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\wedge \left(0\le {A}\wedge {A}<{M}\right)\right)\to {A}\mathrm{mod}{M}={A}$
27 23 25 26 syl2anc ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\wedge \left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\right)\to {A}\mathrm{mod}{M}={A}$
28 15 22 27 3eqtrd ${⊢}\left(\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\wedge \left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\right)\to \left({N}\cdot {M}+{A}\right)\mathrm{mod}{M}={A}$
29 28 ex ${⊢}\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\to \left(\left({A}\in ℝ\wedge 0\le {A}\wedge {A}<{M}\right)\to \left({N}\cdot {M}+{A}\right)\mathrm{mod}{M}={A}\right)$
30 5 29 sylbid ${⊢}\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\in \left[0,{M}\right)\to \left({N}\cdot {M}+{A}\right)\mathrm{mod}{M}={A}\right)$
31 30 3impia ${⊢}\left({N}\in ℤ\wedge {M}\in {ℝ}^{+}\wedge {A}\in \left[0,{M}\right)\right)\to \left({N}\cdot {M}+{A}\right)\mathrm{mod}{M}={A}$