Step | Hyp | Ref
| Expression |
1 | | fveq2 6888 |
. . . . . . . 8
โข (๐ฅ = 0 โ
(โคโฅโ๐ฅ) =
(โคโฅโ0)) |
2 | | fveq2 6888 |
. . . . . . . . . 10
โข (๐ฅ = 0 โ (!โ๐ฅ) =
(!โ0)) |
3 | 2 | oveq2d 7421 |
. . . . . . . . 9
โข (๐ฅ = 0 โ (๐ pCnt (!โ๐ฅ)) = (๐ pCnt (!โ0))) |
4 | | fvoveq1 7428 |
. . . . . . . . . 10
โข (๐ฅ = 0 โ
(โโ(๐ฅ / (๐โ๐))) = (โโ(0 / (๐โ๐)))) |
5 | 4 | sumeq2sdv 15646 |
. . . . . . . . 9
โข (๐ฅ = 0 โ ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) = ฮฃ๐ โ (1...๐)(โโ(0 / (๐โ๐)))) |
6 | 3, 5 | eqeq12d 2748 |
. . . . . . . 8
โข (๐ฅ = 0 โ ((๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) โ (๐ pCnt (!โ0)) = ฮฃ๐ โ (1...๐)(โโ(0 / (๐โ๐))))) |
7 | 1, 6 | raleqbidv 3342 |
. . . . . . 7
โข (๐ฅ = 0 โ (โ๐ โ
(โคโฅโ๐ฅ)(๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) โ โ๐ โ
(โคโฅโ0)(๐ pCnt (!โ0)) = ฮฃ๐ โ (1...๐)(โโ(0 / (๐โ๐))))) |
8 | 7 | imbi2d 340 |
. . . . . 6
โข (๐ฅ = 0 โ ((๐ โ โ โ โ๐ โ
(โคโฅโ๐ฅ)(๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐)))) โ (๐ โ โ โ โ๐ โ
(โคโฅโ0)(๐ pCnt (!โ0)) = ฮฃ๐ โ (1...๐)(โโ(0 / (๐โ๐)))))) |
9 | | fveq2 6888 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (โคโฅโ๐ฅ) =
(โคโฅโ๐)) |
10 | | fveq2 6888 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (!โ๐ฅ) = (!โ๐)) |
11 | 10 | oveq2d 7421 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ (๐ pCnt (!โ๐ฅ)) = (๐ pCnt (!โ๐))) |
12 | | fvoveq1 7428 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (โโ(๐ฅ / (๐โ๐))) = (โโ(๐ / (๐โ๐)))) |
13 | 12 | sumeq2sdv 15646 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) |
14 | 11, 13 | eqeq12d 2748 |
. . . . . . . 8
โข (๐ฅ = ๐ โ ((๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) โ (๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
15 | 9, 14 | raleqbidv 3342 |
. . . . . . 7
โข (๐ฅ = ๐ โ (โ๐ โ (โคโฅโ๐ฅ)(๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) โ โ๐ โ (โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
16 | 15 | imbi2d 340 |
. . . . . 6
โข (๐ฅ = ๐ โ ((๐ โ โ โ โ๐ โ
(โคโฅโ๐ฅ)(๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐)))) โ (๐ โ โ โ โ๐ โ
(โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))))) |
17 | | fveq2 6888 |
. . . . . . . 8
โข (๐ฅ = (๐ + 1) โ
(โคโฅโ๐ฅ) = (โคโฅโ(๐ + 1))) |
18 | | fveq2 6888 |
. . . . . . . . . 10
โข (๐ฅ = (๐ + 1) โ (!โ๐ฅ) = (!โ(๐ + 1))) |
19 | 18 | oveq2d 7421 |
. . . . . . . . 9
โข (๐ฅ = (๐ + 1) โ (๐ pCnt (!โ๐ฅ)) = (๐ pCnt (!โ(๐ + 1)))) |
20 | | fvoveq1 7428 |
. . . . . . . . . 10
โข (๐ฅ = (๐ + 1) โ (โโ(๐ฅ / (๐โ๐))) = (โโ((๐ + 1) / (๐โ๐)))) |
21 | 20 | sumeq2sdv 15646 |
. . . . . . . . 9
โข (๐ฅ = (๐ + 1) โ ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐)))) |
22 | 19, 21 | eqeq12d 2748 |
. . . . . . . 8
โข (๐ฅ = (๐ + 1) โ ((๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) โ (๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))))) |
23 | 17, 22 | raleqbidv 3342 |
. . . . . . 7
โข (๐ฅ = (๐ + 1) โ (โ๐ โ (โคโฅโ๐ฅ)(๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) โ โ๐ โ (โคโฅโ(๐ + 1))(๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))))) |
24 | 23 | imbi2d 340 |
. . . . . 6
โข (๐ฅ = (๐ + 1) โ ((๐ โ โ โ โ๐ โ
(โคโฅโ๐ฅ)(๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐)))) โ (๐ โ โ โ โ๐ โ
(โคโฅโ(๐ + 1))(๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐)))))) |
25 | | fveq2 6888 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (โคโฅโ๐ฅ) =
(โคโฅโ๐)) |
26 | | fveq2 6888 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (!โ๐ฅ) = (!โ๐)) |
27 | 26 | oveq2d 7421 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ (๐ pCnt (!โ๐ฅ)) = (๐ pCnt (!โ๐))) |
28 | | fvoveq1 7428 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (โโ(๐ฅ / (๐โ๐))) = (โโ(๐ / (๐โ๐)))) |
29 | 28 | sumeq2sdv 15646 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) |
30 | 27, 29 | eqeq12d 2748 |
. . . . . . . 8
โข (๐ฅ = ๐ โ ((๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) โ (๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
31 | 25, 30 | raleqbidv 3342 |
. . . . . . 7
โข (๐ฅ = ๐ โ (โ๐ โ (โคโฅโ๐ฅ)(๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) โ โ๐ โ (โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
32 | 31 | imbi2d 340 |
. . . . . 6
โข (๐ฅ = ๐ โ ((๐ โ โ โ โ๐ โ
(โคโฅโ๐ฅ)(๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐)))) โ (๐ โ โ โ โ๐ โ
(โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))))) |
33 | | fzfid 13934 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ
(โคโฅโ0)) โ (1...๐) โ Fin) |
34 | | sumz 15664 |
. . . . . . . . . 10
โข
(((1...๐) โ
(โคโฅโ1) โจ (1...๐) โ Fin) โ ฮฃ๐ โ (1...๐)0 = 0) |
35 | 34 | olcs 874 |
. . . . . . . . 9
โข
((1...๐) โ Fin
โ ฮฃ๐ โ
(1...๐)0 =
0) |
36 | 33, 35 | syl 17 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ
(โคโฅโ0)) โ ฮฃ๐ โ (1...๐)0 = 0) |
37 | | 0nn0 12483 |
. . . . . . . . . 10
โข 0 โ
โ0 |
38 | | elfznn 13526 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ ๐ โ โ) |
39 | 38 | nnnn0d 12528 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ ๐ โ โ0) |
40 | | nn0uz 12860 |
. . . . . . . . . . . 12
โข
โ0 = (โคโฅโ0) |
41 | 39, 40 | eleqtrdi 2843 |
. . . . . . . . . . 11
โข (๐ โ (1...๐) โ ๐ โ
(โคโฅโ0)) |
42 | 41 | adantl 482 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ
(โคโฅโ0)) โง ๐ โ (1...๐)) โ ๐ โ
(โคโฅโ0)) |
43 | | simpll 765 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ
(โคโฅโ0)) โง ๐ โ (1...๐)) โ ๐ โ โ) |
44 | | pcfaclem 16827 |
. . . . . . . . . 10
โข ((0
โ โ0 โง ๐ โ (โคโฅโ0)
โง ๐ โ โ)
โ (โโ(0 / (๐โ๐))) = 0) |
45 | 37, 42, 43, 44 | mp3an2i 1466 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ
(โคโฅโ0)) โง ๐ โ (1...๐)) โ (โโ(0 / (๐โ๐))) = 0) |
46 | 45 | sumeq2dv 15645 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ
(โคโฅโ0)) โ ฮฃ๐ โ (1...๐)(โโ(0 / (๐โ๐))) = ฮฃ๐ โ (1...๐)0) |
47 | | fac0 14232 |
. . . . . . . . . . 11
โข
(!โ0) = 1 |
48 | 47 | oveq2i 7416 |
. . . . . . . . . 10
โข (๐ pCnt (!โ0)) = (๐ pCnt 1) |
49 | | pc1 16784 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ pCnt 1) = 0) |
50 | 48, 49 | eqtrid 2784 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ pCnt (!โ0)) =
0) |
51 | 50 | adantr 481 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ
(โคโฅโ0)) โ (๐ pCnt (!โ0)) = 0) |
52 | 36, 46, 51 | 3eqtr4rd 2783 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ
(โคโฅโ0)) โ (๐ pCnt (!โ0)) = ฮฃ๐ โ (1...๐)(โโ(0 / (๐โ๐)))) |
53 | 52 | ralrimiva 3146 |
. . . . . 6
โข (๐ โ โ โ
โ๐ โ
(โคโฅโ0)(๐ pCnt (!โ0)) = ฮฃ๐ โ (1...๐)(โโ(0 / (๐โ๐)))) |
54 | | nn0z 12579 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ๐ โ
โค) |
55 | 54 | adantr 481 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
โค) |
56 | | uzid 12833 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ
(โคโฅโ๐)) |
57 | | peano2uz 12881 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ๐) โ (๐ + 1) โ
(โคโฅโ๐)) |
58 | 55, 56, 57 | 3syl 18 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + 1) โ
(โคโฅโ๐)) |
59 | | uzss 12841 |
. . . . . . . . . 10
โข ((๐ + 1) โ
(โคโฅโ๐) โ (โคโฅโ(๐ + 1)) โ
(โคโฅโ๐)) |
60 | | ssralv 4049 |
. . . . . . . . . 10
โข
((โคโฅโ(๐ + 1)) โ
(โคโฅโ๐) โ (โ๐ โ (โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ โ๐ โ (โคโฅโ(๐ + 1))(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
61 | 58, 59, 60 | 3syl 18 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ)
โ (โ๐ โ
(โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ โ๐ โ (โคโฅโ(๐ + 1))(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
62 | | oveq1 7412 |
. . . . . . . . . . 11
โข ((๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ ((๐ pCnt (!โ๐)) + (๐ pCnt (๐ + 1))) = (ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) + (๐ pCnt (๐ + 1)))) |
63 | | simpll 765 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ๐ โ โ0) |
64 | | facp1 14234 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ (!โ(๐ + 1)) =
((!โ๐) ยท
(๐ + 1))) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (!โ(๐ + 1)) = ((!โ๐) ยท (๐ + 1))) |
66 | 65 | oveq2d 7421 |
. . . . . . . . . . . . 13
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ pCnt (!โ(๐ + 1))) = (๐ pCnt ((!โ๐) ยท (๐ + 1)))) |
67 | | simplr 767 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ๐ โ โ) |
68 | | faccl 14239 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
69 | | nnz 12575 |
. . . . . . . . . . . . . . . 16
โข
((!โ๐) โ
โ โ (!โ๐)
โ โค) |
70 | | nnne0 12242 |
. . . . . . . . . . . . . . . 16
โข
((!โ๐) โ
โ โ (!โ๐)
โ 0) |
71 | 69, 70 | jca 512 |
. . . . . . . . . . . . . . 15
โข
((!โ๐) โ
โ โ ((!โ๐)
โ โค โง (!โ๐) โ 0)) |
72 | 63, 68, 71 | 3syl 18 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((!โ๐) โ โค โง (!โ๐) โ 0)) |
73 | | nn0p1nn 12507 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
74 | | nnz 12575 |
. . . . . . . . . . . . . . . 16
โข ((๐ + 1) โ โ โ
(๐ + 1) โ
โค) |
75 | | nnne0 12242 |
. . . . . . . . . . . . . . . 16
โข ((๐ + 1) โ โ โ
(๐ + 1) โ
0) |
76 | 74, 75 | jca 512 |
. . . . . . . . . . . . . . 15
โข ((๐ + 1) โ โ โ
((๐ + 1) โ โค
โง (๐ + 1) โ
0)) |
77 | 63, 73, 76 | 3syl 18 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐ + 1) โ โค โง (๐ + 1) โ 0)) |
78 | | pcmul 16780 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง
((!โ๐) โ โค
โง (!โ๐) โ 0)
โง ((๐ + 1) โ
โค โง (๐ + 1) โ
0)) โ (๐ pCnt
((!โ๐) ยท
(๐ + 1))) = ((๐ pCnt (!โ๐)) + (๐ pCnt (๐ + 1)))) |
79 | 67, 72, 77, 78 | syl3anc 1371 |
. . . . . . . . . . . . 13
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ pCnt ((!โ๐) ยท (๐ + 1))) = ((๐ pCnt (!โ๐)) + (๐ pCnt (๐ + 1)))) |
80 | 66, 79 | eqtr2d 2773 |
. . . . . . . . . . . 12
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐ pCnt (!โ๐)) + (๐ pCnt (๐ + 1))) = (๐ pCnt (!โ(๐ + 1)))) |
81 | 63 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ๐ โ โ0) |
82 | 81 | nn0zd 12580 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ๐ โ โค) |
83 | | prmnn 16607 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ ๐ โ
โ) |
84 | 83 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ๐ โ โ) |
85 | | nnexpcl 14036 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โ
โ) |
86 | 84, 39, 85 | syl2an 596 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (๐โ๐) โ โ) |
87 | | fldivp1 16826 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง (๐โ๐) โ โ) โ
((โโ((๐ + 1) /
(๐โ๐))) โ (โโ(๐ / (๐โ๐)))) = if((๐โ๐) โฅ (๐ + 1), 1, 0)) |
88 | 82, 86, 87 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ((โโ((๐ + 1) / (๐โ๐))) โ (โโ(๐ / (๐โ๐)))) = if((๐โ๐) โฅ (๐ + 1), 1, 0)) |
89 | | elfzuz 13493 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (1...๐) โ ๐ โ
(โคโฅโ1)) |
90 | 63, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ + 1) โ โ) |
91 | 67, 90 | pccld 16779 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ pCnt (๐ + 1)) โ
โ0) |
92 | 91 | nn0zd 12580 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ pCnt (๐ + 1)) โ โค) |
93 | | elfz5 13489 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ
(โคโฅโ1) โง (๐ pCnt (๐ + 1)) โ โค) โ (๐ โ (1...(๐ pCnt (๐ + 1))) โ ๐ โค (๐ pCnt (๐ + 1)))) |
94 | 89, 92, 93 | syl2anr 597 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (๐ โ (1...(๐ pCnt (๐ + 1))) โ ๐ โค (๐ pCnt (๐ + 1)))) |
95 | | simpllr 774 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ๐ โ โ) |
96 | 81, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (๐ + 1) โ โ) |
97 | 96 | nnzd 12581 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (๐ + 1) โ โค) |
98 | 39 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ๐ โ โ0) |
99 | | pcdvdsb 16798 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง (๐ + 1) โ โค โง ๐ โ โ0)
โ (๐ โค (๐ pCnt (๐ + 1)) โ (๐โ๐) โฅ (๐ + 1))) |
100 | 95, 97, 98, 99 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (๐ โค (๐ pCnt (๐ + 1)) โ (๐โ๐) โฅ (๐ + 1))) |
101 | 94, 100 | bitr2d 279 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ((๐โ๐) โฅ (๐ + 1) โ ๐ โ (1...(๐ pCnt (๐ + 1))))) |
102 | 101 | ifbid 4550 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ if((๐โ๐) โฅ (๐ + 1), 1, 0) = if(๐ โ (1...(๐ pCnt (๐ + 1))), 1, 0)) |
103 | 88, 102 | eqtrd 2772 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ((โโ((๐ + 1) / (๐โ๐))) โ (โโ(๐ / (๐โ๐)))) = if(๐ โ (1...(๐ pCnt (๐ + 1))), 1, 0)) |
104 | 103 | sumeq2dv 15645 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (1...๐)((โโ((๐ + 1) / (๐โ๐))) โ (โโ(๐ / (๐โ๐)))) = ฮฃ๐ โ (1...๐)if(๐ โ (1...(๐ pCnt (๐ + 1))), 1, 0)) |
105 | | fzfid 13934 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (1...๐) โ Fin) |
106 | 63 | nn0red 12529 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ๐ โ โ) |
107 | | peano2re 11383 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ (๐ + 1) โ
โ) |
108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ + 1) โ โ) |
109 | 108 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (๐ + 1) โ โ) |
110 | 109, 86 | nndivred 12262 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ((๐ + 1) / (๐โ๐)) โ โ) |
111 | 110 | flcld 13759 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (โโ((๐ + 1) / (๐โ๐))) โ โค) |
112 | 111 | zcnd 12663 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (โโ((๐ + 1) / (๐โ๐))) โ โ) |
113 | 106 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ๐ โ โ) |
114 | 113, 86 | nndivred 12262 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (๐ / (๐โ๐)) โ โ) |
115 | 114 | flcld 13759 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (โโ(๐ / (๐โ๐))) โ โค) |
116 | 115 | zcnd 12663 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (โโ(๐ / (๐โ๐))) โ โ) |
117 | 105, 112,
116 | fsumsub 15730 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (1...๐)((โโ((๐ + 1) / (๐โ๐))) โ (โโ(๐ / (๐โ๐)))) = (ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))) โ ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
118 | | fzfi 13933 |
. . . . . . . . . . . . . . . 16
โข
(1...๐) โ
Fin |
119 | 91 | nn0red 12529 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ pCnt (๐ + 1)) โ โ) |
120 | | eluzelz 12828 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ
(โคโฅโ(๐ + 1)) โ ๐ โ โค) |
121 | 120 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ๐ โ โค) |
122 | 121 | zred 12662 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ๐ โ โ) |
123 | | prmuz2 16629 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
124 | 123 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ๐ โ
(โคโฅโ2)) |
125 | 90 | nnnn0d 12528 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ + 1) โ
โ0) |
126 | | bernneq3 14190 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ
(โคโฅโ2) โง (๐ + 1) โ โ0) โ
(๐ + 1) < (๐โ(๐ + 1))) |
127 | 124, 125,
126 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ + 1) < (๐โ(๐ + 1))) |
128 | 119, 108 | letrid 11362 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐ pCnt (๐ + 1)) โค (๐ + 1) โจ (๐ + 1) โค (๐ pCnt (๐ + 1)))) |
129 | 128 | ord 862 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (ยฌ (๐ pCnt (๐ + 1)) โค (๐ + 1) โ (๐ + 1) โค (๐ pCnt (๐ + 1)))) |
130 | 90 | nnzd 12581 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ + 1) โ โค) |
131 | | pcdvdsb 16798 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ โ โง (๐ + 1) โ โค โง
(๐ + 1) โ
โ0) โ ((๐ + 1) โค (๐ pCnt (๐ + 1)) โ (๐โ(๐ + 1)) โฅ (๐ + 1))) |
132 | 67, 130, 125, 131 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐ + 1) โค (๐ pCnt (๐ + 1)) โ (๐โ(๐ + 1)) โฅ (๐ + 1))) |
133 | 84, 125 | nnexpcld 14204 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐โ(๐ + 1)) โ โ) |
134 | 133 | nnzd 12581 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐โ(๐ + 1)) โ โค) |
135 | | dvdsle 16249 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐โ(๐ + 1)) โ โค โง (๐ + 1) โ โ) โ
((๐โ(๐ + 1)) โฅ (๐ + 1) โ (๐โ(๐ + 1)) โค (๐ + 1))) |
136 | 134, 90, 135 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐โ(๐ + 1)) โฅ (๐ + 1) โ (๐โ(๐ + 1)) โค (๐ + 1))) |
137 | 133 | nnred 12223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐โ(๐ + 1)) โ โ) |
138 | 137, 108 | lenltd 11356 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐โ(๐ + 1)) โค (๐ + 1) โ ยฌ (๐ + 1) < (๐โ(๐ + 1)))) |
139 | 136, 138 | sylibd 238 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐โ(๐ + 1)) โฅ (๐ + 1) โ ยฌ (๐ + 1) < (๐โ(๐ + 1)))) |
140 | 132, 139 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐ + 1) โค (๐ pCnt (๐ + 1)) โ ยฌ (๐ + 1) < (๐โ(๐ + 1)))) |
141 | 129, 140 | syld 47 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (ยฌ (๐ pCnt (๐ + 1)) โค (๐ + 1) โ ยฌ (๐ + 1) < (๐โ(๐ + 1)))) |
142 | 127, 141 | mt4d 117 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ pCnt (๐ + 1)) โค (๐ + 1)) |
143 | | eluzle 12831 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ
(โคโฅโ(๐ + 1)) โ (๐ + 1) โค ๐) |
144 | 143 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ + 1) โค ๐) |
145 | 119, 108,
122, 142, 144 | letrd 11367 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ pCnt (๐ + 1)) โค ๐) |
146 | | eluz 12832 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ pCnt (๐ + 1)) โ โค โง ๐ โ โค) โ (๐ โ
(โคโฅโ(๐ pCnt (๐ + 1))) โ (๐ pCnt (๐ + 1)) โค ๐)) |
147 | 92, 121, 146 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ โ (โคโฅโ(๐ pCnt (๐ + 1))) โ (๐ pCnt (๐ + 1)) โค ๐)) |
148 | 145, 147 | mpbird 256 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ๐ โ (โคโฅโ(๐ pCnt (๐ + 1)))) |
149 | | fzss2 13537 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ
(โคโฅโ(๐ pCnt (๐ + 1))) โ (1...(๐ pCnt (๐ + 1))) โ (1...๐)) |
150 | 148, 149 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (1...(๐ pCnt (๐ + 1))) โ (1...๐)) |
151 | | sumhash 16825 |
. . . . . . . . . . . . . . . 16
โข
(((1...๐) โ Fin
โง (1...(๐ pCnt (๐ + 1))) โ (1...๐)) โ ฮฃ๐ โ (1...๐)if(๐ โ (1...(๐ pCnt (๐ + 1))), 1, 0) = (โฏโ(1...(๐ pCnt (๐ + 1))))) |
152 | 118, 150,
151 | sylancr 587 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (1...๐)if(๐ โ (1...(๐ pCnt (๐ + 1))), 1, 0) = (โฏโ(1...(๐ pCnt (๐ + 1))))) |
153 | | hashfz1 14302 |
. . . . . . . . . . . . . . . 16
โข ((๐ pCnt (๐ + 1)) โ โ0 โ
(โฏโ(1...(๐ pCnt
(๐ + 1)))) = (๐ pCnt (๐ + 1))) |
154 | 91, 153 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (โฏโ(1...(๐ pCnt (๐ + 1)))) = (๐ pCnt (๐ + 1))) |
155 | 152, 154 | eqtrd 2772 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (1...๐)if(๐ โ (1...(๐ pCnt (๐ + 1))), 1, 0) = (๐ pCnt (๐ + 1))) |
156 | 104, 117,
155 | 3eqtr3d 2780 |
. . . . . . . . . . . . 13
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))) โ ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) = (๐ pCnt (๐ + 1))) |
157 | 105, 112 | fsumcl 15675 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))) โ โ) |
158 | 105, 116 | fsumcl 15675 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ โ) |
159 | 119 | recnd 11238 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ pCnt (๐ + 1)) โ โ) |
160 | 157, 158,
159 | subaddd 11585 |
. . . . . . . . . . . . 13
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))) โ ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) = (๐ pCnt (๐ + 1)) โ (ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) + (๐ pCnt (๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))))) |
161 | 156, 160 | mpbid 231 |
. . . . . . . . . . . 12
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) + (๐ pCnt (๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐)))) |
162 | 80, 161 | eqeq12d 2748 |
. . . . . . . . . . 11
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (((๐ pCnt (!โ๐)) + (๐ pCnt (๐ + 1))) = (ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) + (๐ pCnt (๐ + 1))) โ (๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))))) |
163 | 62, 162 | imbitrid 243 |
. . . . . . . . . 10
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ (๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))))) |
164 | 163 | ralimdva 3167 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ)
โ (โ๐ โ
(โคโฅโ(๐ + 1))(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ โ๐ โ (โคโฅโ(๐ + 1))(๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))))) |
165 | 61, 164 | syld 47 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ)
โ (โ๐ โ
(โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ โ๐ โ (โคโฅโ(๐ + 1))(๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))))) |
166 | 165 | ex 413 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ โ โ
โ (โ๐ โ
(โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ โ๐ โ (โคโฅโ(๐ + 1))(๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐)))))) |
167 | 166 | a2d 29 |
. . . . . 6
โข (๐ โ โ0
โ ((๐ โ โ
โ โ๐ โ
(โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) โ (๐ โ โ โ โ๐ โ
(โคโฅโ(๐ + 1))(๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐)))))) |
168 | 8, 16, 24, 32, 53, 167 | nn0ind 12653 |
. . . . 5
โข (๐ โ โ0
โ (๐ โ โ
โ โ๐ โ
(โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
169 | 168 | imp 407 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ โ)
โ โ๐ โ
(โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) |
170 | | oveq2 7413 |
. . . . . . 7
โข (๐ = ๐ โ (1...๐) = (1...๐)) |
171 | 170 | sumeq1d 15643 |
. . . . . 6
โข (๐ = ๐ โ ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) |
172 | 171 | eqeq2d 2743 |
. . . . 5
โข (๐ = ๐ โ ((๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ (๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
173 | 172 | rspcv 3608 |
. . . 4
โข (๐ โ
(โคโฅโ๐) โ (โ๐ โ (โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ (๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
174 | 169, 173 | syl5 34 |
. . 3
โข (๐ โ
(โคโฅโ๐) โ ((๐ โ โ0 โง ๐ โ โ) โ (๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
175 | 174 | 3impib 1116 |
. 2
โข ((๐ โ
(โคโฅโ๐) โง ๐ โ โ0 โง ๐ โ โ) โ (๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) |
176 | 175 | 3com12 1123 |
1
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐) โง ๐ โ โ) โ (๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) |