# 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
`|- ( ( A e. RR /\ M e. RR+ ) -> ( A mod M ) = ( ( A - M ) mod M ) )`

### Proof

Step Hyp Ref Expression
1 modid0
` |-  ( M e. RR+ -> ( M mod M ) = 0 )`
` |-  ( ( A e. RR /\ M e. RR+ ) -> ( M mod M ) = 0 )`
3 modge0
` |-  ( ( A e. RR /\ M e. RR+ ) -> 0 <_ ( A mod M ) )`
4 2 3 eqbrtrd
` |-  ( ( A e. RR /\ M e. RR+ ) -> ( M mod M ) <_ ( A mod M ) )`
5 simpl
` |-  ( ( A e. RR /\ M e. RR+ ) -> A e. RR )`
6 rpre
` |-  ( M e. RR+ -> M e. RR )`
` |-  ( ( A e. RR /\ M e. RR+ ) -> M e. RR )`
8 simpr
` |-  ( ( A e. RR /\ M e. RR+ ) -> M e. RR+ )`
9 modsubdir
` |-  ( ( A e. RR /\ M e. RR /\ M e. RR+ ) -> ( ( M mod M ) <_ ( A mod M ) <-> ( ( A - M ) mod M ) = ( ( A mod M ) - ( M mod M ) ) ) )`
10 5 7 8 9 syl3anc
` |-  ( ( A e. RR /\ M e. RR+ ) -> ( ( M mod M ) <_ ( A mod M ) <-> ( ( A - M ) mod M ) = ( ( A mod M ) - ( M mod M ) ) ) )`
11 4 10 mpbid
` |-  ( ( A e. RR /\ M e. RR+ ) -> ( ( A - M ) mod M ) = ( ( A mod M ) - ( M mod M ) ) )`
12 2 eqcomd
` |-  ( ( A e. RR /\ M e. RR+ ) -> 0 = ( M mod M ) )`
13 12 oveq2d
` |-  ( ( A e. RR /\ M e. RR+ ) -> ( ( A mod M ) - 0 ) = ( ( A mod M ) - ( M mod M ) ) )`
14 modcl
` |-  ( ( A e. RR /\ M e. RR+ ) -> ( A mod M ) e. RR )`
15 14 recnd
` |-  ( ( A e. RR /\ M e. RR+ ) -> ( A mod M ) e. CC )`
16 15 subid1d
` |-  ( ( A e. RR /\ M e. RR+ ) -> ( ( A mod M ) - 0 ) = ( A mod M ) )`
17 11 13 16 3eqtr2rd
` |-  ( ( A e. RR /\ M e. RR+ ) -> ( A mod M ) = ( ( A - M ) mod M ) )`