This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem modsubmod

Description: The difference of a real number modulo a positive real number and another 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 modsubmod 
|- ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( ( ( A mod M ) - B ) 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 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> B e. RR )
5 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> M e. RR+ )
6 modabs2 
 |-  ( ( A e. RR /\ M e. RR+ ) -> ( ( A mod M ) mod M ) = ( A mod M ) )
7 6 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( ( A mod M ) mod M ) = ( A mod M ) )
8 eqidd 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( B mod M ) = ( B mod M ) )
9 2 3 4 4 5 7 8 modsub12d 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( ( ( A mod M ) - B ) mod M ) = ( ( A - B ) mod M ) )