znunit

Description: The units of Z/nZ are the integers coprime to the base. (Contributed by Mario Carneiro, 18-Apr-2016)

	Ref	Expression
Hypotheses	znchr.y	$⊢ Y = ℤ / N ℤ$
	znunit.u	$⊢ U = Unit (Y)$
	znunit.l	$⊢ L = ℤRHom (Y)$
Assertion	znunit	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (L (A) \in U \leftrightarrow A \gcd N = 1)$

Proof

Step	Hyp	Ref	Expression
1		znchr.y	$⊢ Y = ℤ / N ℤ$
2		znunit.u	$⊢ U = Unit (Y)$
3		znunit.l	$⊢ L = ℤRHom (Y)$
4	1	zncrng	$⊢ N \in ℕ_{0} \to Y \in CRing$
5	4	adantr	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to Y \in CRing$
6		eqid	$⊢ 1_{Y} = 1_{Y}$
7		eqid	$⊢ ∥_{r} (Y) = ∥_{r} (Y)$
8	2 6 7	crngunit	$⊢ Y \in CRing \to (L (A) \in U \leftrightarrow L (A) ∥_{r} (Y) 1_{Y})$
9	5 8	syl	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (L (A) \in U \leftrightarrow L (A) ∥_{r} (Y) 1_{Y})$
10		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
11	1 10 3	znzrhfo	$⊢ N \in ℕ_{0} \to L : ℤ \underset{onto}{⟶} {Base}_{Y}$
12	11	adantr	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to L : ℤ \underset{onto}{⟶} {Base}_{Y}$
13		fof	$⊢ L : ℤ \underset{onto}{⟶} {Base}_{Y} \to L : ℤ ⟶ {Base}_{Y}$
14	12 13	syl	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to L : ℤ ⟶ {Base}_{Y}$
15		ffvelrn	$⊢ (L : ℤ ⟶ {Base}_{Y} \land A \in ℤ) \to L (A) \in {Base}_{Y}$
16	14 15	sylancom	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to L (A) \in {Base}_{Y}$
17		eqid	$⊢ \cdot_{Y} = \cdot_{Y}$
18	10 7 17	dvdsr2	$⊢ L (A) \in {Base}_{Y} \to (L (A) ∥_{r} (Y) 1_{Y} \leftrightarrow \exists x \in {Base}_{Y} x \cdot_{Y} L (A) = 1_{Y})$
19	16 18	syl	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (L (A) ∥_{r} (Y) 1_{Y} \leftrightarrow \exists x \in {Base}_{Y} x \cdot_{Y} L (A) = 1_{Y})$
20		forn	$⊢ L : ℤ \underset{onto}{⟶} {Base}_{Y} \to ran L = {Base}_{Y}$
21	12 20	syl	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to ran L = {Base}_{Y}$
22	21	rexeqdv	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (\exists x \in ran L x \cdot_{Y} L (A) = 1_{Y} \leftrightarrow \exists x \in {Base}_{Y} x \cdot_{Y} L (A) = 1_{Y})$
23		ffn	$⊢ L : ℤ ⟶ {Base}_{Y} \to L Fn ℤ$
24		oveq1	$⊢ x = L (n) \to x \cdot_{Y} L (A) = L (n) \cdot_{Y} L (A)$
25	24	eqeq1d	$⊢ x = L (n) \to (x \cdot_{Y} L (A) = 1_{Y} \leftrightarrow L (n) \cdot_{Y} L (A) = 1_{Y})$
26	25	rexrn	$⊢ L Fn ℤ \to (\exists x \in ran L x \cdot_{Y} L (A) = 1_{Y} \leftrightarrow \exists n \in ℤ L (n) \cdot_{Y} L (A) = 1_{Y})$
27	14 23 26	3syl	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (\exists x \in ran L x \cdot_{Y} L (A) = 1_{Y} \leftrightarrow \exists n \in ℤ L (n) \cdot_{Y} L (A) = 1_{Y})$
28	22 27	bitr3d	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (\exists x \in {Base}_{Y} x \cdot_{Y} L (A) = 1_{Y} \leftrightarrow \exists n \in ℤ L (n) \cdot_{Y} L (A) = 1_{Y})$
29		crngring	$⊢ Y \in CRing \to Y \in Ring$
30	5 29	syl	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to Y \in Ring$
31	3	zrhrhm	$⊢ Y \in Ring \to L \in (ℤ_{ring} RingHom Y)$
32	30 31	syl	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to L \in (ℤ_{ring} RingHom Y)$
33	32	adantr	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \to L \in (ℤ_{ring} RingHom Y)$
34		simpr	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \to n \in ℤ$
35		simplr	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \to A \in ℤ$
36		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
37		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
38	36 37 17	rhmmul	$⊢ (L \in (ℤ_{ring} RingHom Y) \land n \in ℤ \land A \in ℤ) \to L (n A) = L (n) \cdot_{Y} L (A)$
39	33 34 35 38	syl3anc	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \to L (n A) = L (n) \cdot_{Y} L (A)$
40	30	adantr	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \to Y \in Ring$
41	3 6	zrh1	$⊢ Y \in Ring \to L (1) = 1_{Y}$
42	40 41	syl	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \to L (1) = 1_{Y}$
43	39 42	eqeq12d	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \to (L (n A) = L (1) \leftrightarrow L (n) \cdot_{Y} L (A) = 1_{Y})$
44		simpll	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \to N \in ℕ_{0}$
45	34 35	zmulcld	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \to n A \in ℤ$
46		1zzd	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \to 1 \in ℤ$
47	1 3	zndvds	$⊢ (N \in ℕ_{0} \land n A \in ℤ \land 1 \in ℤ) \to (L (n A) = L (1) \leftrightarrow N ∥ (n A - 1))$
48	44 45 46 47	syl3anc	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \to (L (n A) = L (1) \leftrightarrow N ∥ (n A - 1))$
49	43 48	bitr3d	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \to (L (n) \cdot_{Y} L (A) = 1_{Y} \leftrightarrow N ∥ (n A - 1))$
50	49	rexbidva	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (\exists n \in ℤ L (n) \cdot_{Y} L (A) = 1_{Y} \leftrightarrow \exists n \in ℤ N ∥ (n A - 1))$
51		simplr	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to A \in ℤ$
52		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
53	52	ad2antrr	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to N \in ℤ$
54		gcddvds	$⊢ (A \in ℤ \land N \in ℤ) \to ((A \gcd N) ∥ A \land (A \gcd N) ∥ N)$
55	51 53 54	syl2anc	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to ((A \gcd N) ∥ A \land (A \gcd N) ∥ N)$
56	55	simpld	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to (A \gcd N) ∥ A$
57	51 53	gcdcld	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to A \gcd N \in ℕ_{0}$
58	57	nn0zd	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to A \gcd N \in ℤ$
59	34	adantrr	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to n \in ℤ$
60		dvdsmultr2	$⊢ (A \gcd N \in ℤ \land n \in ℤ \land A \in ℤ) \to ((A \gcd N) ∥ A \to (A \gcd N) ∥ n A)$
61	58 59 51 60	syl3anc	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to ((A \gcd N) ∥ A \to (A \gcd N) ∥ n A)$
62	56 61	mpd	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to (A \gcd N) ∥ n A$
63	45	adantrr	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to n A \in ℤ$
64		1zzd	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to 1 \in ℤ$
65		peano2zm	$⊢ n A \in ℤ \to n A - 1 \in ℤ$
66	63 65	syl	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to n A - 1 \in ℤ$
67	55	simprd	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to (A \gcd N) ∥ N$
68		simprr	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to N ∥ (n A - 1)$
69	58 53 66 67 68	dvdstrd	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to (A \gcd N) ∥ (n A - 1)$
70		dvdssub2	$⊢ ((A \gcd N \in ℤ \land n A \in ℤ \land 1 \in ℤ) \land (A \gcd N) ∥ (n A - 1)) \to ((A \gcd N) ∥ n A \leftrightarrow (A \gcd N) ∥ 1)$
71	58 63 64 69 70	syl31anc	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to ((A \gcd N) ∥ n A \leftrightarrow (A \gcd N) ∥ 1)$
72	62 71	mpbid	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to (A \gcd N) ∥ 1$
73		dvds1	$⊢ A \gcd N \in ℕ_{0} \to ((A \gcd N) ∥ 1 \leftrightarrow A \gcd N = 1)$
74	57 73	syl	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to ((A \gcd N) ∥ 1 \leftrightarrow A \gcd N = 1)$
75	72 74	mpbid	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land (n \in ℤ \land N ∥ (n A - 1))) \to A \gcd N = 1$
76	75	rexlimdvaa	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (\exists n \in ℤ N ∥ (n A - 1) \to A \gcd N = 1)$
77		simpr	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to A \in ℤ$
78	52	adantr	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to N \in ℤ$
79		bezout	$⊢ (A \in ℤ \land N \in ℤ) \to \exists n \in ℤ \exists m \in ℤ A \gcd N = A n + N m$
80	77 78 79	syl2anc	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to \exists n \in ℤ \exists m \in ℤ A \gcd N = A n + N m$
81		eqeq1	$⊢ A \gcd N = 1 \to (A \gcd N = A n + N m \leftrightarrow 1 = A n + N m)$
82	81	2rexbidv	$⊢ A \gcd N = 1 \to (\exists n \in ℤ \exists m \in ℤ A \gcd N = A n + N m \leftrightarrow \exists n \in ℤ \exists m \in ℤ 1 = A n + N m)$
83	80 82	syl5ibcom	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (A \gcd N = 1 \to \exists n \in ℤ \exists m \in ℤ 1 = A n + N m)$
84	52	ad3antrrr	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to N \in ℤ$
85		dvdsmul1	$⊢ (N \in ℤ \land m \in ℤ) \to N ∥ N m$
86	84 85	sylancom	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to N ∥ N m$
87		zmulcl	$⊢ (N \in ℤ \land m \in ℤ) \to N m \in ℤ$
88	84 87	sylancom	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to N m \in ℤ$
89		dvdsnegb	$⊢ (N \in ℤ \land N m \in ℤ) \to (N ∥ N m \leftrightarrow N ∥ (- N m))$
90	84 88 89	syl2anc	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to (N ∥ N m \leftrightarrow N ∥ (- N m))$
91	86 90	mpbid	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to N ∥ (- N m)$
92	35	adantr	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to A \in ℤ$
93	92	zcnd	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to A \in ℂ$
94		zcn	$⊢ n \in ℤ \to n \in ℂ$
95	94	ad2antlr	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to n \in ℂ$
96	93 95	mulcomd	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to A n = n A$
97	96	oveq1d	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to A n + N m = n A + N m$
98	95 93	mulcld	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to n A \in ℂ$
99	88	zcnd	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to N m \in ℂ$
100	98 99	subnegd	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to n A - (- N m) = n A + N m$
101	97 100	eqtr4d	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to A n + N m = n A - (- N m)$
102	101	oveq2d	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to n A - (A n + N m) = n A - (n A - (- N m))$
103	99	negcld	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to - N m \in ℂ$
104	98 103	nncand	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to n A - (n A - (- N m)) = - N m$
105	102 104	eqtrd	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to n A - (A n + N m) = - N m$
106	91 105	breqtrrd	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to N ∥ (n A - (A n + N m))$
107		oveq2	$⊢ 1 = A n + N m \to n A - 1 = n A - (A n + N m)$
108	107	breq2d	$⊢ 1 = A n + N m \to (N ∥ (n A - 1) \leftrightarrow N ∥ (n A - (A n + N m)))$
109	106 108	syl5ibrcom	$⊢ (((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \land m \in ℤ) \to (1 = A n + N m \to N ∥ (n A - 1))$
110	109	rexlimdva	$⊢ ((N \in ℕ_{0} \land A \in ℤ) \land n \in ℤ) \to (\exists m \in ℤ 1 = A n + N m \to N ∥ (n A - 1))$
111	110	reximdva	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (\exists n \in ℤ \exists m \in ℤ 1 = A n + N m \to \exists n \in ℤ N ∥ (n A - 1))$
112	83 111	syld	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (A \gcd N = 1 \to \exists n \in ℤ N ∥ (n A - 1))$
113	76 112	impbid	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (\exists n \in ℤ N ∥ (n A - 1) \leftrightarrow A \gcd N = 1)$
114	28 50 113	3bitrd	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (\exists x \in {Base}_{Y} x \cdot_{Y} L (A) = 1_{Y} \leftrightarrow A \gcd N = 1)$
115	9 19 114	3bitrd	$⊢ (N \in ℕ_{0} \land A \in ℤ) \to (L (A) \in U \leftrightarrow A \gcd N = 1)$

Metamath Proof Explorer

Theorem znunit

Proof