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 )
2 1 adantl 
 |-  ( ( 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 )
7 6 adantl 
 |-  ( ( 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 ) )