phiprmpw

Description: Value of the Euler phi function at a prime power. Theorem 2.5(a) in ApostolNT p. 28. (Contributed by Mario Carneiro, 24-Feb-2014)

		Ref	Expression
	Assertion	phiprmpw	$⊢ (P \in ℙ \land K \in ℕ) \to ϕ (P^{K}) = P^{K - 1} (P - 1)$

Proof

Step	Hyp	Ref	Expression
1		prmnn	$⊢ P \in ℙ \to P \in ℕ$
2		nnnn0	$⊢ K \in ℕ \to K \in ℕ_{0}$
3		nnexpcl	$⊢ (P \in ℕ \land K \in ℕ_{0}) \to P^{K} \in ℕ$
4	1 2 3	syl2an	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K} \in ℕ$
5		phival	$⊢ P^{K} \in ℕ \to ϕ (P^{K}) = \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\|$
6	4 5	syl	$⊢ (P \in ℙ \land K \in ℕ) \to ϕ (P^{K}) = \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\|$
7		nnm1nn0	$⊢ K \in ℕ \to K - 1 \in ℕ_{0}$
8		nnexpcl	$⊢ (P \in ℕ \land K - 1 \in ℕ_{0}) \to P^{K - 1} \in ℕ$
9	1 7 8	syl2an	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K - 1} \in ℕ$
10	9	nncnd	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K - 1} \in ℂ$
11	1	nncnd	$⊢ P \in ℙ \to P \in ℂ$
12	11	adantr	$⊢ (P \in ℙ \land K \in ℕ) \to P \in ℂ$
13		ax-1cn	$⊢ 1 \in ℂ$
14		subdi	$⊢ (P^{K - 1} \in ℂ \land P \in ℂ \land 1 \in ℂ) \to P^{K - 1} (P - 1) = P^{K - 1} P - P^{K - 1} \cdot 1$
15	13 14	mp3an3	$⊢ (P^{K - 1} \in ℂ \land P \in ℂ) \to P^{K - 1} (P - 1) = P^{K - 1} P - P^{K - 1} \cdot 1$
16	10 12 15	syl2anc	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K - 1} (P - 1) = P^{K - 1} P - P^{K - 1} \cdot 1$
17	10	mulid1d	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K - 1} \cdot 1 = P^{K - 1}$
18	17	oveq2d	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K - 1} P - P^{K - 1} \cdot 1 = P^{K - 1} P - P^{K - 1}$
19		fzfi	$⊢ (1 \dots P^{K}) \in Fin$
20		ssrab2	$⊢ \{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\} \subseteq (1 \dots P^{K})$
21		ssfi	$⊢ ((1 \dots P^{K}) \in Fin \land \{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\} \subseteq (1 \dots P^{K})) \to \{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\} \in Fin$
22	19 20 21	mp2an	$⊢ \{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\} \in Fin$
23		ssrab2	$⊢ \{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\} \subseteq (1 \dots P^{K})$
24		ssfi	$⊢ ((1 \dots P^{K}) \in Fin \land \{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\} \subseteq (1 \dots P^{K})) \to \{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\} \in Fin$
25	19 23 24	mp2an	$⊢ \{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\} \in Fin$
26		inrab	$⊢ \{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\} \cap \{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\} = \{x \in (1 \dots P^{K}) \| (x \gcd P^{K} = 1 \land P ∥ (x - 0))\}$
27		elfzelz	$⊢ x \in (1 \dots P^{K}) \to x \in ℤ$
28		prmz	$⊢ P \in ℙ \to P \in ℤ$
29		rpexp	$⊢ (P \in ℤ \land x \in ℤ \land K \in ℕ) \to (P^{K} \gcd x = 1 \leftrightarrow P \gcd x = 1)$
30	28 29	syl3an1	$⊢ (P \in ℙ \land x \in ℤ \land K \in ℕ) \to (P^{K} \gcd x = 1 \leftrightarrow P \gcd x = 1)$
31	30	3expa	$⊢ ((P \in ℙ \land x \in ℤ) \land K \in ℕ) \to (P^{K} \gcd x = 1 \leftrightarrow P \gcd x = 1)$
32	31	an32s	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in ℤ) \to (P^{K} \gcd x = 1 \leftrightarrow P \gcd x = 1)$
33		simpr	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in ℤ) \to x \in ℤ$
34		zexpcl	$⊢ (P \in ℤ \land K \in ℕ_{0}) \to P^{K} \in ℤ$
35	28 2 34	syl2an	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K} \in ℤ$
36	35	adantr	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in ℤ) \to P^{K} \in ℤ$
37	33 36	gcdcomd	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in ℤ) \to x \gcd P^{K} = P^{K} \gcd x$
38	37	eqeq1d	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in ℤ) \to (x \gcd P^{K} = 1 \leftrightarrow P^{K} \gcd x = 1)$
39		coprm	$⊢ (P \in ℙ \land x \in ℤ) \to (\neg P ∥ x \leftrightarrow P \gcd x = 1)$
40	39	adantlr	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in ℤ) \to (\neg P ∥ x \leftrightarrow P \gcd x = 1)$
41	32 38 40	3bitr4d	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in ℤ) \to (x \gcd P^{K} = 1 \leftrightarrow \neg P ∥ x)$
42		zcn	$⊢ x \in ℤ \to x \in ℂ$
43	42	adantl	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in ℤ) \to x \in ℂ$
44	43	subid1d	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in ℤ) \to x - 0 = x$
45	44	breq2d	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in ℤ) \to (P ∥ (x - 0) \leftrightarrow P ∥ x)$
46	45	notbid	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in ℤ) \to (\neg P ∥ (x - 0) \leftrightarrow \neg P ∥ x)$
47	41 46	bitr4d	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in ℤ) \to (x \gcd P^{K} = 1 \leftrightarrow \neg P ∥ (x - 0))$
48	27 47	sylan2	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in (1 \dots P^{K})) \to (x \gcd P^{K} = 1 \leftrightarrow \neg P ∥ (x - 0))$
49	48	biimpd	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in (1 \dots P^{K})) \to (x \gcd P^{K} = 1 \to \neg P ∥ (x - 0))$
50		imnan	$⊢ (x \gcd P^{K} = 1 \to \neg P ∥ (x - 0)) \leftrightarrow \neg (x \gcd P^{K} = 1 \land P ∥ (x - 0))$
51	49 50	sylib	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in (1 \dots P^{K})) \to \neg (x \gcd P^{K} = 1 \land P ∥ (x - 0))$
52	51	ralrimiva	$⊢ (P \in ℙ \land K \in ℕ) \to \forall x \in (1 \dots P^{K}) \neg (x \gcd P^{K} = 1 \land P ∥ (x - 0))$
53		rabeq0	$⊢ \{x \in (1 \dots P^{K}) \| (x \gcd P^{K} = 1 \land P ∥ (x - 0))\} = \emptyset \leftrightarrow \forall x \in (1 \dots P^{K}) \neg (x \gcd P^{K} = 1 \land P ∥ (x - 0))$
54	52 53	sylibr	$⊢ (P \in ℙ \land K \in ℕ) \to \{x \in (1 \dots P^{K}) \| (x \gcd P^{K} = 1 \land P ∥ (x - 0))\} = \emptyset$
55	26 54	syl5eq	$⊢ (P \in ℙ \land K \in ℕ) \to \{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\} \cap \{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\} = \emptyset$
56		hashun	$⊢ (\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\} \in Fin \land \{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\} \in Fin \land \{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\} \cap \{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\} = \emptyset) \to \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\} \cup \{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\}\| = \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\| + \|\{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\}\|$
57	22 25 55 56	mp3an12i	$⊢ (P \in ℙ \land K \in ℕ) \to \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\} \cup \{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\}\| = \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\| + \|\{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\}\|$
58		unrab	$⊢ \{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\} \cup \{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\} = \{x \in (1 \dots P^{K}) \| (x \gcd P^{K} = 1 \lor P ∥ (x - 0))\}$
59	48	biimprd	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in (1 \dots P^{K})) \to (\neg P ∥ (x - 0) \to x \gcd P^{K} = 1)$
60	59	con1d	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in (1 \dots P^{K})) \to (\neg x \gcd P^{K} = 1 \to P ∥ (x - 0))$
61	60	orrd	$⊢ ((P \in ℙ \land K \in ℕ) \land x \in (1 \dots P^{K})) \to (x \gcd P^{K} = 1 \lor P ∥ (x - 0))$
62	61	ralrimiva	$⊢ (P \in ℙ \land K \in ℕ) \to \forall x \in (1 \dots P^{K}) (x \gcd P^{K} = 1 \lor P ∥ (x - 0))$
63		rabid2	$⊢ (1 \dots P^{K}) = \{x \in (1 \dots P^{K}) \| (x \gcd P^{K} = 1 \lor P ∥ (x - 0))\} \leftrightarrow \forall x \in (1 \dots P^{K}) (x \gcd P^{K} = 1 \lor P ∥ (x - 0))$
64	62 63	sylibr	$⊢ (P \in ℙ \land K \in ℕ) \to (1 \dots P^{K}) = \{x \in (1 \dots P^{K}) \| (x \gcd P^{K} = 1 \lor P ∥ (x - 0))\}$
65	58 64	eqtr4id	$⊢ (P \in ℙ \land K \in ℕ) \to \{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\} \cup \{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\} = (1 \dots P^{K})$
66	65	fveq2d	$⊢ (P \in ℙ \land K \in ℕ) \to \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\} \cup \{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\}\| = \|(1 \dots P^{K})\|$
67	4	nnnn0d	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K} \in ℕ_{0}$
68		hashfz1	$⊢ P^{K} \in ℕ_{0} \to \|(1 \dots P^{K})\| = P^{K}$
69	67 68	syl	$⊢ (P \in ℙ \land K \in ℕ) \to \|(1 \dots P^{K})\| = P^{K}$
70		expm1t	$⊢ (P \in ℂ \land K \in ℕ) \to P^{K} = P^{K - 1} P$
71	11 70	sylan	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K} = P^{K - 1} P$
72	66 69 71	3eqtrd	$⊢ (P \in ℙ \land K \in ℕ) \to \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\} \cup \{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\}\| = P^{K - 1} P$
73	1	adantr	$⊢ (P \in ℙ \land K \in ℕ) \to P \in ℕ$
74		1zzd	$⊢ (P \in ℙ \land K \in ℕ) \to 1 \in ℤ$
75		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
76		1m1e0	$⊢ 1 - 1 = 0$
77	76	fveq2i	$⊢ ℤ_{\geq (1 - 1)} = ℤ_{\geq 0}$
78	75 77	eqtr4i	$⊢ ℕ_{0} = ℤ_{\geq (1 - 1)}$
79	67 78	eleqtrdi	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K} \in ℤ_{\geq (1 - 1)}$
80		0zd	$⊢ (P \in ℙ \land K \in ℕ) \to 0 \in ℤ$
81	73 74 79 80	hashdvds	$⊢ (P \in ℙ \land K \in ℕ) \to \|\{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\}\| = ⌊\frac{P^{K} - 0}{P}⌋ - ⌊\frac{1 - 1 - 0}{P}⌋$
82	4	nncnd	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K} \in ℂ$
83	82	subid1d	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K} - 0 = P^{K}$
84	83	oveq1d	$⊢ (P \in ℙ \land K \in ℕ) \to \frac{P^{K} - 0}{P} = \frac{P^{K}}{P}$
85	73	nnne0d	$⊢ (P \in ℙ \land K \in ℕ) \to P \neq 0$
86		nnz	$⊢ K \in ℕ \to K \in ℤ$
87	86	adantl	$⊢ (P \in ℙ \land K \in ℕ) \to K \in ℤ$
88	12 85 87	expm1d	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K - 1} = \frac{P^{K}}{P}$
89	84 88	eqtr4d	$⊢ (P \in ℙ \land K \in ℕ) \to \frac{P^{K} - 0}{P} = P^{K - 1}$
90	89	fveq2d	$⊢ (P \in ℙ \land K \in ℕ) \to ⌊\frac{P^{K} - 0}{P}⌋ = ⌊P^{K - 1}⌋$
91	9	nnzd	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K - 1} \in ℤ$
92		flid	$⊢ P^{K - 1} \in ℤ \to ⌊P^{K - 1}⌋ = P^{K - 1}$
93	91 92	syl	$⊢ (P \in ℙ \land K \in ℕ) \to ⌊P^{K - 1}⌋ = P^{K - 1}$
94	90 93	eqtrd	$⊢ (P \in ℙ \land K \in ℕ) \to ⌊\frac{P^{K} - 0}{P}⌋ = P^{K - 1}$
95	76	oveq1i	$⊢ 1 - 1 - 0 = 0 - 0$
96		0m0e0	$⊢ 0 - 0 = 0$
97	95 96	eqtri	$⊢ 1 - 1 - 0 = 0$
98	97	oveq1i	$⊢ \frac{1 - 1 - 0}{P} = \frac{0}{P}$
99	12 85	div0d	$⊢ (P \in ℙ \land K \in ℕ) \to \frac{0}{P} = 0$
100	98 99	syl5eq	$⊢ (P \in ℙ \land K \in ℕ) \to \frac{1 - 1 - 0}{P} = 0$
101	100	fveq2d	$⊢ (P \in ℙ \land K \in ℕ) \to ⌊\frac{1 - 1 - 0}{P}⌋ = ⌊0⌋$
102		0z	$⊢ 0 \in ℤ$
103		flid	$⊢ 0 \in ℤ \to ⌊0⌋ = 0$
104	102 103	ax-mp	$⊢ ⌊0⌋ = 0$
105	101 104	eqtrdi	$⊢ (P \in ℙ \land K \in ℕ) \to ⌊\frac{1 - 1 - 0}{P}⌋ = 0$
106	94 105	oveq12d	$⊢ (P \in ℙ \land K \in ℕ) \to ⌊\frac{P^{K} - 0}{P}⌋ - ⌊\frac{1 - 1 - 0}{P}⌋ = P^{K - 1} - 0$
107	10	subid1d	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K - 1} - 0 = P^{K - 1}$
108	81 106 107	3eqtrd	$⊢ (P \in ℙ \land K \in ℕ) \to \|\{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\}\| = P^{K - 1}$
109	108	oveq2d	$⊢ (P \in ℙ \land K \in ℕ) \to \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\| + \|\{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\}\| = \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\| + P^{K - 1}$
110		hashcl	$⊢ \{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\} \in Fin \to \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\| \in ℕ_{0}$
111	22 110	ax-mp	$⊢ \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\| \in ℕ_{0}$
112	111	nn0cni	$⊢ \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\| \in ℂ$
113		addcom	$⊢ (\|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\| \in ℂ \land P^{K - 1} \in ℂ) \to \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\| + P^{K - 1} = P^{K - 1} + \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\|$
114	112 10 113	sylancr	$⊢ (P \in ℙ \land K \in ℕ) \to \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\| + P^{K - 1} = P^{K - 1} + \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\|$
115	109 114	eqtrd	$⊢ (P \in ℙ \land K \in ℕ) \to \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\| + \|\{x \in (1 \dots P^{K}) \| P ∥ (x - 0)\}\| = P^{K - 1} + \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\|$
116	57 72 115	3eqtr3rd	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K - 1} + \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\| = P^{K - 1} P$
117	10 12	mulcld	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K - 1} P \in ℂ$
118	112	a1i	$⊢ (P \in ℙ \land K \in ℕ) \to \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\| \in ℂ$
119	117 10 118	subaddd	$⊢ (P \in ℙ \land K \in ℕ) \to (P^{K - 1} P - P^{K - 1} = \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\| \leftrightarrow P^{K - 1} + \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\| = P^{K - 1} P)$
120	116 119	mpbird	$⊢ (P \in ℙ \land K \in ℕ) \to P^{K - 1} P - P^{K - 1} = \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\|$
121	16 18 120	3eqtrrd	$⊢ (P \in ℙ \land K \in ℕ) \to \|\{x \in (1 \dots P^{K}) \| x \gcd P^{K} = 1\}\| = P^{K - 1} (P - 1)$
122	6 121	eqtrd	$⊢ (P \in ℙ \land K \in ℕ) \to ϕ (P^{K}) = P^{K - 1} (P - 1)$

Metamath Proof Explorer

Theorem phiprmpw

Proof