Metamath Proof Explorer

Theorem congrep

Description: Every integer is congruent to some number in the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014)

Ref Expression
Assertion congrep ⊢ A ∈ ℕ ∧ N ∈ ℤ → ∃ a ∈ 0 … A − 1 A ∥ a − N

Proof

Step Hyp Ref Expression
1 zmodfz ⊢ N ∈ ℤ ∧ A ∈ ℕ → N mod A ∈ 0 … A − 1
2 1 ancoms ⊢ A ∈ ℕ ∧ N ∈ ℤ → N mod A ∈ 0 … A − 1
3 nnz ⊢ A ∈ ℕ → A ∈ ℤ
4 3 adantr ⊢ A ∈ ℕ ∧ N ∈ ℤ → A ∈ ℤ
5 simpr ⊢ A ∈ ℕ ∧ N ∈ ℤ → N ∈ ℤ
6 zmodcl ⊢ N ∈ ℤ ∧ A ∈ ℕ → N mod A ∈ ℕ 0
7 6 ancoms ⊢ A ∈ ℕ ∧ N ∈ ℤ → N mod A ∈ ℕ 0
8 7 nn0zd ⊢ A ∈ ℕ ∧ N ∈ ℤ → N mod A ∈ ℤ
9 zre ⊢ N ∈ ℤ → N ∈ ℝ
10 nnrp ⊢ A ∈ ℕ → A ∈ ℝ +
11 moddifz ⊢ N ∈ ℝ ∧ A ∈ ℝ + → N − N mod A A ∈ ℤ
12 9 10 11 syl2anr ⊢ A ∈ ℕ ∧ N ∈ ℤ → N − N mod A A ∈ ℤ
13 nnne0 ⊢ A ∈ ℕ → A ≠ 0
14 13 adantr ⊢ A ∈ ℕ ∧ N ∈ ℤ → A ≠ 0
15 5 8 zsubcld ⊢ A ∈ ℕ ∧ N ∈ ℤ → N − N mod A ∈ ℤ
16 dvdsval2 ⊢ A ∈ ℤ ∧ A ≠ 0 ∧ N − N mod A ∈ ℤ → A ∥ N − N mod A ↔ N − N mod A A ∈ ℤ
17 4 14 15 16 syl3anc ⊢ A ∈ ℕ ∧ N ∈ ℤ → A ∥ N − N mod A ↔ N − N mod A A ∈ ℤ
18 12 17 mpbird ⊢ A ∈ ℕ ∧ N ∈ ℤ → A ∥ N − N mod A
19 congsym ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N mod A ∈ ℤ ∧ A ∥ N − N mod A → A ∥ N mod A − N
20 4 5 8 18 19 syl22anc ⊢ A ∈ ℕ ∧ N ∈ ℤ → A ∥ N mod A − N
21 oveq1 ⊢ a = N mod A → a − N = N mod A − N
22 21 breq2d ⊢ a = N mod A → A ∥ a − N ↔ A ∥ N mod A − N
23 22 rspcev ⊢ N mod A ∈ 0 … A − 1 ∧ A ∥ N mod A − N → ∃ a ∈ 0 … A − 1 A ∥ a − N
24 2 20 23 syl2anc ⊢ A ∈ ℕ ∧ N ∈ ℤ → ∃ a ∈ 0 … A − 1 A ∥ a − N