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

Metamath Proof Explorer

Theorem modadd2mod

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

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

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( B e. RR -> B e. CC )
2 1 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> B e. CC )
3 modcl 
 |-  ( ( A e. RR /\ M e. RR+ ) -> ( A mod M ) e. RR )
4 3 recnd 
 |-  ( ( A e. RR /\ M e. RR+ ) -> ( A mod M ) e. CC )
5 4 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( A mod M ) e. CC )
6 2 5 addcomd 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( B + ( A mod M ) ) = ( ( A mod M ) + B ) )
7 6 oveq1d 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( ( B + ( A mod M ) ) mod M ) = ( ( ( A mod M ) + B ) mod M ) )
8 modaddmod 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( ( ( A mod M ) + B ) mod M ) = ( ( A + B ) mod M ) )
9 recn 
 |-  ( A e. RR -> A e. CC )
10 addcom 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
11 9 1 10 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) = ( B + A ) )
12 11 oveq1d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) mod M ) = ( ( B + A ) mod M ) )
13 12 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( ( A + B ) mod M ) = ( ( B + A ) mod M ) )
14 7 8 13 3eqtrd 
 |-  ( ( A e. RR /\ B e. RR /\ M e. RR+ ) -> ( ( B + ( A mod M ) ) mod M ) = ( ( B + A ) mod M ) )