Metamath Proof Explorer

Theorem modcyc2

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

Ref Expression
Assertion modcyc2 ⊢ A ∈ ℝ ∧ B ∈ ℝ + ∧ N ∈ ℤ → A − B ⋅ N mod B = A mod B

Proof

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