# Metamath Proof Explorer

## Theorem negmod

Description: The negation of a number modulo a positive number is equal to the difference of the modulus and the number modulo the modulus. (Contributed by AV, 5-Jul-2020)

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

### Proof

Step Hyp Ref Expression
1 rpcn ${⊢}{N}\in {ℝ}^{+}\to {N}\in ℂ$
2 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
3 negsub ${⊢}\left({N}\in ℂ\wedge {A}\in ℂ\right)\to {N}+\left(-{A}\right)={N}-{A}$
4 1 2 3 syl2anr ${⊢}\left({A}\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to {N}+\left(-{A}\right)={N}-{A}$
5 4 eqcomd ${⊢}\left({A}\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to {N}-{A}={N}+\left(-{A}\right)$
6 5 oveq1d ${⊢}\left({A}\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to \left({N}-{A}\right)\mathrm{mod}{N}=\left({N}+\left(-{A}\right)\right)\mathrm{mod}{N}$
7 1 mulid2d ${⊢}{N}\in {ℝ}^{+}\to 1\cdot {N}={N}$
8 7 adantl ${⊢}\left({A}\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to 1\cdot {N}={N}$
9 8 oveq1d ${⊢}\left({A}\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to 1\cdot {N}+\left(-{A}\right)={N}+\left(-{A}\right)$
10 9 oveq1d ${⊢}\left({A}\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to \left(1\cdot {N}+\left(-{A}\right)\right)\mathrm{mod}{N}=\left({N}+\left(-{A}\right)\right)\mathrm{mod}{N}$
11 1cnd ${⊢}{A}\in ℝ\to 1\in ℂ$
12 mulcl ${⊢}\left(1\in ℂ\wedge {N}\in ℂ\right)\to 1\cdot {N}\in ℂ$
13 11 1 12 syl2an ${⊢}\left({A}\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to 1\cdot {N}\in ℂ$
14 renegcl ${⊢}{A}\in ℝ\to -{A}\in ℝ$
15 14 recnd ${⊢}{A}\in ℝ\to -{A}\in ℂ$
16 15 adantr ${⊢}\left({A}\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to -{A}\in ℂ$
17 13 16 addcomd ${⊢}\left({A}\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to 1\cdot {N}+\left(-{A}\right)=-{A}+1\cdot {N}$
18 17 oveq1d ${⊢}\left({A}\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to \left(1\cdot {N}+\left(-{A}\right)\right)\mathrm{mod}{N}=\left(-{A}+1\cdot {N}\right)\mathrm{mod}{N}$
19 14 adantr ${⊢}\left({A}\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to -{A}\in ℝ$
20 simpr ${⊢}\left({A}\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to {N}\in {ℝ}^{+}$
21 1zzd ${⊢}\left({A}\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to 1\in ℤ$
22 modcyc ${⊢}\left(-{A}\in ℝ\wedge {N}\in {ℝ}^{+}\wedge 1\in ℤ\right)\to \left(-{A}+1\cdot {N}\right)\mathrm{mod}{N}=\left(-{A}\right)\mathrm{mod}{N}$
23 19 20 21 22 syl3anc ${⊢}\left({A}\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to \left(-{A}+1\cdot {N}\right)\mathrm{mod}{N}=\left(-{A}\right)\mathrm{mod}{N}$
24 18 23 eqtrd ${⊢}\left({A}\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to \left(1\cdot {N}+\left(-{A}\right)\right)\mathrm{mod}{N}=\left(-{A}\right)\mathrm{mod}{N}$
25 6 10 24 3eqtr2rd ${⊢}\left({A}\in ℝ\wedge {N}\in {ℝ}^{+}\right)\to \left(-{A}\right)\mathrm{mod}{N}=\left({N}-{A}\right)\mathrm{mod}{N}$