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