Theorem phiprmpw 11887

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

Assertion

Ref	Expression
phiprmpw	⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (ϕ‘(𝑃↑𝐾)) = ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)))

Proof of Theorem phiprmpw

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		prmnn 11780	. . . 4 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2		nnnn0 8977	. . . 4 ⊢ (𝐾 ∈ ℕ → 𝐾 ∈ ℕ0)
3		nnexpcl 10299	. . . 4 ⊢ ((𝑃 ∈ ℕ ∧ 𝐾 ∈ ℕ0) → (𝑃↑𝐾) ∈ ℕ)
4	1, 2, 3	syl2an 287	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℕ)
5		phival 11878	. . 3 ⊢ ((𝑃↑𝐾) ∈ ℕ → (ϕ‘(𝑃↑𝐾)) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}))
6	4, 5	syl 14	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (ϕ‘(𝑃↑𝐾)) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}))
7		nnm1nn0 9011	. . . . . 6 ⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈ ℕ0)
8		nnexpcl 10299	. . . . . 6 ⊢ ((𝑃 ∈ ℕ ∧ (𝐾 − 1) ∈ ℕ0) → (𝑃↑(𝐾 − 1)) ∈ ℕ)
9	1, 7, 8	syl2an 287	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈ ℕ)
10	9	nncnd 8727	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈ ℂ)
11	1	nncnd 8727	. . . . 5 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℂ)
12	11	adantr 274	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 ∈ ℂ)
13		ax-1cn 7706	. . . . 5 ⊢ 1 ∈ ℂ
14		subdi 8140	. . . . 5 ⊢ (((𝑃↑(𝐾 − 1)) ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1)))
15	13, 14	mp3an3 1304	. . . 4 ⊢ (((𝑃↑(𝐾 − 1)) ∈ ℂ ∧ 𝑃 ∈ ℂ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1)))
16	10, 12, 15	syl2anc 408	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1)))
17	10	mulid1d 7776	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · 1) = (𝑃↑(𝐾 − 1)))
18	17	oveq2d 5783	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1))))
19		phivalfi 11877	. . . . . . 7 ⊢ ((𝑃↑𝐾) ∈ ℕ → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin)
20	4, 19	syl 14	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin)
21		1zzd 9074	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 1 ∈ ℤ)
22		prmz 11781	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
23		zexpcl 10301	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℤ ∧ 𝐾 ∈ ℕ0) → (𝑃↑𝐾) ∈ ℤ)
24	22, 2, 23	syl2an 287	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℤ)
25	21, 24	fzfigd 10197	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (1...(𝑃↑𝐾)) ∈ Fin)
26	22	ad2antrr 479	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → 𝑃 ∈ ℤ)
27		elfzelz 9799	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...(𝑃↑𝐾)) → 𝑥 ∈ ℤ)
28	27	adantl 275	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → 𝑥 ∈ ℤ)
29		0zd 9059	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → 0 ∈ ℤ)
30	28, 29	zsubcld 9171	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (𝑥 − 0) ∈ ℤ)
31		zdvdsdc 11503	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℤ ∧ (𝑥 − 0) ∈ ℤ) → DECID 𝑃 ∥ (𝑥 − 0))
32	26, 30, 31	syl2anc 408	. . . . . . . 8 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → DECID 𝑃 ∥ (𝑥 − 0))
33	32	ralrimiva 2503	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ∀𝑥 ∈ (1...(𝑃↑𝐾))DECID 𝑃 ∥ (𝑥 − 0))
34	25, 33	ssfirab 6815	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ∈ Fin)
35		inrab 3343	. . . . . . 7 ⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∩ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))}
36		rpexp 11820	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1))
37	22, 36	syl3an1 1249	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1))
38	37	3expa 1181	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1))
39	38	an32s 557	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1))
40		simpr 109	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℤ)
41	24	adantr 274	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑃↑𝐾) ∈ ℤ)
42		gcdcom 11651	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℤ ∧ (𝑃↑𝐾) ∈ ℤ) → (𝑥 gcd (𝑃↑𝐾)) = ((𝑃↑𝐾) gcd 𝑥))
43	40, 41, 42	syl2anc 408	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 gcd (𝑃↑𝐾)) = ((𝑃↑𝐾) gcd 𝑥))
44	43	eqeq1d 2146	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ((𝑃↑𝐾) gcd 𝑥) = 1))
45		coprm 11811	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) → (¬ 𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1))
46	45	adantlr 468	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (¬ 𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1))
47	39, 44, 46	3bitr4d 219	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ 𝑥))
48		zcn 9052	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℂ)
49	48	adantl 275	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℂ)
50	49	subid1d 8055	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 − 0) = 𝑥)
51	50	breq2d 3936	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑃 ∥ (𝑥 − 0) ↔ 𝑃 ∥ 𝑥))
52	51	notbid 656	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (¬ 𝑃 ∥ (𝑥 − 0) ↔ ¬ 𝑃 ∥ 𝑥))
53	47, 52	bitr4d 190	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ (𝑥 − 0)))
54	27, 53	sylan2 284	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ (𝑥 − 0)))
55	54	biimpd 143	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 → ¬ 𝑃 ∥ (𝑥 − 0)))
56		imnan 679	. . . . . . . . . 10 ⊢ (((𝑥 gcd (𝑃↑𝐾)) = 1 → ¬ 𝑃 ∥ (𝑥 − 0)) ↔ ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0)))
57	55, 56	sylib 121	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0)))
58	57	ralrimiva 2503	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ∀𝑥 ∈ (1...(𝑃↑𝐾)) ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0)))
59		rabeq0 3387	. . . . . . . 8 ⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))} = ∅ ↔ ∀𝑥 ∈ (1...(𝑃↑𝐾)) ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0)))
60	58, 59	sylibr 133	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))} = ∅)
61	35, 60	syl5eq 2182	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∩ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = ∅)
62		hashun 10544	. . . . . 6 ⊢ (({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin ∧ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ∈ Fin ∧ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∩ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = ∅) → (♯‘({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})))
63	20, 34, 61, 62	syl3anc 1216	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (♯‘({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})))
64	54	biimprd 157	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (¬ 𝑃 ∥ (𝑥 − 0) → (𝑥 gcd (𝑃↑𝐾)) = 1))
65		con1dc 841	. . . . . . . . . . . 12 ⊢ (DECID 𝑃 ∥ (𝑥 − 0) → ((¬ 𝑃 ∥ (𝑥 − 0) → (𝑥 gcd (𝑃↑𝐾)) = 1) → (¬ (𝑥 gcd (𝑃↑𝐾)) = 1 → 𝑃 ∥ (𝑥 − 0))))
66	32, 64, 65	sylc 62	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (¬ (𝑥 gcd (𝑃↑𝐾)) = 1 → 𝑃 ∥ (𝑥 − 0)))
67	24	adantr 274	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (𝑃↑𝐾) ∈ ℤ)
68	28, 67	gcdcld 11646	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (𝑥 gcd (𝑃↑𝐾)) ∈ ℕ0)
69	68	nn0zd 9164	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (𝑥 gcd (𝑃↑𝐾)) ∈ ℤ)
70		1zzd 9074	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → 1 ∈ ℤ)
71		zdceq 9119	. . . . . . . . . . . . 13 ⊢ (((𝑥 gcd (𝑃↑𝐾)) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑥 gcd (𝑃↑𝐾)) = 1)
72	69, 70, 71	syl2anc 408	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → DECID (𝑥 gcd (𝑃↑𝐾)) = 1)
73		dfordc 877	. . . . . . . . . . . 12 ⊢ (DECID (𝑥 gcd (𝑃↑𝐾)) = 1 → (((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0)) ↔ (¬ (𝑥 gcd (𝑃↑𝐾)) = 1 → 𝑃 ∥ (𝑥 − 0))))
74	72, 73	syl 14	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0)) ↔ (¬ (𝑥 gcd (𝑃↑𝐾)) = 1 → 𝑃 ∥ (𝑥 − 0))))
75	66, 74	mpbird 166	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0)))
76	75	ralrimiva 2503	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ∀𝑥 ∈ (1...(𝑃↑𝐾))((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0)))
77		rabid2 2605	. . . . . . . . 9 ⊢ ((1...(𝑃↑𝐾)) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))} ↔ ∀𝑥 ∈ (1...(𝑃↑𝐾))((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0)))
78	76, 77	sylibr 133	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (1...(𝑃↑𝐾)) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))})
79		unrab 3342	. . . . . . . 8 ⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))}
80	78, 79	syl6reqr 2189	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = (1...(𝑃↑𝐾)))
81	80	fveq2d 5418	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (♯‘({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = (♯‘(1...(𝑃↑𝐾))))
82	4	nnnn0d 9023	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℕ0)
83		hashfz1 10522	. . . . . . 7 ⊢ ((𝑃↑𝐾) ∈ ℕ0 → (♯‘(1...(𝑃↑𝐾))) = (𝑃↑𝐾))
84	82, 83	syl 14	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (♯‘(1...(𝑃↑𝐾))) = (𝑃↑𝐾))
85		expm1t 10314	. . . . . . 7 ⊢ ((𝑃 ∈ ℂ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) = ((𝑃↑(𝐾 − 1)) · 𝑃))
86	11, 85	sylan 281	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) = ((𝑃↑(𝐾 − 1)) · 𝑃))
87	81, 84, 86	3eqtrd 2174	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (♯‘({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((𝑃↑(𝐾 − 1)) · 𝑃))
88		hashcl 10520	. . . . . . . 8 ⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin → (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℕ0)
89	20, 88	syl 14	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℕ0)
90	89	nn0cnd 9025	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℂ)
91	1	adantr 274	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 ∈ ℕ)
92		nn0uz 9353	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
93		1m1e0 8782	. . . . . . . . . . . 12 ⊢ (1 − 1) = 0
94	93	fveq2i 5417	. . . . . . . . . . 11 ⊢ (ℤ≥‘(1 − 1)) = (ℤ≥‘0)
95	92, 94	eqtr4i 2161	. . . . . . . . . 10 ⊢ ℕ0 = (ℤ≥‘(1 − 1))
96	82, 95	eleqtrdi 2230	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ (ℤ≥‘(1 − 1)))
97		0zd 9059	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 0 ∈ ℤ)
98	91, 21, 96, 97	hashdvds 11886	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = ((⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) − (⌊‘(((1 − 1) − 0) / 𝑃))))
99	4	nncnd 8727	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℂ)
100	99	subid1d 8055	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑𝐾) − 0) = (𝑃↑𝐾))
101	100	oveq1d 5782	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) − 0) / 𝑃) = ((𝑃↑𝐾) / 𝑃))
102	91	nnap0d 8759	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 # 0)
103		nnz 9066	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ ℕ → 𝐾 ∈ ℤ)
104	103	adantl 275	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝐾 ∈ ℤ)
105	12, 102, 104	expm1apd 10427	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) = ((𝑃↑𝐾) / 𝑃))
106	101, 105	eqtr4d 2173	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) − 0) / 𝑃) = (𝑃↑(𝐾 − 1)))
107	106	fveq2d 5418	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) = (⌊‘(𝑃↑(𝐾 − 1))))
108	9	nnzd 9165	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈ ℤ)
109		flid 10050	. . . . . . . . . . 11 ⊢ ((𝑃↑(𝐾 − 1)) ∈ ℤ → (⌊‘(𝑃↑(𝐾 − 1))) = (𝑃↑(𝐾 − 1)))
110	108, 109	syl 14	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (⌊‘(𝑃↑(𝐾 − 1))) = (𝑃↑(𝐾 − 1)))
111	107, 110	eqtrd 2170	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) = (𝑃↑(𝐾 − 1)))
112	93	oveq1i 5777	. . . . . . . . . . . . . 14 ⊢ ((1 − 1) − 0) = (0 − 0)
113		0m0e0 8825	. . . . . . . . . . . . . 14 ⊢ (0 − 0) = 0
114	112, 113	eqtri 2158	. . . . . . . . . . . . 13 ⊢ ((1 − 1) − 0) = 0
115	114	oveq1i 5777	. . . . . . . . . . . 12 ⊢ (((1 − 1) − 0) / 𝑃) = (0 / 𝑃)
116	12, 102	div0apd 8540	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (0 / 𝑃) = 0)
117	115, 116	syl5eq 2182	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((1 − 1) − 0) / 𝑃) = 0)
118	117	fveq2d 5418	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (⌊‘(((1 − 1) − 0) / 𝑃)) = (⌊‘0))
119		0z 9058	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
120		flid 10050	. . . . . . . . . . 11 ⊢ (0 ∈ ℤ → (⌊‘0) = 0)
121	119, 120	ax-mp 5	. . . . . . . . . 10 ⊢ (⌊‘0) = 0
122	118, 121	syl6eq 2186	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (⌊‘(((1 − 1) − 0) / 𝑃)) = 0)
123	111, 122	oveq12d 5785	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) − (⌊‘(((1 − 1) − 0) / 𝑃))) = ((𝑃↑(𝐾 − 1)) − 0))
124	10	subid1d 8055	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) − 0) = (𝑃↑(𝐾 − 1)))
125	98, 123, 124	3eqtrd 2174	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = (𝑃↑(𝐾 − 1)))
126	125	oveq2d 5783	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (𝑃↑(𝐾 − 1))))
127	90, 10, 126	comraddd 7912	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})))
128	63, 87, 127	3eqtr3rd 2179	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) = ((𝑃↑(𝐾 − 1)) · 𝑃))
129	10, 12	mulcld 7779	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · 𝑃) ∈ ℂ)
130	129, 10, 90	subaddd 8084	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1))) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ↔ ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) = ((𝑃↑(𝐾 − 1)) · 𝑃)))
131	128, 130	mpbird 166	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1))) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}))
132	16, 18, 131	3eqtrrd 2175	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) = ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)))
133	6, 132	eqtrd 2170	1 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (ϕ‘(𝑃↑𝐾)) = ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 697  DECID wdc 819   = wceq 1331   ∈ wcel 1480  ∀wral 2414  {crab 2418   ∪ cun 3064   ∩ cin 3065  ∅c0 3358   class class class wbr 3924  ‘cfv 5118  (class class class)co 5767  Fincfn 6627  ℂcc 7611  0cc0 7613  1c1 7614   + caddc 7616   · cmul 7618   − cmin 7926   / cdiv 8425  ℕcn 8713  ℕ₀cn0 8970  ℤcz 9047  ℤ_≥cuz 9319  ...cfz 9783  ⌊cfl 10034  ↑cexp 10285  ♯chash 10514   ∥ cdvds 11482   gcd cgcd 11624  ℙcprime 11777  ϕcphi 11875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-coll 4038  ax-sep 4041  ax-nul 4049  ax-pow 4093  ax-pr 4126  ax-un 4350  ax-setind 4447  ax-iinf 4497  ax-cnex 7704  ax-resscn 7705  ax-1cn 7706  ax-1re 7707  ax-icn 7708  ax-addcl 7709  ax-addrcl 7710  ax-mulcl 7711  ax-mulrcl 7712  ax-addcom 7713  ax-mulcom 7714  ax-addass 7715  ax-mulass 7716  ax-distr 7717  ax-i2m1 7718  ax-0lt1 7719  ax-1rid 7720  ax-0id 7721  ax-rnegex 7722  ax-precex 7723  ax-cnre 7724  ax-pre-ltirr 7725  ax-pre-ltwlin 7726  ax-pre-lttrn 7727  ax-pre-apti 7728  ax-pre-ltadd 7729  ax-pre-mulgt0 7730  ax-pre-mulext 7731  ax-arch 7732  ax-caucvg 7733

This theorem depends on definitions:  df-bi 116  df-stab 816  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2000  df-mo 2001  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ne 2307  df-nel 2402  df-ral 2419  df-rex 2420  df-reu 2421  df-rmo 2422  df-rab 2423  df-v 2683  df-sbc 2905  df-csb 2999  df-dif 3068  df-un 3070  df-in 3072  df-ss 3079  df-nul 3359  df-if 3470  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-int 3767  df-iun 3810  df-br 3925  df-opab 3985  df-mpt 3986  df-tr 4022  df-id 4210  df-po 4213  df-iso 4214  df-iord 4283  df-on 4285  df-ilim 4286  df-suc 4288  df-iom 4500  df-xp 4540  df-rel 4541  df-cnv 4542  df-co 4543  df-dm 4544  df-rn 4545  df-res 4546  df-ima 4547  df-iota 5083  df-fun 5120  df-fn 5121  df-f 5122  df-f1 5123  df-fo 5124  df-f1o 5125  df-fv 5126  df-riota 5723  df-ov 5770  df-oprab 5771  df-mpo 5772  df-1st 6031  df-2nd 6032  df-recs 6195  df-irdg 6260  df-frec 6281  df-1o 6306  df-2o 6307  df-oadd 6310  df-er 6422  df-en 6628  df-dom 6629  df-fin 6630  df-sup 6864  df-pnf 7795  df-mnf 7796  df-xr 7797  df-ltxr 7798  df-le 7799  df-sub 7928  df-neg 7929  df-reap 8330  df-ap 8337  df-div 8426  df-inn 8714  df-2 8772  df-3 8773  df-4 8774  df-n0 8971  df-z 9048  df-uz 9320  df-q 9405  df-rp 9435  df-fz 9784  df-fzo 9913  df-fl 10036  df-mod 10089  df-seqfrec 10212  df-exp 10286  df-ihash 10515  df-cj 10607  df-re 10608  df-im 10609  df-rsqrt 10763  df-abs 10764  df-dvds 11483  df-gcd 11625  df-prm 11778  df-phi 11876

This theorem is referenced by:  phiprm  11888