Theorem 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	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
	zndvds.2	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
Assertion	zndvds	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝐵 ) ↔ 𝑁 ∥ ( 𝐴 − 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zncyg.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2		zndvds.2	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
3		eqcom	⊢ ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝐵 ) ↔ ( 𝐿 ‘ 𝐵 ) = ( 𝐿 ‘ 𝐴 ) )
4		eqid	⊢ ( RSpan ‘ ℤring ) = ( RSpan ‘ ℤring )
5		eqid	⊢ ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) = ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) )
6	4 5 1 2	znzrhval	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐵 ∈ ℤ ) → ( 𝐿 ‘ 𝐵 ) = [ 𝐵 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) )
7	6	3adant2	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐿 ‘ 𝐵 ) = [ 𝐵 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) )
8	4 5 1 2	znzrhval	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( 𝐿 ‘ 𝐴 ) = [ 𝐴 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) )
9	8	3adant3	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐿 ‘ 𝐴 ) = [ 𝐴 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) )
10	7 9	eqeq12d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐵 ) = ( 𝐿 ‘ 𝐴 ) ↔ [ 𝐵 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) = [ 𝐴 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) )
11		zringring	⊢ ℤring ∈ Ring
12		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
13	12	3ad2ant1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝑁 ∈ ℤ )
14	13	snssd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → { 𝑁 } ⊆ ℤ )
15		zringbas	⊢ ℤ = ( Base ‘ ℤring )
16		eqid	⊢ ( LIdeal ‘ ℤring ) = ( LIdeal ‘ ℤring )
17	4 15 16	rspcl	⊢ ( ( ℤring ∈ Ring ∧ { 𝑁 } ⊆ ℤ ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) )
18	11 14 17	sylancr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) )
19	16	lidlsubg	⊢ ( ( ℤring ∈ Ring ∧ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ∈ ( SubGrp ‘ ℤring ) )
20	11 18 19	sylancr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ∈ ( SubGrp ‘ ℤring ) )
21	15 5	eqger	⊢ ( ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ∈ ( SubGrp ‘ ℤring ) → ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) Er ℤ )
22	20 21	syl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) Er ℤ )
23		simp3	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℤ )
24	22 23	erth	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) 𝐴 ↔ [ 𝐵 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) = [ 𝐴 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) )
25		zringabl	⊢ ℤring ∈ Abel
26	15 16	lidlss	⊢ ( ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ⊆ ℤ )
27	18 26	syl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ⊆ ℤ )
28		eqid	⊢ ( -g ‘ ℤring ) = ( -g ‘ ℤring )
29	15 28 5	eqgabl	⊢ ( ( ℤring ∈ Abel ∧ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ⊆ ℤ ) → ( 𝐵 ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) 𝐴 ↔ ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) )
30	25 27 29	sylancr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) 𝐴 ↔ ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) )
31		simp2	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℤ )
32	23 31	jca	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ) )
33	32	biantrurd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ↔ ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) )
34		df-3an	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ↔ ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) )
35	33 34	bitr4di	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ↔ ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) ) )
36		zsubrg	⊢ ℤ ∈ ( SubRing ‘ ℂfld )
37		subrgsubg	⊢ ( ℤ ∈ ( SubRing ‘ ℂfld ) → ℤ ∈ ( SubGrp ‘ ℂfld ) )
38	36 37	mp1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ℤ ∈ ( SubGrp ‘ ℂfld ) )
39		cnfldsub	⊢ − = ( -g ‘ ℂfld )
40		df-zring	⊢ ℤring = ( ℂfld ↾s ℤ )
41	39 40 28	subgsub	⊢ ( ( ℤ ∈ ( SubGrp ‘ ℂfld ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) = ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) )
42	38 41	syld3an1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) = ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) )
43	42	eqcomd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) = ( 𝐴 − 𝐵 ) )
44		dvdsrzring	⊢ ∥ = ( ∥r ‘ ℤring )
45	15 4 44	rspsn	⊢ ( ( ℤring ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) = { 𝑥 ∣ 𝑁 ∥ 𝑥 } )
46	11 13 45	sylancr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) = { 𝑥 ∣ 𝑁 ∥ 𝑥 } )
47	43 46	eleq12d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ↔ ( 𝐴 − 𝐵 ) ∈ { 𝑥 ∣ 𝑁 ∥ 𝑥 } ) )
48		ovex	⊢ ( 𝐴 − 𝐵 ) ∈ V
49		breq2	⊢ ( 𝑥 = ( 𝐴 − 𝐵 ) → ( 𝑁 ∥ 𝑥 ↔ 𝑁 ∥ ( 𝐴 − 𝐵 ) ) )
50	48 49	elab	⊢ ( ( 𝐴 − 𝐵 ) ∈ { 𝑥 ∣ 𝑁 ∥ 𝑥 } ↔ 𝑁 ∥ ( 𝐴 − 𝐵 ) )
51	47 50	bitrdi	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 ( -g ‘ ℤring ) 𝐵 ) ∈ ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ↔ 𝑁 ∥ ( 𝐴 − 𝐵 ) ) )
52	30 35 51	3bitr2d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑁 } ) ) 𝐴 ↔ 𝑁 ∥ ( 𝐴 − 𝐵 ) ) )
53	10 24 52	3bitr2d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐵 ) = ( 𝐿 ‘ 𝐴 ) ↔ 𝑁 ∥ ( 𝐴 − 𝐵 ) ) )
54	3 53	syl5bb	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ 𝐵 ) ↔ 𝑁 ∥ ( 𝐴 − 𝐵 ) ) )