Metamath Proof Explorer

Theorem modsubmodmod

Description: The difference of a real number modulo a positive real number and another real number modulo this positive real number equals the difference of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018)

Ref Expression
Assertion modsubmodmod 
|- ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( ( ( A mod M ) - ( B mod M ) ) mod M ) = ( ( A - B ) mod M ) )

Proof

Step Hyp Ref Expression
1 modcl 
 |-  ( ( A e. RR /\ M e. RR+ ) -> ( A mod M ) e. RR )
2 1 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( A mod M ) e. RR )
3 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> A e. RR )
4 modcl 
 |-  ( ( B e. RR /\ M e. RR+ ) -> ( B mod M ) e. RR )
5 4 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( B mod M ) e. RR )
6 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> B e. RR )
7 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> M e. RR+ )
8 modabs2 
 |-  ( ( A e. RR /\ M e. RR+ ) -> ( ( A mod M ) mod M ) = ( A mod M ) )
9 8 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( ( A mod M ) mod M ) = ( A mod M ) )
10 modabs2 
 |-  ( ( B e. RR /\ M e. RR+ ) -> ( ( B mod M ) mod M ) = ( B mod M ) )
11 10 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( ( B mod M ) mod M ) = ( B mod M ) )
12 2 3 5 6 7 9 11 modsub12d 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( ( ( A mod M ) - ( B mod M ) ) mod M ) = ( ( A - B ) mod M ) )