Theorem phiprmpw 13023

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.)

Assertion

Ref	Expression
phiprmpw	|- ( ( P e. Prime /\ K e. NN ) -> ( phi ` ( P ^ K ) ) = ( ( P ^ ( K - 1 ) ) x. ( P - 1 ) ) )

Proof of Theorem phiprmpw

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		prmnn 12907	. . . 4 |- ( P e. Prime -> P e. NN )
2		nnnn0 9575	. . . 4 |- ( K e. NN -> K e. NN0 )
3		nnexpcl 11004	. . . 4 |- ( ( P e. NN /\ K e. NN0 ) -> ( P ^ K ) e. NN )
4	1, 2, 3	syl2an 289	. . 3 |- ( ( P e. Prime /\ K e. NN ) -> ( P ^ K ) e. NN )
5		phival 13014	. . 3 |- ( ( P ^ K ) e. NN -> ( phi ` ( P ^ K ) ) = (♯ ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) )
6	4, 5	syl 14	. 2 |- ( ( P e. Prime /\ K e. NN ) -> ( phi ` ( P ^ K ) ) = (♯ ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) )
7		nnm1nn0 9609	. . . . . 6 |- ( K e. NN -> ( K - 1 ) e. NN0 )
8		nnexpcl 11004	. . . . . 6 |- ( ( P e. NN /\ ( K - 1 ) e. NN0 ) -> ( P ^ ( K - 1 ) ) e. NN )
9	1, 7, 8	syl2an 289	. . . . 5 |- ( ( P e. Prime /\ K e. NN ) -> ( P ^ ( K - 1 ) ) e. NN )
10	9	nncnd 9321	. . . 4 |- ( ( P e. Prime /\ K e. NN ) -> ( P ^ ( K - 1 ) ) e. CC )
11	1	nncnd 9321	. . . . 5 |- ( P e. Prime -> P e. CC )
12	11	adantr 276	. . . 4 |- ( ( P e. Prime /\ K e. NN ) -> P e. CC )
13		ax-1cn 8273	. . . . 5 |- 1 e. CC
14		subdi 8714	. . . . 5 |- ( ( ( P ^ ( K - 1 ) ) e. CC /\ P e. CC /\ 1 e. CC ) -> ( ( P ^ ( K - 1 ) ) x. ( P - 1 ) ) = ( ( ( P ^ ( K - 1 ) ) x. P ) - ( ( P ^ ( K - 1 ) ) x. 1 ) ) )
15	13, 14	mp3an3 1367	. . . 4 |- ( ( ( P ^ ( K - 1 ) ) e. CC /\ P e. CC ) -> ( ( P ^ ( K - 1 ) ) x. ( P - 1 ) ) = ( ( ( P ^ ( K - 1 ) ) x. P ) - ( ( P ^ ( K - 1 ) ) x. 1 ) ) )
16	10, 12, 15	syl2anc 415	. . 3 |- ( ( P e. Prime /\ K e. NN ) -> ( ( P ^ ( K - 1 ) ) x. ( P - 1 ) ) = ( ( ( P ^ ( K - 1 ) ) x. P ) - ( ( P ^ ( K - 1 ) ) x. 1 ) ) )
17	10	mulridd 8344	. . . 4 |- ( ( P e. Prime /\ K e. NN ) -> ( ( P ^ ( K - 1 ) ) x. 1 ) = ( P ^ ( K - 1 ) ) )
18	17	oveq2d 6101	. . 3 |- ( ( P e. Prime /\ K e. NN ) -> ( ( ( P ^ ( K - 1 ) ) x. P ) - ( ( P ^ ( K - 1 ) ) x. 1 ) ) = ( ( ( P ^ ( K - 1 ) ) x. P ) - ( P ^ ( K - 1 ) ) ) )
19		phivalfi 13013	. . . . . . 7 |- ( ( P ^ K ) e. NN -> { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } e. Fin )
20	4, 19	syl 14	. . . . . 6 |- ( ( P e. Prime /\ K e. NN ) -> { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } e. Fin )
21		1zzd 9676	. . . . . . . 8 |- ( ( P e. Prime /\ K e. NN ) -> 1 e. ZZ )
22		prmz 12908	. . . . . . . . 9 |- ( P e. Prime -> P e. ZZ )
23		zexpcl 11006	. . . . . . . . 9 |- ( ( P e. ZZ /\ K e. NN0 ) -> ( P ^ K ) e. ZZ )
24	22, 2, 23	syl2an 289	. . . . . . . 8 |- ( ( P e. Prime /\ K e. NN ) -> ( P ^ K ) e. ZZ )
25	21, 24	fzfigd 10883	. . . . . . 7 |- ( ( P e. Prime /\ K e. NN ) -> ( 1 ... ( P ^ K ) ) e. Fin )
26	22	ad2antrr 492	. . . . . . . . 9 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> P e. ZZ )
27		elfzelz 10439	. . . . . . . . . . 11 |- ( x e. ( 1 ... ( P ^ K ) ) -> x e. ZZ )
28	27	adantl 277	. . . . . . . . . 10 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> x e. ZZ )
29		0zd 9661	. . . . . . . . . 10 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> 0 e. ZZ )
30	28, 29	zsubcld 9778	. . . . . . . . 9 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> ( x - 0 ) e. ZZ )
31		zdvdsdc 12598	. . . . . . . . 9 |- ( ( P e. ZZ /\ ( x - 0 ) e. ZZ ) -> DECID P || ( x - 0 ) )
32	26, 30, 31	syl2anc 415	. . . . . . . 8 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> DECID P || ( x - 0 ) )
33	32	ralrimiva 2623	. . . . . . 7 |- ( ( P e. Prime /\ K e. NN ) -> A. x e. ( 1 ... ( P ^ K ) )DECID P || ( x - 0 ) )
34	25, 33	ssfirab 7244	. . . . . 6 |- ( ( P e. Prime /\ K e. NN ) -> { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } e. Fin )
35		inrab 3505	. . . . . . 7 |- ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } i^i { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) = { x e. ( 1 ... ( P ^ K ) ) | ( ( x gcd ( P ^ K ) ) = 1 /\ P || ( x - 0 ) ) }
36		rpexp 12951	. . . . . . . . . . . . . . . . 17 |- ( ( P e. ZZ /\ x e. ZZ /\ K e. NN ) -> ( ( ( P ^ K ) gcd x ) = 1 <-> ( P gcd x ) = 1 ) )
37	22, 36	syl3an1 1311	. . . . . . . . . . . . . . . 16 |- ( ( P e. Prime /\ x e. ZZ /\ K e. NN ) -> ( ( ( P ^ K ) gcd x ) = 1 <-> ( P gcd x ) = 1 ) )
38	37	3expa 1234	. . . . . . . . . . . . . . 15 |- ( ( ( P e. Prime /\ x e. ZZ ) /\ K e. NN ) -> ( ( ( P ^ K ) gcd x ) = 1 <-> ( P gcd x ) = 1 ) )
39	38	an32s 574	. . . . . . . . . . . . . 14 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( ( ( P ^ K ) gcd x ) = 1 <-> ( P gcd x ) = 1 ) )
40		simpr 110	. . . . . . . . . . . . . . . 16 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> x e. ZZ )
41	24	adantr 276	. . . . . . . . . . . . . . . 16 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( P ^ K ) e. ZZ )
42		gcdcom 12769	. . . . . . . . . . . . . . . 16 |- ( ( x e. ZZ /\ ( P ^ K ) e. ZZ ) -> ( x gcd ( P ^ K ) ) = ( ( P ^ K ) gcd x ) )
43	40, 41, 42	syl2anc 415	. . . . . . . . . . . . . . 15 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( x gcd ( P ^ K ) ) = ( ( P ^ K ) gcd x ) )
44	43	eqeq1d 2247	. . . . . . . . . . . . . 14 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( ( x gcd ( P ^ K ) ) = 1 <-> ( ( P ^ K ) gcd x ) = 1 ) )
45		coprm 12942	. . . . . . . . . . . . . . 15 |- ( ( P e. Prime /\ x e. ZZ ) -> ( -. P || x <-> ( P gcd x ) = 1 ) )
46	45	adantlr 481	. . . . . . . . . . . . . 14 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( -. P || x <-> ( P gcd x ) = 1 ) )
47	39, 44, 46	3bitr4d 220	. . . . . . . . . . . . 13 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( ( x gcd ( P ^ K ) ) = 1 <-> -. P || x ) )
48		zcn 9654	. . . . . . . . . . . . . . . . 17 |- ( x e. ZZ -> x e. CC )
49	48	adantl 277	. . . . . . . . . . . . . . . 16 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> x e. CC )
50	49	subid1d 8628	. . . . . . . . . . . . . . 15 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( x - 0 ) = x )
51	50	breq2d 4142	. . . . . . . . . . . . . 14 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( P || ( x - 0 ) <-> P || x ) )
52	51	notbid 677	. . . . . . . . . . . . 13 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( -. P || ( x - 0 ) <-> -. P || x ) )
53	47, 52	bitr4d 191	. . . . . . . . . . . 12 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ZZ ) -> ( ( x gcd ( P ^ K ) ) = 1 <-> -. P || ( x - 0 ) ) )
54	27, 53	sylan2 286	. . . . . . . . . . 11 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> ( ( x gcd ( P ^ K ) ) = 1 <-> -. P || ( x - 0 ) ) )
55	54	biimpd 144	. . . . . . . . . 10 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> ( ( x gcd ( P ^ K ) ) = 1 -> -. P || ( x - 0 ) ) )
56		imnan 701	. . . . . . . . . 10 |- ( ( ( x gcd ( P ^ K ) ) = 1 -> -. P || ( x - 0 ) ) <-> -. ( ( x gcd ( P ^ K ) ) = 1 /\ P || ( x - 0 ) ) )
57	55, 56	sylib 122	. . . . . . . . 9 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> -. ( ( x gcd ( P ^ K ) ) = 1 /\ P || ( x - 0 ) ) )
58	57	ralrimiva 2623	. . . . . . . 8 |- ( ( P e. Prime /\ K e. NN ) -> A. x e. ( 1 ... ( P ^ K ) ) -. ( ( x gcd ( P ^ K ) ) = 1 /\ P || ( x - 0 ) ) )
59		rabeq0 3552	. . . . . . . 8 |- ( { x e. ( 1 ... ( P ^ K ) ) | ( ( x gcd ( P ^ K ) ) = 1 /\ P || ( x - 0 ) ) } = (/) <-> A. x e. ( 1 ... ( P ^ K ) ) -. ( ( x gcd ( P ^ K ) ) = 1 /\ P || ( x - 0 ) ) )
60	58, 59	sylibr 134	. . . . . . 7 |- ( ( P e. Prime /\ K e. NN ) -> { x e. ( 1 ... ( P ^ K ) ) | ( ( x gcd ( P ^ K ) ) = 1 /\ P || ( x - 0 ) ) } = (/) )
61	35, 60	eqtrid 2283	. . . . . 6 |- ( ( P e. Prime /\ K e. NN ) -> ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } i^i { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) = (/) )
62		hashun 11261	. . . . . 6 |- ( ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } e. Fin /\ { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } e. Fin /\ ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } i^i { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) = (/) ) -> (♯ ` ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } u. { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) ) = ( (♯ ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) + (♯ ` { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) ) )
63	20, 34, 61, 62	syl3anc 1278	. . . . 5 |- ( ( P e. Prime /\ K e. NN ) -> (♯ ` ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } u. { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) ) = ( (♯ ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) + (♯ ` { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) ) )
64		unrab 3504	. . . . . . . 8 |- ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } u. { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) = { x e. ( 1 ... ( P ^ K ) ) | ( ( x gcd ( P ^ K ) ) = 1 \/ P || ( x - 0 ) ) }
65	54	biimprd 158	. . . . . . . . . . . 12 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> ( -. P || ( x - 0 ) -> ( x gcd ( P ^ K ) ) = 1 ) )
66		con1dc 868	. . . . . . . . . . . 12 |- (DECID P || ( x - 0 ) -> ( ( -. P || ( x - 0 ) -> ( x gcd ( P ^ K ) ) = 1 ) -> ( -. ( x gcd ( P ^ K ) ) = 1 -> P || ( x - 0 ) ) ) )
67	32, 65, 66	sylc 62	. . . . . . . . . . 11 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> ( -. ( x gcd ( P ^ K ) ) = 1 -> P || ( x - 0 ) ) )
68	24	adantr 276	. . . . . . . . . . . . . . 15 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> ( P ^ K ) e. ZZ )
69	28, 68	gcdcld 12764	. . . . . . . . . . . . . 14 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> ( x gcd ( P ^ K ) ) e. NN0 )
70	69	nn0zd 9771	. . . . . . . . . . . . 13 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> ( x gcd ( P ^ K ) ) e. ZZ )
71		1zzd 9676	. . . . . . . . . . . . 13 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> 1 e. ZZ )
72		zdceq 9725	. . . . . . . . . . . . 13 |- ( ( ( x gcd ( P ^ K ) ) e. ZZ /\ 1 e. ZZ ) -> DECID ( x gcd ( P ^ K ) ) = 1 )
73	70, 71, 72	syl2anc 415	. . . . . . . . . . . 12 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> DECID ( x gcd ( P ^ K ) ) = 1 )
74		dfordc 904	. . . . . . . . . . . 12 |- (DECID ( x gcd ( P ^ K ) ) = 1 -> ( ( ( x gcd ( P ^ K ) ) = 1 \/ P || ( x - 0 ) ) <-> ( -. ( x gcd ( P ^ K ) ) = 1 -> P || ( x - 0 ) ) ) )
75	73, 74	syl 14	. . . . . . . . . . 11 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> ( ( ( x gcd ( P ^ K ) ) = 1 \/ P || ( x - 0 ) ) <-> ( -. ( x gcd ( P ^ K ) ) = 1 -> P || ( x - 0 ) ) ) )
76	67, 75	mpbird 167	. . . . . . . . . 10 |- ( ( ( P e. Prime /\ K e. NN ) /\ x e. ( 1 ... ( P ^ K ) ) ) -> ( ( x gcd ( P ^ K ) ) = 1 \/ P || ( x - 0 ) ) )
77	76	ralrimiva 2623	. . . . . . . . 9 |- ( ( P e. Prime /\ K e. NN ) -> A. x e. ( 1 ... ( P ^ K ) ) ( ( x gcd ( P ^ K ) ) = 1 \/ P || ( x - 0 ) ) )
78		rabid2 2729	. . . . . . . . 9 |- ( ( 1 ... ( P ^ K ) ) = { x e. ( 1 ... ( P ^ K ) ) | ( ( x gcd ( P ^ K ) ) = 1 \/ P || ( x - 0 ) ) } <-> A. x e. ( 1 ... ( P ^ K ) ) ( ( x gcd ( P ^ K ) ) = 1 \/ P || ( x - 0 ) ) )
79	77, 78	sylibr 134	. . . . . . . 8 |- ( ( P e. Prime /\ K e. NN ) -> ( 1 ... ( P ^ K ) ) = { x e. ( 1 ... ( P ^ K ) ) | ( ( x gcd ( P ^ K ) ) = 1 \/ P || ( x - 0 ) ) } )
80	64, 79	eqtr4id 2290	. . . . . . 7 |- ( ( P e. Prime /\ K e. NN ) -> ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } u. { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) = ( 1 ... ( P ^ K ) ) )
81	80	fveq2d 5699	. . . . . 6 |- ( ( P e. Prime /\ K e. NN ) -> (♯ ` ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } u. { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) ) = (♯ ` ( 1 ... ( P ^ K ) ) ) )
82	4	nnnn0d 9625	. . . . . . 7 |- ( ( P e. Prime /\ K e. NN ) -> ( P ^ K ) e. NN0 )
83		hashfz1 11238	. . . . . . 7 |- ( ( P ^ K ) e. NN0 -> (♯ ` ( 1 ... ( P ^ K ) ) ) = ( P ^ K ) )
84	82, 83	syl 14	. . . . . 6 |- ( ( P e. Prime /\ K e. NN ) -> (♯ ` ( 1 ... ( P ^ K ) ) ) = ( P ^ K ) )
85		expm1t 11019	. . . . . . 7 |- ( ( P e. CC /\ K e. NN ) -> ( P ^ K ) = ( ( P ^ ( K - 1 ) ) x. P ) )
86	11, 85	sylan 283	. . . . . 6 |- ( ( P e. Prime /\ K e. NN ) -> ( P ^ K ) = ( ( P ^ ( K - 1 ) ) x. P ) )
87	81, 84, 86	3eqtrd 2275	. . . . 5 |- ( ( P e. Prime /\ K e. NN ) -> (♯ ` ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } u. { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) ) = ( ( P ^ ( K - 1 ) ) x. P ) )
88		hashcl 11236	. . . . . . . 8 |- ( { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } e. Fin -> (♯ ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) e. NN0 )
89	20, 88	syl 14	. . . . . . 7 |- ( ( P e. Prime /\ K e. NN ) -> (♯ ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) e. NN0 )
90	89	nn0cnd 9627	. . . . . 6 |- ( ( P e. Prime /\ K e. NN ) -> (♯ ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) e. CC )
91	1	adantr 276	. . . . . . . . 9 |- ( ( P e. Prime /\ K e. NN ) -> P e. NN )
92		nn0uz 9967	. . . . . . . . . . 11 |- NN0 = ( ZZ>= ` 0 )
93		1m1e0 9376	. . . . . . . . . . . 12 |- ( 1 - 1 ) = 0
94	93	fveq2i 5698	. . . . . . . . . . 11 |- ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
95	92, 94	eqtr4i 2262	. . . . . . . . . 10 |- NN0 = ( ZZ>= ` ( 1 - 1 ) )
96	82, 95	eleqtrdi 2331	. . . . . . . . 9 |- ( ( P e. Prime /\ K e. NN ) -> ( P ^ K ) e. ( ZZ>= ` ( 1 - 1 ) ) )
97		0zd 9661	. . . . . . . . 9 |- ( ( P e. Prime /\ K e. NN ) -> 0 e. ZZ )
98	91, 21, 96, 97	hashdvds 13022	. . . . . . . 8 |- ( ( P e. Prime /\ K e. NN ) -> (♯ ` { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) = ( ( |_ ` ( ( ( P ^ K ) - 0 ) / P ) ) - ( |_ ` ( ( ( 1 - 1 ) - 0 ) / P ) ) ) )
99	4	nncnd 9321	. . . . . . . . . . . . . 14 |- ( ( P e. Prime /\ K e. NN ) -> ( P ^ K ) e. CC )
100	99	subid1d 8628	. . . . . . . . . . . . 13 |- ( ( P e. Prime /\ K e. NN ) -> ( ( P ^ K ) - 0 ) = ( P ^ K ) )
101	100	oveq1d 6100	. . . . . . . . . . . 12 |- ( ( P e. Prime /\ K e. NN ) -> ( ( ( P ^ K ) - 0 ) / P ) = ( ( P ^ K ) / P ) )
102	91	nnap0d 9353	. . . . . . . . . . . . 13 |- ( ( P e. Prime /\ K e. NN ) -> P # 0 )
103		nnz 9668	. . . . . . . . . . . . . 14 |- ( K e. NN -> K e. ZZ )
104	103	adantl 277	. . . . . . . . . . . . 13 |- ( ( P e. Prime /\ K e. NN ) -> K e. ZZ )
105	12, 102, 104	expm1apd 11136	. . . . . . . . . . . 12 |- ( ( P e. Prime /\ K e. NN ) -> ( P ^ ( K - 1 ) ) = ( ( P ^ K ) / P ) )
106	101, 105	eqtr4d 2274	. . . . . . . . . . 11 |- ( ( P e. Prime /\ K e. NN ) -> ( ( ( P ^ K ) - 0 ) / P ) = ( P ^ ( K - 1 ) ) )
107	106	fveq2d 5699	. . . . . . . . . 10 |- ( ( P e. Prime /\ K e. NN ) -> ( |_ ` ( ( ( P ^ K ) - 0 ) / P ) ) = ( |_ ` ( P ^ ( K - 1 ) ) ) )
108	9	nnzd 9772	. . . . . . . . . . 11 |- ( ( P e. Prime /\ K e. NN ) -> ( P ^ ( K - 1 ) ) e. ZZ )
109		flid 10734	. . . . . . . . . . 11 |- ( ( P ^ ( K - 1 ) ) e. ZZ -> ( |_ ` ( P ^ ( K - 1 ) ) ) = ( P ^ ( K - 1 ) ) )
110	108, 109	syl 14	. . . . . . . . . 10 |- ( ( P e. Prime /\ K e. NN ) -> ( |_ ` ( P ^ ( K - 1 ) ) ) = ( P ^ ( K - 1 ) ) )
111	107, 110	eqtrd 2271	. . . . . . . . 9 |- ( ( P e. Prime /\ K e. NN ) -> ( |_ ` ( ( ( P ^ K ) - 0 ) / P ) ) = ( P ^ ( K - 1 ) ) )
112	93	oveq1i 6095	. . . . . . . . . . . . . 14 |- ( ( 1 - 1 ) - 0 ) = ( 0 - 0 )
113		0m0e0 9419	. . . . . . . . . . . . . 14 |- ( 0 - 0 ) = 0
114	112, 113	eqtri 2259	. . . . . . . . . . . . 13 |- ( ( 1 - 1 ) - 0 ) = 0
115	114	oveq1i 6095	. . . . . . . . . . . 12 |- ( ( ( 1 - 1 ) - 0 ) / P ) = ( 0 / P )
116	12, 102	div0apd 9120	. . . . . . . . . . . 12 |- ( ( P e. Prime /\ K e. NN ) -> ( 0 / P ) = 0 )
117	115, 116	eqtrid 2283	. . . . . . . . . . 11 |- ( ( P e. Prime /\ K e. NN ) -> ( ( ( 1 - 1 ) - 0 ) / P ) = 0 )
118	117	fveq2d 5699	. . . . . . . . . 10 |- ( ( P e. Prime /\ K e. NN ) -> ( |_ ` ( ( ( 1 - 1 ) - 0 ) / P ) ) = ( |_ ` 0 ) )
119		0z 9660	. . . . . . . . . . 11 |- 0 e. ZZ
120		flid 10734	. . . . . . . . . . 11 |- ( 0 e. ZZ -> ( |_ ` 0 ) = 0 )
121	119, 120	ax-mp 5	. . . . . . . . . 10 |- ( |_ ` 0 ) = 0
122	118, 121	eqtrdi 2287	. . . . . . . . 9 |- ( ( P e. Prime /\ K e. NN ) -> ( |_ ` ( ( ( 1 - 1 ) - 0 ) / P ) ) = 0 )
123	111, 122	oveq12d 6103	. . . . . . . 8 |- ( ( P e. Prime /\ K e. NN ) -> ( ( |_ ` ( ( ( P ^ K ) - 0 ) / P ) ) - ( |_ ` ( ( ( 1 - 1 ) - 0 ) / P ) ) ) = ( ( P ^ ( K - 1 ) ) - 0 ) )
124	10	subid1d 8628	. . . . . . . 8 |- ( ( P e. Prime /\ K e. NN ) -> ( ( P ^ ( K - 1 ) ) - 0 ) = ( P ^ ( K - 1 ) ) )
125	98, 123, 124	3eqtrd 2275	. . . . . . 7 |- ( ( P e. Prime /\ K e. NN ) -> (♯ ` { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) = ( P ^ ( K - 1 ) ) )
126	125	oveq2d 6101	. . . . . 6 |- ( ( P e. Prime /\ K e. NN ) -> ( (♯ ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) + (♯ ` { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) ) = ( (♯ ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) + ( P ^ ( K - 1 ) ) ) )
127	90, 10, 126	comraddd 8485	. . . . 5 |- ( ( P e. Prime /\ K e. NN ) -> ( (♯ ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) + (♯ ` { x e. ( 1 ... ( P ^ K ) ) | P || ( x - 0 ) } ) ) = ( ( P ^ ( K - 1 ) ) + (♯ ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) ) )
128	63, 87, 127	3eqtr3rd 2280	. . . 4 |- ( ( P e. Prime /\ K e. NN ) -> ( ( P ^ ( K - 1 ) ) + (♯ ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) ) = ( ( P ^ ( K - 1 ) ) x. P ) )
129	10, 12	mulcld 8347	. . . . 5 |- ( ( P e. Prime /\ K e. NN ) -> ( ( P ^ ( K - 1 ) ) x. P ) e. CC )
130	129, 10, 90	subaddd 8657	. . . 4 |- ( ( P e. Prime /\ K e. NN ) -> ( ( ( ( P ^ ( K - 1 ) ) x. P ) - ( P ^ ( K - 1 ) ) ) = (♯ ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) <-> ( ( P ^ ( K - 1 ) ) + (♯ ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) ) = ( ( P ^ ( K - 1 ) ) x. P ) ) )
131	128, 130	mpbird 167	. . 3 |- ( ( P e. Prime /\ K e. NN ) -> ( ( ( P ^ ( K - 1 ) ) x. P ) - ( P ^ ( K - 1 ) ) ) = (♯ ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) )
132	16, 18, 131	3eqtrrd 2276	. 2 |- ( ( P e. Prime /\ K e. NN ) -> (♯ ` { x e. ( 1 ... ( P ^ K ) ) | ( x gcd ( P ^ K ) ) = 1 } ) = ( ( P ^ ( K - 1 ) ) x. ( P - 1 ) ) )
133	6, 132	eqtrd 2271	1 |- ( ( P e. Prime /\ K e. NN ) -> ( phi ` ( P ^ K ) ) = ( ( P ^ ( K - 1 ) ) x. ( P - 1 ) ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 720  DECID wdc 846   = wceq 1402   e. wcel 2209   A.wral 2528   {crab 2532   u. cun 3218   i^i cin 3219   (/)c0 3520   class class class wbr 4130   ` cfv 5377  (class class class)co 6085   Fincfn 7022   CCcc 8178   0cc0 8180   1c1 8181   + caddc 8183   x. cmul 8185   - cmin 8499   / cdiv 9005   NNcn 9307   NN0cn0 9568   ZZcz 9649   ZZ>=cuz 9931   ...cfz 10422   |_cfl 10714   ^cexp 10990  ♯chash 11230   || cdvds 12573   gcd cgcd 12749   Primecprime 12904   phicphi 13010

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4246  ax-sep 4249  ax-nul 4259  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-iinf 4735  ax-cnex 8271  ax-resscn 8272  ax-1cn 8273  ax-1re 8274  ax-icn 8275  ax-addcl 8276  ax-addrcl 8277  ax-mulcl 8278  ax-mulrcl 8279  ax-addcom 8280  ax-mulcom 8281  ax-addass 8282  ax-mulass 8283  ax-distr 8284  ax-i2m1 8285  ax-0lt1 8286  ax-1rid 8287  ax-0id 8288  ax-rnegex 8289  ax-precex 8290  ax-cnre 8291  ax-pre-ltirr 8292  ax-pre-ltwlin 8293  ax-pre-lttrn 8294  ax-pre-apti 8295  ax-pre-ltadd 8296  ax-pre-mulgt0 8297  ax-pre-mulext 8298  ax-arch 8299  ax-caucvg 8300

This proof depends on definitions:  df-bi 117  df-stab 843  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rmo 2536  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3639  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4131  df-opab 4193  df-mpt 4194  df-tr 4230  df-id 4438  df-po 4441  df-iso 4442  df-iord 4511  df-on 4513  df-ilim 4514  df-suc 4516  df-iom 4738  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-riota 6038  df-ov 6088  df-oprab 6089  df-mpo 6090  df-1st 6374  df-2nd 6375  df-recs 6576  df-irdg 6641  df-frec 6662  df-1o 6687  df-2o 6688  df-oadd 6691  df-er 6807  df-en 7023  df-dom 7024  df-fin 7025  df-sup 7325  df-pnf 8363  df-mnf 8364  df-xr 8365  df-ltxr 8366  df-le 8367  df-sub 8501  df-neg 8502  df-reap 8906  df-ap 8913  df-div 9006  df-inn 9308  df-2 9366  df-3 9367  df-4 9368  df-n0 9569  df-z 9650  df-uz 9932  df-q 10030  df-rp 10066  df-fz 10423  df-fzo 10561  df-fl 10716  df-mod 10775  df-seqfrec 10900  df-exp 10991  df-ihash 11231  df-cj 11623  df-re 11624  df-im 11625  df-rsqrt 11780  df-abs 11781  df-dvds 12574  df-gcd 12750  df-prm 12905  df-phi 13012

This theorem is used by:  phiprm  13024