Theorem modcyc

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

	Ref	Expression
Assertion	modcyc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) mod 𝐵 ) = ( 𝐴 mod 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
2		rpre	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ )
3		remulcl	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑁 · 𝐵 ) ∈ ℝ )
4	1 2 3	syl2an	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( 𝑁 · 𝐵 ) ∈ ℝ )
5		readdcl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑁 · 𝐵 ) ∈ ℝ ) → ( 𝐴 + ( 𝑁 · 𝐵 ) ) ∈ ℝ )
6	4 5	sylan2	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) ) → ( 𝐴 + ( 𝑁 · 𝐵 ) ) ∈ ℝ )
7	6	3impb	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 + ( 𝑁 · 𝐵 ) ) ∈ ℝ )
8		simp3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℝ+ )
9		modval	⊢ ( ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) mod 𝐵 ) = ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) − ( 𝐵 · ( ⌊ ‘ ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) / 𝐵 ) ) ) ) )
10	7 8 9	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) mod 𝐵 ) = ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) − ( 𝐵 · ( ⌊ ‘ ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) / 𝐵 ) ) ) ) )
11		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
12	11	3ad2ant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
13	4	recnd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( 𝑁 · 𝐵 ) ∈ ℂ )
14	13	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( 𝑁 · 𝐵 ) ∈ ℂ )
15		rpcnne0	⊢ ( 𝐵 ∈ ℝ+ → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
16	15	3ad2ant3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
17		divdir	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑁 · 𝐵 ) ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) / 𝐵 ) = ( ( 𝐴 / 𝐵 ) + ( ( 𝑁 · 𝐵 ) / 𝐵 ) ) )
18	12 14 16 17	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) / 𝐵 ) = ( ( 𝐴 / 𝐵 ) + ( ( 𝑁 · 𝐵 ) / 𝐵 ) ) )
19		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
20		divcan4	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝑁 · 𝐵 ) / 𝐵 ) = 𝑁 )
21	20	3expb	⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝑁 · 𝐵 ) / 𝐵 ) = 𝑁 )
22	19 15 21	syl2an	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝑁 · 𝐵 ) / 𝐵 ) = 𝑁 )
23	22	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝑁 · 𝐵 ) / 𝐵 ) = 𝑁 )
24	23	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 / 𝐵 ) + ( ( 𝑁 · 𝐵 ) / 𝐵 ) ) = ( ( 𝐴 / 𝐵 ) + 𝑁 ) )
25	18 24	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) / 𝐵 ) = ( ( 𝐴 / 𝐵 ) + 𝑁 ) )
26	25	fveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) / 𝐵 ) ) = ( ⌊ ‘ ( ( 𝐴 / 𝐵 ) + 𝑁 ) ) )
27		rerpdivcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
28	27	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
29		simp2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → 𝑁 ∈ ℤ )
30		fladdz	⊢ ( ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 𝑁 ∈ ℤ ) → ( ⌊ ‘ ( ( 𝐴 / 𝐵 ) + 𝑁 ) ) = ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) + 𝑁 ) )
31	28 29 30	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ ( ( 𝐴 / 𝐵 ) + 𝑁 ) ) = ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) + 𝑁 ) )
32	26 31	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) / 𝐵 ) ) = ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) + 𝑁 ) )
33	32	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 · ( ⌊ ‘ ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) / 𝐵 ) ) ) = ( 𝐵 · ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) + 𝑁 ) ) )
34		rpcn	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
35	34	3ad2ant3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
36		reflcl	⊢ ( ( 𝐴 / 𝐵 ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℝ )
37	36	recnd	⊢ ( ( 𝐴 / 𝐵 ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℂ )
38	27 37	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℂ )
39	38	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℂ )
40	19	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → 𝑁 ∈ ℂ )
41	35 39 40	adddid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 · ( ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) + 𝑁 ) ) = ( ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) + ( 𝐵 · 𝑁 ) ) )
42		mulcom	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑁 · 𝐵 ) = ( 𝐵 · 𝑁 ) )
43	19 34 42	syl2an	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( 𝑁 · 𝐵 ) = ( 𝐵 · 𝑁 ) )
44	43	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( 𝑁 · 𝐵 ) = ( 𝐵 · 𝑁 ) )
45	44	eqcomd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 · 𝑁 ) = ( 𝑁 · 𝐵 ) )
46	45	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) + ( 𝐵 · 𝑁 ) ) = ( ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) + ( 𝑁 · 𝐵 ) ) )
47	33 41 46	3eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 · ( ⌊ ‘ ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) / 𝐵 ) ) ) = ( ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) + ( 𝑁 · 𝐵 ) ) )
48	47	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) − ( 𝐵 · ( ⌊ ‘ ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) / 𝐵 ) ) ) ) = ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) − ( ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) + ( 𝑁 · 𝐵 ) ) ) )
49	34	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
50	49 38	mulcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ∈ ℂ )
51	50	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ∈ ℂ )
52	12 51 14	pnpcan2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) − ( ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) + ( 𝑁 · 𝐵 ) ) ) = ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
53	10 48 52	3eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) mod 𝐵 ) = ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
54		modval	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) = ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
55	54	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 mod 𝐵 ) = ( 𝐴 − ( 𝐵 · ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) ) )
56	53 55	eqtr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) mod 𝐵 ) = ( 𝐴 mod 𝐵 ) )
57	56	3com23	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 + ( 𝑁 · 𝐵 ) ) mod 𝐵 ) = ( 𝐴 mod 𝐵 ) )