Theorem modcyc2

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

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

Proof

Step	Hyp	Ref	Expression
1		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2		rpcn	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
3		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
4		mulneg1	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝑁 · 𝐵 ) = - ( 𝑁 · 𝐵 ) )
5	4	ancoms	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( - 𝑁 · 𝐵 ) = - ( 𝑁 · 𝐵 ) )
6		mulcom	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝐵 · 𝑁 ) = ( 𝑁 · 𝐵 ) )
7	6	negeqd	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → - ( 𝐵 · 𝑁 ) = - ( 𝑁 · 𝐵 ) )
8	5 7	eqtr4d	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( - 𝑁 · 𝐵 ) = - ( 𝐵 · 𝑁 ) )
9	8	3adant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( - 𝑁 · 𝐵 ) = - ( 𝐵 · 𝑁 ) )
10	9	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝐴 + ( - 𝑁 · 𝐵 ) ) = ( 𝐴 + - ( 𝐵 · 𝑁 ) ) )
11		mulcl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝐵 · 𝑁 ) ∈ ℂ )
12		negsub	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 · 𝑁 ) ∈ ℂ ) → ( 𝐴 + - ( 𝐵 · 𝑁 ) ) = ( 𝐴 − ( 𝐵 · 𝑁 ) ) )
13	11 12	sylan2	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) → ( 𝐴 + - ( 𝐵 · 𝑁 ) ) = ( 𝐴 − ( 𝐵 · 𝑁 ) ) )
14	13	3impb	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝐴 + - ( 𝐵 · 𝑁 ) ) = ( 𝐴 − ( 𝐵 · 𝑁 ) ) )
15	10 14	eqtr2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝐴 − ( 𝐵 · 𝑁 ) ) = ( 𝐴 + ( - 𝑁 · 𝐵 ) ) )
16	1 2 3 15	syl3an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 − ( 𝐵 · 𝑁 ) ) = ( 𝐴 + ( - 𝑁 · 𝐵 ) ) )
17	16	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 − ( 𝐵 · 𝑁 ) ) mod 𝐵 ) = ( ( 𝐴 + ( - 𝑁 · 𝐵 ) ) mod 𝐵 ) )
18		znegcl	⊢ ( 𝑁 ∈ ℤ → - 𝑁 ∈ ℤ )
19		modcyc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ - 𝑁 ∈ ℤ ) → ( ( 𝐴 + ( - 𝑁 · 𝐵 ) ) mod 𝐵 ) = ( 𝐴 mod 𝐵 ) )
20	18 19	syl3an3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 + ( - 𝑁 · 𝐵 ) ) mod 𝐵 ) = ( 𝐴 mod 𝐵 ) )
21	17 20	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 − ( 𝐵 · 𝑁 ) ) mod 𝐵 ) = ( 𝐴 mod 𝐵 ) )