Metamath Proof Explorer

Theorem muladdmodid

Description: The sum of a positive real number less than an upper bound and the product of an integer and the upper bound is the positive real number modulo the upper bound. (Contributed by AV, 5-Jul-2020)

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

Proof

Step Hyp Ref Expression
1 0red 
 |-  ( M e. RR+ -> 0 e. RR )
2 rpxr 
 |-  ( M e. RR+ -> M e. RR* )
3 elico2 
 |-  ( ( 0 e. RR /\ M e. RR* ) -> ( A e. ( 0 [,) M ) <-> ( A e. RR /\ 0 <_ A /\ A < M ) ) )
4 1 2 3 syl2anc 
 |-  ( M e. RR+ -> ( A e. ( 0 [,) M ) <-> ( A e. RR /\ 0 <_ A /\ A < M ) ) )
5 4 adantl 
 |-  ( ( N e. ZZ /\ M e. RR+ ) -> ( A e. ( 0 [,) M ) <-> ( A e. RR /\ 0 <_ A /\ A < M ) ) )
6 zcn 
 |-  ( N e. ZZ -> N e. CC )
7 rpcn 
 |-  ( M e. RR+ -> M e. CC )
8 mulcl 
 |-  ( ( N e. CC /\ M e. CC ) -> ( N x. M ) e. CC )
9 6 7 8 syl2an 
 |-  ( ( N e. ZZ /\ M e. RR+ ) -> ( N x. M ) e. CC )
10 9 adantr 
 |-  ( ( ( N e. ZZ /\ M e. RR+ ) /\ ( A e. RR /\ 0 <_ A /\ A < M ) ) -> ( N x. M ) e. CC )
11 recn 
 |-  ( A e. RR -> A e. CC )
12 11 3ad2ant1 
 |-  ( ( A e. RR /\ 0 <_ A /\ A < M ) -> A e. CC )
13 12 adantl 
 |-  ( ( ( N e. ZZ /\ M e. RR+ ) /\ ( A e. RR /\ 0 <_ A /\ A < M ) ) -> A e. CC )
14 10 13 addcomd 
 |-  ( ( ( N e. ZZ /\ M e. RR+ ) /\ ( A e. RR /\ 0 <_ A /\ A < M ) ) -> ( ( N x. M ) + A ) = ( A + ( N x. M ) ) )
15 14 oveq1d 
 |-  ( ( ( N e. ZZ /\ M e. RR+ ) /\ ( A e. RR /\ 0 <_ A /\ A < M ) ) -> ( ( ( N x. M ) + A ) mod M ) = ( ( A + ( N x. M ) ) mod M ) )
16 simp1 
 |-  ( ( A e. RR /\ 0 <_ A /\ A < M ) -> A e. RR )
17 16 adantl 
 |-  ( ( ( N e. ZZ /\ M e. RR+ ) /\ ( A e. RR /\ 0 <_ A /\ A < M ) ) -> A e. RR )
18 simpr 
 |-  ( ( N e. ZZ /\ M e. RR+ ) -> M e. RR+ )
19 18 adantr 
 |-  ( ( ( N e. ZZ /\ M e. RR+ ) /\ ( A e. RR /\ 0 <_ A /\ A < M ) ) -> M e. RR+ )
20 simpll 
 |-  ( ( ( N e. ZZ /\ M e. RR+ ) /\ ( A e. RR /\ 0 <_ A /\ A < M ) ) -> N e. ZZ )
21 modcyc 
 |-  ( ( A e. RR /\ M e. RR+ /\ N e. ZZ ) -> ( ( A + ( N x. M ) ) mod M ) = ( A mod M ) )
22 17 19 20 21 syl3anc 
 |-  ( ( ( N e. ZZ /\ M e. RR+ ) /\ ( A e. RR /\ 0 <_ A /\ A < M ) ) -> ( ( A + ( N x. M ) ) mod M ) = ( A mod M ) )
23 18 16 anim12ci 
 |-  ( ( ( N e. ZZ /\ M e. RR+ ) /\ ( A e. RR /\ 0 <_ A /\ A < M ) ) -> ( A e. RR /\ M e. RR+ ) )
24 3simpc 
 |-  ( ( A e. RR /\ 0 <_ A /\ A < M ) -> ( 0 <_ A /\ A < M ) )
25 24 adantl 
 |-  ( ( ( N e. ZZ /\ M e. RR+ ) /\ ( A e. RR /\ 0 <_ A /\ A < M ) ) -> ( 0 <_ A /\ A < M ) )
26 modid 
 |-  ( ( ( A e. RR /\ M e. RR+ ) /\ ( 0 <_ A /\ A < M ) ) -> ( A mod M ) = A )
27 23 25 26 syl2anc 
 |-  ( ( ( N e. ZZ /\ M e. RR+ ) /\ ( A e. RR /\ 0 <_ A /\ A < M ) ) -> ( A mod M ) = A )
28 15 22 27 3eqtrd 
 |-  ( ( ( N e. ZZ /\ M e. RR+ ) /\ ( A e. RR /\ 0 <_ A /\ A < M ) ) -> ( ( ( N x. M ) + A ) mod M ) = A )
29 28 ex 
 |-  ( ( N e. ZZ /\ M e. RR+ ) -> ( ( A e. RR /\ 0 <_ A /\ A < M ) -> ( ( ( N x. M ) + A ) mod M ) = A ) )
30 5 29 sylbid 
 |-  ( ( N e. ZZ /\ M e. RR+ ) -> ( A e. ( 0 [,) M ) -> ( ( ( N x. M ) + A ) mod M ) = A ) )
31 30 3impia 
 |-  ( ( N e. ZZ /\ M e. RR+ /\ A e. ( 0 [,) M ) ) -> ( ( ( N x. M ) + A ) mod M ) = A )