Metamath Proof Explorer

Theorem modcyc2

Description: The modulo operation is periodic. (Contributed by NM, 12-Nov-2008)

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

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 rpcn 
 |-  ( B e. RR+ -> B e. CC )
3 zcn 
 |-  ( N e. ZZ -> N e. CC )
4 mulneg1 
 |-  ( ( N e. CC /\ B e. CC ) -> ( -u N x. B ) = -u ( N x. B ) )
5 4 ancoms 
 |-  ( ( B e. CC /\ N e. CC ) -> ( -u N x. B ) = -u ( N x. B ) )
6 mulcom 
 |-  ( ( B e. CC /\ N e. CC ) -> ( B x. N ) = ( N x. B ) )
7 6 negeqd 
 |-  ( ( B e. CC /\ N e. CC ) -> -u ( B x. N ) = -u ( N x. B ) )
8 5 7 eqtr4d 
 |-  ( ( B e. CC /\ N e. CC ) -> ( -u N x. B ) = -u ( B x. N ) )
9 8 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ N e. CC ) -> ( -u N x. B ) = -u ( B x. N ) )
10 9 oveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ N e. CC ) -> ( A + ( -u N x. B ) ) = ( A + -u ( B x. N ) ) )
11 mulcl 
 |-  ( ( B e. CC /\ N e. CC ) -> ( B x. N ) e. CC )
12 negsub 
 |-  ( ( A e. CC /\ ( B x. N ) e. CC ) -> ( A + -u ( B x. N ) ) = ( A - ( B x. N ) ) )
13 11 12 sylan2 
 |-  ( ( A e. CC /\ ( B e. CC /\ N e. CC ) ) -> ( A + -u ( B x. N ) ) = ( A - ( B x. N ) ) )
14 13 3impb 
 |-  ( ( A e. CC /\ B e. CC /\ N e. CC ) -> ( A + -u ( B x. N ) ) = ( A - ( B x. N ) ) )
15 10 14 eqtr2d 
 |-  ( ( A e. CC /\ B e. CC /\ N e. CC ) -> ( A - ( B x. N ) ) = ( A + ( -u N x. B ) ) )
16 1 2 3 15 syl3an 
 |-  ( ( A e. RR /\ B e. RR+ /\ N e. ZZ ) -> ( A - ( B x. N ) ) = ( A + ( -u N x. B ) ) )
17 16 oveq1d 
 |-  ( ( A e. RR /\ B e. RR+ /\ N e. ZZ ) -> ( ( A - ( B x. N ) ) mod B ) = ( ( A + ( -u N x. B ) ) mod B ) )
18 znegcl 
 |-  ( N e. ZZ -> -u N e. ZZ )
19 modcyc 
 |-  ( ( A e. RR /\ B e. RR+ /\ -u N e. ZZ ) -> ( ( A + ( -u N x. B ) ) mod B ) = ( A mod B ) )
20 18 19 syl3an3 
 |-  ( ( A e. RR /\ B e. RR+ /\ N e. ZZ ) -> ( ( A + ( -u N x. B ) ) mod B ) = ( A mod B ) )
21 17 20 eqtrd 
 |-  ( ( A e. RR /\ B e. RR+ /\ N e. ZZ ) -> ( ( A - ( B x. N ) ) mod B ) = ( A mod B ) )