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	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ∃ 𝑎 ∈ ( 0 ... ( 𝐴 − 1 ) ) 𝐴 ∥ ( 𝑎 − 𝑁 ) )

Proof

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