dfphi2

Description: Alternate definition of the Euler phi function. (Contributed by Mario Carneiro, 23-Feb-2014) (Revised by Mario Carneiro, 2-May-2016)

		Ref	Expression
	Assertion	dfphi2	$⊢ N \in ℕ \to ϕ (N) = \|\{x \in (0 ..^N) \| x \gcd N = 1\}\|$

Proof

Step	Hyp	Ref	Expression
1		elnn1uz2	$⊢ N \in ℕ \leftrightarrow (N = 1 \lor N \in ℤ_{\geq 2})$
2		phi1	$⊢ ϕ (1) = 1$
3		0z	$⊢ 0 \in ℤ$
4		hashsng	$⊢ 0 \in ℤ \to \|\{0\}\| = 1$
5	3 4	ax-mp	$⊢ \|\{0\}\| = 1$
6		rabid2	$⊢ \{0\} = \{x \in \{0\} \| x \gcd 1 = 1\} \leftrightarrow \forall x \in \{0\} x \gcd 1 = 1$
7		elsni	$⊢ x \in \{0\} \to x = 0$
8	7	oveq1d	$⊢ x \in \{0\} \to x \gcd 1 = 0 \gcd 1$
9		gcd1	$⊢ 0 \in ℤ \to 0 \gcd 1 = 1$
10	3 9	ax-mp	$⊢ 0 \gcd 1 = 1$
11	8 10	eqtrdi	$⊢ x \in \{0\} \to x \gcd 1 = 1$
12	6 11	mprgbir	$⊢ \{0\} = \{x \in \{0\} \| x \gcd 1 = 1\}$
13	12	fveq2i	$⊢ \|\{0\}\| = \|\{x \in \{0\} \| x \gcd 1 = 1\}\|$
14	2 5 13	3eqtr2i	$⊢ ϕ (1) = \|\{x \in \{0\} \| x \gcd 1 = 1\}\|$
15		fveq2	$⊢ N = 1 \to ϕ (N) = ϕ (1)$
16		oveq2	$⊢ N = 1 \to (0 ..^N) = (0 ..^1)$
17		fzo01	$⊢ (0 ..^1) = \{0\}$
18	16 17	eqtrdi	$⊢ N = 1 \to (0 ..^N) = \{0\}$
19		oveq2	$⊢ N = 1 \to x \gcd N = x \gcd 1$
20	19	eqeq1d	$⊢ N = 1 \to (x \gcd N = 1 \leftrightarrow x \gcd 1 = 1)$
21	18 20	rabeqbidv	$⊢ N = 1 \to \{x \in (0 ..^N) \| x \gcd N = 1\} = \{x \in \{0\} \| x \gcd 1 = 1\}$
22	21	fveq2d	$⊢ N = 1 \to \|\{x \in (0 ..^N) \| x \gcd N = 1\}\| = \|\{x \in \{0\} \| x \gcd 1 = 1\}\|$
23	14 15 22	3eqtr4a	$⊢ N = 1 \to ϕ (N) = \|\{x \in (0 ..^N) \| x \gcd N = 1\}\|$
24		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
25		phival	$⊢ N \in ℕ \to ϕ (N) = \|\{x \in (1 \dots N) \| x \gcd N = 1\}\|$
26	24 25	syl	$⊢ N \in ℤ_{\geq 2} \to ϕ (N) = \|\{x \in (1 \dots N) \| x \gcd N = 1\}\|$
27		fzossfz	$⊢ (1 ..^N) \subseteq (1 \dots N)$
28	27	a1i	$⊢ N \in ℤ_{\geq 2} \to (1 ..^N) \subseteq (1 \dots N)$
29		sseqin2	$⊢ (1 ..^N) \subseteq (1 \dots N) \leftrightarrow (1 \dots N) \cap (1 ..^N) = (1 ..^N)$
30	28 29	sylib	$⊢ N \in ℤ_{\geq 2} \to (1 \dots N) \cap (1 ..^N) = (1 ..^N)$
31		fzo0ss1	$⊢ (1 ..^N) \subseteq (0 ..^N)$
32		sseqin2	$⊢ (1 ..^N) \subseteq (0 ..^N) \leftrightarrow (0 ..^N) \cap (1 ..^N) = (1 ..^N)$
33	31 32	mpbi	$⊢ (0 ..^N) \cap (1 ..^N) = (1 ..^N)$
34	30 33	eqtr4di	$⊢ N \in ℤ_{\geq 2} \to (1 \dots N) \cap (1 ..^N) = (0 ..^N) \cap (1 ..^N)$
35	34	rabeqdv	$⊢ N \in ℤ_{\geq 2} \to \{x \in ((1 \dots N) \cap (1 ..^N)) \| x \gcd N = 1\} = \{x \in ((0 ..^N) \cap (1 ..^N)) \| x \gcd N = 1\}$
36		inrab2	$⊢ \{x \in (1 \dots N) \| x \gcd N = 1\} \cap (1 ..^N) = \{x \in ((1 \dots N) \cap (1 ..^N)) \| x \gcd N = 1\}$
37		inrab2	$⊢ \{x \in (0 ..^N) \| x \gcd N = 1\} \cap (1 ..^N) = \{x \in ((0 ..^N) \cap (1 ..^N)) \| x \gcd N = 1\}$
38	35 36 37	3eqtr4g	$⊢ N \in ℤ_{\geq 2} \to \{x \in (1 \dots N) \| x \gcd N = 1\} \cap (1 ..^N) = \{x \in (0 ..^N) \| x \gcd N = 1\} \cap (1 ..^N)$
39		phibndlem	$⊢ N \in ℤ_{\geq 2} \to \{x \in (1 \dots N) \| x \gcd N = 1\} \subseteq (1 \dots N - 1)$
40		eluzelz	$⊢ N \in ℤ_{\geq 2} \to N \in ℤ$
41		fzoval	$⊢ N \in ℤ \to (1 ..^N) = (1 \dots N - 1)$
42	40 41	syl	$⊢ N \in ℤ_{\geq 2} \to (1 ..^N) = (1 \dots N - 1)$
43	39 42	sseqtrrd	$⊢ N \in ℤ_{\geq 2} \to \{x \in (1 \dots N) \| x \gcd N = 1\} \subseteq (1 ..^N)$
44		dfss2	$⊢ \{x \in (1 \dots N) \| x \gcd N = 1\} \subseteq (1 ..^N) \leftrightarrow \{x \in (1 \dots N) \| x \gcd N = 1\} \cap (1 ..^N) = \{x \in (1 \dots N) \| x \gcd N = 1\}$
45	43 44	sylib	$⊢ N \in ℤ_{\geq 2} \to \{x \in (1 \dots N) \| x \gcd N = 1\} \cap (1 ..^N) = \{x \in (1 \dots N) \| x \gcd N = 1\}$
46		gcd0id	$⊢ N \in ℤ \to 0 \gcd N = \|N\|$
47	40 46	syl	$⊢ N \in ℤ_{\geq 2} \to 0 \gcd N = \|N\|$
48		eluzelre	$⊢ N \in ℤ_{\geq 2} \to N \in ℝ$
49		eluzge2nn0	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ_{0}$
50	49	nn0ge0d	$⊢ N \in ℤ_{\geq 2} \to 0 \leq N$
51	48 50	absidd	$⊢ N \in ℤ_{\geq 2} \to \|N\| = N$
52	47 51	eqtrd	$⊢ N \in ℤ_{\geq 2} \to 0 \gcd N = N$
53		eluz2b3	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (N \in ℕ \land N \neq 1)$
54	53	simprbi	$⊢ N \in ℤ_{\geq 2} \to N \neq 1$
55	52 54	eqnetrd	$⊢ N \in ℤ_{\geq 2} \to 0 \gcd N \neq 1$
56	55	adantr	$⊢ (N \in ℤ_{\geq 2} \land x \in (0 ..^N)) \to 0 \gcd N \neq 1$
57	7	oveq1d	$⊢ x \in \{0\} \to x \gcd N = 0 \gcd N$
58	57 17	eleq2s	$⊢ x \in (0 ..^1) \to x \gcd N = 0 \gcd N$
59	58	neeq1d	$⊢ x \in (0 ..^1) \to (x \gcd N \neq 1 \leftrightarrow 0 \gcd N \neq 1)$
60	56 59	syl5ibrcom	$⊢ (N \in ℤ_{\geq 2} \land x \in (0 ..^N)) \to (x \in (0 ..^1) \to x \gcd N \neq 1)$
61	60	necon2bd	$⊢ (N \in ℤ_{\geq 2} \land x \in (0 ..^N)) \to (x \gcd N = 1 \to \neg x \in (0 ..^1))$
62		simpr	$⊢ (N \in ℤ_{\geq 2} \land x \in (0 ..^N)) \to x \in (0 ..^N)$
63		1z	$⊢ 1 \in ℤ$
64		fzospliti	$⊢ (x \in (0 ..^N) \land 1 \in ℤ) \to (x \in (0 ..^1) \lor x \in (1 ..^N))$
65	62 63 64	sylancl	$⊢ (N \in ℤ_{\geq 2} \land x \in (0 ..^N)) \to (x \in (0 ..^1) \lor x \in (1 ..^N))$
66	65	ord	$⊢ (N \in ℤ_{\geq 2} \land x \in (0 ..^N)) \to (\neg x \in (0 ..^1) \to x \in (1 ..^N))$
67	61 66	syld	$⊢ (N \in ℤ_{\geq 2} \land x \in (0 ..^N)) \to (x \gcd N = 1 \to x \in (1 ..^N))$
68	67	ralrimiva	$⊢ N \in ℤ_{\geq 2} \to \forall x \in (0 ..^N) (x \gcd N = 1 \to x \in (1 ..^N))$
69		rabss	$⊢ \{x \in (0 ..^N) \| x \gcd N = 1\} \subseteq (1 ..^N) \leftrightarrow \forall x \in (0 ..^N) (x \gcd N = 1 \to x \in (1 ..^N))$
70	68 69	sylibr	$⊢ N \in ℤ_{\geq 2} \to \{x \in (0 ..^N) \| x \gcd N = 1\} \subseteq (1 ..^N)$
71		dfss2	$⊢ \{x \in (0 ..^N) \| x \gcd N = 1\} \subseteq (1 ..^N) \leftrightarrow \{x \in (0 ..^N) \| x \gcd N = 1\} \cap (1 ..^N) = \{x \in (0 ..^N) \| x \gcd N = 1\}$
72	70 71	sylib	$⊢ N \in ℤ_{\geq 2} \to \{x \in (0 ..^N) \| x \gcd N = 1\} \cap (1 ..^N) = \{x \in (0 ..^N) \| x \gcd N = 1\}$
73	38 45 72	3eqtr3d	$⊢ N \in ℤ_{\geq 2} \to \{x \in (1 \dots N) \| x \gcd N = 1\} = \{x \in (0 ..^N) \| x \gcd N = 1\}$
74	73	fveq2d	$⊢ N \in ℤ_{\geq 2} \to \|\{x \in (1 \dots N) \| x \gcd N = 1\}\| = \|\{x \in (0 ..^N) \| x \gcd N = 1\}\|$
75	26 74	eqtrd	$⊢ N \in ℤ_{\geq 2} \to ϕ (N) = \|\{x \in (0 ..^N) \| x \gcd N = 1\}\|$
76	23 75	jaoi	$⊢ (N = 1 \lor N \in ℤ_{\geq 2}) \to ϕ (N) = \|\{x \in (0 ..^N) \| x \gcd N = 1\}\|$
77	1 76	sylbi	$⊢ N \in ℕ \to ϕ (N) = \|\{x \in (0 ..^N) \| x \gcd N = 1\}\|$

Metamath Proof Explorer

Theorem dfphi2

Proof