Metamath Proof Explorer

Theorem muladdmod

Description: A real number is the sum of the number and a multiple of a positive real number modulo the positive real number. (Contributed by AV, 7-Sep-2025)

Ref Expression
Assertion muladdmod 
|- ( ( A e. RR /\ M e. RR+ /\ N e. ZZ ) -> ( ( ( N x. M ) + A ) mod M ) = ( A mod M ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( N e. ZZ -> N e. RR )
2 1 3ad2ant3 
 |-  ( ( A e. RR /\ M e. RR+ /\ N e. ZZ ) -> N e. RR )
3 rpre 
 |-  ( M e. RR+ -> M e. RR )
4 3 3ad2ant2 
 |-  ( ( A e. RR /\ M e. RR+ /\ N e. ZZ ) -> M e. RR )
5 2 4 remulcld 
 |-  ( ( A e. RR /\ M e. RR+ /\ N e. ZZ ) -> ( N x. M ) e. RR )
6 simp1 
 |-  ( ( A e. RR /\ M e. RR+ /\ N e. ZZ ) -> A e. RR )
7 simp2 
 |-  ( ( A e. RR /\ M e. RR+ /\ N e. ZZ ) -> M e. RR+ )
8 modaddmod 
 |-  ( ( ( N x. M ) e. RR /\ A e. RR /\ M e. RR+ ) -> ( ( ( ( N x. M ) mod M ) + A ) mod M ) = ( ( ( N x. M ) + A ) mod M ) )
9 5 6 7 8 syl3anc 
 |-  ( ( A e. RR /\ M e. RR+ /\ N e. ZZ ) -> ( ( ( ( N x. M ) mod M ) + A ) mod M ) = ( ( ( N x. M ) + A ) mod M ) )
10 pm3.22 
 |-  ( ( M e. RR+ /\ N e. ZZ ) -> ( N e. ZZ /\ M e. RR+ ) )
11 10 3adant1 
 |-  ( ( A e. RR /\ M e. RR+ /\ N e. ZZ ) -> ( N e. ZZ /\ M e. RR+ ) )
12 mulmod0 
 |-  ( ( N e. ZZ /\ M e. RR+ ) -> ( ( N x. M ) mod M ) = 0 )
13 11 12 syl 
 |-  ( ( A e. RR /\ M e. RR+ /\ N e. ZZ ) -> ( ( N x. M ) mod M ) = 0 )
14 13 oveq1d 
 |-  ( ( A e. RR /\ M e. RR+ /\ N e. ZZ ) -> ( ( ( N x. M ) mod M ) + A ) = ( 0 + A ) )
15 recn 
 |-  ( A e. RR -> A e. CC )
16 15 addlidd 
 |-  ( A e. RR -> ( 0 + A ) = A )
17 16 3ad2ant1 
 |-  ( ( A e. RR /\ M e. RR+ /\ N e. ZZ ) -> ( 0 + A ) = A )
18 14 17 eqtrd 
 |-  ( ( A e. RR /\ M e. RR+ /\ N e. ZZ ) -> ( ( ( N x. M ) mod M ) + A ) = A )
19 18 oveq1d 
 |-  ( ( A e. RR /\ M e. RR+ /\ N e. ZZ ) -> ( ( ( ( N x. M ) mod M ) + A ) mod M ) = ( A mod M ) )
20 9 19 eqtr3d 
 |-  ( ( A e. RR /\ M e. RR+ /\ N e. ZZ ) -> ( ( ( N x. M ) + A ) mod M ) = ( A mod M ) )