Theorem phiprmpw 16915

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 16812	. . . 4 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2		nnnn0 12583	. . . 4 ⊢ (𝐾 ∈ ℕ → 𝐾 ∈ ℕ0)
3		nnexpcl 14186	. . . 4 ⊢ ((𝑃 ∈ ℕ ∧ 𝐾 ∈ ℕ0) → (𝑃↑𝐾) ∈ ℕ)
4	1, 2, 3	syl2an 608	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℕ)
5		phival 16906	. . 3 ⊢ ((𝑃↑𝐾) ∈ ℕ → (ϕ‘(𝑃↑𝐾)) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}))
6	4, 5	syl 18	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (ϕ‘(𝑃↑𝐾)) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}))
7		nnm1nn0 12617	. . . . . 6 ⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈ ℕ0)
8		nnexpcl 14186	. . . . . 6 ⊢ ((𝑃 ∈ ℕ ∧ (𝐾 − 1) ∈ ℕ0) → (𝑃↑(𝐾 − 1)) ∈ ℕ)
9	1, 7, 8	syl2an 608	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈ ℕ)
10	9	nncnd 12321	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈ ℂ)
11	1	nncnd 12321	. . . . 5 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℂ)
12	11	adantr 486	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 ∈ ℂ)
13		ax-1cn 11230	. . . . 5 ⊢ 1 ∈ ℂ
14		subdi 11719	. . . . 5 ⊢ (((𝑃↑(𝐾 − 1)) ∈ ℂ ∧ 𝑃 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1)))
15	13, 14	mp3an3 1479	. . . 4 ⊢ (((𝑃↑(𝐾 − 1)) ∈ ℂ ∧ 𝑃 ∈ ℂ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1)))
16	10, 12, 15	syl2anc 596	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1)))
17	10	mulridd 11298	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · 1) = (𝑃↑(𝐾 − 1)))
18	17	oveq2d 7424	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑(𝐾 − 1)) · 𝑃) − ((𝑃↑(𝐾 − 1)) · 1)) = (((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1))))
19		fzfi 14084	. . . . . . 7 ⊢ (1...(𝑃↑𝐾)) ∈ Fin
20		ssrab2 4027	. . . . . . 7 ⊢ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ⊆ (1...(𝑃↑𝐾))
21		ssfi 9166	. . . . . . 7 ⊢ (((1...(𝑃↑𝐾)) ∈ Fin ∧ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ⊆ (1...(𝑃↑𝐾))) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin)
22	19, 20, 21	mp2an 705	. . . . . 6 ⊢ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin
23		ssrab2 4027	. . . . . . 7 ⊢ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ⊆ (1...(𝑃↑𝐾))
24		ssfi 9166	. . . . . . 7 ⊢ (((1...(𝑃↑𝐾)) ∈ Fin ∧ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ⊆ (1...(𝑃↑𝐾))) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ∈ Fin)
25	19, 23, 24	mp2an 705	. . . . . 6 ⊢ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ∈ Fin
26		inrab 4261	. . . . . . 7 ⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∩ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))}
27		elfzelz 13626	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (1...(𝑃↑𝐾)) → 𝑥 ∈ ℤ)
28		prmz 16813	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
29		rpexp 16861	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1))
30	28, 29	syl3an1 1181	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1))
31	30	3expa 1136	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1))
32	31	an32s 665	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (((𝑃↑𝐾) gcd 𝑥) = 1 ↔ (𝑃 gcd 𝑥) = 1))
33		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℤ)
34		zexpcl 14188	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ ℤ ∧ 𝐾 ∈ ℕ0) → (𝑃↑𝐾) ∈ ℤ)
35	28, 2, 34	syl2an 608	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℤ)
36	35	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑃↑𝐾) ∈ ℤ)
37	33, 36	gcdcomd 16652	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 gcd (𝑃↑𝐾)) = ((𝑃↑𝐾) gcd 𝑥))
38	37	eqeq1d 2762	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ((𝑃↑𝐾) gcd 𝑥) = 1))
39		coprm 16850	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ) → (¬ 𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1))
40	39	adantlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (¬ 𝑃 ∥ 𝑥 ↔ (𝑃 gcd 𝑥) = 1))
41	32, 38, 40	3bitr4d 314	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ 𝑥))
42		zcn 12668	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℂ)
43	42	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℂ)
44	43	subid1d 11630	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑥 − 0) = 𝑥)
45	44	breq2d 5114	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (𝑃 ∥ (𝑥 − 0) ↔ 𝑃 ∥ 𝑥))
46	45	notbid 321	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → (¬ 𝑃 ∥ (𝑥 − 0) ↔ ¬ 𝑃 ∥ 𝑥))
47	41, 46	bitr4d 285	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ (𝑥 − 0)))
48	27, 47	sylan2 605	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ↔ ¬ 𝑃 ∥ (𝑥 − 0)))
49	48	biimpd 232	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 → ¬ 𝑃 ∥ (𝑥 − 0)))
50		imnan 405	. . . . . . . . . 10 ⊢ (((𝑥 gcd (𝑃↑𝐾)) = 1 → ¬ 𝑃 ∥ (𝑥 − 0)) ↔ ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0)))
51	49, 50	sylib 221	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0)))
52	51	ralrimiva 3154	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ∀𝑥 ∈ (1...(𝑃↑𝐾)) ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0)))
53		rabeq0 4337	. . . . . . . 8 ⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))} = ∅ ↔ ∀𝑥 ∈ (1...(𝑃↑𝐾)) ¬ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0)))
54	52, 53	sylibr 237	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∧ 𝑃 ∥ (𝑥 − 0))} = ∅)
55	26, 54	eqtrid 2807	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∩ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = ∅)
56		hashun 14494	. . . . . 6 ⊢ (({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin ∧ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)} ∈ Fin ∧ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∩ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = ∅) → (♯‘({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})))
57	22, 25, 55, 56	mp3an12i 1494	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (♯‘({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})))
58		unrab 4260	. . . . . . . 8 ⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))}
59	48	biimprd 251	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (¬ 𝑃 ∥ (𝑥 − 0) → (𝑥 gcd (𝑃↑𝐾)) = 1))
60	59	con1d 146	. . . . . . . . . . 11 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → (¬ (𝑥 gcd (𝑃↑𝐾)) = 1 → 𝑃 ∥ (𝑥 − 0)))
61	60	orrd 877	. . . . . . . . . 10 ⊢ (((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑃↑𝐾))) → ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0)))
62	61	ralrimiva 3154	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ∀𝑥 ∈ (1...(𝑃↑𝐾))((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0)))
63		rabid2 3444	. . . . . . . . 9 ⊢ ((1...(𝑃↑𝐾)) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))} ↔ ∀𝑥 ∈ (1...(𝑃↑𝐾))((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0)))
64	62, 63	sylibr 237	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (1...(𝑃↑𝐾)) = {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ ((𝑥 gcd (𝑃↑𝐾)) = 1 ∨ 𝑃 ∥ (𝑥 − 0))})
65	58, 64	eqtr4id 2814	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = (1...(𝑃↑𝐾)))
66	65	fveq2d 6877	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (♯‘({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = (♯‘(1...(𝑃↑𝐾))))
67	4	nnnn0d 12637	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℕ0)
68		hashfz1 14458	. . . . . . 7 ⊢ ((𝑃↑𝐾) ∈ ℕ0 → (♯‘(1...(𝑃↑𝐾))) = (𝑃↑𝐾))
69	67, 68	syl 18	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (♯‘(1...(𝑃↑𝐾))) = (𝑃↑𝐾))
70		expm1t 14202	. . . . . . 7 ⊢ ((𝑃 ∈ ℂ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) = ((𝑃↑(𝐾 − 1)) · 𝑃))
71	11, 70	sylan 592	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) = ((𝑃↑(𝐾 − 1)) · 𝑃))
72	66, 69, 71	3eqtrd 2799	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (♯‘({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∪ {𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((𝑃↑(𝐾 − 1)) · 𝑃))
73	1	adantr 486	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 ∈ ℕ)
74		1zzd 12697	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 1 ∈ ℤ)
75		nn0uz 12973	. . . . . . . . . . 11 ⊢ ℕ0 = (ℤ≥‘0)
76		1m1e0 12385	. . . . . . . . . . . 12 ⊢ (1 − 1) = 0
77	76	fveq2i 6876	. . . . . . . . . . 11 ⊢ (ℤ≥‘(1 − 1)) = (ℤ≥‘0)
78	75, 77	eqtr4i 2786	. . . . . . . . . 10 ⊢ ℕ0 = (ℤ≥‘(1 − 1))
79	67, 78	eleqtrdi 2870	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ (ℤ≥‘(1 − 1)))
80		0zd 12675	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 0 ∈ ℤ)
81	73, 74, 79, 80	hashdvds 16914	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = ((⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) − (⌊‘(((1 − 1) − 0) / 𝑃))))
82	4	nncnd 12321	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑𝐾) ∈ ℂ)
83	82	subid1d 11630	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑𝐾) − 0) = (𝑃↑𝐾))
84	83	oveq1d 7423	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) − 0) / 𝑃) = ((𝑃↑𝐾) / 𝑃))
85	73	nnne0d 12358	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝑃 ≠ 0)
86		nnz 12684	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ ℕ → 𝐾 ∈ ℤ)
87	86	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → 𝐾 ∈ ℤ)
88	12, 85, 87	expm1d 14268	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) = ((𝑃↑𝐾) / 𝑃))
89	84, 88	eqtr4d 2798	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑𝐾) − 0) / 𝑃) = (𝑃↑(𝐾 − 1)))
90	89	fveq2d 6877	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) = (⌊‘(𝑃↑(𝐾 − 1))))
91	9	nnzd 12689	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (𝑃↑(𝐾 − 1)) ∈ ℤ)
92		flid 13917	. . . . . . . . . . 11 ⊢ ((𝑃↑(𝐾 − 1)) ∈ ℤ → (⌊‘(𝑃↑(𝐾 − 1))) = (𝑃↑(𝐾 − 1)))
93	91, 92	syl 18	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (⌊‘(𝑃↑(𝐾 − 1))) = (𝑃↑(𝐾 − 1)))
94	90, 93	eqtrd 2795	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) = (𝑃↑(𝐾 − 1)))
95	76	oveq1i 7418	. . . . . . . . . . . . . 14 ⊢ ((1 − 1) − 0) = (0 − 0)
96		0m0e0 12431	. . . . . . . . . . . . . 14 ⊢ (0 − 0) = 0
97	95, 96	eqtri 2783	. . . . . . . . . . . . 13 ⊢ ((1 − 1) − 0) = 0
98	97	oveq1i 7418	. . . . . . . . . . . 12 ⊢ (((1 − 1) − 0) / 𝑃) = (0 / 𝑃)
99	12, 85	div0d 12062	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (0 / 𝑃) = 0)
100	98, 99	eqtrid 2807	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((1 − 1) − 0) / 𝑃) = 0)
101	100	fveq2d 6877	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (⌊‘(((1 − 1) − 0) / 𝑃)) = (⌊‘0))
102		0z 12674	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
103		flid 13917	. . . . . . . . . . 11 ⊢ (0 ∈ ℤ → (⌊‘0) = 0)
104	102, 103	ax-mp 5	. . . . . . . . . 10 ⊢ (⌊‘0) = 0
105	101, 104	eqtrdi 2811	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (⌊‘(((1 − 1) − 0) / 𝑃)) = 0)
106	94, 105	oveq12d 7426	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((⌊‘(((𝑃↑𝐾) − 0) / 𝑃)) − (⌊‘(((1 − 1) − 0) / 𝑃))) = ((𝑃↑(𝐾 − 1)) − 0))
107	10	subid1d 11630	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) − 0) = (𝑃↑(𝐾 − 1)))
108	81, 106, 107	3eqtrd 2799	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)}) = (𝑃↑(𝐾 − 1)))
109	108	oveq2d 7424	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (𝑃↑(𝐾 − 1))))
110		hashcl 14468	. . . . . . . . 9 ⊢ ({𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1} ∈ Fin → (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℕ0)
111	22, 110	ax-mp 5	. . . . . . . 8 ⊢ (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℕ0
112	111	nn0cni 12588	. . . . . . 7 ⊢ (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℂ
113		addcom 11468	. . . . . . 7 ⊢ (((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℂ ∧ (𝑃↑(𝐾 − 1)) ∈ ℂ) → ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (𝑃↑(𝐾 − 1))) = ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})))
114	112, 10, 113	sylancr 599	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (𝑃↑(𝐾 − 1))) = ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})))
115	109, 114	eqtrd 2795	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ 𝑃 ∥ (𝑥 − 0)})) = ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})))
116	57, 72, 115	3eqtr3rd 2804	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) = ((𝑃↑(𝐾 − 1)) · 𝑃))
117	10, 12	mulcld 11301	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((𝑃↑(𝐾 − 1)) · 𝑃) ∈ ℂ)
118	112	a1i 11	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ∈ ℂ)
119	117, 10, 118	subaddd 11659	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → ((((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1))) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) ↔ ((𝑃↑(𝐾 − 1)) + (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1})) = ((𝑃↑(𝐾 − 1)) · 𝑃)))
120	116, 119	mpbird 260	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (((𝑃↑(𝐾 − 1)) · 𝑃) − (𝑃↑(𝐾 − 1))) = (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}))
121	16, 18, 120	3eqtrrd 2800	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (♯‘{𝑥 ∈ (1...(𝑃↑𝐾)) ∣ (𝑥 gcd (𝑃↑𝐾)) = 1}) = ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)))
122	6, 121	eqtrd 2795	1 ⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (ϕ‘(𝑃↑𝐾)) = ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145  ∀wral 3076  {crab 3412   ∪ cun 3896   ∩ cin 3897   ⊆ wss 3898  ∅c0 4278   class class class wbr 5102  ‘cfv 6527  (class class class)co 7408  Fincfn 8951  ℂcc 11170  0cc0 11172  1c1 11173   + caddc 11175   · cmul 11177   − cmin 11513   / cdiv 11943  ℕcn 12305  ℕ₀cn0 12576  ℤcz 12663  ℤ_≥cuz 12935  ...cfz 13609  ⌊cfl 13899  ↑cexp 14173  ♯chash 14442   ∥ cdvds 16390   gcd cgcd 16632  ℙcprime 16809  ϕcphi 16903

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-cnex 11228  ax-resscn 11229  ax-1cn 11230  ax-icn 11231  ax-addcl 11232  ax-addrcl 11233  ax-mulcl 11234  ax-mulrcl 11235  ax-mulcom 11236  ax-addass 11237  ax-mulass 11238  ax-distr 11239  ax-i2m1 11240  ax-1ne0 11241  ax-1rid 11242  ax-rnegex 11243  ax-rrecex 11244  ax-cnre 11245  ax-pre-lttri 11246  ax-pre-lttrn 11247  ax-pre-ltadd 11248  ax-pre-mulgt0 11249  ax-pre-sup 11250

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6293  df-ord 6354  df-on 6355  df-lim 6356  df-suc 6357  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7861  df-1st 7984  df-2nd 7985  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-1o 8454  df-2o 8455  df-oadd 8458  df-er 8695  df-en 8952  df-dom 8953  df-sdom 8954  df-fin 8955  df-sup 9412  df-inf 9413  df-dju 9954  df-card 9992  df-pnf 11317  df-mnf 11318  df-xr 11319  df-ltxr 11320  df-le 11321  df-sub 11515  df-neg 11516  df-div 11944  df-nn 12306  df-2 12375  df-3 12376  df-n0 12577  df-z 12664  df-uz 12936  df-rp 13091  df-fz 13610  df-fl 13901  df-mod 13979  df-seq 14114  df-exp 14174  df-hash 14443  df-cj 15234  df-re 15235  df-im 15236  df-sqrt 15370  df-abs 15371  df-dvds 16391  df-gcd 16633  df-prm 16810  df-phi 16905

This theorem is used by:  phiprm  16916