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