Step | Hyp | Ref
| Expression |
1 | | 2nn 12233 |
. . . . 5
โข 2 โ
โ |
2 | | nnmulcl 12184 |
. . . . 5
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
3 | 1, 2 | mpan 689 |
. . . 4
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
4 | 3 | adantr 482 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท ๐) โ
โ) |
5 | | nnnn0 12427 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โ0) |
6 | | fzctr 13560 |
. . . . 5
โข (๐ โ โ0
โ ๐ โ (0...(2
ยท ๐))) |
7 | 5, 6 | syl 17 |
. . . 4
โข (๐ โ โ โ ๐ โ (0...(2 ยท ๐))) |
8 | 7 | adantr 482 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ (0...(2 ยท ๐))) |
9 | | simpr 486 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
10 | | pcbc 16779 |
. . 3
โข (((2
ยท ๐) โ โ
โง ๐ โ (0...(2
ยท ๐)) โง ๐ โ โ) โ (๐ pCnt ((2 ยท ๐)C๐)) = ฮฃ๐ โ (1...(2 ยท ๐))((โโ((2 ยท ๐) / (๐โ๐))) โ ((โโ(((2 ยท
๐) โ ๐) / (๐โ๐))) + (โโ(๐ / (๐โ๐)))))) |
11 | 4, 8, 9, 10 | syl3anc 1372 |
. 2
โข ((๐ โ โ โง ๐ โ โ) โ (๐ pCnt ((2 ยท ๐)C๐)) = ฮฃ๐ โ (1...(2 ยท ๐))((โโ((2 ยท ๐) / (๐โ๐))) โ ((โโ(((2 ยท
๐) โ ๐) / (๐โ๐))) + (โโ(๐ / (๐โ๐)))))) |
12 | | nncn 12168 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
13 | 12 | 2timesd 12403 |
. . . . . . . . 9
โข (๐ โ โ โ (2
ยท ๐) = (๐ + ๐)) |
14 | 12, 12, 13 | mvrladdd 11575 |
. . . . . . . 8
โข (๐ โ โ โ ((2
ยท ๐) โ ๐) = ๐) |
15 | 14 | fvoveq1d 7384 |
. . . . . . 7
โข (๐ โ โ โ
(โโ(((2 ยท ๐) โ ๐) / (๐โ๐))) = (โโ(๐ / (๐โ๐)))) |
16 | 15 | oveq1d 7377 |
. . . . . 6
โข (๐ โ โ โ
((โโ(((2 ยท ๐) โ ๐) / (๐โ๐))) + (โโ(๐ / (๐โ๐)))) = ((โโ(๐ / (๐โ๐))) + (โโ(๐ / (๐โ๐))))) |
17 | 16 | ad2antrr 725 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((โโ(((2
ยท ๐) โ ๐) / (๐โ๐))) + (โโ(๐ / (๐โ๐)))) = ((โโ(๐ / (๐โ๐))) + (โโ(๐ / (๐โ๐))))) |
18 | | nnre 12167 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
19 | 18 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ๐ โ โ) |
20 | | prmnn 16557 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
21 | 20 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
22 | | elfznn 13477 |
. . . . . . . . . . 11
โข (๐ โ (1...(2 ยท ๐)) โ ๐ โ โ) |
23 | 22 | nnnn0d 12480 |
. . . . . . . . . 10
โข (๐ โ (1...(2 ยท ๐)) โ ๐ โ โ0) |
24 | | nnexpcl 13987 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โ
โ) |
25 | 21, 23, 24 | syl2an 597 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (๐โ๐) โ โ) |
26 | 19, 25 | nndivred 12214 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (๐ / (๐โ๐)) โ โ) |
27 | 26 | flcld 13710 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (โโ(๐ / (๐โ๐))) โ โค) |
28 | 27 | zcnd 12615 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (โโ(๐ / (๐โ๐))) โ โ) |
29 | 28 | 2timesd 12403 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ (2 ยท
(โโ(๐ / (๐โ๐)))) = ((โโ(๐ / (๐โ๐))) + (โโ(๐ / (๐โ๐))))) |
30 | 17, 29 | eqtr4d 2780 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((โโ(((2
ยท ๐) โ ๐) / (๐โ๐))) + (โโ(๐ / (๐โ๐)))) = (2 ยท (โโ(๐ / (๐โ๐))))) |
31 | 30 | oveq2d 7378 |
. . 3
โข (((๐ โ โ โง ๐ โ โ) โง ๐ โ (1...(2 ยท ๐))) โ ((โโ((2
ยท ๐) / (๐โ๐))) โ ((โโ(((2 ยท
๐) โ ๐) / (๐โ๐))) + (โโ(๐ / (๐โ๐))))) = ((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐)))))) |
32 | 31 | sumeq2dv 15595 |
. 2
โข ((๐ โ โ โง ๐ โ โ) โ
ฮฃ๐ โ (1...(2
ยท ๐))((โโ((2 ยท ๐) / (๐โ๐))) โ ((โโ(((2 ยท
๐) โ ๐) / (๐โ๐))) + (โโ(๐ / (๐โ๐))))) = ฮฃ๐ โ (1...(2 ยท ๐))((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐)))))) |
33 | 11, 32 | eqtrd 2777 |
1
โข ((๐ โ โ โง ๐ โ โ) โ (๐ pCnt ((2 ยท ๐)C๐)) = ฮฃ๐ โ (1...(2 ยท ๐))((โโ((2 ยท ๐) / (๐โ๐))) โ (2 ยท (โโ(๐ / (๐โ๐)))))) |