znunithash

Description: The size of the unit group of Z/nZ . (Contributed by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	znchr.y	$⊢ Y = ℤ / N ℤ$
	znunit.u	$⊢ U = Unit (Y)$
Assertion	znunithash	$⊢ N \in ℕ \to \|U\| = ϕ (N)$

Proof

Step	Hyp	Ref	Expression
1		znchr.y	$⊢ Y = ℤ / N ℤ$
2		znunit.u	$⊢ U = Unit (Y)$
3		dfphi2	$⊢ N \in ℕ \to ϕ (N) = \|\{x \in (0 ..^N) \| x \gcd N = 1\}\|$
4		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
5		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
6		eqid	$⊢ {ℤRHom (Y) ↾}_{if (N = 0, ℤ, (0 ..^N))} = {ℤRHom (Y) ↾}_{if (N = 0, ℤ, (0 ..^N))}$
7		eqid	$⊢ if (N = 0, ℤ, (0 ..^N)) = if (N = 0, ℤ, (0 ..^N))$
8	1 5 6 7	znf1o	$⊢ N \in ℕ_{0} \to ({ℤRHom (Y) ↾}_{if (N = 0, ℤ, (0 ..^N))}) : if (N = 0, ℤ, (0 ..^N)) \underset{1-1 onto}{⟶} {Base}_{Y}$
9	4 8	syl	$⊢ N \in ℕ \to ({ℤRHom (Y) ↾}_{if (N = 0, ℤ, (0 ..^N))}) : if (N = 0, ℤ, (0 ..^N)) \underset{1-1 onto}{⟶} {Base}_{Y}$
10		nnne0	$⊢ N \in ℕ \to N \neq 0$
11		ifnefalse	$⊢ N \neq 0 \to if (N = 0, ℤ, (0 ..^N)) = (0 ..^N)$
12		reseq2	$⊢ if (N = 0, ℤ, (0 ..^N)) = (0 ..^N) \to {ℤRHom (Y) ↾}_{if (N = 0, ℤ, (0 ..^N))} = {ℤRHom (Y) ↾}_{(0 ..^N)}$
13	12	f1oeq1d	$⊢ if (N = 0, ℤ, (0 ..^N)) = (0 ..^N) \to (({ℤRHom (Y) ↾}_{if (N = 0, ℤ, (0 ..^N))}) : if (N = 0, ℤ, (0 ..^N)) \underset{1-1 onto}{⟶} {Base}_{Y} \leftrightarrow ({ℤRHom (Y) ↾}_{(0 ..^N)}) : if (N = 0, ℤ, (0 ..^N)) \underset{1-1 onto}{⟶} {Base}_{Y})$
14		f1oeq2	$⊢ if (N = 0, ℤ, (0 ..^N)) = (0 ..^N) \to (({ℤRHom (Y) ↾}_{(0 ..^N)}) : if (N = 0, ℤ, (0 ..^N)) \underset{1-1 onto}{⟶} {Base}_{Y} \leftrightarrow ({ℤRHom (Y) ↾}_{(0 ..^N)}) : (0 ..^N) \underset{1-1 onto}{⟶} {Base}_{Y})$
15	13 14	bitrd	$⊢ if (N = 0, ℤ, (0 ..^N)) = (0 ..^N) \to (({ℤRHom (Y) ↾}_{if (N = 0, ℤ, (0 ..^N))}) : if (N = 0, ℤ, (0 ..^N)) \underset{1-1 onto}{⟶} {Base}_{Y} \leftrightarrow ({ℤRHom (Y) ↾}_{(0 ..^N)}) : (0 ..^N) \underset{1-1 onto}{⟶} {Base}_{Y})$
16	10 11 15	3syl	$⊢ N \in ℕ \to (({ℤRHom (Y) ↾}_{if (N = 0, ℤ, (0 ..^N))}) : if (N = 0, ℤ, (0 ..^N)) \underset{1-1 onto}{⟶} {Base}_{Y} \leftrightarrow ({ℤRHom (Y) ↾}_{(0 ..^N)}) : (0 ..^N) \underset{1-1 onto}{⟶} {Base}_{Y})$
17	9 16	mpbid	$⊢ N \in ℕ \to ({ℤRHom (Y) ↾}_{(0 ..^N)}) : (0 ..^N) \underset{1-1 onto}{⟶} {Base}_{Y}$
18		f1ofn	$⊢ ({ℤRHom (Y) ↾}_{(0 ..^N)}) : (0 ..^N) \underset{1-1 onto}{⟶} {Base}_{Y} \to ({ℤRHom (Y) ↾}_{(0 ..^N)}) Fn (0 ..^N)$
19		elpreima	$⊢ ({ℤRHom (Y) ↾}_{(0 ..^N)}) Fn (0 ..^N) \to (x \in {({ℤRHom (Y) ↾}_{(0 ..^N)})}^{-1} [U] \leftrightarrow (x \in (0 ..^N) \land ({ℤRHom (Y) ↾}_{(0 ..^N)}) (x) \in U))$
20	17 18 19	3syl	$⊢ N \in ℕ \to (x \in {({ℤRHom (Y) ↾}_{(0 ..^N)})}^{-1} [U] \leftrightarrow (x \in (0 ..^N) \land ({ℤRHom (Y) ↾}_{(0 ..^N)}) (x) \in U))$
21		fvres	$⊢ x \in (0 ..^N) \to ({ℤRHom (Y) ↾}_{(0 ..^N)}) (x) = ℤRHom (Y) (x)$
22	21	adantl	$⊢ (N \in ℕ \land x \in (0 ..^N)) \to ({ℤRHom (Y) ↾}_{(0 ..^N)}) (x) = ℤRHom (Y) (x)$
23	22	eleq1d	$⊢ (N \in ℕ \land x \in (0 ..^N)) \to (({ℤRHom (Y) ↾}_{(0 ..^N)}) (x) \in U \leftrightarrow ℤRHom (Y) (x) \in U)$
24		elfzoelz	$⊢ x \in (0 ..^N) \to x \in ℤ$
25		eqid	$⊢ ℤRHom (Y) = ℤRHom (Y)$
26	1 2 25	znunit	$⊢ (N \in ℕ_{0} \land x \in ℤ) \to (ℤRHom (Y) (x) \in U \leftrightarrow x \gcd N = 1)$
27	4 24 26	syl2an	$⊢ (N \in ℕ \land x \in (0 ..^N)) \to (ℤRHom (Y) (x) \in U \leftrightarrow x \gcd N = 1)$
28	23 27	bitrd	$⊢ (N \in ℕ \land x \in (0 ..^N)) \to (({ℤRHom (Y) ↾}_{(0 ..^N)}) (x) \in U \leftrightarrow x \gcd N = 1)$
29	28	pm5.32da	$⊢ N \in ℕ \to ((x \in (0 ..^N) \land ({ℤRHom (Y) ↾}_{(0 ..^N)}) (x) \in U) \leftrightarrow (x \in (0 ..^N) \land x \gcd N = 1))$
30	20 29	bitrd	$⊢ N \in ℕ \to (x \in {({ℤRHom (Y) ↾}_{(0 ..^N)})}^{-1} [U] \leftrightarrow (x \in (0 ..^N) \land x \gcd N = 1))$
31	30	eqabdv	$⊢ N \in ℕ \to {({ℤRHom (Y) ↾}_{(0 ..^N)})}^{-1} [U] = \{x \| (x \in (0 ..^N) \land x \gcd N = 1)\}$
32		df-rab	$⊢ \{x \in (0 ..^N) \| x \gcd N = 1\} = \{x \| (x \in (0 ..^N) \land x \gcd N = 1)\}$
33	31 32	eqtr4di	$⊢ N \in ℕ \to {({ℤRHom (Y) ↾}_{(0 ..^N)})}^{-1} [U] = \{x \in (0 ..^N) \| x \gcd N = 1\}$
34	33	fveq2d	$⊢ N \in ℕ \to \|{({ℤRHom (Y) ↾}_{(0 ..^N)})}^{-1} [U]\| = \|\{x \in (0 ..^N) \| x \gcd N = 1\}\|$
35		f1ocnv	$⊢ ({ℤRHom (Y) ↾}_{(0 ..^N)}) : (0 ..^N) \underset{1-1 onto}{⟶} {Base}_{Y} \to {({ℤRHom (Y) ↾}_{(0 ..^N)})}^{-1} : {Base}_{Y} \underset{1-1 onto}{⟶} (0 ..^N)$
36		f1of1	$⊢ {({ℤRHom (Y) ↾}_{(0 ..^N)})}^{-1} : {Base}_{Y} \underset{1-1 onto}{⟶} (0 ..^N) \to {({ℤRHom (Y) ↾}_{(0 ..^N)})}^{-1} : {Base}_{Y} \underset{1-1}{⟶} (0 ..^N)$
37	17 35 36	3syl	$⊢ N \in ℕ \to {({ℤRHom (Y) ↾}_{(0 ..^N)})}^{-1} : {Base}_{Y} \underset{1-1}{⟶} (0 ..^N)$
38		ovexd	$⊢ N \in ℕ \to (0 ..^N) \in V$
39	5 2	unitss	$⊢ U \subseteq {Base}_{Y}$
40	39	a1i	$⊢ N \in ℕ \to U \subseteq {Base}_{Y}$
41	2	fvexi	$⊢ U \in V$
42	41	a1i	$⊢ N \in ℕ \to U \in V$
43		f1imaen2g	$⊢ (({({ℤRHom (Y) ↾}_{(0 ..^N)})}^{-1} : {Base}_{Y} \underset{1-1}{⟶} (0 ..^N) \land (0 ..^N) \in V) \land (U \subseteq {Base}_{Y} \land U \in V)) \to {({ℤRHom (Y) ↾}_{(0 ..^N)})}^{-1} [U] \approx U$
44	37 38 40 42 43	syl22anc	$⊢ N \in ℕ \to {({ℤRHom (Y) ↾}_{(0 ..^N)})}^{-1} [U] \approx U$
45		hasheni	$⊢ {({ℤRHom (Y) ↾}_{(0 ..^N)})}^{-1} [U] \approx U \to \|{({ℤRHom (Y) ↾}_{(0 ..^N)})}^{-1} [U]\| = \|U\|$
46	44 45	syl	$⊢ N \in ℕ \to \|{({ℤRHom (Y) ↾}_{(0 ..^N)})}^{-1} [U]\| = \|U\|$
47	3 34 46	3eqtr2rd	$⊢ N \in ℕ \to \|U\| = ϕ (N)$

Metamath Proof Explorer

Theorem znunithash

Proof