# Metamath Proof Explorer

## Theorem modcyc2

Description: The modulo operation is periodic. (Contributed by NM, 12-Nov-2008)

Ref Expression
Assertion modcyc2 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\wedge {N}\in ℤ\right)\to \left({A}-{B}\cdot {N}\right)\mathrm{mod}{B}={A}\mathrm{mod}{B}$

### Proof

Step Hyp Ref Expression
1 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
2 rpcn ${⊢}{B}\in {ℝ}^{+}\to {B}\in ℂ$
3 zcn ${⊢}{N}\in ℤ\to {N}\in ℂ$
4 mulneg1 ${⊢}\left({N}\in ℂ\wedge {B}\in ℂ\right)\to -{N}{B}=-{N}{B}$
5 4 ancoms ${⊢}\left({B}\in ℂ\wedge {N}\in ℂ\right)\to -{N}{B}=-{N}{B}$
6 mulcom ${⊢}\left({B}\in ℂ\wedge {N}\in ℂ\right)\to {B}\cdot {N}={N}{B}$
7 6 negeqd ${⊢}\left({B}\in ℂ\wedge {N}\in ℂ\right)\to -{B}\cdot {N}=-{N}{B}$
8 5 7 eqtr4d ${⊢}\left({B}\in ℂ\wedge {N}\in ℂ\right)\to -{N}{B}=-{B}\cdot {N}$
9 8 3adant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {N}\in ℂ\right)\to -{N}{B}=-{B}\cdot {N}$
10 9 oveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {N}\in ℂ\right)\to {A}+-{N}{B}={A}+\left(-{B}\cdot {N}\right)$
11 mulcl ${⊢}\left({B}\in ℂ\wedge {N}\in ℂ\right)\to {B}\cdot {N}\in ℂ$
12 negsub ${⊢}\left({A}\in ℂ\wedge {B}\cdot {N}\in ℂ\right)\to {A}+\left(-{B}\cdot {N}\right)={A}-{B}\cdot {N}$
13 11 12 sylan2 ${⊢}\left({A}\in ℂ\wedge \left({B}\in ℂ\wedge {N}\in ℂ\right)\right)\to {A}+\left(-{B}\cdot {N}\right)={A}-{B}\cdot {N}$
14 13 3impb ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {N}\in ℂ\right)\to {A}+\left(-{B}\cdot {N}\right)={A}-{B}\cdot {N}$
15 10 14 eqtr2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {N}\in ℂ\right)\to {A}-{B}\cdot {N}={A}+-{N}{B}$
16 1 2 3 15 syl3an ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\wedge {N}\in ℤ\right)\to {A}-{B}\cdot {N}={A}+-{N}{B}$
17 16 oveq1d ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\wedge {N}\in ℤ\right)\to \left({A}-{B}\cdot {N}\right)\mathrm{mod}{B}=\left({A}+-{N}{B}\right)\mathrm{mod}{B}$
18 znegcl ${⊢}{N}\in ℤ\to -{N}\in ℤ$
19 modcyc ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\wedge -{N}\in ℤ\right)\to \left({A}+-{N}{B}\right)\mathrm{mod}{B}={A}\mathrm{mod}{B}$
20 18 19 syl3an3 ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\wedge {N}\in ℤ\right)\to \left({A}+-{N}{B}\right)\mathrm{mod}{B}={A}\mathrm{mod}{B}$
21 17 20 eqtrd ${⊢}\left({A}\in ℝ\wedge {B}\in {ℝ}^{+}\wedge {N}\in ℤ\right)\to \left({A}-{B}\cdot {N}\right)\mathrm{mod}{B}={A}\mathrm{mod}{B}$