Metamath Proof Explorer

Theorem fsumcube

Description: Express the sum of cubes in closed terms. (Contributed by Scott Fenton, 16-Jun-2015)

Ref Expression
Assertion fsumcube ( ๐‘‡ โˆˆ โ„•0 โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘‡ ) ( ๐‘˜ โ†‘ 3 ) = ( ( ( ๐‘‡ โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) / 4 ) )

Proof

Step Hyp Ref Expression
1 3nn0 โŠข 3 โˆˆ โ„•0
2 fsumkthpow โŠข ( ( 3 โˆˆ โ„•0 โˆง ๐‘‡ โˆˆ โ„•0 ) โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘‡ ) ( ๐‘˜ โ†‘ 3 ) = ( ( ( ( 3 + 1 ) BernPoly ( ๐‘‡ + 1 ) ) โˆ’ ( ( 3 + 1 ) BernPoly 0 ) ) / ( 3 + 1 ) ) )
3 1 2 mpan โŠข ( ๐‘‡ โˆˆ โ„•0 โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘‡ ) ( ๐‘˜ โ†‘ 3 ) = ( ( ( ( 3 + 1 ) BernPoly ( ๐‘‡ + 1 ) ) โˆ’ ( ( 3 + 1 ) BernPoly 0 ) ) / ( 3 + 1 ) ) )
4 df-4 โŠข 4 = ( 3 + 1 )
5 4 oveq1i โŠข ( 4 BernPoly ( ๐‘‡ + 1 ) ) = ( ( 3 + 1 ) BernPoly ( ๐‘‡ + 1 ) )
6 4 oveq1i โŠข ( 4 BernPoly 0 ) = ( ( 3 + 1 ) BernPoly 0 )
7 5 6 oveq12i โŠข ( ( 4 BernPoly ( ๐‘‡ + 1 ) ) โˆ’ ( 4 BernPoly 0 ) ) = ( ( ( 3 + 1 ) BernPoly ( ๐‘‡ + 1 ) ) โˆ’ ( ( 3 + 1 ) BernPoly 0 ) )
8 7 4 oveq12i โŠข ( ( ( 4 BernPoly ( ๐‘‡ + 1 ) ) โˆ’ ( 4 BernPoly 0 ) ) / 4 ) = ( ( ( ( 3 + 1 ) BernPoly ( ๐‘‡ + 1 ) ) โˆ’ ( ( 3 + 1 ) BernPoly 0 ) ) / ( 3 + 1 ) )
9 nn0cn โŠข ( ๐‘‡ โˆˆ โ„•0 โ†’ ๐‘‡ โˆˆ โ„‚ )
10 peano2cn โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ๐‘‡ + 1 ) โˆˆ โ„‚ )
11 9 10 syl โŠข ( ๐‘‡ โˆˆ โ„•0 โ†’ ( ๐‘‡ + 1 ) โˆˆ โ„‚ )
12 bpoly4 โŠข ( ( ๐‘‡ + 1 ) โˆˆ โ„‚ โ†’ ( 4 BernPoly ( ๐‘‡ + 1 ) ) = ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 1 / 3 0 ) ) )
13 11 12 syl โŠข ( ๐‘‡ โˆˆ โ„•0 โ†’ ( 4 BernPoly ( ๐‘‡ + 1 ) ) = ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 1 / 3 0 ) ) )
14 4nn โŠข 4 โˆˆ โ„•
15 0exp โŠข ( 4 โˆˆ โ„• โ†’ ( 0 โ†‘ 4 ) = 0 )
16 14 15 ax-mp โŠข ( 0 โ†‘ 4 ) = 0
17 3nn โŠข 3 โˆˆ โ„•
18 0exp โŠข ( 3 โˆˆ โ„• โ†’ ( 0 โ†‘ 3 ) = 0 )
19 17 18 ax-mp โŠข ( 0 โ†‘ 3 ) = 0
20 19 oveq2i โŠข ( 2 ยท ( 0 โ†‘ 3 ) ) = ( 2 ยท 0 )
21 2t0e0 โŠข ( 2 ยท 0 ) = 0
22 20 21 eqtri โŠข ( 2 ยท ( 0 โ†‘ 3 ) ) = 0
23 16 22 oveq12i โŠข ( ( 0 โ†‘ 4 ) โˆ’ ( 2 ยท ( 0 โ†‘ 3 ) ) ) = ( 0 โˆ’ 0 )
24 0m0e0 โŠข ( 0 โˆ’ 0 ) = 0
25 23 24 eqtri โŠข ( ( 0 โ†‘ 4 ) โˆ’ ( 2 ยท ( 0 โ†‘ 3 ) ) ) = 0
26 sq0 โŠข ( 0 โ†‘ 2 ) = 0
27 25 26 oveq12i โŠข ( ( ( 0 โ†‘ 4 ) โˆ’ ( 2 ยท ( 0 โ†‘ 3 ) ) ) + ( 0 โ†‘ 2 ) ) = ( 0 + 0 )
28 00id โŠข ( 0 + 0 ) = 0
29 27 28 eqtri โŠข ( ( ( 0 โ†‘ 4 ) โˆ’ ( 2 ยท ( 0 โ†‘ 3 ) ) ) + ( 0 โ†‘ 2 ) ) = 0
30 29 oveq1i โŠข ( ( ( ( 0 โ†‘ 4 ) โˆ’ ( 2 ยท ( 0 โ†‘ 3 ) ) ) + ( 0 โ†‘ 2 ) ) โˆ’ ( 1 / 3 0 ) ) = ( 0 โˆ’ ( 1 / 3 0 ) )
31 0cn โŠข 0 โˆˆ โ„‚
32 bpoly4 โŠข ( 0 โˆˆ โ„‚ โ†’ ( 4 BernPoly 0 ) = ( ( ( ( 0 โ†‘ 4 ) โˆ’ ( 2 ยท ( 0 โ†‘ 3 ) ) ) + ( 0 โ†‘ 2 ) ) โˆ’ ( 1 / 3 0 ) ) )
33 31 32 ax-mp โŠข ( 4 BernPoly 0 ) = ( ( ( ( 0 โ†‘ 4 ) โˆ’ ( 2 ยท ( 0 โ†‘ 3 ) ) ) + ( 0 โ†‘ 2 ) ) โˆ’ ( 1 / 3 0 ) )
34 df-neg โŠข - ( 1 / 3 0 ) = ( 0 โˆ’ ( 1 / 3 0 ) )
35 30 33 34 3eqtr4i โŠข ( 4 BernPoly 0 ) = - ( 1 / 3 0 )
36 35 a1i โŠข ( ๐‘‡ โˆˆ โ„•0 โ†’ ( 4 BernPoly 0 ) = - ( 1 / 3 0 ) )
37 13 36 oveq12d โŠข ( ๐‘‡ โˆˆ โ„•0 โ†’ ( ( 4 BernPoly ( ๐‘‡ + 1 ) ) โˆ’ ( 4 BernPoly 0 ) ) = ( ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 1 / 3 0 ) ) โˆ’ - ( 1 / 3 0 ) ) )
38 4nn0 โŠข 4 โˆˆ โ„•0
39 expcl โŠข ( ( ( ๐‘‡ + 1 ) โˆˆ โ„‚ โˆง 4 โˆˆ โ„•0 ) โ†’ ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆˆ โ„‚ )
40 38 39 mpan2 โŠข ( ( ๐‘‡ + 1 ) โˆˆ โ„‚ โ†’ ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆˆ โ„‚ )
41 2cn โŠข 2 โˆˆ โ„‚
42 expcl โŠข ( ( ( ๐‘‡ + 1 ) โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0 ) โ†’ ( ( ๐‘‡ + 1 ) โ†‘ 3 ) โˆˆ โ„‚ )
43 1 42 mpan2 โŠข ( ( ๐‘‡ + 1 ) โˆˆ โ„‚ โ†’ ( ( ๐‘‡ + 1 ) โ†‘ 3 ) โˆˆ โ„‚ )
44 mulcl โŠข ( ( 2 โˆˆ โ„‚ โˆง ( ( ๐‘‡ + 1 ) โ†‘ 3 ) โˆˆ โ„‚ ) โ†’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) โˆˆ โ„‚ )
45 41 43 44 sylancr โŠข ( ( ๐‘‡ + 1 ) โˆˆ โ„‚ โ†’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) โˆˆ โ„‚ )
46 40 45 subcld โŠข ( ( ๐‘‡ + 1 ) โˆˆ โ„‚ โ†’ ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) โˆˆ โ„‚ )
47 sqcl โŠข ( ( ๐‘‡ + 1 ) โˆˆ โ„‚ โ†’ ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆˆ โ„‚ )
48 46 47 addcld โŠข ( ( ๐‘‡ + 1 ) โˆˆ โ„‚ โ†’ ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆˆ โ„‚ )
49 10 48 syl โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆˆ โ„‚ )
50 9 49 syl โŠข ( ๐‘‡ โˆˆ โ„•0 โ†’ ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆˆ โ„‚ )
51 0nn0 โŠข 0 โˆˆ โ„•0
52 1 51 deccl โŠข 3 0 โˆˆ โ„•0
53 52 nn0cni โŠข 3 0 โˆˆ โ„‚
54 52 nn0rei โŠข 3 0 โˆˆ โ„
55 10pos โŠข 0 < 1 0
56 17 51 51 55 declti โŠข 0 < 3 0
57 54 56 gt0ne0ii โŠข 3 0 โ‰  0
58 53 57 reccli โŠข ( 1 / 3 0 ) โˆˆ โ„‚
59 subcl โŠข ( ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆˆ โ„‚ โˆง ( 1 / 3 0 ) โˆˆ โ„‚ ) โ†’ ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 1 / 3 0 ) ) โˆˆ โ„‚ )
60 50 58 59 sylancl โŠข ( ๐‘‡ โˆˆ โ„•0 โ†’ ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 1 / 3 0 ) ) โˆˆ โ„‚ )
61 subneg โŠข ( ( ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 1 / 3 0 ) ) โˆˆ โ„‚ โˆง ( 1 / 3 0 ) โˆˆ โ„‚ ) โ†’ ( ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 1 / 3 0 ) ) โˆ’ - ( 1 / 3 0 ) ) = ( ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 1 / 3 0 ) ) + ( 1 / 3 0 ) ) )
62 60 58 61 sylancl โŠข ( ๐‘‡ โˆˆ โ„•0 โ†’ ( ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 1 / 3 0 ) ) โˆ’ - ( 1 / 3 0 ) ) = ( ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 1 / 3 0 ) ) + ( 1 / 3 0 ) ) )
63 npcan โŠข ( ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆˆ โ„‚ โˆง ( 1 / 3 0 ) โˆˆ โ„‚ ) โ†’ ( ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 1 / 3 0 ) ) + ( 1 / 3 0 ) ) = ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) )
64 49 58 63 sylancl โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 1 / 3 0 ) ) + ( 1 / 3 0 ) ) = ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) )
65 9 64 syl โŠข ( ๐‘‡ โˆˆ โ„•0 โ†’ ( ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 1 / 3 0 ) ) + ( 1 / 3 0 ) ) = ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) )
66 2p2e4 โŠข ( 2 + 2 ) = 4
67 66 eqcomi โŠข 4 = ( 2 + 2 )
68 67 oveq2i โŠข ( ( ๐‘‡ + 1 ) โ†‘ 4 ) = ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 2 ) )
69 df-3 โŠข 3 = ( 2 + 1 )
70 69 oveq2i โŠข ( ( ๐‘‡ + 1 ) โ†‘ 3 ) = ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 1 ) )
71 70 oveq2i โŠข ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) = ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 1 ) ) )
72 68 71 oveq12i โŠข ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) = ( ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 2 ) ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 1 ) ) ) )
73 72 oveq1i โŠข ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) = ( ( ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 2 ) ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 1 ) ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) )
74 2nn0 โŠข 2 โˆˆ โ„•0
75 expadd โŠข ( ( ( ๐‘‡ + 1 ) โˆˆ โ„‚ โˆง 2 โˆˆ โ„•0 โˆง 2 โˆˆ โ„•0 ) โ†’ ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 2 ) ) = ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) )
76 74 74 75 mp3an23 โŠข ( ( ๐‘‡ + 1 ) โˆˆ โ„‚ โ†’ ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 2 ) ) = ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) )
77 1nn0 โŠข 1 โˆˆ โ„•0
78 expadd โŠข ( ( ( ๐‘‡ + 1 ) โˆˆ โ„‚ โˆง 2 โˆˆ โ„•0 โˆง 1 โˆˆ โ„•0 ) โ†’ ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 1 ) ) = ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) )
79 74 77 78 mp3an23 โŠข ( ( ๐‘‡ + 1 ) โˆˆ โ„‚ โ†’ ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 1 ) ) = ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) )
80 79 oveq2d โŠข ( ( ๐‘‡ + 1 ) โˆˆ โ„‚ โ†’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 1 ) ) ) = ( 2 ยท ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) ) )
81 76 80 oveq12d โŠข ( ( ๐‘‡ + 1 ) โˆˆ โ„‚ โ†’ ( ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 2 ) ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 1 ) ) ) ) = ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 2 ยท ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) ) ) )
82 10 81 syl โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 2 ) ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 1 ) ) ) ) = ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 2 ยท ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) ) ) )
83 10 sqcld โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆˆ โ„‚ )
84 83 mulridd โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท 1 ) = ( ( ๐‘‡ + 1 ) โ†‘ 2 ) )
85 84 eqcomd โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ๐‘‡ + 1 ) โ†‘ 2 ) = ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท 1 ) )
86 82 85 oveq12d โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 2 ) ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 1 ) ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) = ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 2 ยท ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) ) ) + ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท 1 ) ) )
87 10 exp1d โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ๐‘‡ + 1 ) โ†‘ 1 ) = ( ๐‘‡ + 1 ) )
88 87 oveq2d โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) = ( 2 ยท ( ๐‘‡ + 1 ) ) )
89 88 oveq2d โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) ) = ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( 2 ยท ( ๐‘‡ + 1 ) ) ) )
90 89 oveq2d โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) ) ) = ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( 2 ยท ( ๐‘‡ + 1 ) ) ) ) )
91 87 10 eqeltrd โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ๐‘‡ + 1 ) โ†‘ 1 ) โˆˆ โ„‚ )
92 mul12 โŠข ( ( 2 โˆˆ โ„‚ โˆง ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆˆ โ„‚ โˆง ( ( ๐‘‡ + 1 ) โ†‘ 1 ) โˆˆ โ„‚ ) โ†’ ( 2 ยท ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) ) = ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) ) )
93 41 83 91 92 mp3an2i โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( 2 ยท ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) ) = ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) ) )
94 93 oveq2d โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 2 ยท ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) ) ) = ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) ) ) )
95 mulcl โŠข ( ( 2 โˆˆ โ„‚ โˆง ( ๐‘‡ + 1 ) โˆˆ โ„‚ ) โ†’ ( 2 ยท ( ๐‘‡ + 1 ) ) โˆˆ โ„‚ )
96 41 10 95 sylancr โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( 2 ยท ( ๐‘‡ + 1 ) ) โˆˆ โ„‚ )
97 83 83 96 subdid โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) ) = ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( 2 ยท ( ๐‘‡ + 1 ) ) ) ) )
98 90 94 97 3eqtr4d โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 2 ยท ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) ) ) = ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) ) )
99 98 oveq1d โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 2 ยท ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) ) ) + ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท 1 ) ) = ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) ) + ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท 1 ) ) )
100 83 96 subcld โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) โˆˆ โ„‚ )
101 ax-1cn โŠข 1 โˆˆ โ„‚
102 adddi โŠข ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆˆ โ„‚ โˆง ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ ) โ†’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) + 1 ) ) = ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) ) + ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท 1 ) ) )
103 101 102 mp3an3 โŠข ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆˆ โ„‚ โˆง ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) โˆˆ โ„‚ ) โ†’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) + 1 ) ) = ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) ) + ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท 1 ) ) )
104 83 100 103 syl2anc โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) + 1 ) ) = ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) ) + ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท 1 ) ) )
105 99 104 eqtr4d โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 2 ยท ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) ) ) + ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท 1 ) ) = ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) + 1 ) ) )
106 adddi โŠข ( ( 2 โˆˆ โ„‚ โˆง ๐‘‡ โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ ) โ†’ ( 2 ยท ( ๐‘‡ + 1 ) ) = ( ( 2 ยท ๐‘‡ ) + ( 2 ยท 1 ) ) )
107 41 101 106 mp3an13 โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( 2 ยท ( ๐‘‡ + 1 ) ) = ( ( 2 ยท ๐‘‡ ) + ( 2 ยท 1 ) ) )
108 2t1e2 โŠข ( 2 ยท 1 ) = 2
109 108 oveq2i โŠข ( ( 2 ยท ๐‘‡ ) + ( 2 ยท 1 ) ) = ( ( 2 ยท ๐‘‡ ) + 2 )
110 107 109 eqtrdi โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( 2 ยท ( ๐‘‡ + 1 ) ) = ( ( 2 ยท ๐‘‡ ) + 2 ) )
111 110 oveq1d โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( 2 ยท ( ๐‘‡ + 1 ) ) โˆ’ 1 ) = ( ( ( 2 ยท ๐‘‡ ) + 2 ) โˆ’ 1 ) )
112 mulcl โŠข ( ( 2 โˆˆ โ„‚ โˆง ๐‘‡ โˆˆ โ„‚ ) โ†’ ( 2 ยท ๐‘‡ ) โˆˆ โ„‚ )
113 41 112 mpan โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( 2 ยท ๐‘‡ ) โˆˆ โ„‚ )
114 addsubass โŠข ( ( ( 2 ยท ๐‘‡ ) โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ ) โ†’ ( ( ( 2 ยท ๐‘‡ ) + 2 ) โˆ’ 1 ) = ( ( 2 ยท ๐‘‡ ) + ( 2 โˆ’ 1 ) ) )
115 41 101 114 mp3an23 โŠข ( ( 2 ยท ๐‘‡ ) โˆˆ โ„‚ โ†’ ( ( ( 2 ยท ๐‘‡ ) + 2 ) โˆ’ 1 ) = ( ( 2 ยท ๐‘‡ ) + ( 2 โˆ’ 1 ) ) )
116 113 115 syl โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( 2 ยท ๐‘‡ ) + 2 ) โˆ’ 1 ) = ( ( 2 ยท ๐‘‡ ) + ( 2 โˆ’ 1 ) ) )
117 2m1e1 โŠข ( 2 โˆ’ 1 ) = 1
118 117 oveq2i โŠข ( ( 2 ยท ๐‘‡ ) + ( 2 โˆ’ 1 ) ) = ( ( 2 ยท ๐‘‡ ) + 1 )
119 116 118 eqtrdi โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( 2 ยท ๐‘‡ ) + 2 ) โˆ’ 1 ) = ( ( 2 ยท ๐‘‡ ) + 1 ) )
120 111 119 eqtrd โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( 2 ยท ( ๐‘‡ + 1 ) ) โˆ’ 1 ) = ( ( 2 ยท ๐‘‡ ) + 1 ) )
121 120 oveq2d โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( ( 2 ยท ( ๐‘‡ + 1 ) ) โˆ’ 1 ) ) = ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( ( 2 ยท ๐‘‡ ) + 1 ) ) )
122 subsub โŠข ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆˆ โ„‚ โˆง ( 2 ยท ( ๐‘‡ + 1 ) ) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ ) โ†’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( ( 2 ยท ( ๐‘‡ + 1 ) ) โˆ’ 1 ) ) = ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) + 1 ) )
123 101 122 mp3an3 โŠข ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆˆ โ„‚ โˆง ( 2 ยท ( ๐‘‡ + 1 ) ) โˆˆ โ„‚ ) โ†’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( ( 2 ยท ( ๐‘‡ + 1 ) ) โˆ’ 1 ) ) = ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) + 1 ) )
124 83 96 123 syl2anc โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( ( 2 ยท ( ๐‘‡ + 1 ) ) โˆ’ 1 ) ) = ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) + 1 ) )
125 sqcl โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ๐‘‡ โ†‘ 2 ) โˆˆ โ„‚ )
126 peano2cn โŠข ( ( 2 ยท ๐‘‡ ) โˆˆ โ„‚ โ†’ ( ( 2 ยท ๐‘‡ ) + 1 ) โˆˆ โ„‚ )
127 113 126 syl โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( 2 ยท ๐‘‡ ) + 1 ) โˆˆ โ„‚ )
128 binom21 โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ๐‘‡ + 1 ) โ†‘ 2 ) = ( ( ( ๐‘‡ โ†‘ 2 ) + ( 2 ยท ๐‘‡ ) ) + 1 ) )
129 addass โŠข ( ( ( ๐‘‡ โ†‘ 2 ) โˆˆ โ„‚ โˆง ( 2 ยท ๐‘‡ ) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ ) โ†’ ( ( ( ๐‘‡ โ†‘ 2 ) + ( 2 ยท ๐‘‡ ) ) + 1 ) = ( ( ๐‘‡ โ†‘ 2 ) + ( ( 2 ยท ๐‘‡ ) + 1 ) ) )
130 101 129 mp3an3 โŠข ( ( ( ๐‘‡ โ†‘ 2 ) โˆˆ โ„‚ โˆง ( 2 ยท ๐‘‡ ) โˆˆ โ„‚ ) โ†’ ( ( ( ๐‘‡ โ†‘ 2 ) + ( 2 ยท ๐‘‡ ) ) + 1 ) = ( ( ๐‘‡ โ†‘ 2 ) + ( ( 2 ยท ๐‘‡ ) + 1 ) ) )
131 125 113 130 syl2anc โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ๐‘‡ โ†‘ 2 ) + ( 2 ยท ๐‘‡ ) ) + 1 ) = ( ( ๐‘‡ โ†‘ 2 ) + ( ( 2 ยท ๐‘‡ ) + 1 ) ) )
132 128 131 eqtrd โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ๐‘‡ + 1 ) โ†‘ 2 ) = ( ( ๐‘‡ โ†‘ 2 ) + ( ( 2 ยท ๐‘‡ ) + 1 ) ) )
133 125 127 132 mvrraddd โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( ( 2 ยท ๐‘‡ ) + 1 ) ) = ( ๐‘‡ โ†‘ 2 ) )
134 121 124 133 3eqtr3d โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) + 1 ) = ( ๐‘‡ โ†‘ 2 ) )
135 134 oveq2d โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) โˆ’ ( 2 ยท ( ๐‘‡ + 1 ) ) ) + 1 ) ) = ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ๐‘‡ โ†‘ 2 ) ) )
136 83 125 mulcomd โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ๐‘‡ โ†‘ 2 ) ) = ( ( ๐‘‡ โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) )
137 105 135 136 3eqtrd โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 2 ยท ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 1 ) ) ) ) + ( ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ยท 1 ) ) = ( ( ๐‘‡ โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) )
138 86 137 eqtrd โŠข ( ๐‘‡ โˆˆ โ„‚ โ†’ ( ( ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 2 ) ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 1 ) ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) = ( ( ๐‘‡ โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) )
139 9 138 syl โŠข ( ๐‘‡ โˆˆ โ„•0 โ†’ ( ( ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 2 ) ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ ( 2 + 1 ) ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) = ( ( ๐‘‡ โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) )
140 73 139 eqtrid โŠข ( ๐‘‡ โˆˆ โ„•0 โ†’ ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) = ( ( ๐‘‡ โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) )
141 65 140 eqtrd โŠข ( ๐‘‡ โˆˆ โ„•0 โ†’ ( ( ( ( ( ( ๐‘‡ + 1 ) โ†‘ 4 ) โˆ’ ( 2 ยท ( ( ๐‘‡ + 1 ) โ†‘ 3 ) ) ) + ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) โˆ’ ( 1 / 3 0 ) ) + ( 1 / 3 0 ) ) = ( ( ๐‘‡ โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) )
142 37 62 141 3eqtrd โŠข ( ๐‘‡ โˆˆ โ„•0 โ†’ ( ( 4 BernPoly ( ๐‘‡ + 1 ) ) โˆ’ ( 4 BernPoly 0 ) ) = ( ( ๐‘‡ โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) )
143 142 oveq1d โŠข ( ๐‘‡ โˆˆ โ„•0 โ†’ ( ( ( 4 BernPoly ( ๐‘‡ + 1 ) ) โˆ’ ( 4 BernPoly 0 ) ) / 4 ) = ( ( ( ๐‘‡ โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) / 4 ) )
144 8 143 eqtr3id โŠข ( ๐‘‡ โˆˆ โ„•0 โ†’ ( ( ( ( 3 + 1 ) BernPoly ( ๐‘‡ + 1 ) ) โˆ’ ( ( 3 + 1 ) BernPoly 0 ) ) / ( 3 + 1 ) ) = ( ( ( ๐‘‡ โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) / 4 ) )
145 3 144 eqtrd โŠข ( ๐‘‡ โˆˆ โ„•0 โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘‡ ) ( ๐‘˜ โ†‘ 3 ) = ( ( ( ๐‘‡ โ†‘ 2 ) ยท ( ( ๐‘‡ + 1 ) โ†‘ 2 ) ) / 4 ) )