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 ) )