# Metamath Proof Explorer

## Theorem modeqmodmin

Description: A real number equals the difference of the real number and a positive real number modulo the positive real number. (Contributed by AV, 3-Nov-2018)

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

### Proof

Step Hyp Ref Expression
1 modid0 ${⊢}{M}\in {ℝ}^{+}\to {M}\mathrm{mod}{M}=0$
2 1 adantl ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to {M}\mathrm{mod}{M}=0$
3 modge0 ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to 0\le {A}\mathrm{mod}{M}$
4 2 3 eqbrtrd ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to {M}\mathrm{mod}{M}\le {A}\mathrm{mod}{M}$
5 simpl ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to {A}\in ℝ$
6 rpre ${⊢}{M}\in {ℝ}^{+}\to {M}\in ℝ$
7 6 adantl ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to {M}\in ℝ$
8 simpr ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to {M}\in {ℝ}^{+}$
9 modsubdir ${⊢}\left({A}\in ℝ\wedge {M}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({M}\mathrm{mod}{M}\le {A}\mathrm{mod}{M}↔\left({A}-{M}\right)\mathrm{mod}{M}=\left({A}\mathrm{mod}{M}\right)-\left({M}\mathrm{mod}{M}\right)\right)$
10 5 7 8 9 syl3anc ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({M}\mathrm{mod}{M}\le {A}\mathrm{mod}{M}↔\left({A}-{M}\right)\mathrm{mod}{M}=\left({A}\mathrm{mod}{M}\right)-\left({M}\mathrm{mod}{M}\right)\right)$
11 4 10 mpbid ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({A}-{M}\right)\mathrm{mod}{M}=\left({A}\mathrm{mod}{M}\right)-\left({M}\mathrm{mod}{M}\right)$
12 2 eqcomd ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to 0={M}\mathrm{mod}{M}$
13 12 oveq2d ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{M}\right)-0=\left({A}\mathrm{mod}{M}\right)-\left({M}\mathrm{mod}{M}\right)$
14 modcl ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{M}\in ℝ$
15 14 recnd ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{M}\in ℂ$
16 15 subid1d ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{M}\right)-0={A}\mathrm{mod}{M}$
17 11 13 16 3eqtr2rd ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{M}=\left({A}-{M}\right)\mathrm{mod}{M}$