znrrg

Description: The regular elements of Z/nZ are exactly the units. (This theorem fails for N = 0 , where all nonzero integers are regular, but only +- 1 are units.) (Contributed by Mario Carneiro, 18-Apr-2016)

	Ref	Expression
Hypotheses	znchr.y	$⊢ Y = ℤ / N ℤ$
	znunit.u	$⊢ U = Unit (Y)$
	znrrg.e	$⊢ E = RLReg (Y)$
Assertion	znrrg	$⊢ N \in ℕ \to E = U$

Proof

Step	Hyp	Ref	Expression
1		znchr.y	$⊢ Y = ℤ / N ℤ$
2		znunit.u	$⊢ U = Unit (Y)$
3		znrrg.e	$⊢ E = RLReg (Y)$
4		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
5		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
6		eqid	$⊢ ℤRHom (Y) = ℤRHom (Y)$
7	1 5 6	znzrhfo	$⊢ N \in ℕ_{0} \to ℤRHom (Y) : ℤ \underset{onto}{⟶} {Base}_{Y}$
8	4 7	syl	$⊢ N \in ℕ \to ℤRHom (Y) : ℤ \underset{onto}{⟶} {Base}_{Y}$
9	3 5	rrgss	$⊢ E \subseteq {Base}_{Y}$
10	9	sseli	$⊢ x \in E \to x \in {Base}_{Y}$
11		foelrn	$⊢ (ℤRHom (Y) : ℤ \underset{onto}{⟶} {Base}_{Y} \land x \in {Base}_{Y}) \to \exists n \in ℤ x = ℤRHom (Y) (n)$
12	8 10 11	syl2an	$⊢ (N \in ℕ \land x \in E) \to \exists n \in ℤ x = ℤRHom (Y) (n)$
13	12	ex	$⊢ N \in ℕ \to (x \in E \to \exists n \in ℤ x = ℤRHom (Y) (n))$
14		nncn	$⊢ N \in ℕ \to N \in ℂ$
15	14	ad2antrr	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to N \in ℂ$
16		simplr	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to n \in ℤ$
17		nnz	$⊢ N \in ℕ \to N \in ℤ$
18	17	ad2antrr	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to N \in ℤ$
19		nnne0	$⊢ N \in ℕ \to N \neq 0$
20	19	ad2antrr	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to N \neq 0$
21		simpr	$⊢ (n = 0 \land N = 0) \to N = 0$
22	21	necon3ai	$⊢ N \neq 0 \to \neg (n = 0 \land N = 0)$
23	20 22	syl	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to \neg (n = 0 \land N = 0)$
24		gcdn0cl	$⊢ ((n \in ℤ \land N \in ℤ) \land \neg (n = 0 \land N = 0)) \to n \gcd N \in ℕ$
25	16 18 23 24	syl21anc	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to n \gcd N \in ℕ$
26	25	nncnd	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to n \gcd N \in ℂ$
27	25	nnne0d	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to n \gcd N \neq 0$
28	15 26 27	divcan2d	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to (n \gcd N) (\frac{N}{n \gcd N}) = N$
29		gcddvds	$⊢ (n \in ℤ \land N \in ℤ) \to ((n \gcd N) ∥ n \land (n \gcd N) ∥ N)$
30	16 18 29	syl2anc	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to ((n \gcd N) ∥ n \land (n \gcd N) ∥ N)$
31	30	simpld	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to (n \gcd N) ∥ n$
32	25	nnzd	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to n \gcd N \in ℤ$
33	30	simprd	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to (n \gcd N) ∥ N$
34		simpll	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to N \in ℕ$
35		nndivdvds	$⊢ (N \in ℕ \land n \gcd N \in ℕ) \to ((n \gcd N) ∥ N \leftrightarrow \frac{N}{n \gcd N} \in ℕ)$
36	34 25 35	syl2anc	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to ((n \gcd N) ∥ N \leftrightarrow \frac{N}{n \gcd N} \in ℕ)$
37	33 36	mpbid	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to \frac{N}{n \gcd N} \in ℕ$
38	37	nnzd	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to \frac{N}{n \gcd N} \in ℤ$
39		dvdsmulc	$⊢ (n \gcd N \in ℤ \land n \in ℤ \land \frac{N}{n \gcd N} \in ℤ) \to ((n \gcd N) ∥ n \to (n \gcd N) (\frac{N}{n \gcd N}) ∥ n (\frac{N}{n \gcd N}))$
40	32 16 38 39	syl3anc	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to ((n \gcd N) ∥ n \to (n \gcd N) (\frac{N}{n \gcd N}) ∥ n (\frac{N}{n \gcd N}))$
41	31 40	mpd	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to (n \gcd N) (\frac{N}{n \gcd N}) ∥ n (\frac{N}{n \gcd N})$
42	28 41	eqbrtrrd	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to N ∥ n (\frac{N}{n \gcd N})$
43		simpr	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to ℤRHom (Y) (n) \in E$
44	4	ad2antrr	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to N \in ℕ_{0}$
45	44 7	syl	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to ℤRHom (Y) : ℤ \underset{onto}{⟶} {Base}_{Y}$
46		fof	$⊢ ℤRHom (Y) : ℤ \underset{onto}{⟶} {Base}_{Y} \to ℤRHom (Y) : ℤ ⟶ {Base}_{Y}$
47	45 46	syl	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to ℤRHom (Y) : ℤ ⟶ {Base}_{Y}$
48	47 38	ffvelrnd	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to ℤRHom (Y) (\frac{N}{n \gcd N}) \in {Base}_{Y}$
49		eqid	$⊢ \cdot_{Y} = \cdot_{Y}$
50		eqid	$⊢ 0_{Y} = 0_{Y}$
51	3 5 49 50	rrgeq0i	$⊢ (ℤRHom (Y) (n) \in E \land ℤRHom (Y) (\frac{N}{n \gcd N}) \in {Base}_{Y}) \to (ℤRHom (Y) (n) \cdot_{Y} ℤRHom (Y) (\frac{N}{n \gcd N}) = 0_{Y} \to ℤRHom (Y) (\frac{N}{n \gcd N}) = 0_{Y})$
52	43 48 51	syl2anc	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to (ℤRHom (Y) (n) \cdot_{Y} ℤRHom (Y) (\frac{N}{n \gcd N}) = 0_{Y} \to ℤRHom (Y) (\frac{N}{n \gcd N}) = 0_{Y})$
53	1	zncrng	$⊢ N \in ℕ_{0} \to Y \in CRing$
54	4 53	syl	$⊢ N \in ℕ \to Y \in CRing$
55		crngring	$⊢ Y \in CRing \to Y \in Ring$
56	54 55	syl	$⊢ N \in ℕ \to Y \in Ring$
57	56	ad2antrr	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to Y \in Ring$
58	6	zrhrhm	$⊢ Y \in Ring \to ℤRHom (Y) \in (ℤ_{ring} RingHom Y)$
59	57 58	syl	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to ℤRHom (Y) \in (ℤ_{ring} RingHom Y)$
60		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
61		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
62	60 61 49	rhmmul	$⊢ (ℤRHom (Y) \in (ℤ_{ring} RingHom Y) \land n \in ℤ \land \frac{N}{n \gcd N} \in ℤ) \to ℤRHom (Y) (n (\frac{N}{n \gcd N})) = ℤRHom (Y) (n) \cdot_{Y} ℤRHom (Y) (\frac{N}{n \gcd N})$
63	59 16 38 62	syl3anc	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to ℤRHom (Y) (n (\frac{N}{n \gcd N})) = ℤRHom (Y) (n) \cdot_{Y} ℤRHom (Y) (\frac{N}{n \gcd N})$
64	63	eqeq1d	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to (ℤRHom (Y) (n (\frac{N}{n \gcd N})) = 0_{Y} \leftrightarrow ℤRHom (Y) (n) \cdot_{Y} ℤRHom (Y) (\frac{N}{n \gcd N}) = 0_{Y})$
65	16 38	zmulcld	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to n (\frac{N}{n \gcd N}) \in ℤ$
66	1 6 50	zndvds0	$⊢ (N \in ℕ_{0} \land n (\frac{N}{n \gcd N}) \in ℤ) \to (ℤRHom (Y) (n (\frac{N}{n \gcd N})) = 0_{Y} \leftrightarrow N ∥ n (\frac{N}{n \gcd N}))$
67	44 65 66	syl2anc	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to (ℤRHom (Y) (n (\frac{N}{n \gcd N})) = 0_{Y} \leftrightarrow N ∥ n (\frac{N}{n \gcd N}))$
68	64 67	bitr3d	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to (ℤRHom (Y) (n) \cdot_{Y} ℤRHom (Y) (\frac{N}{n \gcd N}) = 0_{Y} \leftrightarrow N ∥ n (\frac{N}{n \gcd N}))$
69	1 6 50	zndvds0	$⊢ (N \in ℕ_{0} \land \frac{N}{n \gcd N} \in ℤ) \to (ℤRHom (Y) (\frac{N}{n \gcd N}) = 0_{Y} \leftrightarrow N ∥ (\frac{N}{n \gcd N}))$
70	44 38 69	syl2anc	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to (ℤRHom (Y) (\frac{N}{n \gcd N}) = 0_{Y} \leftrightarrow N ∥ (\frac{N}{n \gcd N}))$
71	52 68 70	3imtr3d	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to (N ∥ n (\frac{N}{n \gcd N}) \to N ∥ (\frac{N}{n \gcd N}))$
72	42 71	mpd	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to N ∥ (\frac{N}{n \gcd N})$
73	15 26 27	divcan1d	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to (\frac{N}{n \gcd N}) (n \gcd N) = N$
74	37	nncnd	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to \frac{N}{n \gcd N} \in ℂ$
75	74	mulid1d	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to (\frac{N}{n \gcd N}) \cdot 1 = \frac{N}{n \gcd N}$
76	72 73 75	3brtr4d	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to (\frac{N}{n \gcd N}) (n \gcd N) ∥ (\frac{N}{n \gcd N}) \cdot 1$
77		1zzd	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to 1 \in ℤ$
78	37	nnne0d	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to \frac{N}{n \gcd N} \neq 0$
79		dvdscmulr	$⊢ (n \gcd N \in ℤ \land 1 \in ℤ \land (\frac{N}{n \gcd N} \in ℤ \land \frac{N}{n \gcd N} \neq 0)) \to ((\frac{N}{n \gcd N}) (n \gcd N) ∥ (\frac{N}{n \gcd N}) \cdot 1 \leftrightarrow (n \gcd N) ∥ 1)$
80	32 77 38 78 79	syl112anc	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to ((\frac{N}{n \gcd N}) (n \gcd N) ∥ (\frac{N}{n \gcd N}) \cdot 1 \leftrightarrow (n \gcd N) ∥ 1)$
81	76 80	mpbid	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to (n \gcd N) ∥ 1$
82	16 18	gcdcld	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to n \gcd N \in ℕ_{0}$
83		dvds1	$⊢ n \gcd N \in ℕ_{0} \to ((n \gcd N) ∥ 1 \leftrightarrow n \gcd N = 1)$
84	82 83	syl	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to ((n \gcd N) ∥ 1 \leftrightarrow n \gcd N = 1)$
85	81 84	mpbid	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to n \gcd N = 1$
86	1 2 6	znunit	$⊢ (N \in ℕ_{0} \land n \in ℤ) \to (ℤRHom (Y) (n) \in U \leftrightarrow n \gcd N = 1)$
87	44 16 86	syl2anc	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to (ℤRHom (Y) (n) \in U \leftrightarrow n \gcd N = 1)$
88	85 87	mpbird	$⊢ ((N \in ℕ \land n \in ℤ) \land ℤRHom (Y) (n) \in E) \to ℤRHom (Y) (n) \in U$
89	88	ex	$⊢ (N \in ℕ \land n \in ℤ) \to (ℤRHom (Y) (n) \in E \to ℤRHom (Y) (n) \in U)$
90		eleq1	$⊢ x = ℤRHom (Y) (n) \to (x \in E \leftrightarrow ℤRHom (Y) (n) \in E)$
91		eleq1	$⊢ x = ℤRHom (Y) (n) \to (x \in U \leftrightarrow ℤRHom (Y) (n) \in U)$
92	90 91	imbi12d	$⊢ x = ℤRHom (Y) (n) \to ((x \in E \to x \in U) \leftrightarrow (ℤRHom (Y) (n) \in E \to ℤRHom (Y) (n) \in U))$
93	89 92	syl5ibrcom	$⊢ (N \in ℕ \land n \in ℤ) \to (x = ℤRHom (Y) (n) \to (x \in E \to x \in U))$
94	93	rexlimdva	$⊢ N \in ℕ \to (\exists n \in ℤ x = ℤRHom (Y) (n) \to (x \in E \to x \in U))$
95	94	com23	$⊢ N \in ℕ \to (x \in E \to (\exists n \in ℤ x = ℤRHom (Y) (n) \to x \in U))$
96	13 95	mpdd	$⊢ N \in ℕ \to (x \in E \to x \in U)$
97	96	ssrdv	$⊢ N \in ℕ \to E \subseteq U$
98	3 2	unitrrg	$⊢ Y \in Ring \to U \subseteq E$
99	56 98	syl	$⊢ N \in ℕ \to U \subseteq E$
100	97 99	eqssd	$⊢ N \in ℕ \to E = U$

Metamath Proof Explorer

Theorem znrrg

Proof