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 \in ℕ \land N \in ℤ) \to \exists a \in (0 \dots A - 1) A ∥ (a - N)$

Proof

Step	Hyp	Ref	Expression
1		zmodfz	$⊢ (N \in ℤ \land A \in ℕ) \to N \mod A \in (0 \dots A - 1)$
2	1	ancoms	$⊢ (A \in ℕ \land N \in ℤ) \to N \mod A \in (0 \dots A - 1)$
3		nnz	$⊢ A \in ℕ \to A \in ℤ$
4	3	adantr	$⊢ (A \in ℕ \land N \in ℤ) \to A \in ℤ$
5		simpr	$⊢ (A \in ℕ \land N \in ℤ) \to N \in ℤ$
6		zmodcl	$⊢ (N \in ℤ \land A \in ℕ) \to N \mod A \in ℕ_{0}$
7	6	ancoms	$⊢ (A \in ℕ \land N \in ℤ) \to N \mod A \in ℕ_{0}$
8	7	nn0zd	$⊢ (A \in ℕ \land N \in ℤ) \to N \mod A \in ℤ$
9		zre	$⊢ N \in ℤ \to N \in ℝ$
10		nnrp	$⊢ A \in ℕ \to A \in ℝ^{+}$
11		moddifz	$⊢ (N \in ℝ \land A \in ℝ^{+}) \to \frac{N - (N \mod A)}{A} \in ℤ$
12	9 10 11	syl2anr	$⊢ (A \in ℕ \land N \in ℤ) \to \frac{N - (N \mod A)}{A} \in ℤ$
13		nnne0	$⊢ A \in ℕ \to A \neq 0$
14	13	adantr	$⊢ (A \in ℕ \land N \in ℤ) \to A \neq 0$
15	5 8	zsubcld	$⊢ (A \in ℕ \land N \in ℤ) \to N - (N \mod A) \in ℤ$
16		dvdsval2	$⊢ (A \in ℤ \land A \neq 0 \land N - (N \mod A) \in ℤ) \to (A ∥ (N - (N \mod A)) \leftrightarrow \frac{N - (N \mod A)}{A} \in ℤ)$
17	4 14 15 16	syl3anc	$⊢ (A \in ℕ \land N \in ℤ) \to (A ∥ (N - (N \mod A)) \leftrightarrow \frac{N - (N \mod A)}{A} \in ℤ)$
18	12 17	mpbird	$⊢ (A \in ℕ \land N \in ℤ) \to A ∥ (N - (N \mod A))$
19		congsym	$⊢ ((A \in ℤ \land N \in ℤ) \land (N \mod A \in ℤ \land A ∥ (N - (N \mod A)))) \to A ∥ ((N \mod A) - N)$
20	4 5 8 18 19	syl22anc	$⊢ (A \in ℕ \land N \in ℤ) \to A ∥ ((N \mod A) - N)$
21		oveq1	$⊢ a = N \mod A \to a - N = (N \mod A) - N$
22	21	breq2d	$⊢ a = N \mod A \to (A ∥ (a - N) \leftrightarrow A ∥ ((N \mod A) - N))$
23	22	rspcev	$⊢ (N \mod A \in (0 \dots A - 1) \land A ∥ ((N \mod A) - N)) \to \exists a \in (0 \dots A - 1) A ∥ (a - N)$
24	2 20 23	syl2anc	$⊢ (A \in ℕ \land N \in ℤ) \to \exists a \in (0 \dots A - 1) A ∥ (a - N)$

Metamath Proof Explorer

Theorem congrep

Proof