Step |
Hyp |
Ref |
Expression |
1 |
|
2nn |
โข 2 โ โ |
2 |
|
nnmulcl |
โข ( ( 2 โ โ โง ๐ โ โ ) โ ( 2 ยท ๐ ) โ โ ) |
3 |
1 2
|
mpan |
โข ( ๐ โ โ โ ( 2 ยท ๐ ) โ โ ) |
4 |
3
|
adantr |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( 2 ยท ๐ ) โ โ ) |
5 |
|
nnnn0 |
โข ( ๐ โ โ โ ๐ โ โ0 ) |
6 |
|
fzctr |
โข ( ๐ โ โ0 โ ๐ โ ( 0 ... ( 2 ยท ๐ ) ) ) |
7 |
5 6
|
syl |
โข ( ๐ โ โ โ ๐ โ ( 0 ... ( 2 ยท ๐ ) ) ) |
8 |
7
|
adantr |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ๐ โ ( 0 ... ( 2 ยท ๐ ) ) ) |
9 |
|
simpr |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ๐ โ โ ) |
10 |
|
pcbc |
โข ( ( ( 2 ยท ๐ ) โ โ โง ๐ โ ( 0 ... ( 2 ยท ๐ ) ) โง ๐ โ โ ) โ ( ๐ pCnt ( ( 2 ยท ๐ ) C ๐ ) ) = ฮฃ ๐ โ ( 1 ... ( 2 ยท ๐ ) ) ( ( โ โ ( ( 2 ยท ๐ ) / ( ๐ โ ๐ ) ) ) โ ( ( โ โ ( ( ( 2 ยท ๐ ) โ ๐ ) / ( ๐ โ ๐ ) ) ) + ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) ) ) ) |
11 |
4 8 9 10
|
syl3anc |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ๐ pCnt ( ( 2 ยท ๐ ) C ๐ ) ) = ฮฃ ๐ โ ( 1 ... ( 2 ยท ๐ ) ) ( ( โ โ ( ( 2 ยท ๐ ) / ( ๐ โ ๐ ) ) ) โ ( ( โ โ ( ( ( 2 ยท ๐ ) โ ๐ ) / ( ๐ โ ๐ ) ) ) + ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) ) ) ) |
12 |
|
nncn |
โข ( ๐ โ โ โ ๐ โ โ ) |
13 |
12
|
2timesd |
โข ( ๐ โ โ โ ( 2 ยท ๐ ) = ( ๐ + ๐ ) ) |
14 |
12 12 13
|
mvrladdd |
โข ( ๐ โ โ โ ( ( 2 ยท ๐ ) โ ๐ ) = ๐ ) |
15 |
14
|
fvoveq1d |
โข ( ๐ โ โ โ ( โ โ ( ( ( 2 ยท ๐ ) โ ๐ ) / ( ๐ โ ๐ ) ) ) = ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) ) |
16 |
15
|
oveq1d |
โข ( ๐ โ โ โ ( ( โ โ ( ( ( 2 ยท ๐ ) โ ๐ ) / ( ๐ โ ๐ ) ) ) + ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) ) = ( ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) + ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) ) ) |
17 |
16
|
ad2antrr |
โข ( ( ( ๐ โ โ โง ๐ โ โ ) โง ๐ โ ( 1 ... ( 2 ยท ๐ ) ) ) โ ( ( โ โ ( ( ( 2 ยท ๐ ) โ ๐ ) / ( ๐ โ ๐ ) ) ) + ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) ) = ( ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) + ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) ) ) |
18 |
|
nnre |
โข ( ๐ โ โ โ ๐ โ โ ) |
19 |
18
|
ad2antrr |
โข ( ( ( ๐ โ โ โง ๐ โ โ ) โง ๐ โ ( 1 ... ( 2 ยท ๐ ) ) ) โ ๐ โ โ ) |
20 |
|
prmnn |
โข ( ๐ โ โ โ ๐ โ โ ) |
21 |
20
|
adantl |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ๐ โ โ ) |
22 |
|
elfznn |
โข ( ๐ โ ( 1 ... ( 2 ยท ๐ ) ) โ ๐ โ โ ) |
23 |
22
|
nnnn0d |
โข ( ๐ โ ( 1 ... ( 2 ยท ๐ ) ) โ ๐ โ โ0 ) |
24 |
|
nnexpcl |
โข ( ( ๐ โ โ โง ๐ โ โ0 ) โ ( ๐ โ ๐ ) โ โ ) |
25 |
21 23 24
|
syl2an |
โข ( ( ( ๐ โ โ โง ๐ โ โ ) โง ๐ โ ( 1 ... ( 2 ยท ๐ ) ) ) โ ( ๐ โ ๐ ) โ โ ) |
26 |
19 25
|
nndivred |
โข ( ( ( ๐ โ โ โง ๐ โ โ ) โง ๐ โ ( 1 ... ( 2 ยท ๐ ) ) ) โ ( ๐ / ( ๐ โ ๐ ) ) โ โ ) |
27 |
26
|
flcld |
โข ( ( ( ๐ โ โ โง ๐ โ โ ) โง ๐ โ ( 1 ... ( 2 ยท ๐ ) ) ) โ ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) โ โค ) |
28 |
27
|
zcnd |
โข ( ( ( ๐ โ โ โง ๐ โ โ ) โง ๐ โ ( 1 ... ( 2 ยท ๐ ) ) ) โ ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) โ โ ) |
29 |
28
|
2timesd |
โข ( ( ( ๐ โ โ โง ๐ โ โ ) โง ๐ โ ( 1 ... ( 2 ยท ๐ ) ) ) โ ( 2 ยท ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) ) = ( ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) + ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) ) ) |
30 |
17 29
|
eqtr4d |
โข ( ( ( ๐ โ โ โง ๐ โ โ ) โง ๐ โ ( 1 ... ( 2 ยท ๐ ) ) ) โ ( ( โ โ ( ( ( 2 ยท ๐ ) โ ๐ ) / ( ๐ โ ๐ ) ) ) + ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) ) = ( 2 ยท ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) ) ) |
31 |
30
|
oveq2d |
โข ( ( ( ๐ โ โ โง ๐ โ โ ) โง ๐ โ ( 1 ... ( 2 ยท ๐ ) ) ) โ ( ( โ โ ( ( 2 ยท ๐ ) / ( ๐ โ ๐ ) ) ) โ ( ( โ โ ( ( ( 2 ยท ๐ ) โ ๐ ) / ( ๐ โ ๐ ) ) ) + ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) ) ) = ( ( โ โ ( ( 2 ยท ๐ ) / ( ๐ โ ๐ ) ) ) โ ( 2 ยท ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) ) ) ) |
32 |
31
|
sumeq2dv |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ฮฃ ๐ โ ( 1 ... ( 2 ยท ๐ ) ) ( ( โ โ ( ( 2 ยท ๐ ) / ( ๐ โ ๐ ) ) ) โ ( ( โ โ ( ( ( 2 ยท ๐ ) โ ๐ ) / ( ๐ โ ๐ ) ) ) + ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) ) ) = ฮฃ ๐ โ ( 1 ... ( 2 ยท ๐ ) ) ( ( โ โ ( ( 2 ยท ๐ ) / ( ๐ โ ๐ ) ) ) โ ( 2 ยท ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) ) ) ) |
33 |
11 32
|
eqtrd |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ๐ pCnt ( ( 2 ยท ๐ ) C ๐ ) ) = ฮฃ ๐ โ ( 1 ... ( 2 ยท ๐ ) ) ( ( โ โ ( ( 2 ยท ๐ ) / ( ๐ โ ๐ ) ) ) โ ( 2 ยท ( โ โ ( ๐ / ( ๐ โ ๐ ) ) ) ) ) ) |