zndvds

Description: Express equality of equivalence classes in ZZ / n ZZ in terms of divisibility. (Contributed by Mario Carneiro, 15-Jun-2015)

	Ref	Expression
Hypotheses	zncyg.y	$⊢ Y = ℤ / N ℤ$
	zndvds.2	$⊢ L = ℤRHom (Y)$
Assertion	zndvds	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to (L (A) = L (B) \leftrightarrow N ∥ (A - B))$

Proof

Step	Hyp	Ref	Expression
1		zncyg.y	$⊢ Y = ℤ / N ℤ$
2		zndvds.2	$⊢ L = ℤRHom (Y)$
3		eqcom	$⊢ L (A) = L (B) \leftrightarrow L (B) = L (A)$
4		eqid	$⊢ RSpan (ℤ_{ring}) = RSpan (ℤ_{ring})$
5		eqid	$⊢ ℤ_{ring} ~_{QG} RSpan (ℤ_{ring}) (\{N\}) = ℤ_{ring} ~_{QG} RSpan (ℤ_{ring}) (\{N\})$
6	4 5 1 2	znzrhval	$⊢ (N \in ℕ_{0} \land B \in ℤ) \to L (B) = [B] (ℤ_{ring} ~_{QG} RSpan (ℤ_{ring}) (\{N\}))$
7	6	3adant2	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to L (B) = [B] (ℤ_{ring} ~_{QG} RSpan (ℤ_{ring}) (\{N\}))$
8	4 5 1 2	znzrhval	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to L (A) = [A] (ℤ_{ring} ~_{QG} RSpan (ℤ_{ring}) (\{N\}))$
9	8	3adant3	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to L (A) = [A] (ℤ_{ring} ~_{QG} RSpan (ℤ_{ring}) (\{N\}))$
10	7 9	eqeq12d	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to (L (B) = L (A) \leftrightarrow [B] (ℤ_{ring} ~_{QG} RSpan (ℤ_{ring}) (\{N\})) = [A] (ℤ_{ring} ~_{QG} RSpan (ℤ_{ring}) (\{N\})))$
11		zringring	$⊢ ℤ_{ring} \in Ring$
12		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
13	12	3ad2ant1	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to N \in ℤ$
14	13	snssd	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to \{N\} \subseteq ℤ$
15		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
16		eqid	$⊢ LIdeal (ℤ_{ring}) = LIdeal (ℤ_{ring})$
17	4 15 16	rspcl	$⊢ (ℤ_{ring} \in Ring \land \{N\} \subseteq ℤ) \to RSpan (ℤ_{ring}) (\{N\}) \in LIdeal (ℤ_{ring})$
18	11 14 17	sylancr	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to RSpan (ℤ_{ring}) (\{N\}) \in LIdeal (ℤ_{ring})$
19	16	lidlsubg	$⊢ (ℤ_{ring} \in Ring \land RSpan (ℤ_{ring}) (\{N\}) \in LIdeal (ℤ_{ring})) \to RSpan (ℤ_{ring}) (\{N\}) \in SubGrp (ℤ_{ring})$
20	11 18 19	sylancr	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to RSpan (ℤ_{ring}) (\{N\}) \in SubGrp (ℤ_{ring})$
21	15 5	eqger	$⊢ RSpan (ℤ_{ring}) (\{N\}) \in SubGrp (ℤ_{ring}) \to (ℤ_{ring} ~_{QG} RSpan (ℤ_{ring}) (\{N\})) Er ℤ$
22	20 21	syl	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to (ℤ_{ring} ~_{QG} RSpan (ℤ_{ring}) (\{N\})) Er ℤ$
23		simp3	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to B \in ℤ$
24	22 23	erth	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to (B (ℤ_{ring} ~_{QG} RSpan (ℤ_{ring}) (\{N\})) A \leftrightarrow [B] (ℤ_{ring} ~_{QG} RSpan (ℤ_{ring}) (\{N\})) = [A] (ℤ_{ring} ~_{QG} RSpan (ℤ_{ring}) (\{N\})))$
25		zringabl	$⊢ ℤ_{ring} \in Abel$
26	15 16	lidlss	$⊢ RSpan (ℤ_{ring}) (\{N\}) \in LIdeal (ℤ_{ring}) \to RSpan (ℤ_{ring}) (\{N\}) \subseteq ℤ$
27	18 26	syl	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to RSpan (ℤ_{ring}) (\{N\}) \subseteq ℤ$
28		eqid	$⊢ -_{ℤ_{ring}} = -_{ℤ_{ring}}$
29	15 28 5	eqgabl	$⊢ (ℤ_{ring} \in Abel \land RSpan (ℤ_{ring}) (\{N\}) \subseteq ℤ) \to (B (ℤ_{ring} ~_{QG} RSpan (ℤ_{ring}) (\{N\})) A \leftrightarrow (B \in ℤ \land A \in ℤ \land A -_{ℤ_{ring}} B \in RSpan (ℤ_{ring}) (\{N\})))$
30	25 27 29	sylancr	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to (B (ℤ_{ring} ~_{QG} RSpan (ℤ_{ring}) (\{N\})) A \leftrightarrow (B \in ℤ \land A \in ℤ \land A -_{ℤ_{ring}} B \in RSpan (ℤ_{ring}) (\{N\})))$
31		simp2	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to A \in ℤ$
32	23 31	jca	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to (B \in ℤ \land A \in ℤ)$
33	32	biantrurd	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to (A -_{ℤ_{ring}} B \in RSpan (ℤ_{ring}) (\{N\}) \leftrightarrow ((B \in ℤ \land A \in ℤ) \land A -_{ℤ_{ring}} B \in RSpan (ℤ_{ring}) (\{N\})))$
34		df-3an	$⊢ (B \in ℤ \land A \in ℤ \land A -_{ℤ_{ring}} B \in RSpan (ℤ_{ring}) (\{N\})) \leftrightarrow ((B \in ℤ \land A \in ℤ) \land A -_{ℤ_{ring}} B \in RSpan (ℤ_{ring}) (\{N\}))$
35	33 34	bitr4di	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to (A -_{ℤ_{ring}} B \in RSpan (ℤ_{ring}) (\{N\}) \leftrightarrow (B \in ℤ \land A \in ℤ \land A -_{ℤ_{ring}} B \in RSpan (ℤ_{ring}) (\{N\})))$
36		zsubrg	$⊢ ℤ \in SubRing (ℂ_{fld})$
37		subrgsubg	$⊢ ℤ \in SubRing (ℂ_{fld}) \to ℤ \in SubGrp (ℂ_{fld})$
38	36 37	mp1i	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to ℤ \in SubGrp (ℂ_{fld})$
39		cnfldsub	$⊢ - = -_{ℂ_{fld}}$
40		df-zring	$⊢ ℤ_{ring} = ℂ_{fld} ↾_{𝑠} ℤ$
41	39 40 28	subgsub	$⊢ (ℤ \in SubGrp (ℂ_{fld}) \land A \in ℤ \land B \in ℤ) \to A - B = A -_{ℤ_{ring}} B$
42	38 41	syld3an1	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to A - B = A -_{ℤ_{ring}} B$
43	42	eqcomd	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to A -_{ℤ_{ring}} B = A - B$
44		dvdsrzring	$⊢ ∥ = ∥_{r} (ℤ_{ring})$
45	15 4 44	rspsn	$⊢ (ℤ_{ring} \in Ring \land N \in ℤ) \to RSpan (ℤ_{ring}) (\{N\}) = \{x \| N ∥ x\}$
46	11 13 45	sylancr	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to RSpan (ℤ_{ring}) (\{N\}) = \{x \| N ∥ x\}$
47	43 46	eleq12d	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to (A -_{ℤ_{ring}} B \in RSpan (ℤ_{ring}) (\{N\}) \leftrightarrow A - B \in \{x \| N ∥ x\})$
48		ovex	$⊢ A - B \in V$
49		breq2	$⊢ x = A - B \to (N ∥ x \leftrightarrow N ∥ (A - B))$
50	48 49	elab	$⊢ A - B \in \{x \| N ∥ x\} \leftrightarrow N ∥ (A - B)$
51	47 50	bitrdi	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to (A -_{ℤ_{ring}} B \in RSpan (ℤ_{ring}) (\{N\}) \leftrightarrow N ∥ (A - B))$
52	30 35 51	3bitr2d	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to (B (ℤ_{ring} ~_{QG} RSpan (ℤ_{ring}) (\{N\})) A \leftrightarrow N ∥ (A - B))$
53	10 24 52	3bitr2d	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to (L (B) = L (A) \leftrightarrow N ∥ (A - B))$
54	3 53	bitrid	$⊢ (N \in ℕ_{0} \land A \in ℤ \land B \in ℤ) \to (L (A) = L (B) \leftrightarrow N ∥ (A - B))$

Metamath Proof Explorer

Theorem zndvds

Proof