Step | Hyp | Ref
| Expression |
1 | | fwddifnp1.1 |
. . . . . . 7
β’ (π β π β
β0) |
2 | | elfzelz 13450 |
. . . . . . 7
β’ (π β (0...(π + 1)) β π β β€) |
3 | | bcpasc 14230 |
. . . . . . 7
β’ ((π β β0
β§ π β β€)
β ((πCπ) + (πC(π β 1))) = ((π + 1)Cπ)) |
4 | 1, 2, 3 | syl2an 597 |
. . . . . 6
β’ ((π β§ π β (0...(π + 1))) β ((πCπ) + (πC(π β 1))) = ((π + 1)Cπ)) |
5 | 4 | oveq1d 7376 |
. . . . 5
β’ ((π β§ π β (0...(π + 1))) β (((πCπ) + (πC(π β 1))) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π)))) = (((π + 1)Cπ) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π))))) |
6 | | bccl 14231 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π β β€)
β (πCπ) β
β0) |
7 | 1, 2, 6 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(π + 1))) β (πCπ) β
β0) |
8 | 7 | nn0cnd 12483 |
. . . . . . . . 9
β’ ((π β§ π β (0...(π + 1))) β (πCπ) β β) |
9 | | peano2zm 12554 |
. . . . . . . . . . . 12
β’ (π β β€ β (π β 1) β
β€) |
10 | 2, 9 | syl 17 |
. . . . . . . . . . 11
β’ (π β (0...(π + 1)) β (π β 1) β β€) |
11 | | bccl 14231 |
. . . . . . . . . . 11
β’ ((π β β0
β§ (π β 1) β
β€) β (πC(π β 1)) β
β0) |
12 | 1, 10, 11 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(π + 1))) β (πC(π β 1)) β
β0) |
13 | 12 | nn0cnd 12483 |
. . . . . . . . 9
β’ ((π β§ π β (0...(π + 1))) β (πC(π β 1)) β β) |
14 | 8, 13 | addcomd 11365 |
. . . . . . . 8
β’ ((π β§ π β (0...(π + 1))) β ((πCπ) + (πC(π β 1))) = ((πC(π β 1)) + (πCπ))) |
15 | 14 | oveq1d 7376 |
. . . . . . 7
β’ ((π β§ π β (0...(π + 1))) β (((πCπ) + (πC(π β 1))) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π)))) = (((πC(π β 1)) + (πCπ)) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π))))) |
16 | | peano2nn0 12461 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (π + 1) β
β0) |
17 | 1, 16 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (π + 1) β
β0) |
18 | 17 | nn0zd 12533 |
. . . . . . . . . . . 12
β’ (π β (π + 1) β β€) |
19 | | zsubcl 12553 |
. . . . . . . . . . . 12
β’ (((π + 1) β β€ β§ π β β€) β ((π + 1) β π) β β€) |
20 | 18, 2, 19 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(π + 1))) β ((π + 1) β π) β β€) |
21 | | m1expcl 14001 |
. . . . . . . . . . 11
β’ (((π + 1) β π) β β€ β (-1β((π + 1) β π)) β β€) |
22 | 20, 21 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(π + 1))) β (-1β((π + 1) β π)) β β€) |
23 | 22 | zcnd 12616 |
. . . . . . . . 9
β’ ((π β§ π β (0...(π + 1))) β (-1β((π + 1) β π)) β β) |
24 | | fwddifnp1.3 |
. . . . . . . . . . 11
β’ (π β πΉ:π΄βΆβ) |
25 | 24 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(π + 1))) β πΉ:π΄βΆβ) |
26 | | fwddifnp1.5 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(π + 1))) β (π + π) β π΄) |
27 | 25, 26 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ ((π β§ π β (0...(π + 1))) β (πΉβ(π + π)) β β) |
28 | 23, 27 | mulcld 11183 |
. . . . . . . 8
β’ ((π β§ π β (0...(π + 1))) β ((-1β((π + 1) β π)) Β· (πΉβ(π + π))) β β) |
29 | 13, 8, 28 | adddird 11188 |
. . . . . . 7
β’ ((π β§ π β (0...(π + 1))) β (((πC(π β 1)) + (πCπ)) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π)))) = (((πC(π β 1)) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π)))) + ((πCπ) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π)))))) |
30 | 15, 29 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π β (0...(π + 1))) β (((πCπ) + (πC(π β 1))) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π)))) = (((πC(π β 1)) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π)))) + ((πCπ) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π)))))) |
31 | 1 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(π + 1))) β π β
β0) |
32 | 31 | nn0cnd 12483 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(π + 1))) β π β β) |
33 | 2 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(π + 1))) β π β β€) |
34 | 33 | zcnd 12616 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(π + 1))) β π β β) |
35 | | 1cnd 11158 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(π + 1))) β 1 β
β) |
36 | 32, 34, 35 | subsub3d 11550 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(π + 1))) β (π β (π β 1)) = ((π + 1) β π)) |
37 | 36 | eqcomd 2739 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(π + 1))) β ((π + 1) β π) = (π β (π β 1))) |
38 | 37 | oveq2d 7377 |
. . . . . . . . 9
β’ ((π β§ π β (0...(π + 1))) β (-1β((π + 1) β π)) = (-1β(π β (π β 1)))) |
39 | 38 | oveq1d 7376 |
. . . . . . . 8
β’ ((π β§ π β (0...(π + 1))) β ((-1β((π + 1) β π)) Β· (πΉβ(π + π))) = ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) |
40 | 39 | oveq2d 7377 |
. . . . . . 7
β’ ((π β§ π β (0...(π + 1))) β ((πC(π β 1)) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π)))) = ((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π))))) |
41 | 32, 35, 34 | addsubd 11541 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(π + 1))) β ((π + 1) β π) = ((π β π) + 1)) |
42 | 41 | oveq2d 7377 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(π + 1))) β (-1β((π + 1) β π)) = (-1β((π β π) + 1))) |
43 | | neg1cn 12275 |
. . . . . . . . . . . . . . 15
β’ -1 β
β |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(π + 1))) β -1 β
β) |
45 | | neg1ne0 12277 |
. . . . . . . . . . . . . . 15
β’ -1 β
0 |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(π + 1))) β -1 β 0) |
47 | 1 | nn0zd 12533 |
. . . . . . . . . . . . . . 15
β’ (π β π β β€) |
48 | | zsubcl 12553 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β€) β (π β π) β β€) |
49 | 47, 2, 48 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(π + 1))) β (π β π) β β€) |
50 | 44, 46, 49 | expp1zd 14069 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(π + 1))) β (-1β((π β π) + 1)) = ((-1β(π β π)) Β· -1)) |
51 | 42, 50 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(π + 1))) β (-1β((π + 1) β π)) = ((-1β(π β π)) Β· -1)) |
52 | | m1expcl 14001 |
. . . . . . . . . . . . . . 15
β’ ((π β π) β β€ β (-1β(π β π)) β β€) |
53 | 49, 52 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(π + 1))) β (-1β(π β π)) β β€) |
54 | 53 | zcnd 12616 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(π + 1))) β (-1β(π β π)) β β) |
55 | 54, 44 | mulcomd 11184 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(π + 1))) β ((-1β(π β π)) Β· -1) = (-1 Β·
(-1β(π β π)))) |
56 | 54 | mulm1d 11615 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(π + 1))) β (-1 Β· (-1β(π β π))) = -(-1β(π β π))) |
57 | 51, 55, 56 | 3eqtrd 2777 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(π + 1))) β (-1β((π + 1) β π)) = -(-1β(π β π))) |
58 | 57 | oveq1d 7376 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(π + 1))) β ((-1β((π + 1) β π)) Β· (πΉβ(π + π))) = (-(-1β(π β π)) Β· (πΉβ(π + π)))) |
59 | 54, 27 | mulneg1d 11616 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(π + 1))) β (-(-1β(π β π)) Β· (πΉβ(π + π))) = -((-1β(π β π)) Β· (πΉβ(π + π)))) |
60 | 58, 59 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β§ π β (0...(π + 1))) β ((-1β((π + 1) β π)) Β· (πΉβ(π + π))) = -((-1β(π β π)) Β· (πΉβ(π + π)))) |
61 | 60 | oveq2d 7377 |
. . . . . . . 8
β’ ((π β§ π β (0...(π + 1))) β ((πCπ) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π)))) = ((πCπ) Β· -((-1β(π β π)) Β· (πΉβ(π + π))))) |
62 | 54, 27 | mulcld 11183 |
. . . . . . . . 9
β’ ((π β§ π β (0...(π + 1))) β ((-1β(π β π)) Β· (πΉβ(π + π))) β β) |
63 | 8, 62 | mulneg2d 11617 |
. . . . . . . 8
β’ ((π β§ π β (0...(π + 1))) β ((πCπ) Β· -((-1β(π β π)) Β· (πΉβ(π + π)))) = -((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π))))) |
64 | 61, 63 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ π β (0...(π + 1))) β ((πCπ) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π)))) = -((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π))))) |
65 | 40, 64 | oveq12d 7379 |
. . . . . 6
β’ ((π β§ π β (0...(π + 1))) β (((πC(π β 1)) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π)))) + ((πCπ) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π))))) = (((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) + -((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))))) |
66 | | zsubcl 12553 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ (π β 1) β β€)
β (π β (π β 1)) β
β€) |
67 | 47, 10, 66 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(π + 1))) β (π β (π β 1)) β β€) |
68 | | m1expcl 14001 |
. . . . . . . . . . 11
β’ ((π β (π β 1)) β β€ β
(-1β(π β (π β 1))) β
β€) |
69 | 67, 68 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(π + 1))) β (-1β(π β (π β 1))) β
β€) |
70 | 69 | zcnd 12616 |
. . . . . . . . 9
β’ ((π β§ π β (0...(π + 1))) β (-1β(π β (π β 1))) β
β) |
71 | 70, 27 | mulcld 11183 |
. . . . . . . 8
β’ ((π β§ π β (0...(π + 1))) β ((-1β(π β (π β 1))) Β· (πΉβ(π + π))) β β) |
72 | 13, 71 | mulcld 11183 |
. . . . . . 7
β’ ((π β§ π β (0...(π + 1))) β ((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) β β) |
73 | 8, 62 | mulcld 11183 |
. . . . . . 7
β’ ((π β§ π β (0...(π + 1))) β ((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))) β β) |
74 | 72, 73 | negsubd 11526 |
. . . . . 6
β’ ((π β§ π β (0...(π + 1))) β (((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) + -((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π))))) = (((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) β ((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))))) |
75 | 30, 65, 74 | 3eqtrd 2777 |
. . . . 5
β’ ((π β§ π β (0...(π + 1))) β (((πCπ) + (πC(π β 1))) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π)))) = (((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) β ((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))))) |
76 | 5, 75 | eqtr3d 2775 |
. . . 4
β’ ((π β§ π β (0...(π + 1))) β (((π + 1)Cπ) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π)))) = (((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) β ((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))))) |
77 | 76 | sumeq2dv 15596 |
. . 3
β’ (π β Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π)))) = Ξ£π β (0...(π + 1))(((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) β ((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))))) |
78 | | fzfid 13887 |
. . . 4
β’ (π β (0...(π + 1)) β Fin) |
79 | 78, 72, 73 | fsumsub 15681 |
. . 3
β’ (π β Ξ£π β (0...(π + 1))(((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) β ((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π))))) = (Ξ£π β (0...(π + 1))((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) β Ξ£π β (0...(π + 1))((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))))) |
80 | | nn0uz 12813 |
. . . . . . . 8
β’
β0 = (β€β₯β0) |
81 | 17, 80 | eleqtrdi 2844 |
. . . . . . 7
β’ (π β (π + 1) β
(β€β₯β0)) |
82 | | oveq1 7368 |
. . . . . . . . 9
β’ (π = 0 β (π β 1) = (0 β 1)) |
83 | 82 | oveq2d 7377 |
. . . . . . . 8
β’ (π = 0 β (πC(π β 1)) = (πC(0 β 1))) |
84 | 82 | oveq2d 7377 |
. . . . . . . . . 10
β’ (π = 0 β (π β (π β 1)) = (π β (0 β 1))) |
85 | 84 | oveq2d 7377 |
. . . . . . . . 9
β’ (π = 0 β (-1β(π β (π β 1))) = (-1β(π β (0 β 1)))) |
86 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π = 0 β (π + π) = (π + 0)) |
87 | 86 | fveq2d 6850 |
. . . . . . . . 9
β’ (π = 0 β (πΉβ(π + π)) = (πΉβ(π + 0))) |
88 | 85, 87 | oveq12d 7379 |
. . . . . . . 8
β’ (π = 0 β ((-1β(π β (π β 1))) Β· (πΉβ(π + π))) = ((-1β(π β (0 β 1))) Β· (πΉβ(π + 0)))) |
89 | 83, 88 | oveq12d 7379 |
. . . . . . 7
β’ (π = 0 β ((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) = ((πC(0 β 1)) Β· ((-1β(π β (0 β 1)))
Β· (πΉβ(π + 0))))) |
90 | 81, 72, 89 | fsum1p 15646 |
. . . . . 6
β’ (π β Ξ£π β (0...(π + 1))((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) = (((πC(0 β 1)) Β· ((-1β(π β (0 β 1)))
Β· (πΉβ(π + 0)))) + Ξ£π β ((0 + 1)...(π + 1))((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))))) |
91 | | df-neg 11396 |
. . . . . . . . . . 11
β’ -1 = (0
β 1) |
92 | 91 | oveq2i 7372 |
. . . . . . . . . 10
β’ (πC-1) = (πC(0 β 1)) |
93 | | bcneg1 34372 |
. . . . . . . . . . 11
β’ (π β β0
β (πC-1) =
0) |
94 | 1, 93 | syl 17 |
. . . . . . . . . 10
β’ (π β (πC-1) = 0) |
95 | 92, 94 | eqtr3id 2787 |
. . . . . . . . 9
β’ (π β (πC(0 β 1)) = 0) |
96 | 95 | oveq1d 7376 |
. . . . . . . 8
β’ (π β ((πC(0 β 1)) Β· ((-1β(π β (0 β 1)))
Β· (πΉβ(π + 0)))) = (0 Β·
((-1β(π β (0
β 1))) Β· (πΉβ(π + 0))))) |
97 | | 0z 12518 |
. . . . . . . . . . . . . . 15
β’ 0 β
β€ |
98 | | 1z 12541 |
. . . . . . . . . . . . . . 15
β’ 1 β
β€ |
99 | | zsubcl 12553 |
. . . . . . . . . . . . . . 15
β’ ((0
β β€ β§ 1 β β€) β (0 β 1) β
β€) |
100 | 97, 98, 99 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ (0
β 1) β β€ |
101 | 100 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (0 β 1) β
β€) |
102 | 47, 101 | zsubcld 12620 |
. . . . . . . . . . . 12
β’ (π β (π β (0 β 1)) β
β€) |
103 | | m1expcl 14001 |
. . . . . . . . . . . 12
β’ ((π β (0 β 1)) β
β€ β (-1β(π
β (0 β 1))) β β€) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . 11
β’ (π β (-1β(π β (0 β 1))) β
β€) |
105 | 104 | zcnd 12616 |
. . . . . . . . . 10
β’ (π β (-1β(π β (0 β 1))) β
β) |
106 | | eluzfz1 13457 |
. . . . . . . . . . . . 13
β’ ((π + 1) β
(β€β₯β0) β 0 β (0...(π + 1))) |
107 | 81, 106 | syl 17 |
. . . . . . . . . . . 12
β’ (π β 0 β (0...(π + 1))) |
108 | 26 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ (π β βπ β (0...(π + 1))(π + π) β π΄) |
109 | 86 | eleq1d 2819 |
. . . . . . . . . . . . 13
β’ (π = 0 β ((π + π) β π΄ β (π + 0) β π΄)) |
110 | 109 | rspcva 3581 |
. . . . . . . . . . . 12
β’ ((0
β (0...(π + 1)) β§
βπ β
(0...(π + 1))(π + π) β π΄) β (π + 0) β π΄) |
111 | 107, 108,
110 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (π + 0) β π΄) |
112 | 24, 111 | ffvelcdmd 7040 |
. . . . . . . . . 10
β’ (π β (πΉβ(π + 0)) β β) |
113 | 105, 112 | mulcld 11183 |
. . . . . . . . 9
β’ (π β ((-1β(π β (0 β 1)))
Β· (πΉβ(π + 0))) β
β) |
114 | 113 | mul02d 11361 |
. . . . . . . 8
β’ (π β (0 Β·
((-1β(π β (0
β 1))) Β· (πΉβ(π + 0)))) = 0) |
115 | 96, 114 | eqtrd 2773 |
. . . . . . 7
β’ (π β ((πC(0 β 1)) Β· ((-1β(π β (0 β 1)))
Β· (πΉβ(π + 0)))) = 0) |
116 | 115 | oveq1d 7376 |
. . . . . 6
β’ (π β (((πC(0 β 1)) Β· ((-1β(π β (0 β 1)))
Β· (πΉβ(π + 0)))) + Ξ£π β ((0 + 1)...(π + 1))((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π))))) = (0 + Ξ£π β ((0 + 1)...(π + 1))((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))))) |
117 | | fzfid 13887 |
. . . . . . . 8
β’ (π β ((0 + 1)...(π + 1)) β
Fin) |
118 | | olc 867 |
. . . . . . . . . 10
β’ (π β ((0 + 1)...(π + 1)) β (π = 0 β¨ π β ((0 + 1)...(π + 1)))) |
119 | | elfzp12 13529 |
. . . . . . . . . . . 12
β’ ((π + 1) β
(β€β₯β0) β (π β (0...(π + 1)) β (π = 0 β¨ π β ((0 + 1)...(π + 1))))) |
120 | 81, 119 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π β (0...(π + 1)) β (π = 0 β¨ π β ((0 + 1)...(π + 1))))) |
121 | 120 | biimpar 479 |
. . . . . . . . . 10
β’ ((π β§ (π = 0 β¨ π β ((0 + 1)...(π + 1)))) β π β (0...(π + 1))) |
122 | 118, 121 | sylan2 594 |
. . . . . . . . 9
β’ ((π β§ π β ((0 + 1)...(π + 1))) β π β (0...(π + 1))) |
123 | 122, 72 | syldan 592 |
. . . . . . . 8
β’ ((π β§ π β ((0 + 1)...(π + 1))) β ((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) β β) |
124 | 117, 123 | fsumcl 15626 |
. . . . . . 7
β’ (π β Ξ£π β ((0 + 1)...(π + 1))((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) β β) |
125 | 124 | addlidd 11364 |
. . . . . 6
β’ (π β (0 + Ξ£π β ((0 + 1)...(π + 1))((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π))))) = Ξ£π β ((0 + 1)...(π + 1))((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π))))) |
126 | 90, 116, 125 | 3eqtrd 2777 |
. . . . 5
β’ (π β Ξ£π β (0...(π + 1))((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) = Ξ£π β ((0 + 1)...(π + 1))((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π))))) |
127 | | fwddifnp1.4 |
. . . . . . . . . . 11
β’ (π β π β β) |
128 | 127 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β ((0 + 1)...(π + 1))) β π β β) |
129 | | 1cnd 11158 |
. . . . . . . . . 10
β’ ((π β§ π β ((0 + 1)...(π + 1))) β 1 β
β) |
130 | | elfzelz 13450 |
. . . . . . . . . . . 12
β’ (π β ((0 + 1)...(π + 1)) β π β β€) |
131 | 130 | zcnd 12616 |
. . . . . . . . . . 11
β’ (π β ((0 + 1)...(π + 1)) β π β β) |
132 | 131 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β ((0 + 1)...(π + 1))) β π β β) |
133 | 128, 129,
132 | ppncand 11560 |
. . . . . . . . 9
β’ ((π β§ π β ((0 + 1)...(π + 1))) β ((π + 1) + (π β 1)) = (π + π)) |
134 | 133 | fveq2d 6850 |
. . . . . . . 8
β’ ((π β§ π β ((0 + 1)...(π + 1))) β (πΉβ((π + 1) + (π β 1))) = (πΉβ(π + π))) |
135 | 134 | oveq2d 7377 |
. . . . . . 7
β’ ((π β§ π β ((0 + 1)...(π + 1))) β ((-1β(π β (π β 1))) Β· (πΉβ((π + 1) + (π β 1)))) = ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) |
136 | 135 | oveq2d 7377 |
. . . . . 6
β’ ((π β§ π β ((0 + 1)...(π + 1))) β ((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ((π + 1) + (π β 1))))) = ((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π))))) |
137 | 136 | sumeq2dv 15596 |
. . . . 5
β’ (π β Ξ£π β ((0 + 1)...(π + 1))((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ((π + 1) + (π β 1))))) = Ξ£π β ((0 + 1)...(π + 1))((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π))))) |
138 | | 1zzd 12542 |
. . . . . . 7
β’ (π β 1 β
β€) |
139 | | 0zd 12519 |
. . . . . . 7
β’ (π β 0 β
β€) |
140 | | elfzelz 13450 |
. . . . . . . . 9
β’ (π β (0...π) β π β β€) |
141 | | bccl 14231 |
. . . . . . . . . 10
β’ ((π β β0
β§ π β β€)
β (πCπ) β
β0) |
142 | 141 | nn0cnd 12483 |
. . . . . . . . 9
β’ ((π β β0
β§ π β β€)
β (πCπ) β
β) |
143 | 1, 140, 142 | syl2an 597 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β (πCπ) β β) |
144 | | zsubcl 12553 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β€) β (π β π) β β€) |
145 | 47, 140, 144 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π)) β (π β π) β β€) |
146 | | m1expcl 14001 |
. . . . . . . . . . 11
β’ ((π β π) β β€ β (-1β(π β π)) β β€) |
147 | 145, 146 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β (-1β(π β π)) β β€) |
148 | 147 | zcnd 12616 |
. . . . . . . . 9
β’ ((π β§ π β (0...π)) β (-1β(π β π)) β β) |
149 | 24 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β πΉ:π΄βΆβ) |
150 | 127 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...π)) β π β β) |
151 | | 1cnd 11158 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...π)) β 1 β β) |
152 | 140 | zcnd 12616 |
. . . . . . . . . . . . . 14
β’ (π β (0...π) β π β β) |
153 | 152 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...π)) β π β β) |
154 | 150, 151,
153 | addassd 11185 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π)) β ((π + 1) + π) = (π + (1 + π))) |
155 | 151, 153 | addcomd 11365 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...π)) β (1 + π) = (π + 1)) |
156 | 155 | oveq2d 7377 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π)) β (π + (1 + π)) = (π + (π + 1))) |
157 | 154, 156 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π)) β ((π + 1) + π) = (π + (π + 1))) |
158 | | fzp1elp1 13503 |
. . . . . . . . . . . 12
β’ (π β (0...π) β (π + 1) β (0...(π + 1))) |
159 | | oveq2 7369 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β (π + π) = (π + (π + 1))) |
160 | 159 | eleq1d 2819 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β ((π + π) β π΄ β (π + (π + 1)) β π΄)) |
161 | 160 | rspccv 3580 |
. . . . . . . . . . . . . 14
β’
(βπ β
(0...(π + 1))(π + π) β π΄ β ((π + 1) β (0...(π + 1)) β (π + (π + 1)) β π΄)) |
162 | 108, 161 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β ((π + 1) β (0...(π + 1)) β (π + (π + 1)) β π΄)) |
163 | 162 | imp 408 |
. . . . . . . . . . . 12
β’ ((π β§ (π + 1) β (0...(π + 1))) β (π + (π + 1)) β π΄) |
164 | 158, 163 | sylan2 594 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π)) β (π + (π + 1)) β π΄) |
165 | 157, 164 | eqeltrd 2834 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β ((π + 1) + π) β π΄) |
166 | 149, 165 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ ((π β§ π β (0...π)) β (πΉβ((π + 1) + π)) β β) |
167 | 148, 166 | mulcld 11183 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β ((-1β(π β π)) Β· (πΉβ((π + 1) + π))) β β) |
168 | 143, 167 | mulcld 11183 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β ((πCπ) Β· ((-1β(π β π)) Β· (πΉβ((π + 1) + π)))) β β) |
169 | | oveq2 7369 |
. . . . . . . 8
β’ (π = (π β 1) β (πCπ) = (πC(π β 1))) |
170 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π = (π β 1) β (π β π) = (π β (π β 1))) |
171 | 170 | oveq2d 7377 |
. . . . . . . . 9
β’ (π = (π β 1) β (-1β(π β π)) = (-1β(π β (π β 1)))) |
172 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π = (π β 1) β ((π + 1) + π) = ((π + 1) + (π β 1))) |
173 | 172 | fveq2d 6850 |
. . . . . . . . 9
β’ (π = (π β 1) β (πΉβ((π + 1) + π)) = (πΉβ((π + 1) + (π β 1)))) |
174 | 171, 173 | oveq12d 7379 |
. . . . . . . 8
β’ (π = (π β 1) β ((-1β(π β π)) Β· (πΉβ((π + 1) + π))) = ((-1β(π β (π β 1))) Β· (πΉβ((π + 1) + (π β 1))))) |
175 | 169, 174 | oveq12d 7379 |
. . . . . . 7
β’ (π = (π β 1) β ((πCπ) Β· ((-1β(π β π)) Β· (πΉβ((π + 1) + π)))) = ((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ((π + 1) + (π β 1)))))) |
176 | 138, 139,
47, 168, 175 | fsumshft 15673 |
. . . . . 6
β’ (π β Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ((π + 1) + π)))) = Ξ£π β ((0 + 1)...(π + 1))((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ((π + 1) + (π β 1)))))) |
177 | | oveq2 7369 |
. . . . . . . 8
β’ (π = π β (πCπ) = (πCπ)) |
178 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π = π β (π β π) = (π β π)) |
179 | 178 | oveq2d 7377 |
. . . . . . . . 9
β’ (π = π β (-1β(π β π)) = (-1β(π β π))) |
180 | | oveq2 7369 |
. . . . . . . . . 10
β’ (π = π β ((π + 1) + π) = ((π + 1) + π)) |
181 | 180 | fveq2d 6850 |
. . . . . . . . 9
β’ (π = π β (πΉβ((π + 1) + π)) = (πΉβ((π + 1) + π))) |
182 | 179, 181 | oveq12d 7379 |
. . . . . . . 8
β’ (π = π β ((-1β(π β π)) Β· (πΉβ((π + 1) + π))) = ((-1β(π β π)) Β· (πΉβ((π + 1) + π)))) |
183 | 177, 182 | oveq12d 7379 |
. . . . . . 7
β’ (π = π β ((πCπ) Β· ((-1β(π β π)) Β· (πΉβ((π + 1) + π)))) = ((πCπ) Β· ((-1β(π β π)) Β· (πΉβ((π + 1) + π))))) |
184 | 183 | cbvsumv 15589 |
. . . . . 6
β’
Ξ£π β
(0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ((π + 1) + π)))) = Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ((π + 1) + π)))) |
185 | 176, 184 | eqtr3di 2788 |
. . . . 5
β’ (π β Ξ£π β ((0 + 1)...(π + 1))((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ((π + 1) + (π β 1))))) = Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ((π + 1) + π))))) |
186 | 126, 137,
185 | 3eqtr2d 2779 |
. . . 4
β’ (π β Ξ£π β (0...(π + 1))((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) = Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ((π + 1) + π))))) |
187 | 1, 80 | eleqtrdi 2844 |
. . . . . 6
β’ (π β π β
(β€β₯β0)) |
188 | | oveq2 7369 |
. . . . . . 7
β’ (π = (π + 1) β (πCπ) = (πC(π + 1))) |
189 | | oveq2 7369 |
. . . . . . . . 9
β’ (π = (π + 1) β (π β π) = (π β (π + 1))) |
190 | 189 | oveq2d 7377 |
. . . . . . . 8
β’ (π = (π + 1) β (-1β(π β π)) = (-1β(π β (π + 1)))) |
191 | | oveq2 7369 |
. . . . . . . . 9
β’ (π = (π + 1) β (π + π) = (π + (π + 1))) |
192 | 191 | fveq2d 6850 |
. . . . . . . 8
β’ (π = (π + 1) β (πΉβ(π + π)) = (πΉβ(π + (π + 1)))) |
193 | 190, 192 | oveq12d 7379 |
. . . . . . 7
β’ (π = (π + 1) β ((-1β(π β π)) Β· (πΉβ(π + π))) = ((-1β(π β (π + 1))) Β· (πΉβ(π + (π + 1))))) |
194 | 188, 193 | oveq12d 7379 |
. . . . . 6
β’ (π = (π + 1) β ((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))) = ((πC(π + 1)) Β· ((-1β(π β (π + 1))) Β· (πΉβ(π + (π + 1)))))) |
195 | 187, 73, 194 | fsump1 15649 |
. . . . 5
β’ (π β Ξ£π β (0...(π + 1))((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))) = (Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))) + ((πC(π + 1)) Β· ((-1β(π β (π + 1))) Β· (πΉβ(π + (π + 1))))))) |
196 | | bcval 14213 |
. . . . . . . . . 10
β’ ((π β β0
β§ (π + 1) β
β€) β (πC(π + 1)) = if((π + 1) β (0...π), ((!βπ) / ((!β(π β (π + 1))) Β· (!β(π + 1)))), 0)) |
197 | 1, 18, 196 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (πC(π + 1)) = if((π + 1) β (0...π), ((!βπ) / ((!β(π β (π + 1))) Β· (!β(π + 1)))), 0)) |
198 | | fzp1nel 13534 |
. . . . . . . . . 10
β’ Β¬
(π + 1) β (0...π) |
199 | 198 | iffalsei 4500 |
. . . . . . . . 9
β’ if((π + 1) β (0...π), ((!βπ) / ((!β(π β (π + 1))) Β· (!β(π + 1)))), 0) = 0 |
200 | 197, 199 | eqtrdi 2789 |
. . . . . . . 8
β’ (π β (πC(π + 1)) = 0) |
201 | 200 | oveq1d 7376 |
. . . . . . 7
β’ (π β ((πC(π + 1)) Β· ((-1β(π β (π + 1))) Β· (πΉβ(π + (π + 1))))) = (0 Β· ((-1β(π β (π + 1))) Β· (πΉβ(π + (π + 1)))))) |
202 | 47, 18 | zsubcld 12620 |
. . . . . . . . . 10
β’ (π β (π β (π + 1)) β β€) |
203 | | m1expcl 14001 |
. . . . . . . . . . 11
β’ ((π β (π + 1)) β β€ β (-1β(π β (π + 1))) β β€) |
204 | 203 | zcnd 12616 |
. . . . . . . . . 10
β’ ((π β (π + 1)) β β€ β (-1β(π β (π + 1))) β β) |
205 | 202, 204 | syl 17 |
. . . . . . . . 9
β’ (π β (-1β(π β (π + 1))) β β) |
206 | | eluzfz2 13458 |
. . . . . . . . . . . 12
β’ ((π + 1) β
(β€β₯β0) β (π + 1) β (0...(π + 1))) |
207 | 81, 206 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π + 1) β (0...(π + 1))) |
208 | 191 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π = (π + 1) β ((π + π) β π΄ β (π + (π + 1)) β π΄)) |
209 | 208 | rspcv 3579 |
. . . . . . . . . . 11
β’ ((π + 1) β (0...(π + 1)) β (βπ β (0...(π + 1))(π + π) β π΄ β (π + (π + 1)) β π΄)) |
210 | 207, 108,
209 | sylc 65 |
. . . . . . . . . 10
β’ (π β (π + (π + 1)) β π΄) |
211 | 24, 210 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ (π β (πΉβ(π + (π + 1))) β β) |
212 | 205, 211 | mulcld 11183 |
. . . . . . . 8
β’ (π β ((-1β(π β (π + 1))) Β· (πΉβ(π + (π + 1)))) β β) |
213 | 212 | mul02d 11361 |
. . . . . . 7
β’ (π β (0 Β·
((-1β(π β (π + 1))) Β· (πΉβ(π + (π + 1))))) = 0) |
214 | 201, 213 | eqtrd 2773 |
. . . . . 6
β’ (π β ((πC(π + 1)) Β· ((-1β(π β (π + 1))) Β· (πΉβ(π + (π + 1))))) = 0) |
215 | 214 | oveq2d 7377 |
. . . . 5
β’ (π β (Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))) + ((πC(π + 1)) Β· ((-1β(π β (π + 1))) Β· (πΉβ(π + (π + 1)))))) = (Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))) + 0)) |
216 | | fzfid 13887 |
. . . . . . 7
β’ (π β (0...π) β Fin) |
217 | | fzelp1 13502 |
. . . . . . . 8
β’ (π β (0...π) β π β (0...(π + 1))) |
218 | 217, 73 | sylan2 594 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β ((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))) β β) |
219 | 216, 218 | fsumcl 15626 |
. . . . . 6
β’ (π β Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))) β β) |
220 | 219 | addridd 11363 |
. . . . 5
β’ (π β (Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))) + 0) = Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π))))) |
221 | 195, 215,
220 | 3eqtrd 2777 |
. . . 4
β’ (π β Ξ£π β (0...(π + 1))((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))) = Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π))))) |
222 | 186, 221 | oveq12d 7379 |
. . 3
β’ (π β (Ξ£π β (0...(π + 1))((πC(π β 1)) Β· ((-1β(π β (π β 1))) Β· (πΉβ(π + π)))) β Ξ£π β (0...(π + 1))((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π))))) = (Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ((π + 1) + π)))) β Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))))) |
223 | 77, 79, 222 | 3eqtrd 2777 |
. 2
β’ (π β Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π)))) = (Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ((π + 1) + π)))) β Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))))) |
224 | | fwddifnp1.2 |
. . 3
β’ (π β π΄ β β) |
225 | 17, 224, 24, 127, 26 | fwddifnval 34801 |
. 2
β’ (π β (((π + 1) β³n πΉ)βπ) = Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· ((-1β((π + 1) β π)) Β· (πΉβ(π + π))))) |
226 | | peano2cn 11335 |
. . . . 5
β’ (π β β β (π + 1) β
β) |
227 | 127, 226 | syl 17 |
. . . 4
β’ (π β (π + 1) β β) |
228 | 127 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β π β β) |
229 | | 1cnd 11158 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β 1 β β) |
230 | | elfzelz 13450 |
. . . . . . . . 9
β’ (π β (0...π) β π β β€) |
231 | 230 | zcnd 12616 |
. . . . . . . 8
β’ (π β (0...π) β π β β) |
232 | 231 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β π β β) |
233 | 228, 229,
232 | addassd 11185 |
. . . . . 6
β’ ((π β§ π β (0...π)) β ((π + 1) + π) = (π + (1 + π))) |
234 | 229, 232 | addcomd 11365 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β (1 + π) = (π + 1)) |
235 | 234 | oveq2d 7377 |
. . . . . 6
β’ ((π β§ π β (0...π)) β (π + (1 + π)) = (π + (π + 1))) |
236 | 233, 235 | eqtrd 2773 |
. . . . 5
β’ ((π β§ π β (0...π)) β ((π + 1) + π) = (π + (π + 1))) |
237 | | fzp1elp1 13503 |
. . . . . 6
β’ (π β (0...π) β (π + 1) β (0...(π + 1))) |
238 | | oveq1 7368 |
. . . . . . . . . 10
β’ (π = π β (π + 1) = (π + 1)) |
239 | 238 | eleq1d 2819 |
. . . . . . . . 9
β’ (π = π β ((π + 1) β (0...(π + 1)) β (π + 1) β (0...(π + 1)))) |
240 | 239 | anbi2d 630 |
. . . . . . . 8
β’ (π = π β ((π β§ (π + 1) β (0...(π + 1))) β (π β§ (π + 1) β (0...(π + 1))))) |
241 | 238 | oveq2d 7377 |
. . . . . . . . 9
β’ (π = π β (π + (π + 1)) = (π + (π + 1))) |
242 | 241 | eleq1d 2819 |
. . . . . . . 8
β’ (π = π β ((π + (π + 1)) β π΄ β (π + (π + 1)) β π΄)) |
243 | 240, 242 | imbi12d 345 |
. . . . . . 7
β’ (π = π β (((π β§ (π + 1) β (0...(π + 1))) β (π + (π + 1)) β π΄) β ((π β§ (π + 1) β (0...(π + 1))) β (π + (π + 1)) β π΄))) |
244 | 243, 163 | chvarvv 2003 |
. . . . . 6
β’ ((π β§ (π + 1) β (0...(π + 1))) β (π + (π + 1)) β π΄) |
245 | 237, 244 | sylan2 594 |
. . . . 5
β’ ((π β§ π β (0...π)) β (π + (π + 1)) β π΄) |
246 | 236, 245 | eqeltrd 2834 |
. . . 4
β’ ((π β§ π β (0...π)) β ((π + 1) + π) β π΄) |
247 | 1, 224, 24, 227, 246 | fwddifnval 34801 |
. . 3
β’ (π β ((π β³n πΉ)β(π + 1)) = Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ((π + 1) + π))))) |
248 | 217, 26 | sylan2 594 |
. . . 4
β’ ((π β§ π β (0...π)) β (π + π) β π΄) |
249 | 1, 224, 24, 127, 248 | fwddifnval 34801 |
. . 3
β’ (π β ((π β³n πΉ)βπ) = Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π))))) |
250 | 247, 249 | oveq12d 7379 |
. 2
β’ (π β (((π β³n πΉ)β(π + 1)) β ((π β³n πΉ)βπ)) = (Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ((π + 1) + π)))) β Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))))) |
251 | 223, 225,
250 | 3eqtr4d 2783 |
1
β’ (π β (((π + 1) β³n πΉ)βπ) = (((π β³n πΉ)β(π + 1)) β ((π β³n πΉ)βπ))) |