# Metamath Proof Explorer

## Theorem modm1p1mod0

Description: If a real number modulo a positive real number equals the positive real number decreased by 1, the real number increased by 1 modulo the positive real number equals 0. (Contributed by AV, 2-Nov-2018)

Ref Expression
Assertion modm1p1mod0 ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{M}={M}-1\to \left({A}+1\right)\mathrm{mod}{M}=0\right)$

### Proof

Step Hyp Ref Expression
1 1re ${⊢}1\in ℝ$
2 modaddmod ${⊢}\left({A}\in ℝ\wedge 1\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left(\left({A}\mathrm{mod}{M}\right)+1\right)\mathrm{mod}{M}=\left({A}+1\right)\mathrm{mod}{M}$
3 1 2 mp3an2 ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left(\left({A}\mathrm{mod}{M}\right)+1\right)\mathrm{mod}{M}=\left({A}+1\right)\mathrm{mod}{M}$
4 3 eqcomd ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({A}+1\right)\mathrm{mod}{M}=\left(\left({A}\mathrm{mod}{M}\right)+1\right)\mathrm{mod}{M}$
5 4 adantr ${⊢}\left(\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={M}-1\right)\to \left({A}+1\right)\mathrm{mod}{M}=\left(\left({A}\mathrm{mod}{M}\right)+1\right)\mathrm{mod}{M}$
6 oveq1 ${⊢}{A}\mathrm{mod}{M}={M}-1\to \left({A}\mathrm{mod}{M}\right)+1={M}-1+1$
7 6 oveq1d ${⊢}{A}\mathrm{mod}{M}={M}-1\to \left(\left({A}\mathrm{mod}{M}\right)+1\right)\mathrm{mod}{M}=\left({M}-1+1\right)\mathrm{mod}{M}$
8 rpcn ${⊢}{M}\in {ℝ}^{+}\to {M}\in ℂ$
9 npcan1 ${⊢}{M}\in ℂ\to {M}-1+1={M}$
10 8 9 syl ${⊢}{M}\in {ℝ}^{+}\to {M}-1+1={M}$
11 10 oveq1d ${⊢}{M}\in {ℝ}^{+}\to \left({M}-1+1\right)\mathrm{mod}{M}={M}\mathrm{mod}{M}$
12 modid0 ${⊢}{M}\in {ℝ}^{+}\to {M}\mathrm{mod}{M}=0$
13 11 12 eqtrd ${⊢}{M}\in {ℝ}^{+}\to \left({M}-1+1\right)\mathrm{mod}{M}=0$
14 13 adantl ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({M}-1+1\right)\mathrm{mod}{M}=0$
15 7 14 sylan9eqr ${⊢}\left(\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={M}-1\right)\to \left(\left({A}\mathrm{mod}{M}\right)+1\right)\mathrm{mod}{M}=0$
16 5 15 eqtrd ${⊢}\left(\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{M}={M}-1\right)\to \left({A}+1\right)\mathrm{mod}{M}=0$
17 16 ex ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{M}={M}-1\to \left({A}+1\right)\mathrm{mod}{M}=0\right)$