This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem modcyc

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

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

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( N e. ZZ -> N e. RR )
2 rpre 
 |-  ( B e. RR+ -> B e. RR )
3 remulcl 
 |-  ( ( N e. RR /\ B e. RR ) -> ( N x. B ) e. RR )
4 1 2 3 syl2an 
 |-  ( ( N e. ZZ /\ B e. RR+ ) -> ( N x. B ) e. RR )
5 readdcl 
 |-  ( ( A e. RR /\ ( N x. B ) e. RR ) -> ( A + ( N x. B ) ) e. RR )
6 4 5 sylan2 
 |-  ( ( A e. RR /\ ( N e. ZZ /\ B e. RR+ ) ) -> ( A + ( N x. B ) ) e. RR )
7 6 3impb 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( A + ( N x. B ) ) e. RR )
8 simp3 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> B e. RR+ )
9 modval 
 |-  ( ( ( A + ( N x. B ) ) e. RR /\ B e. RR+ ) -> ( ( A + ( N x. B ) ) mod B ) = ( ( A + ( N x. B ) ) - ( B x. ( |_ ` ( ( A + ( N x. B ) ) / B ) ) ) ) )
10 7 8 9 syl2anc 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( ( A + ( N x. B ) ) mod B ) = ( ( A + ( N x. B ) ) - ( B x. ( |_ ` ( ( A + ( N x. B ) ) / B ) ) ) ) )
11 recn 
 |-  ( A e. RR -> A e. CC )
12 11 3ad2ant1 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> A e. CC )
13 4 recnd 
 |-  ( ( N e. ZZ /\ B e. RR+ ) -> ( N x. B ) e. CC )
14 13 3adant1 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( N x. B ) e. CC )
15 rpcnne0 
 |-  ( B e. RR+ -> ( B e. CC /\ B =/= 0 ) )
16 15 3ad2ant3 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( B e. CC /\ B =/= 0 ) )
17 divdir 
 |-  ( ( A e. CC /\ ( N x. B ) e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A + ( N x. B ) ) / B ) = ( ( A / B ) + ( ( N x. B ) / B ) ) )
18 12 14 16 17 syl3anc 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( ( A + ( N x. B ) ) / B ) = ( ( A / B ) + ( ( N x. B ) / B ) ) )
19 zcn 
 |-  ( N e. ZZ -> N e. CC )
20 divcan4 
 |-  ( ( N e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( N x. B ) / B ) = N )
21 20 3expb 
 |-  ( ( N e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( N x. B ) / B ) = N )
22 19 15 21 syl2an 
 |-  ( ( N e. ZZ /\ B e. RR+ ) -> ( ( N x. B ) / B ) = N )
23 22 3adant1 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( ( N x. B ) / B ) = N )
24 23 oveq2d 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( ( A / B ) + ( ( N x. B ) / B ) ) = ( ( A / B ) + N ) )
25 18 24 eqtrd 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( ( A + ( N x. B ) ) / B ) = ( ( A / B ) + N ) )
26 25 fveq2d 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( |_ ` ( ( A + ( N x. B ) ) / B ) ) = ( |_ ` ( ( A / B ) + N ) ) )
27 rerpdivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )
28 27 3adant2 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( A / B ) e. RR )
29 simp2 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> N e. ZZ )
30 fladdz 
 |-  ( ( ( A / B ) e. RR /\ N e. ZZ ) -> ( |_ ` ( ( A / B ) + N ) ) = ( ( |_ ` ( A / B ) ) + N ) )
31 28 29 30 syl2anc 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( |_ ` ( ( A / B ) + N ) ) = ( ( |_ ` ( A / B ) ) + N ) )
32 26 31 eqtrd 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( |_ ` ( ( A + ( N x. B ) ) / B ) ) = ( ( |_ ` ( A / B ) ) + N ) )
33 32 oveq2d 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( B x. ( |_ ` ( ( A + ( N x. B ) ) / B ) ) ) = ( B x. ( ( |_ ` ( A / B ) ) + N ) ) )
34 rpcn 
 |-  ( B e. RR+ -> B e. CC )
35 34 3ad2ant3 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> B e. CC )
36 reflcl 
 |-  ( ( A / B ) e. RR -> ( |_ ` ( A / B ) ) e. RR )
37 36 recnd 
 |-  ( ( A / B ) e. RR -> ( |_ ` ( A / B ) ) e. CC )
38 27 37 syl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. CC )
39 38 3adant2 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. CC )
40 19 3ad2ant2 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> N e. CC )
41 35 39 40 adddid 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( B x. ( ( |_ ` ( A / B ) ) + N ) ) = ( ( B x. ( |_ ` ( A / B ) ) ) + ( B x. N ) ) )
42 mulcom 
 |-  ( ( N e. CC /\ B e. CC ) -> ( N x. B ) = ( B x. N ) )
43 19 34 42 syl2an 
 |-  ( ( N e. ZZ /\ B e. RR+ ) -> ( N x. B ) = ( B x. N ) )
44 43 3adant1 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( N x. B ) = ( B x. N ) )
45 44 eqcomd 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( B x. N ) = ( N x. B ) )
46 45 oveq2d 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( ( B x. ( |_ ` ( A / B ) ) ) + ( B x. N ) ) = ( ( B x. ( |_ ` ( A / B ) ) ) + ( N x. B ) ) )
47 33 41 46 3eqtrd 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( B x. ( |_ ` ( ( A + ( N x. B ) ) / B ) ) ) = ( ( B x. ( |_ ` ( A / B ) ) ) + ( N x. B ) ) )
48 47 oveq2d 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( ( A + ( N x. B ) ) - ( B x. ( |_ ` ( ( A + ( N x. B ) ) / B ) ) ) ) = ( ( A + ( N x. B ) ) - ( ( B x. ( |_ ` ( A / B ) ) ) + ( N x. B ) ) ) )
49 34 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B e. CC )
50 49 38 mulcld 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( B x. ( |_ ` ( A / B ) ) ) e. CC )
51 50 3adant2 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( B x. ( |_ ` ( A / B ) ) ) e. CC )
52 12 51 14 pnpcan2d 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( ( A + ( N x. B ) ) - ( ( B x. ( |_ ` ( A / B ) ) ) + ( N x. B ) ) ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
53 10 48 52 3eqtrd 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( ( A + ( N x. B ) ) mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
54 modval 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
55 54 3adant2 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
56 53 55 eqtr4d 
 |-  ( ( A e. RR /\ N e. ZZ /\ B e. RR+ ) -> ( ( A + ( N x. B ) ) mod B ) = ( A mod B ) )
57 56 3com23 
 |-  ( ( A e. RR /\ B e. RR+ /\ N e. ZZ ) -> ( ( A + ( N x. B ) ) mod B ) = ( A mod B ) )