Step | Hyp | Ref
| Expression |
1 | | fveq2 5515 |
. . . . . . . 8
โข (๐ฅ = 0 โ
(โคโฅโ๐ฅ) =
(โคโฅโ0)) |
2 | | fveq2 5515 |
. . . . . . . . . 10
โข (๐ฅ = 0 โ (!โ๐ฅ) =
(!โ0)) |
3 | 2 | oveq2d 5890 |
. . . . . . . . 9
โข (๐ฅ = 0 โ (๐ pCnt (!โ๐ฅ)) = (๐ pCnt (!โ0))) |
4 | | fvoveq1 5897 |
. . . . . . . . . 10
โข (๐ฅ = 0 โ
(โโ(๐ฅ / (๐โ๐))) = (โโ(0 / (๐โ๐)))) |
5 | 4 | sumeq2sdv 11377 |
. . . . . . . . 9
โข (๐ฅ = 0 โ ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) = ฮฃ๐ โ (1...๐)(โโ(0 / (๐โ๐)))) |
6 | 3, 5 | eqeq12d 2192 |
. . . . . . . 8
โข (๐ฅ = 0 โ ((๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) โ (๐ pCnt (!โ0)) = ฮฃ๐ โ (1...๐)(โโ(0 / (๐โ๐))))) |
7 | 1, 6 | raleqbidv 2684 |
. . . . . . 7
โข (๐ฅ = 0 โ (โ๐ โ
(โคโฅโ๐ฅ)(๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) โ โ๐ โ
(โคโฅโ0)(๐ pCnt (!โ0)) = ฮฃ๐ โ (1...๐)(โโ(0 / (๐โ๐))))) |
8 | 7 | imbi2d 230 |
. . . . . 6
โข (๐ฅ = 0 โ ((๐ โ โ โ โ๐ โ
(โคโฅโ๐ฅ)(๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐)))) โ (๐ โ โ โ โ๐ โ
(โคโฅโ0)(๐ pCnt (!โ0)) = ฮฃ๐ โ (1...๐)(โโ(0 / (๐โ๐)))))) |
9 | | fveq2 5515 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (โคโฅโ๐ฅ) =
(โคโฅโ๐)) |
10 | | fveq2 5515 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (!โ๐ฅ) = (!โ๐)) |
11 | 10 | oveq2d 5890 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ (๐ pCnt (!โ๐ฅ)) = (๐ pCnt (!โ๐))) |
12 | | fvoveq1 5897 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (โโ(๐ฅ / (๐โ๐))) = (โโ(๐ / (๐โ๐)))) |
13 | 12 | sumeq2sdv 11377 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) |
14 | 11, 13 | eqeq12d 2192 |
. . . . . . . 8
โข (๐ฅ = ๐ โ ((๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) โ (๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
15 | 9, 14 | raleqbidv 2684 |
. . . . . . 7
โข (๐ฅ = ๐ โ (โ๐ โ (โคโฅโ๐ฅ)(๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) โ โ๐ โ (โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
16 | 15 | imbi2d 230 |
. . . . . 6
โข (๐ฅ = ๐ โ ((๐ โ โ โ โ๐ โ
(โคโฅโ๐ฅ)(๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐)))) โ (๐ โ โ โ โ๐ โ
(โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))))) |
17 | | fveq2 5515 |
. . . . . . . 8
โข (๐ฅ = (๐ + 1) โ
(โคโฅโ๐ฅ) = (โคโฅโ(๐ + 1))) |
18 | | fveq2 5515 |
. . . . . . . . . 10
โข (๐ฅ = (๐ + 1) โ (!โ๐ฅ) = (!โ(๐ + 1))) |
19 | 18 | oveq2d 5890 |
. . . . . . . . 9
โข (๐ฅ = (๐ + 1) โ (๐ pCnt (!โ๐ฅ)) = (๐ pCnt (!โ(๐ + 1)))) |
20 | | fvoveq1 5897 |
. . . . . . . . . 10
โข (๐ฅ = (๐ + 1) โ (โโ(๐ฅ / (๐โ๐))) = (โโ((๐ + 1) / (๐โ๐)))) |
21 | 20 | sumeq2sdv 11377 |
. . . . . . . . 9
โข (๐ฅ = (๐ + 1) โ ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐)))) |
22 | 19, 21 | eqeq12d 2192 |
. . . . . . . 8
โข (๐ฅ = (๐ + 1) โ ((๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) โ (๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))))) |
23 | 17, 22 | raleqbidv 2684 |
. . . . . . 7
โข (๐ฅ = (๐ + 1) โ (โ๐ โ (โคโฅโ๐ฅ)(๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) โ โ๐ โ (โคโฅโ(๐ + 1))(๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))))) |
24 | 23 | imbi2d 230 |
. . . . . 6
โข (๐ฅ = (๐ + 1) โ ((๐ โ โ โ โ๐ โ
(โคโฅโ๐ฅ)(๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐)))) โ (๐ โ โ โ โ๐ โ
(โคโฅโ(๐ + 1))(๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐)))))) |
25 | | fveq2 5515 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (โคโฅโ๐ฅ) =
(โคโฅโ๐)) |
26 | | fveq2 5515 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (!โ๐ฅ) = (!โ๐)) |
27 | 26 | oveq2d 5890 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ (๐ pCnt (!โ๐ฅ)) = (๐ pCnt (!โ๐))) |
28 | | fvoveq1 5897 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (โโ(๐ฅ / (๐โ๐))) = (โโ(๐ / (๐โ๐)))) |
29 | 28 | sumeq2sdv 11377 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) |
30 | 27, 29 | eqeq12d 2192 |
. . . . . . . 8
โข (๐ฅ = ๐ โ ((๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) โ (๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
31 | 25, 30 | raleqbidv 2684 |
. . . . . . 7
โข (๐ฅ = ๐ โ (โ๐ โ (โคโฅโ๐ฅ)(๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐))) โ โ๐ โ (โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
32 | 31 | imbi2d 230 |
. . . . . 6
โข (๐ฅ = ๐ โ ((๐ โ โ โ โ๐ โ
(โคโฅโ๐ฅ)(๐ pCnt (!โ๐ฅ)) = ฮฃ๐ โ (1...๐)(โโ(๐ฅ / (๐โ๐)))) โ (๐ โ โ โ โ๐ โ
(โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))))) |
33 | | 1zzd 9279 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ
(โคโฅโ0)) โ 1 โ โค) |
34 | | eluzelz 9536 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ0) โ ๐ โ โค) |
35 | 34 | adantl 277 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ
(โคโฅโ0)) โ ๐ โ โค) |
36 | 33, 35 | fzfigd 10430 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ
(โคโฅโ0)) โ (1...๐) โ Fin) |
37 | | isumz 11396 |
. . . . . . . . . 10
โข (((1
โ โค โง (1...๐) โ (โคโฅโ1)
โง โ๐ โ
(โคโฅโ1)DECID ๐ โ (1...๐)) โจ (1...๐) โ Fin) โ ฮฃ๐ โ (1...๐)0 = 0) |
38 | 37 | olcs 736 |
. . . . . . . . 9
โข
((1...๐) โ Fin
โ ฮฃ๐ โ
(1...๐)0 =
0) |
39 | 36, 38 | syl 14 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ
(โคโฅโ0)) โ ฮฃ๐ โ (1...๐)0 = 0) |
40 | | 0nn0 9190 |
. . . . . . . . . 10
โข 0 โ
โ0 |
41 | | elfznn 10053 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ ๐ โ โ) |
42 | 41 | nnnn0d 9228 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ ๐ โ โ0) |
43 | | nn0uz 9561 |
. . . . . . . . . . . 12
โข
โ0 = (โคโฅโ0) |
44 | 42, 43 | eleqtrdi 2270 |
. . . . . . . . . . 11
โข (๐ โ (1...๐) โ ๐ โ
(โคโฅโ0)) |
45 | 44 | adantl 277 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ
(โคโฅโ0)) โง ๐ โ (1...๐)) โ ๐ โ
(โคโฅโ0)) |
46 | | simpll 527 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ
(โคโฅโ0)) โง ๐ โ (1...๐)) โ ๐ โ โ) |
47 | | pcfaclem 12346 |
. . . . . . . . . 10
โข ((0
โ โ0 โง ๐ โ (โคโฅโ0)
โง ๐ โ โ)
โ (โโ(0 / (๐โ๐))) = 0) |
48 | 40, 45, 46, 47 | mp3an2i 1342 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ
(โคโฅโ0)) โง ๐ โ (1...๐)) โ (โโ(0 / (๐โ๐))) = 0) |
49 | 48 | sumeq2dv 11375 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ
(โคโฅโ0)) โ ฮฃ๐ โ (1...๐)(โโ(0 / (๐โ๐))) = ฮฃ๐ โ (1...๐)0) |
50 | | fac0 10707 |
. . . . . . . . . . 11
โข
(!โ0) = 1 |
51 | 50 | oveq2i 5885 |
. . . . . . . . . 10
โข (๐ pCnt (!โ0)) = (๐ pCnt 1) |
52 | | pc1 12304 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ pCnt 1) = 0) |
53 | 51, 52 | eqtrid 2222 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ pCnt (!โ0)) =
0) |
54 | 53 | adantr 276 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ
(โคโฅโ0)) โ (๐ pCnt (!โ0)) = 0) |
55 | 39, 49, 54 | 3eqtr4rd 2221 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ
(โคโฅโ0)) โ (๐ pCnt (!โ0)) = ฮฃ๐ โ (1...๐)(โโ(0 / (๐โ๐)))) |
56 | 55 | ralrimiva 2550 |
. . . . . 6
โข (๐ โ โ โ
โ๐ โ
(โคโฅโ0)(๐ pCnt (!โ0)) = ฮฃ๐ โ (1...๐)(โโ(0 / (๐โ๐)))) |
57 | | nn0z 9272 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ๐ โ
โค) |
58 | 57 | adantr 276 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
โค) |
59 | | uzid 9541 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ
(โคโฅโ๐)) |
60 | | peano2uz 9582 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ๐) โ (๐ + 1) โ
(โคโฅโ๐)) |
61 | 58, 59, 60 | 3syl 17 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ + 1) โ
(โคโฅโ๐)) |
62 | | uzss 9547 |
. . . . . . . . . 10
โข ((๐ + 1) โ
(โคโฅโ๐) โ (โคโฅโ(๐ + 1)) โ
(โคโฅโ๐)) |
63 | | ssralv 3219 |
. . . . . . . . . 10
โข
((โคโฅโ(๐ + 1)) โ
(โคโฅโ๐) โ (โ๐ โ (โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ โ๐ โ (โคโฅโ(๐ + 1))(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
64 | 61, 62, 63 | 3syl 17 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ)
โ (โ๐ โ
(โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ โ๐ โ (โคโฅโ(๐ + 1))(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
65 | | oveq1 5881 |
. . . . . . . . . . 11
โข ((๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ ((๐ pCnt (!โ๐)) + (๐ pCnt (๐ + 1))) = (ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) + (๐ pCnt (๐ + 1)))) |
66 | | simpll 527 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ๐ โ โ0) |
67 | | facp1 10709 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ (!โ(๐ + 1)) =
((!โ๐) ยท
(๐ + 1))) |
68 | 66, 67 | syl 14 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (!โ(๐ + 1)) = ((!โ๐) ยท (๐ + 1))) |
69 | 68 | oveq2d 5890 |
. . . . . . . . . . . . 13
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ pCnt (!โ(๐ + 1))) = (๐ pCnt ((!โ๐) ยท (๐ + 1)))) |
70 | | simplr 528 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ๐ โ โ) |
71 | | faccl 10714 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
72 | | nnz 9271 |
. . . . . . . . . . . . . . . 16
โข
((!โ๐) โ
โ โ (!โ๐)
โ โค) |
73 | | nnne0 8946 |
. . . . . . . . . . . . . . . 16
โข
((!โ๐) โ
โ โ (!โ๐)
โ 0) |
74 | 72, 73 | jca 306 |
. . . . . . . . . . . . . . 15
โข
((!โ๐) โ
โ โ ((!โ๐)
โ โค โง (!โ๐) โ 0)) |
75 | 66, 71, 74 | 3syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((!โ๐) โ โค โง (!โ๐) โ 0)) |
76 | | nn0p1nn 9214 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
77 | | nnz 9271 |
. . . . . . . . . . . . . . . 16
โข ((๐ + 1) โ โ โ
(๐ + 1) โ
โค) |
78 | | nnne0 8946 |
. . . . . . . . . . . . . . . 16
โข ((๐ + 1) โ โ โ
(๐ + 1) โ
0) |
79 | 77, 78 | jca 306 |
. . . . . . . . . . . . . . 15
โข ((๐ + 1) โ โ โ
((๐ + 1) โ โค
โง (๐ + 1) โ
0)) |
80 | 66, 76, 79 | 3syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐ + 1) โ โค โง (๐ + 1) โ 0)) |
81 | | pcmul 12300 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง
((!โ๐) โ โค
โง (!โ๐) โ 0)
โง ((๐ + 1) โ
โค โง (๐ + 1) โ
0)) โ (๐ pCnt
((!โ๐) ยท
(๐ + 1))) = ((๐ pCnt (!โ๐)) + (๐ pCnt (๐ + 1)))) |
82 | 70, 75, 80, 81 | syl3anc 1238 |
. . . . . . . . . . . . 13
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ pCnt ((!โ๐) ยท (๐ + 1))) = ((๐ pCnt (!โ๐)) + (๐ pCnt (๐ + 1)))) |
83 | 69, 82 | eqtr2d 2211 |
. . . . . . . . . . . 12
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐ pCnt (!โ๐)) + (๐ pCnt (๐ + 1))) = (๐ pCnt (!โ(๐ + 1)))) |
84 | 66 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ๐ โ โ0) |
85 | 84 | nn0zd 9372 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ๐ โ โค) |
86 | | prmnn 12109 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ ๐ โ
โ) |
87 | 86 | ad2antlr 489 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ๐ โ โ) |
88 | | nnexpcl 10532 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โ
โ) |
89 | 87, 42, 88 | syl2an 289 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (๐โ๐) โ โ) |
90 | | fldivp1 12345 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง (๐โ๐) โ โ) โ
((โโ((๐ + 1) /
(๐โ๐))) โ (โโ(๐ / (๐โ๐)))) = if((๐โ๐) โฅ (๐ + 1), 1, 0)) |
91 | 85, 89, 90 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ((โโ((๐ + 1) / (๐โ๐))) โ (โโ(๐ / (๐โ๐)))) = if((๐โ๐) โฅ (๐ + 1), 1, 0)) |
92 | | elfzuz 10020 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (1...๐) โ ๐ โ
(โคโฅโ1)) |
93 | 66, 76 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ + 1) โ โ) |
94 | 70, 93 | pccld 12299 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ pCnt (๐ + 1)) โ
โ0) |
95 | 94 | nn0zd 9372 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ pCnt (๐ + 1)) โ โค) |
96 | | elfz5 10016 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ
(โคโฅโ1) โง (๐ pCnt (๐ + 1)) โ โค) โ (๐ โ (1...(๐ pCnt (๐ + 1))) โ ๐ โค (๐ pCnt (๐ + 1)))) |
97 | 92, 95, 96 | syl2anr 290 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (๐ โ (1...(๐ pCnt (๐ + 1))) โ ๐ โค (๐ pCnt (๐ + 1)))) |
98 | | simpllr 534 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ๐ โ โ) |
99 | 84, 76 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (๐ + 1) โ โ) |
100 | 99 | nnzd 9373 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (๐ + 1) โ โค) |
101 | 42 | adantl 277 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ๐ โ โ0) |
102 | | pcdvdsb 12318 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง (๐ + 1) โ โค โง ๐ โ โ0)
โ (๐ โค (๐ pCnt (๐ + 1)) โ (๐โ๐) โฅ (๐ + 1))) |
103 | 98, 100, 101, 102 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (๐ โค (๐ pCnt (๐ + 1)) โ (๐โ๐) โฅ (๐ + 1))) |
104 | 97, 103 | bitr2d 189 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ((๐โ๐) โฅ (๐ + 1) โ ๐ โ (1...(๐ pCnt (๐ + 1))))) |
105 | 104 | ifbid 3555 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ if((๐โ๐) โฅ (๐ + 1), 1, 0) = if(๐ โ (1...(๐ pCnt (๐ + 1))), 1, 0)) |
106 | 91, 105 | eqtrd 2210 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ((โโ((๐ + 1) / (๐โ๐))) โ (โโ(๐ / (๐โ๐)))) = if(๐ โ (1...(๐ pCnt (๐ + 1))), 1, 0)) |
107 | 106 | sumeq2dv 11375 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (1...๐)((โโ((๐ + 1) / (๐โ๐))) โ (โโ(๐ / (๐โ๐)))) = ฮฃ๐ โ (1...๐)if(๐ โ (1...(๐ pCnt (๐ + 1))), 1, 0)) |
108 | | 1zzd 9279 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ 1 โ
โค) |
109 | | eluzelz 9536 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ
(โคโฅโ(๐ + 1)) โ ๐ โ โค) |
110 | 109 | adantl 277 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ๐ โ โค) |
111 | 108, 110 | fzfigd 10430 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (1...๐) โ Fin) |
112 | | znq 9623 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ + 1) โ โค โง
(๐โ๐) โ โ) โ ((๐ + 1) / (๐โ๐)) โ โ) |
113 | 100, 89, 112 | syl2anc 411 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ((๐ + 1) / (๐โ๐)) โ โ) |
114 | 113 | flqcld 10276 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (โโ((๐ + 1) / (๐โ๐))) โ โค) |
115 | 114 | zcnd 9375 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (โโ((๐ + 1) / (๐โ๐))) โ โ) |
116 | | znq 9623 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง (๐โ๐) โ โ) โ (๐ / (๐โ๐)) โ โ) |
117 | 85, 89, 116 | syl2anc 411 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (๐ / (๐โ๐)) โ โ) |
118 | 117 | flqcld 10276 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (โโ(๐ / (๐โ๐))) โ โค) |
119 | 118 | zcnd 9375 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (โโ(๐ / (๐โ๐))) โ โ) |
120 | 111, 115,
119 | fsumsub 11459 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (1...๐)((โโ((๐ + 1) / (๐โ๐))) โ (โโ(๐ / (๐โ๐)))) = (ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))) โ ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
121 | 94 | nn0red 9229 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ pCnt (๐ + 1)) โ โ) |
122 | 66 | nn0red 9229 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ๐ โ โ) |
123 | | peano2re 8092 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ (๐ + 1) โ
โ) |
124 | 122, 123 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ + 1) โ โ) |
125 | 110 | zred 9374 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ๐ โ โ) |
126 | 93 | nnzd 9373 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ + 1) โ โค) |
127 | | zdcle 9328 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ pCnt (๐ + 1)) โ โค โง (๐ + 1) โ โค) โ
DECID (๐
pCnt (๐ + 1)) โค (๐ + 1)) |
128 | 95, 126, 127 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ DECID (๐ pCnt (๐ + 1)) โค (๐ + 1)) |
129 | | zletric 9296 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ pCnt (๐ + 1)) โ โค โง (๐ + 1) โ โค) โ
((๐ pCnt (๐ + 1)) โค (๐ + 1) โจ (๐ + 1) โค (๐ pCnt (๐ + 1)))) |
130 | 95, 126, 129 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐ pCnt (๐ + 1)) โค (๐ + 1) โจ (๐ + 1) โค (๐ pCnt (๐ + 1)))) |
131 | 130 | ord 724 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (ยฌ (๐ pCnt (๐ + 1)) โค (๐ + 1) โ (๐ + 1) โค (๐ pCnt (๐ + 1)))) |
132 | 93 | nnnn0d 9228 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ + 1) โ
โ0) |
133 | | pcdvdsb 12318 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ โ โง (๐ + 1) โ โค โง
(๐ + 1) โ
โ0) โ ((๐ + 1) โค (๐ pCnt (๐ + 1)) โ (๐โ(๐ + 1)) โฅ (๐ + 1))) |
134 | 70, 126, 132, 133 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐ + 1) โค (๐ pCnt (๐ + 1)) โ (๐โ(๐ + 1)) โฅ (๐ + 1))) |
135 | 87, 132 | nnexpcld 10675 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐โ(๐ + 1)) โ โ) |
136 | 135 | nnzd 9373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐โ(๐ + 1)) โ โค) |
137 | | dvdsle 11849 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐โ(๐ + 1)) โ โค โง (๐ + 1) โ โ) โ
((๐โ(๐ + 1)) โฅ (๐ + 1) โ (๐โ(๐ + 1)) โค (๐ + 1))) |
138 | 136, 93, 137 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐โ(๐ + 1)) โฅ (๐ + 1) โ (๐โ(๐ + 1)) โค (๐ + 1))) |
139 | 135 | nnred 8931 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐โ(๐ + 1)) โ โ) |
140 | 139, 124 | lenltd 8074 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐โ(๐ + 1)) โค (๐ + 1) โ ยฌ (๐ + 1) < (๐โ(๐ + 1)))) |
141 | 138, 140 | sylibd 149 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐โ(๐ + 1)) โฅ (๐ + 1) โ ยฌ (๐ + 1) < (๐โ(๐ + 1)))) |
142 | 134, 141 | sylbid 150 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐ + 1) โค (๐ pCnt (๐ + 1)) โ ยฌ (๐ + 1) < (๐โ(๐ + 1)))) |
143 | 131, 142 | syld 45 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (ยฌ (๐ pCnt (๐ + 1)) โค (๐ + 1) โ ยฌ (๐ + 1) < (๐โ(๐ + 1)))) |
144 | | prmuz2 12130 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
145 | 144 | ad2antlr 489 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ๐ โ
(โคโฅโ2)) |
146 | | bernneq3 10642 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ
(โคโฅโ2) โง (๐ + 1) โ โ0) โ
(๐ + 1) < (๐โ(๐ + 1))) |
147 | 145, 132,
146 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ + 1) < (๐โ(๐ + 1))) |
148 | | condc 853 |
. . . . . . . . . . . . . . . . . . . 20
โข
(DECID (๐ pCnt (๐ + 1)) โค (๐ + 1) โ ((ยฌ (๐ pCnt (๐ + 1)) โค (๐ + 1) โ ยฌ (๐ + 1) < (๐โ(๐ + 1))) โ ((๐ + 1) < (๐โ(๐ + 1)) โ (๐ pCnt (๐ + 1)) โค (๐ + 1)))) |
149 | 128, 143,
147, 148 | syl3c 63 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ pCnt (๐ + 1)) โค (๐ + 1)) |
150 | | eluzle 9539 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ
(โคโฅโ(๐ + 1)) โ (๐ + 1) โค ๐) |
151 | 150 | adantl 277 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ + 1) โค ๐) |
152 | 121, 124,
125, 149, 151 | letrd 8080 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ pCnt (๐ + 1)) โค ๐) |
153 | | eluz 9540 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ pCnt (๐ + 1)) โ โค โง ๐ โ โค) โ (๐ โ
(โคโฅโ(๐ pCnt (๐ + 1))) โ (๐ pCnt (๐ + 1)) โค ๐)) |
154 | 95, 110, 153 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ โ (โคโฅโ(๐ pCnt (๐ + 1))) โ (๐ pCnt (๐ + 1)) โค ๐)) |
155 | 152, 154 | mpbird 167 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ๐ โ (โคโฅโ(๐ pCnt (๐ + 1)))) |
156 | | fzss2 10063 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ
(โคโฅโ(๐ pCnt (๐ + 1))) โ (1...(๐ pCnt (๐ + 1))) โ (1...๐)) |
157 | 155, 156 | syl 14 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (1...(๐ pCnt (๐ + 1))) โ (1...๐)) |
158 | | elfzelz 10024 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (1...๐) โ ๐ โ โค) |
159 | 158 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ ๐ โ โค) |
160 | | 1zzd 9279 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ 1 โ โค) |
161 | 95 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ (๐ pCnt (๐ + 1)) โ โค) |
162 | | fzdcel 10039 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง 1 โ
โค โง (๐ pCnt
(๐ + 1)) โ โค)
โ DECID ๐ โ (1...(๐ pCnt (๐ + 1)))) |
163 | 159, 160,
161, 162 | syl3anc 1238 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โง ๐ โ (1...๐)) โ DECID ๐ โ (1...(๐ pCnt (๐ + 1)))) |
164 | 163 | ralrimiva 2550 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ โ๐ โ (1...๐)DECID ๐ โ (1...(๐ pCnt (๐ + 1)))) |
165 | | sumhashdc 12344 |
. . . . . . . . . . . . . . . 16
โข
(((1...๐) โ Fin
โง (1...(๐ pCnt (๐ + 1))) โ (1...๐) โง โ๐ โ (1...๐)DECID ๐ โ (1...(๐ pCnt (๐ + 1)))) โ ฮฃ๐ โ (1...๐)if(๐ โ (1...(๐ pCnt (๐ + 1))), 1, 0) = (โฏโ(1...(๐ pCnt (๐ + 1))))) |
166 | 111, 157,
164, 165 | syl3anc 1238 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (1...๐)if(๐ โ (1...(๐ pCnt (๐ + 1))), 1, 0) = (โฏโ(1...(๐ pCnt (๐ + 1))))) |
167 | | hashfz1 10762 |
. . . . . . . . . . . . . . . 16
โข ((๐ pCnt (๐ + 1)) โ โ0 โ
(โฏโ(1...(๐ pCnt
(๐ + 1)))) = (๐ pCnt (๐ + 1))) |
168 | 94, 167 | syl 14 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (โฏโ(1...(๐ pCnt (๐ + 1)))) = (๐ pCnt (๐ + 1))) |
169 | 166, 168 | eqtrd 2210 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (1...๐)if(๐ โ (1...(๐ pCnt (๐ + 1))), 1, 0) = (๐ pCnt (๐ + 1))) |
170 | 107, 120,
169 | 3eqtr3d 2218 |
. . . . . . . . . . . . 13
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))) โ ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) = (๐ pCnt (๐ + 1))) |
171 | 111, 115 | fsumcl 11407 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))) โ โ) |
172 | 111, 119 | fsumcl 11407 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ โ) |
173 | 94 | nn0cnd 9230 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (๐ pCnt (๐ + 1)) โ โ) |
174 | 171, 172,
173 | subaddd 8285 |
. . . . . . . . . . . . 13
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))) โ ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) = (๐ pCnt (๐ + 1)) โ (ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) + (๐ pCnt (๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))))) |
175 | 170, 174 | mpbid 147 |
. . . . . . . . . . . 12
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) + (๐ pCnt (๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐)))) |
176 | 83, 175 | eqeq12d 2192 |
. . . . . . . . . . 11
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ (((๐ pCnt (!โ๐)) + (๐ pCnt (๐ + 1))) = (ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) + (๐ pCnt (๐ + 1))) โ (๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))))) |
177 | 65, 176 | imbitrid 154 |
. . . . . . . . . 10
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ
(โคโฅโ(๐ + 1))) โ ((๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ (๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))))) |
178 | 177 | ralimdva 2544 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ)
โ (โ๐ โ
(โคโฅโ(๐ + 1))(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ โ๐ โ (โคโฅโ(๐ + 1))(๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))))) |
179 | 64, 178 | syld 45 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ)
โ (โ๐ โ
(โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ โ๐ โ (โคโฅโ(๐ + 1))(๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐))))) |
180 | 179 | ex 115 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ โ โ
โ (โ๐ โ
(โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ โ๐ โ (โคโฅโ(๐ + 1))(๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐)))))) |
181 | 180 | a2d 26 |
. . . . . 6
โข (๐ โ โ0
โ ((๐ โ โ
โ โ๐ โ
(โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) โ (๐ โ โ โ โ๐ โ
(โคโฅโ(๐ + 1))(๐ pCnt (!โ(๐ + 1))) = ฮฃ๐ โ (1...๐)(โโ((๐ + 1) / (๐โ๐)))))) |
182 | 8, 16, 24, 32, 56, 181 | nn0ind 9366 |
. . . . 5
โข (๐ โ โ0
โ (๐ โ โ
โ โ๐ โ
(โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
183 | 182 | imp 124 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ โ)
โ โ๐ โ
(โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) |
184 | | oveq2 5882 |
. . . . . . 7
โข (๐ = ๐ โ (1...๐) = (1...๐)) |
185 | 184 | sumeq1d 11373 |
. . . . . 6
โข (๐ = ๐ โ ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) |
186 | 185 | eqeq2d 2189 |
. . . . 5
โข (๐ = ๐ โ ((๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ (๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
187 | 186 | rspcv 2837 |
. . . 4
โข (๐ โ
(โคโฅโ๐) โ (โ๐ โ (โคโฅโ๐)(๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))) โ (๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
188 | 183, 187 | syl5 32 |
. . 3
โข (๐ โ
(โคโฅโ๐) โ ((๐ โ โ0 โง ๐ โ โ) โ (๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐))))) |
189 | 188 | 3impib 1201 |
. 2
โข ((๐ โ
(โคโฅโ๐) โง ๐ โ โ0 โง ๐ โ โ) โ (๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) |
190 | 189 | 3com12 1207 |
1
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐) โง ๐ โ โ) โ (๐ pCnt (!โ๐)) = ฮฃ๐ โ (1...๐)(โโ(๐ / (๐โ๐)))) |