Metamath Proof Explorer

Theorem 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 ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ฯ• โ€˜ ( ๐‘ƒ โ†‘ ๐พ ) ) = ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ( ๐‘ƒ โˆ’ 1 ) ) )

Proof

Step Hyp Ref Expression
1 prmnn โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„• )
2 nnnn0 โŠข ( ๐พ โˆˆ โ„• โ†’ ๐พ โˆˆ โ„•0 )
3 nnexpcl โŠข ( ( ๐‘ƒ โˆˆ โ„• โˆง ๐พ โˆˆ โ„•0 ) โ†’ ( ๐‘ƒ โ†‘ ๐พ ) โˆˆ โ„• )
4 1 2 3 syl2an โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ๐‘ƒ โ†‘ ๐พ ) โˆˆ โ„• )
5 phival โŠข ( ( ๐‘ƒ โ†‘ ๐พ ) โˆˆ โ„• โ†’ ( ฯ• โ€˜ ( ๐‘ƒ โ†‘ ๐พ ) ) = ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) )
6 4 5 syl โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ฯ• โ€˜ ( ๐‘ƒ โ†‘ ๐พ ) ) = ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) )
7 nnm1nn0 โŠข ( ๐พ โˆˆ โ„• โ†’ ( ๐พ โˆ’ 1 ) โˆˆ โ„•0 )
8 nnexpcl โŠข ( ( ๐‘ƒ โˆˆ โ„• โˆง ( ๐พ โˆ’ 1 ) โˆˆ โ„•0 ) โ†’ ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) โˆˆ โ„• )
9 1 7 8 syl2an โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) โˆˆ โ„• )
10 9 nncnd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) โˆˆ โ„‚ )
11 1 nncnd โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„‚ )
12 11 adantr โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ๐‘ƒ โˆˆ โ„‚ )
13 ax-1cn โŠข 1 โˆˆ โ„‚
14 subdi โŠข ( ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) โˆˆ โ„‚ โˆง ๐‘ƒ โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ( ๐‘ƒ โˆ’ 1 ) ) = ( ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ๐‘ƒ ) โˆ’ ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท 1 ) ) )
15 13 14 mp3an3 โŠข ( ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) โˆˆ โ„‚ โˆง ๐‘ƒ โˆˆ โ„‚ ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ( ๐‘ƒ โˆ’ 1 ) ) = ( ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ๐‘ƒ ) โˆ’ ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท 1 ) ) )
16 10 12 15 syl2anc โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ( ๐‘ƒ โˆ’ 1 ) ) = ( ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ๐‘ƒ ) โˆ’ ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท 1 ) ) )
17 10 mulridd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท 1 ) = ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) )
18 17 oveq2d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ๐‘ƒ ) โˆ’ ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท 1 ) ) = ( ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ๐‘ƒ ) โˆ’ ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ) )
19 fzfi โŠข ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆˆ Fin
20 ssrab2 โŠข { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } โŠ† ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) )
21 ssfi โŠข ( ( ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆˆ Fin โˆง { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } โŠ† ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) ) โ†’ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } โˆˆ Fin )
22 19 20 21 mp2an โŠข { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } โˆˆ Fin
23 ssrab2 โŠข { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) } โŠ† ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) )
24 ssfi โŠข ( ( ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆˆ Fin โˆง { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) } โŠ† ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) ) โ†’ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) } โˆˆ Fin )
25 19 23 24 mp2an โŠข { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) } โˆˆ Fin
26 inrab โŠข ( { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } โˆฉ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) } ) = { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โˆง ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) }
27 elfzelz โŠข ( ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โ†’ ๐‘ฅ โˆˆ โ„ค )
28 prmz โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„ค )
29 rpexp โŠข ( ( ๐‘ƒ โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( ( ๐‘ƒ โ†‘ ๐พ ) gcd ๐‘ฅ ) = 1 โ†” ( ๐‘ƒ gcd ๐‘ฅ ) = 1 ) )
30 28 29 syl3an1 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( ( ๐‘ƒ โ†‘ ๐พ ) gcd ๐‘ฅ ) = 1 โ†” ( ๐‘ƒ gcd ๐‘ฅ ) = 1 ) )
31 30 3expa โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ โ„ค ) โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( ( ๐‘ƒ โ†‘ ๐พ ) gcd ๐‘ฅ ) = 1 โ†” ( ๐‘ƒ gcd ๐‘ฅ ) = 1 ) )
32 31 an32s โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ( ( ๐‘ƒ โ†‘ ๐พ ) gcd ๐‘ฅ ) = 1 โ†” ( ๐‘ƒ gcd ๐‘ฅ ) = 1 ) )
33 simpr โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ๐‘ฅ โˆˆ โ„ค )
34 zexpcl โŠข ( ( ๐‘ƒ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„•0 ) โ†’ ( ๐‘ƒ โ†‘ ๐พ ) โˆˆ โ„ค )
35 28 2 34 syl2an โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ๐‘ƒ โ†‘ ๐พ ) โˆˆ โ„ค )
36 35 adantr โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ๐‘ƒ โ†‘ ๐พ ) โˆˆ โ„ค )
37 33 36 gcdcomd โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = ( ( ๐‘ƒ โ†‘ ๐พ ) gcd ๐‘ฅ ) )
38 37 eqeq1d โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โ†” ( ( ๐‘ƒ โ†‘ ๐พ ) gcd ๐‘ฅ ) = 1 ) )
39 coprm โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ยฌ ๐‘ƒ โˆฅ ๐‘ฅ โ†” ( ๐‘ƒ gcd ๐‘ฅ ) = 1 ) )
40 39 adantlr โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ยฌ ๐‘ƒ โˆฅ ๐‘ฅ โ†” ( ๐‘ƒ gcd ๐‘ฅ ) = 1 ) )
41 32 38 40 3bitr4d โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โ†” ยฌ ๐‘ƒ โˆฅ ๐‘ฅ ) )
42 zcn โŠข ( ๐‘ฅ โˆˆ โ„ค โ†’ ๐‘ฅ โˆˆ โ„‚ )
43 42 adantl โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ๐‘ฅ โˆˆ โ„‚ )
44 43 subid1d โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ๐‘ฅ โˆ’ 0 ) = ๐‘ฅ )
45 44 breq2d โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) โ†” ๐‘ƒ โˆฅ ๐‘ฅ ) )
46 45 notbid โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ยฌ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) โ†” ยฌ ๐‘ƒ โˆฅ ๐‘ฅ ) )
47 41 46 bitr4d โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โ†” ยฌ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) )
48 27 47 sylan2 โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) ) โ†’ ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โ†” ยฌ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) )
49 48 biimpd โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) ) โ†’ ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โ†’ ยฌ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) )
50 imnan โŠข ( ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โ†’ ยฌ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) โ†” ยฌ ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โˆง ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) )
51 49 50 sylib โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) ) โ†’ ยฌ ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โˆง ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) )
52 51 ralrimiva โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ โˆ€ ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) ยฌ ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โˆง ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) )
53 rabeq0 โŠข ( { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โˆง ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) } = โˆ… โ†” โˆ€ ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) ยฌ ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โˆง ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) )
54 52 53 sylibr โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โˆง ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) } = โˆ… )
55 26 54 eqtrid โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } โˆฉ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) } ) = โˆ… )
56 hashun โŠข ( ( { ๐‘ฅ โˆˆ ( 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 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( โ™ฏ โ€˜ ( { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } โˆช { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) } ) ) = ( ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) + ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) } ) ) )
58 unrab โŠข ( { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } โˆช { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) } ) = { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โˆจ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) }
59 48 biimprd โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) ) โ†’ ( ยฌ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) โ†’ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 ) )
60 59 con1d โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) ) โ†’ ( ยฌ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โ†’ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) )
61 60 orrd โŠข ( ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) ) โ†’ ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โˆจ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) )
62 61 ralrimiva โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ โˆ€ ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โˆจ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) )
63 rabid2 โŠข ( ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) = { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โˆจ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) } โ†” โˆ€ ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โˆจ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) )
64 62 63 sylibr โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) = { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 โˆจ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) ) } )
65 58 64 eqtr4id โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } โˆช { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) } ) = ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) )
66 65 fveq2d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( โ™ฏ โ€˜ ( { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } โˆช { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) } ) ) = ( โ™ฏ โ€˜ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) ) )
67 4 nnnn0d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ๐‘ƒ โ†‘ ๐พ ) โˆˆ โ„•0 )
68 hashfz1 โŠข ( ( ๐‘ƒ โ†‘ ๐พ ) โˆˆ โ„•0 โ†’ ( โ™ฏ โ€˜ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) ) = ( ๐‘ƒ โ†‘ ๐พ ) )
69 67 68 syl โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( โ™ฏ โ€˜ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) ) = ( ๐‘ƒ โ†‘ ๐พ ) )
70 expm1t โŠข ( ( ๐‘ƒ โˆˆ โ„‚ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ๐‘ƒ โ†‘ ๐พ ) = ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ๐‘ƒ ) )
71 11 70 sylan โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ๐‘ƒ โ†‘ ๐พ ) = ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ๐‘ƒ ) )
72 66 69 71 3eqtrd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( โ™ฏ โ€˜ ( { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } โˆช { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) } ) ) = ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ๐‘ƒ ) )
73 1 adantr โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ๐‘ƒ โˆˆ โ„• )
74 1zzd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ 1 โˆˆ โ„ค )
75 nn0uz โŠข โ„•0 = ( โ„คโ‰ฅ โ€˜ 0 )
76 1m1e0 โŠข ( 1 โˆ’ 1 ) = 0
77 76 fveq2i โŠข ( โ„คโ‰ฅ โ€˜ ( 1 โˆ’ 1 ) ) = ( โ„คโ‰ฅ โ€˜ 0 )
78 75 77 eqtr4i โŠข โ„•0 = ( โ„คโ‰ฅ โ€˜ ( 1 โˆ’ 1 ) )
79 67 78 eleqtrdi โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ๐‘ƒ โ†‘ ๐พ ) โˆˆ ( โ„คโ‰ฅ โ€˜ ( 1 โˆ’ 1 ) ) )
80 0zd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ 0 โˆˆ โ„ค )
81 73 74 79 80 hashdvds โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) } ) = ( ( โŒŠ โ€˜ ( ( ( ๐‘ƒ โ†‘ ๐พ ) โˆ’ 0 ) / ๐‘ƒ ) ) โˆ’ ( โŒŠ โ€˜ ( ( ( 1 โˆ’ 1 ) โˆ’ 0 ) / ๐‘ƒ ) ) ) )
82 4 nncnd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ๐‘ƒ โ†‘ ๐พ ) โˆˆ โ„‚ )
83 82 subid1d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( ๐‘ƒ โ†‘ ๐พ ) โˆ’ 0 ) = ( ๐‘ƒ โ†‘ ๐พ ) )
84 83 oveq1d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( ( ๐‘ƒ โ†‘ ๐พ ) โˆ’ 0 ) / ๐‘ƒ ) = ( ( ๐‘ƒ โ†‘ ๐พ ) / ๐‘ƒ ) )
85 73 nnne0d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ๐‘ƒ โ‰  0 )
86 nnz โŠข ( ๐พ โˆˆ โ„• โ†’ ๐พ โˆˆ โ„ค )
87 86 adantl โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ๐พ โˆˆ โ„ค )
88 12 85 87 expm1d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) = ( ( ๐‘ƒ โ†‘ ๐พ ) / ๐‘ƒ ) )
89 84 88 eqtr4d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( ( ๐‘ƒ โ†‘ ๐พ ) โˆ’ 0 ) / ๐‘ƒ ) = ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) )
90 89 fveq2d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( โŒŠ โ€˜ ( ( ( ๐‘ƒ โ†‘ ๐พ ) โˆ’ 0 ) / ๐‘ƒ ) ) = ( โŒŠ โ€˜ ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ) )
91 9 nnzd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) โˆˆ โ„ค )
92 flid โŠข ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) โˆˆ โ„ค โ†’ ( โŒŠ โ€˜ ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ) = ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) )
93 91 92 syl โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( โŒŠ โ€˜ ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ) = ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) )
94 90 93 eqtrd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( โŒŠ โ€˜ ( ( ( ๐‘ƒ โ†‘ ๐พ ) โˆ’ 0 ) / ๐‘ƒ ) ) = ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 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 โŠข ( ( ( 1 โˆ’ 1 ) โˆ’ 0 ) / ๐‘ƒ ) = ( 0 / ๐‘ƒ )
99 12 85 div0d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( 0 / ๐‘ƒ ) = 0 )
100 98 99 eqtrid โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( ( 1 โˆ’ 1 ) โˆ’ 0 ) / ๐‘ƒ ) = 0 )
101 100 fveq2d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( โŒŠ โ€˜ ( ( ( 1 โˆ’ 1 ) โˆ’ 0 ) / ๐‘ƒ ) ) = ( โŒŠ โ€˜ 0 ) )
102 0z โŠข 0 โˆˆ โ„ค
103 flid โŠข ( 0 โˆˆ โ„ค โ†’ ( โŒŠ โ€˜ 0 ) = 0 )
104 102 103 ax-mp โŠข ( โŒŠ โ€˜ 0 ) = 0
105 101 104 eqtrdi โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( โŒŠ โ€˜ ( ( ( 1 โˆ’ 1 ) โˆ’ 0 ) / ๐‘ƒ ) ) = 0 )
106 94 105 oveq12d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( โŒŠ โ€˜ ( ( ( ๐‘ƒ โ†‘ ๐พ ) โˆ’ 0 ) / ๐‘ƒ ) ) โˆ’ ( โŒŠ โ€˜ ( ( ( 1 โˆ’ 1 ) โˆ’ 0 ) / ๐‘ƒ ) ) ) = ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) โˆ’ 0 ) )
107 10 subid1d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) โˆ’ 0 ) = ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) )
108 81 106 107 3eqtrd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) } ) = ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) )
109 108 oveq2d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) + ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) } ) ) = ( ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) + ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ) )
110 hashcl โŠข ( { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } โˆˆ Fin โ†’ ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) โˆˆ โ„•0 )
111 22 110 ax-mp โŠข ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) โˆˆ โ„•0
112 111 nn0cni โŠข ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) โˆˆ โ„‚
113 addcom โŠข ( ( ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) โˆˆ โ„‚ โˆง ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) โˆˆ โ„‚ ) โ†’ ( ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) + ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ) = ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) + ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) ) )
114 112 10 113 sylancr โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) + ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ) = ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) + ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) ) )
115 109 114 eqtrd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) + ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ๐‘ƒ โˆฅ ( ๐‘ฅ โˆ’ 0 ) } ) ) = ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) + ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) ) )
116 57 72 115 3eqtr3rd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) + ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) ) = ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ๐‘ƒ ) )
117 10 12 mulcld โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ๐‘ƒ ) โˆˆ โ„‚ )
118 112 a1i โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) โˆˆ โ„‚ )
119 117 10 118 subaddd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ๐‘ƒ ) โˆ’ ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ) = ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) โ†” ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) + ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) ) = ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ๐‘ƒ ) ) )
120 116 119 mpbird โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ๐‘ƒ ) โˆ’ ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ) = ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) )
121 16 18 120 3eqtrrd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( โ™ฏ โ€˜ { ๐‘ฅ โˆˆ ( 1 ... ( ๐‘ƒ โ†‘ ๐พ ) ) โˆฃ ( ๐‘ฅ gcd ( ๐‘ƒ โ†‘ ๐พ ) ) = 1 } ) = ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ( ๐‘ƒ โˆ’ 1 ) ) )
122 6 121 eqtrd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐พ โˆˆ โ„• ) โ†’ ( ฯ• โ€˜ ( ๐‘ƒ โ†‘ ๐พ ) ) = ( ( ๐‘ƒ โ†‘ ( ๐พ โˆ’ 1 ) ) ยท ( ๐‘ƒ โˆ’ 1 ) ) )