moddvds

Description: Two ways to say A == B (mod N ), see also definition in ApostolNT p. 106. (Contributed by Mario Carneiro, 18-Feb-2014)

		Ref	Expression
	Assertion	moddvds	$⊢ (N \in ℕ \land A \in ℤ \land B \in ℤ) \to (A \mod N = B \mod N \leftrightarrow N ∥ (A - B))$

Proof

Step	Hyp	Ref	Expression
1		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
2	1	adantr	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to N \in ℝ^{+}$
3		0mod	$⊢ N \in ℝ^{+} \to 0 \mod N = 0$
4	2 3	syl	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to 0 \mod N = 0$
5	4	eqeq2d	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to ((A - B) \mod N = 0 \mod N \leftrightarrow (A - B) \mod N = 0)$
6		zre	$⊢ A \in ℤ \to A \in ℝ$
7	6	ad2antrl	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to A \in ℝ$
8		zre	$⊢ B \in ℤ \to B \in ℝ$
9	8	ad2antll	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to B \in ℝ$
10	9	renegcld	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to - B \in ℝ$
11		modadd1	$⊢ ((A \in ℝ \land B \in ℝ) \land (- B \in ℝ \land N \in ℝ^{+}) \land A \mod N = B \mod N) \to (A + (- B)) \mod N = (B + (- B)) \mod N$
12	11	3expia	$⊢ ((A \in ℝ \land B \in ℝ) \land (- B \in ℝ \land N \in ℝ^{+})) \to (A \mod N = B \mod N \to (A + (- B)) \mod N = (B + (- B)) \mod N)$
13	7 9 10 2 12	syl22anc	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to (A \mod N = B \mod N \to (A + (- B)) \mod N = (B + (- B)) \mod N)$
14	7	recnd	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to A \in ℂ$
15	9	recnd	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to B \in ℂ$
16	14 15	negsubd	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to A + (- B) = A - B$
17	16	oveq1d	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to (A + (- B)) \mod N = (A - B) \mod N$
18	15	negidd	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to B + (- B) = 0$
19	18	oveq1d	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to (B + (- B)) \mod N = 0 \mod N$
20	17 19	eqeq12d	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to ((A + (- B)) \mod N = (B + (- B)) \mod N \leftrightarrow (A - B) \mod N = 0 \mod N)$
21	13 20	sylibd	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to (A \mod N = B \mod N \to (A - B) \mod N = 0 \mod N)$
22	7 9	resubcld	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to A - B \in ℝ$
23		0red	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to 0 \in ℝ$
24		modadd1	$⊢ ((A - B \in ℝ \land 0 \in ℝ) \land (B \in ℝ \land N \in ℝ^{+}) \land (A - B) \mod N = 0 \mod N) \to (A - B + B) \mod N = (0 + B) \mod N$
25	24	3expia	$⊢ ((A - B \in ℝ \land 0 \in ℝ) \land (B \in ℝ \land N \in ℝ^{+})) \to ((A - B) \mod N = 0 \mod N \to (A - B + B) \mod N = (0 + B) \mod N)$
26	22 23 9 2 25	syl22anc	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to ((A - B) \mod N = 0 \mod N \to (A - B + B) \mod N = (0 + B) \mod N)$
27	14 15	npcand	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to A - B + B = A$
28	27	oveq1d	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to (A - B + B) \mod N = A \mod N$
29	15	addlidd	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to 0 + B = B$
30	29	oveq1d	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to (0 + B) \mod N = B \mod N$
31	28 30	eqeq12d	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to ((A - B + B) \mod N = (0 + B) \mod N \leftrightarrow A \mod N = B \mod N)$
32	26 31	sylibd	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to ((A - B) \mod N = 0 \mod N \to A \mod N = B \mod N)$
33	21 32	impbid	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to (A \mod N = B \mod N \leftrightarrow (A - B) \mod N = 0 \mod N)$
34		zsubcl	$⊢ (A \in ℤ \land B \in ℤ) \to A - B \in ℤ$
35		dvdsval3	$⊢ (N \in ℕ \land A - B \in ℤ) \to (N ∥ (A - B) \leftrightarrow (A - B) \mod N = 0)$
36	34 35	sylan2	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to (N ∥ (A - B) \leftrightarrow (A - B) \mod N = 0)$
37	5 33 36	3bitr4d	$⊢ (N \in ℕ \land (A \in ℤ \land B \in ℤ)) \to (A \mod N = B \mod N \leftrightarrow N ∥ (A - B))$
38	37	3impb	$⊢ (N \in ℕ \land A \in ℤ \land B \in ℤ) \to (A \mod N = B \mod N \leftrightarrow N ∥ (A - B))$

Metamath Proof Explorer

Theorem moddvds

Proof