Metamath Proof Explorer

Theorem bpoly3

Description: The Bernoulli polynomials at three. (Contributed by Scott Fenton, 8-Jul-2015)

Ref Expression
Assertion bpoly3 ( 𝑋 ∈ ℂ → ( 3 BernPoly 𝑋 ) = ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 3nn0 ⊢ 3 ∈ ℕ0
2 bpolyval ⊢ ( ( 3 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 3 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 3 ) − Σ 𝑘 ∈ ( 0 ... ( 3 − 1 ) ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) ) )
3 1 2 mpan ⊢ ( 𝑋 ∈ ℂ → ( 3 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 3 ) − Σ 𝑘 ∈ ( 0 ... ( 3 − 1 ) ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) ) )
4 3m1e2 ⊢ ( 3 − 1 ) = 2
5 df-2 ⊢ 2 = ( 1 + 1 )
6 4 5 eqtri ⊢ ( 3 − 1 ) = ( 1 + 1 )
7 6 oveq2i ⊢ ( 0 ... ( 3 − 1 ) ) = ( 0 ... ( 1 + 1 ) )
8 7 sumeq1i ⊢ Σ 𝑘 ∈ ( 0 ... ( 3 − 1 ) ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 1 + 1 ) ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) )
9 1eluzge0 ⊢ 1 ∈ ( ℤ≥ ‘ 0 )
10 9 a1i ⊢ ( 𝑋 ∈ ℂ → 1 ∈ ( ℤ≥ ‘ 0 ) )
11 0z ⊢ 0 ∈ ℤ
12 fzpr ⊢ ( 0 ∈ ℤ → ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) } )
13 11 12 ax-mp ⊢ ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) }
14 0p1e1 ⊢ ( 0 + 1 ) = 1
15 14 oveq2i ⊢ ( 0 ... ( 0 + 1 ) ) = ( 0 ... 1 )
16 14 preq2i ⊢ { 0 , ( 0 + 1 ) } = { 0 , 1 }
17 13 15 16 3eqtr3ri ⊢ { 0 , 1 } = ( 0 ... 1 )
18 5 sneqi ⊢ { 2 } = { ( 1 + 1 ) }
19 17 18 uneq12i ⊢ ( { 0 , 1 } ∪ { 2 } ) = ( ( 0 ... 1 ) ∪ { ( 1 + 1 ) } )
20 df-tp ⊢ { 0 , 1 , 2 } = ( { 0 , 1 } ∪ { 2 } )
21 fzsuc ⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ... ( 1 + 1 ) ) = ( ( 0 ... 1 ) ∪ { ( 1 + 1 ) } ) )
22 9 21 ax-mp ⊢ ( 0 ... ( 1 + 1 ) ) = ( ( 0 ... 1 ) ∪ { ( 1 + 1 ) } )
23 19 20 22 3eqtr4ri ⊢ ( 0 ... ( 1 + 1 ) ) = { 0 , 1 , 2 }
24 23 eleq2i ⊢ ( 𝑘 ∈ ( 0 ... ( 1 + 1 ) ) ↔ 𝑘 ∈ { 0 , 1 , 2 } )
25 vex ⊢ 𝑘 ∈ V
26 25 eltp ⊢ ( 𝑘 ∈ { 0 , 1 , 2 } ↔ ( 𝑘 = 0 ∨ 𝑘 = 1 ∨ 𝑘 = 2 ) )
27 24 26 bitri ⊢ ( 𝑘 ∈ ( 0 ... ( 1 + 1 ) ) ↔ ( 𝑘 = 0 ∨ 𝑘 = 1 ∨ 𝑘 = 2 ) )
28 oveq2 ⊢ ( 𝑘 = 0 → ( 3 C 𝑘 ) = ( 3 C 0 ) )
29 bcn0 ⊢ ( 3 ∈ ℕ0 → ( 3 C 0 ) = 1 )
30 1 29 ax-mp ⊢ ( 3 C 0 ) = 1
31 28 30 eqtrdi ⊢ ( 𝑘 = 0 → ( 3 C 𝑘 ) = 1 )
32 oveq1 ⊢ ( 𝑘 = 0 → ( 𝑘 BernPoly 𝑋 ) = ( 0 BernPoly 𝑋 ) )
33 oveq2 ⊢ ( 𝑘 = 0 → ( 3 − 𝑘 ) = ( 3 − 0 ) )
34 33 oveq1d ⊢ ( 𝑘 = 0 → ( ( 3 − 𝑘 ) + 1 ) = ( ( 3 − 0 ) + 1 ) )
35 3cn ⊢ 3 ∈ ℂ
36 35 subid1i ⊢ ( 3 − 0 ) = 3
37 36 oveq1i ⊢ ( ( 3 − 0 ) + 1 ) = ( 3 + 1 )
38 df-4 ⊢ 4 = ( 3 + 1 )
39 37 38 eqtr4i ⊢ ( ( 3 − 0 ) + 1 ) = 4
40 34 39 eqtrdi ⊢ ( 𝑘 = 0 → ( ( 3 − 𝑘 ) + 1 ) = 4 )
41 32 40 oveq12d ⊢ ( 𝑘 = 0 → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) = ( ( 0 BernPoly 𝑋 ) / 4 ) )
42 31 41 oveq12d ⊢ ( 𝑘 = 0 → ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = ( 1 · ( ( 0 BernPoly 𝑋 ) / 4 ) ) )
43 bpoly0 ⊢ ( 𝑋 ∈ ℂ → ( 0 BernPoly 𝑋 ) = 1 )
44 43 oveq1d ⊢ ( 𝑋 ∈ ℂ → ( ( 0 BernPoly 𝑋 ) / 4 ) = ( 1 / 4 ) )
45 44 oveq2d ⊢ ( 𝑋 ∈ ℂ → ( 1 · ( ( 0 BernPoly 𝑋 ) / 4 ) ) = ( 1 · ( 1 / 4 ) ) )
46 4cn ⊢ 4 ∈ ℂ
47 4ne0 ⊢ 4 ≠ 0
48 46 47 reccli ⊢ ( 1 / 4 ) ∈ ℂ
49 48 mulid2i ⊢ ( 1 · ( 1 / 4 ) ) = ( 1 / 4 )
50 45 49 eqtrdi ⊢ ( 𝑋 ∈ ℂ → ( 1 · ( ( 0 BernPoly 𝑋 ) / 4 ) ) = ( 1 / 4 ) )
51 42 50 sylan9eqr ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑘 = 0 ) → ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = ( 1 / 4 ) )
52 51 48 eqeltrdi ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑘 = 0 ) → ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) ∈ ℂ )
53 oveq2 ⊢ ( 𝑘 = 1 → ( 3 C 𝑘 ) = ( 3 C 1 ) )
54 bcn1 ⊢ ( 3 ∈ ℕ0 → ( 3 C 1 ) = 3 )
55 1 54 ax-mp ⊢ ( 3 C 1 ) = 3
56 53 55 eqtrdi ⊢ ( 𝑘 = 1 → ( 3 C 𝑘 ) = 3 )
57 oveq1 ⊢ ( 𝑘 = 1 → ( 𝑘 BernPoly 𝑋 ) = ( 1 BernPoly 𝑋 ) )
58 oveq2 ⊢ ( 𝑘 = 1 → ( 3 − 𝑘 ) = ( 3 − 1 ) )
59 58 oveq1d ⊢ ( 𝑘 = 1 → ( ( 3 − 𝑘 ) + 1 ) = ( ( 3 − 1 ) + 1 ) )
60 ax-1cn ⊢ 1 ∈ ℂ
61 npcan ⊢ ( ( 3 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 3 − 1 ) + 1 ) = 3 )
62 35 60 61 mp2an ⊢ ( ( 3 − 1 ) + 1 ) = 3
63 59 62 eqtrdi ⊢ ( 𝑘 = 1 → ( ( 3 − 𝑘 ) + 1 ) = 3 )
64 57 63 oveq12d ⊢ ( 𝑘 = 1 → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) = ( ( 1 BernPoly 𝑋 ) / 3 ) )
65 56 64 oveq12d ⊢ ( 𝑘 = 1 → ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = ( 3 · ( ( 1 BernPoly 𝑋 ) / 3 ) ) )
66 bpoly1 ⊢ ( 𝑋 ∈ ℂ → ( 1 BernPoly 𝑋 ) = ( 𝑋 − ( 1 / 2 ) ) )
67 66 oveq1d ⊢ ( 𝑋 ∈ ℂ → ( ( 1 BernPoly 𝑋 ) / 3 ) = ( ( 𝑋 − ( 1 / 2 ) ) / 3 ) )
68 67 oveq2d ⊢ ( 𝑋 ∈ ℂ → ( 3 · ( ( 1 BernPoly 𝑋 ) / 3 ) ) = ( 3 · ( ( 𝑋 − ( 1 / 2 ) ) / 3 ) ) )
69 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
70 subcl ⊢ ( ( 𝑋 ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) → ( 𝑋 − ( 1 / 2 ) ) ∈ ℂ )
71 69 70 mpan2 ⊢ ( 𝑋 ∈ ℂ → ( 𝑋 − ( 1 / 2 ) ) ∈ ℂ )
72 3ne0 ⊢ 3 ≠ 0
73 divcan2 ⊢ ( ( ( 𝑋 − ( 1 / 2 ) ) ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0 ) → ( 3 · ( ( 𝑋 − ( 1 / 2 ) ) / 3 ) ) = ( 𝑋 − ( 1 / 2 ) ) )
74 35 72 73 mp3an23 ⊢ ( ( 𝑋 − ( 1 / 2 ) ) ∈ ℂ → ( 3 · ( ( 𝑋 − ( 1 / 2 ) ) / 3 ) ) = ( 𝑋 − ( 1 / 2 ) ) )
75 71 74 syl ⊢ ( 𝑋 ∈ ℂ → ( 3 · ( ( 𝑋 − ( 1 / 2 ) ) / 3 ) ) = ( 𝑋 − ( 1 / 2 ) ) )
76 68 75 eqtrd ⊢ ( 𝑋 ∈ ℂ → ( 3 · ( ( 1 BernPoly 𝑋 ) / 3 ) ) = ( 𝑋 − ( 1 / 2 ) ) )
77 65 76 sylan9eqr ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑘 = 1 ) → ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = ( 𝑋 − ( 1 / 2 ) ) )
78 71 adantr ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑘 = 1 ) → ( 𝑋 − ( 1 / 2 ) ) ∈ ℂ )
79 77 78 eqeltrd ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑘 = 1 ) → ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) ∈ ℂ )
80 oveq2 ⊢ ( 𝑘 = 2 → ( 3 C 𝑘 ) = ( 3 C 2 ) )
81 bcn2 ⊢ ( 3 ∈ ℕ0 → ( 3 C 2 ) = ( ( 3 · ( 3 − 1 ) ) / 2 ) )
82 1 81 ax-mp ⊢ ( 3 C 2 ) = ( ( 3 · ( 3 − 1 ) ) / 2 )
83 4 oveq2i ⊢ ( 3 · ( 3 − 1 ) ) = ( 3 · 2 )
84 83 oveq1i ⊢ ( ( 3 · ( 3 − 1 ) ) / 2 ) = ( ( 3 · 2 ) / 2 )
85 2cn ⊢ 2 ∈ ℂ
86 2ne0 ⊢ 2 ≠ 0
87 35 85 86 divcan4i ⊢ ( ( 3 · 2 ) / 2 ) = 3
88 84 87 eqtri ⊢ ( ( 3 · ( 3 − 1 ) ) / 2 ) = 3
89 82 88 eqtri ⊢ ( 3 C 2 ) = 3
90 80 89 eqtrdi ⊢ ( 𝑘 = 2 → ( 3 C 𝑘 ) = 3 )
91 oveq1 ⊢ ( 𝑘 = 2 → ( 𝑘 BernPoly 𝑋 ) = ( 2 BernPoly 𝑋 ) )
92 oveq2 ⊢ ( 𝑘 = 2 → ( 3 − 𝑘 ) = ( 3 − 2 ) )
93 92 oveq1d ⊢ ( 𝑘 = 2 → ( ( 3 − 𝑘 ) + 1 ) = ( ( 3 − 2 ) + 1 ) )
94 2p1e3 ⊢ ( 2 + 1 ) = 3
95 35 85 60 94 subaddrii ⊢ ( 3 − 2 ) = 1
96 95 oveq1i ⊢ ( ( 3 − 2 ) + 1 ) = ( 1 + 1 )
97 96 5 eqtr4i ⊢ ( ( 3 − 2 ) + 1 ) = 2
98 93 97 eqtrdi ⊢ ( 𝑘 = 2 → ( ( 3 − 𝑘 ) + 1 ) = 2 )
99 91 98 oveq12d ⊢ ( 𝑘 = 2 → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) = ( ( 2 BernPoly 𝑋 ) / 2 ) )
100 90 99 oveq12d ⊢ ( 𝑘 = 2 → ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = ( 3 · ( ( 2 BernPoly 𝑋 ) / 2 ) ) )
101 2nn0 ⊢ 2 ∈ ℕ0
102 bpolycl ⊢ ( ( 2 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 2 BernPoly 𝑋 ) ∈ ℂ )
103 101 102 mpan ⊢ ( 𝑋 ∈ ℂ → ( 2 BernPoly 𝑋 ) ∈ ℂ )
104 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
105 div12 ⊢ ( ( 3 ∈ ℂ ∧ ( 2 BernPoly 𝑋 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( 3 · ( ( 2 BernPoly 𝑋 ) / 2 ) ) = ( ( 2 BernPoly 𝑋 ) · ( 3 / 2 ) ) )
106 35 104 105 mp3an13 ⊢ ( ( 2 BernPoly 𝑋 ) ∈ ℂ → ( 3 · ( ( 2 BernPoly 𝑋 ) / 2 ) ) = ( ( 2 BernPoly 𝑋 ) · ( 3 / 2 ) ) )
107 103 106 syl ⊢ ( 𝑋 ∈ ℂ → ( 3 · ( ( 2 BernPoly 𝑋 ) / 2 ) ) = ( ( 2 BernPoly 𝑋 ) · ( 3 / 2 ) ) )
108 35 85 86 divcli ⊢ ( 3 / 2 ) ∈ ℂ
109 mulcom ⊢ ( ( ( 2 BernPoly 𝑋 ) ∈ ℂ ∧ ( 3 / 2 ) ∈ ℂ ) → ( ( 2 BernPoly 𝑋 ) · ( 3 / 2 ) ) = ( ( 3 / 2 ) · ( 2 BernPoly 𝑋 ) ) )
110 103 108 109 sylancl ⊢ ( 𝑋 ∈ ℂ → ( ( 2 BernPoly 𝑋 ) · ( 3 / 2 ) ) = ( ( 3 / 2 ) · ( 2 BernPoly 𝑋 ) ) )
111 bpoly2 ⊢ ( 𝑋 ∈ ℂ → ( 2 BernPoly 𝑋 ) = ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) )
112 111 oveq2d ⊢ ( 𝑋 ∈ ℂ → ( ( 3 / 2 ) · ( 2 BernPoly 𝑋 ) ) = ( ( 3 / 2 ) · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) )
113 sqcl ⊢ ( 𝑋 ∈ ℂ → ( 𝑋 ↑ 2 ) ∈ ℂ )
114 6cn ⊢ 6 ∈ ℂ
115 6re ⊢ 6 ∈ ℝ
116 6pos ⊢ 0 < 6
117 115 116 gt0ne0ii ⊢ 6 ≠ 0
118 114 117 reccli ⊢ ( 1 / 6 ) ∈ ℂ
119 subsub ⊢ ( ( ( 𝑋 ↑ 2 ) ∈ ℂ ∧ 𝑋 ∈ ℂ ∧ ( 1 / 6 ) ∈ ℂ ) → ( ( 𝑋 ↑ 2 ) − ( 𝑋 − ( 1 / 6 ) ) ) = ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) )
120 118 119 mp3an3 ⊢ ( ( ( 𝑋 ↑ 2 ) ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( ( 𝑋 ↑ 2 ) − ( 𝑋 − ( 1 / 6 ) ) ) = ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) )
121 113 120 mpancom ⊢ ( 𝑋 ∈ ℂ → ( ( 𝑋 ↑ 2 ) − ( 𝑋 − ( 1 / 6 ) ) ) = ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) )
122 121 oveq2d ⊢ ( 𝑋 ∈ ℂ → ( ( 3 / 2 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 − ( 1 / 6 ) ) ) ) = ( ( 3 / 2 ) · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) )
123 subcl ⊢ ( ( 𝑋 ∈ ℂ ∧ ( 1 / 6 ) ∈ ℂ ) → ( 𝑋 − ( 1 / 6 ) ) ∈ ℂ )
124 118 123 mpan2 ⊢ ( 𝑋 ∈ ℂ → ( 𝑋 − ( 1 / 6 ) ) ∈ ℂ )
125 subdi ⊢ ( ( ( 3 / 2 ) ∈ ℂ ∧ ( 𝑋 ↑ 2 ) ∈ ℂ ∧ ( 𝑋 − ( 1 / 6 ) ) ∈ ℂ ) → ( ( 3 / 2 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 − ( 1 / 6 ) ) ) ) = ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) )
126 108 113 124 125 mp3an2i ⊢ ( 𝑋 ∈ ℂ → ( ( 3 / 2 ) · ( ( 𝑋 ↑ 2 ) − ( 𝑋 − ( 1 / 6 ) ) ) ) = ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) )
127 112 122 126 3eqtr2d ⊢ ( 𝑋 ∈ ℂ → ( ( 3 / 2 ) · ( 2 BernPoly 𝑋 ) ) = ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) )
128 107 110 127 3eqtrd ⊢ ( 𝑋 ∈ ℂ → ( 3 · ( ( 2 BernPoly 𝑋 ) / 2 ) ) = ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) )
129 100 128 sylan9eqr ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑘 = 2 ) → ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) )
130 mulcl ⊢ ( ( ( 3 / 2 ) ∈ ℂ ∧ ( 𝑋 ↑ 2 ) ∈ ℂ ) → ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ∈ ℂ )
131 108 113 130 sylancr ⊢ ( 𝑋 ∈ ℂ → ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ∈ ℂ )
132 mulcl ⊢ ( ( ( 3 / 2 ) ∈ ℂ ∧ ( 𝑋 − ( 1 / 6 ) ) ∈ ℂ ) → ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ∈ ℂ )
133 108 124 132 sylancr ⊢ ( 𝑋 ∈ ℂ → ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ∈ ℂ )
134 131 133 subcld ⊢ ( 𝑋 ∈ ℂ → ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) ∈ ℂ )
135 134 adantr ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑘 = 2 ) → ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) ∈ ℂ )
136 129 135 eqeltrd ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑘 = 2 ) → ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) ∈ ℂ )
137 52 79 136 3jaodan ⊢ ( ( 𝑋 ∈ ℂ ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ∨ 𝑘 = 2 ) ) → ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) ∈ ℂ )
138 27 137 sylan2b ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 1 + 1 ) ) ) → ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) ∈ ℂ )
139 5 eqeq2i ⊢ ( 𝑘 = 2 ↔ 𝑘 = ( 1 + 1 ) )
140 139 100 sylbir ⊢ ( 𝑘 = ( 1 + 1 ) → ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = ( 3 · ( ( 2 BernPoly 𝑋 ) / 2 ) ) )
141 10 138 140 fsump1 ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 1 + 1 ) ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) + ( 3 · ( ( 2 BernPoly 𝑋 ) / 2 ) ) ) )
142 128 oveq2d ⊢ ( 𝑋 ∈ ℂ → ( Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) + ( 3 · ( ( 2 BernPoly 𝑋 ) / 2 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) + ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) ) )
143 15 sumeq1i ⊢ Σ 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) )
144 0nn0 ⊢ 0 ∈ ℕ0
145 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
146 144 145 eleqtri ⊢ 0 ∈ ( ℤ≥ ‘ 0 )
147 146 a1i ⊢ ( 𝑋 ∈ ℂ → 0 ∈ ( ℤ≥ ‘ 0 ) )
148 13 16 eqtri ⊢ ( 0 ... ( 0 + 1 ) ) = { 0 , 1 }
149 148 eleq2i ⊢ ( 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ↔ 𝑘 ∈ { 0 , 1 } )
150 25 elpr ⊢ ( 𝑘 ∈ { 0 , 1 } ↔ ( 𝑘 = 0 ∨ 𝑘 = 1 ) )
151 149 150 bitri ⊢ ( 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ↔ ( 𝑘 = 0 ∨ 𝑘 = 1 ) )
152 52 79 jaodan ⊢ ( ( 𝑋 ∈ ℂ ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) → ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) ∈ ℂ )
153 151 152 sylan2b ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ) → ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) ∈ ℂ )
154 14 eqeq2i ⊢ ( 𝑘 = ( 0 + 1 ) ↔ 𝑘 = 1 )
155 154 65 sylbi ⊢ ( 𝑘 = ( 0 + 1 ) → ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = ( 3 · ( ( 1 BernPoly 𝑋 ) / 3 ) ) )
156 147 153 155 fsump1 ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) + ( 3 · ( ( 1 BernPoly 𝑋 ) / 3 ) ) ) )
157 50 48 eqeltrdi ⊢ ( 𝑋 ∈ ℂ → ( 1 · ( ( 0 BernPoly 𝑋 ) / 4 ) ) ∈ ℂ )
158 42 fsum1 ⊢ ( ( 0 ∈ ℤ ∧ ( 1 · ( ( 0 BernPoly 𝑋 ) / 4 ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = ( 1 · ( ( 0 BernPoly 𝑋 ) / 4 ) ) )
159 11 157 158 sylancr ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = ( 1 · ( ( 0 BernPoly 𝑋 ) / 4 ) ) )
160 159 50 eqtrd ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = ( 1 / 4 ) )
161 160 76 oveq12d ⊢ ( 𝑋 ∈ ℂ → ( Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) + ( 3 · ( ( 1 BernPoly 𝑋 ) / 3 ) ) ) = ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) )
162 156 161 eqtrd ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) )
163 143 162 syl5eqr ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) )
164 163 oveq1d ⊢ ( 𝑋 ∈ ℂ → ( Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) + ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) ) = ( ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) ) )
165 addcl ⊢ ( ( ( 1 / 4 ) ∈ ℂ ∧ ( 𝑋 − ( 1 / 2 ) ) ∈ ℂ ) → ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) ∈ ℂ )
166 48 71 165 sylancr ⊢ ( 𝑋 ∈ ℂ → ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) ∈ ℂ )
167 166 131 133 addsub12d ⊢ ( 𝑋 ∈ ℂ → ( ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) ) = ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) + ( ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) ) )
168 164 167 eqtrd ⊢ ( 𝑋 ∈ ℂ → ( Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) + ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) ) = ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) + ( ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) ) )
169 133 166 negsubdi2d ⊢ ( 𝑋 ∈ ℂ → - ( ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) − ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) ) = ( ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) )
170 subdi ⊢ ( ( ( 3 / 2 ) ∈ ℂ ∧ 𝑋 ∈ ℂ ∧ ( 1 / 6 ) ∈ ℂ ) → ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) = ( ( ( 3 / 2 ) · 𝑋 ) − ( ( 3 / 2 ) · ( 1 / 6 ) ) ) )
171 108 118 170 mp3an13 ⊢ ( 𝑋 ∈ ℂ → ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) = ( ( ( 3 / 2 ) · 𝑋 ) − ( ( 3 / 2 ) · ( 1 / 6 ) ) ) )
172 addsub12 ⊢ ( ( ( 1 / 4 ) ∈ ℂ ∧ 𝑋 ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) → ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) = ( 𝑋 + ( ( 1 / 4 ) − ( 1 / 2 ) ) ) )
173 48 69 172 mp3an13 ⊢ ( 𝑋 ∈ ℂ → ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) = ( 𝑋 + ( ( 1 / 4 ) − ( 1 / 2 ) ) ) )
174 171 173 oveq12d ⊢ ( 𝑋 ∈ ℂ → ( ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) − ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) ) = ( ( ( ( 3 / 2 ) · 𝑋 ) − ( ( 3 / 2 ) · ( 1 / 6 ) ) ) − ( 𝑋 + ( ( 1 / 4 ) − ( 1 / 2 ) ) ) ) )
175 mulcl ⊢ ( ( ( 3 / 2 ) ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( ( 3 / 2 ) · 𝑋 ) ∈ ℂ )
176 108 175 mpan ⊢ ( 𝑋 ∈ ℂ → ( ( 3 / 2 ) · 𝑋 ) ∈ ℂ )
177 108 118 mulcli ⊢ ( ( 3 / 2 ) · ( 1 / 6 ) ) ∈ ℂ
178 negsub ⊢ ( ( ( ( 3 / 2 ) · 𝑋 ) ∈ ℂ ∧ ( ( 3 / 2 ) · ( 1 / 6 ) ) ∈ ℂ ) → ( ( ( 3 / 2 ) · 𝑋 ) + - ( ( 3 / 2 ) · ( 1 / 6 ) ) ) = ( ( ( 3 / 2 ) · 𝑋 ) − ( ( 3 / 2 ) · ( 1 / 6 ) ) ) )
179 176 177 178 sylancl ⊢ ( 𝑋 ∈ ℂ → ( ( ( 3 / 2 ) · 𝑋 ) + - ( ( 3 / 2 ) · ( 1 / 6 ) ) ) = ( ( ( 3 / 2 ) · 𝑋 ) − ( ( 3 / 2 ) · ( 1 / 6 ) ) ) )
180 179 oveq1d ⊢ ( 𝑋 ∈ ℂ → ( ( ( ( 3 / 2 ) · 𝑋 ) + - ( ( 3 / 2 ) · ( 1 / 6 ) ) ) − ( 𝑋 + ( ( 1 / 4 ) − ( 1 / 2 ) ) ) ) = ( ( ( ( 3 / 2 ) · 𝑋 ) − ( ( 3 / 2 ) · ( 1 / 6 ) ) ) − ( 𝑋 + ( ( 1 / 4 ) − ( 1 / 2 ) ) ) ) )
181 69 48 negsubdi2i ⊢ - ( ( 1 / 2 ) − ( 1 / 4 ) ) = ( ( 1 / 4 ) − ( 1 / 2 ) )
182 85 35 85 mul12i ⊢ ( 2 · ( 3 · 2 ) ) = ( 3 · ( 2 · 2 ) )
183 3t2e6 ⊢ ( 3 · 2 ) = 6
184 183 oveq2i ⊢ ( 2 · ( 3 · 2 ) ) = ( 2 · 6 )
185 2t2e4 ⊢ ( 2 · 2 ) = 4
186 185 oveq2i ⊢ ( 3 · ( 2 · 2 ) ) = ( 3 · 4 )
187 182 184 186 3eqtr3i ⊢ ( 2 · 6 ) = ( 3 · 4 )
188 187 oveq2i ⊢ ( ( 3 · 1 ) / ( 2 · 6 ) ) = ( ( 3 · 1 ) / ( 3 · 4 ) )
189 46 47 pm3.2i ⊢ ( 4 ∈ ℂ ∧ 4 ≠ 0 )
190 35 72 pm3.2i ⊢ ( 3 ∈ ℂ ∧ 3 ≠ 0 )
191 divcan5 ⊢ ( ( 1 ∈ ℂ ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ∧ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) ) → ( ( 3 · 1 ) / ( 3 · 4 ) ) = ( 1 / 4 ) )
192 60 189 190 191 mp3an ⊢ ( ( 3 · 1 ) / ( 3 · 4 ) ) = ( 1 / 4 )
193 188 192 eqtri ⊢ ( ( 3 · 1 ) / ( 2 · 6 ) ) = ( 1 / 4 )
194 35 85 60 114 86 117 divmuldivi ⊢ ( ( 3 / 2 ) · ( 1 / 6 ) ) = ( ( 3 · 1 ) / ( 2 · 6 ) )
195 2t1e2 ⊢ ( 2 · 1 ) = 2
196 195 5 eqtri ⊢ ( 2 · 1 ) = ( 1 + 1 )
197 196 185 oveq12i ⊢ ( ( 2 · 1 ) / ( 2 · 2 ) ) = ( ( 1 + 1 ) / 4 )
198 divcan5 ⊢ ( ( 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 2 · 1 ) / ( 2 · 2 ) ) = ( 1 / 2 ) )
199 60 104 104 198 mp3an ⊢ ( ( 2 · 1 ) / ( 2 · 2 ) ) = ( 1 / 2 )
200 60 60 46 47 divdiri ⊢ ( ( 1 + 1 ) / 4 ) = ( ( 1 / 4 ) + ( 1 / 4 ) )
201 197 199 200 3eqtr3ri ⊢ ( ( 1 / 4 ) + ( 1 / 4 ) ) = ( 1 / 2 )
202 69 48 48 201 subaddrii ⊢ ( ( 1 / 2 ) − ( 1 / 4 ) ) = ( 1 / 4 )
203 193 194 202 3eqtr4ri ⊢ ( ( 1 / 2 ) − ( 1 / 4 ) ) = ( ( 3 / 2 ) · ( 1 / 6 ) )
204 203 negeqi ⊢ - ( ( 1 / 2 ) − ( 1 / 4 ) ) = - ( ( 3 / 2 ) · ( 1 / 6 ) )
205 181 204 eqtr3i ⊢ ( ( 1 / 4 ) − ( 1 / 2 ) ) = - ( ( 3 / 2 ) · ( 1 / 6 ) )
206 48 69 subcli ⊢ ( ( 1 / 4 ) − ( 1 / 2 ) ) ∈ ℂ
207 177 negcli ⊢ - ( ( 3 / 2 ) · ( 1 / 6 ) ) ∈ ℂ
208 206 207 subeq0i ⊢ ( ( ( ( 1 / 4 ) − ( 1 / 2 ) ) − - ( ( 3 / 2 ) · ( 1 / 6 ) ) ) = 0 ↔ ( ( 1 / 4 ) − ( 1 / 2 ) ) = - ( ( 3 / 2 ) · ( 1 / 6 ) ) )
209 205 208 mpbir ⊢ ( ( ( 1 / 4 ) − ( 1 / 2 ) ) − - ( ( 3 / 2 ) · ( 1 / 6 ) ) ) = 0
210 209 oveq2i ⊢ ( ( ( ( 3 / 2 ) · 𝑋 ) − 𝑋 ) − ( ( ( 1 / 4 ) − ( 1 / 2 ) ) − - ( ( 3 / 2 ) · ( 1 / 6 ) ) ) ) = ( ( ( ( 3 / 2 ) · 𝑋 ) − 𝑋 ) − 0 )
211 id ⊢ ( 𝑋 ∈ ℂ → 𝑋 ∈ ℂ )
212 206 a1i ⊢ ( 𝑋 ∈ ℂ → ( ( 1 / 4 ) − ( 1 / 2 ) ) ∈ ℂ )
213 207 a1i ⊢ ( 𝑋 ∈ ℂ → - ( ( 3 / 2 ) · ( 1 / 6 ) ) ∈ ℂ )
214 176 211 212 213 subadd4d ⊢ ( 𝑋 ∈ ℂ → ( ( ( ( 3 / 2 ) · 𝑋 ) − 𝑋 ) − ( ( ( 1 / 4 ) − ( 1 / 2 ) ) − - ( ( 3 / 2 ) · ( 1 / 6 ) ) ) ) = ( ( ( ( 3 / 2 ) · 𝑋 ) + - ( ( 3 / 2 ) · ( 1 / 6 ) ) ) − ( 𝑋 + ( ( 1 / 4 ) − ( 1 / 2 ) ) ) ) )
215 subdir ⊢ ( ( ( 3 / 2 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( ( ( 3 / 2 ) − 1 ) · 𝑋 ) = ( ( ( 3 / 2 ) · 𝑋 ) − ( 1 · 𝑋 ) ) )
216 108 60 215 mp3an12 ⊢ ( 𝑋 ∈ ℂ → ( ( ( 3 / 2 ) − 1 ) · 𝑋 ) = ( ( ( 3 / 2 ) · 𝑋 ) − ( 1 · 𝑋 ) ) )
217 divsubdir ⊢ ( ( 3 ∈ ℂ ∧ 2 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 3 − 2 ) / 2 ) = ( ( 3 / 2 ) − ( 2 / 2 ) ) )
218 35 85 104 217 mp3an ⊢ ( ( 3 − 2 ) / 2 ) = ( ( 3 / 2 ) − ( 2 / 2 ) )
219 95 oveq1i ⊢ ( ( 3 − 2 ) / 2 ) = ( 1 / 2 )
220 2div2e1 ⊢ ( 2 / 2 ) = 1
221 220 oveq2i ⊢ ( ( 3 / 2 ) − ( 2 / 2 ) ) = ( ( 3 / 2 ) − 1 )
222 218 219 221 3eqtr3ri ⊢ ( ( 3 / 2 ) − 1 ) = ( 1 / 2 )
223 222 oveq1i ⊢ ( ( ( 3 / 2 ) − 1 ) · 𝑋 ) = ( ( 1 / 2 ) · 𝑋 )
224 223 a1i ⊢ ( 𝑋 ∈ ℂ → ( ( ( 3 / 2 ) − 1 ) · 𝑋 ) = ( ( 1 / 2 ) · 𝑋 ) )
225 mulid2 ⊢ ( 𝑋 ∈ ℂ → ( 1 · 𝑋 ) = 𝑋 )
226 225 oveq2d ⊢ ( 𝑋 ∈ ℂ → ( ( ( 3 / 2 ) · 𝑋 ) − ( 1 · 𝑋 ) ) = ( ( ( 3 / 2 ) · 𝑋 ) − 𝑋 ) )
227 216 224 226 3eqtr3rd ⊢ ( 𝑋 ∈ ℂ → ( ( ( 3 / 2 ) · 𝑋 ) − 𝑋 ) = ( ( 1 / 2 ) · 𝑋 ) )
228 227 oveq1d ⊢ ( 𝑋 ∈ ℂ → ( ( ( ( 3 / 2 ) · 𝑋 ) − 𝑋 ) − 0 ) = ( ( ( 1 / 2 ) · 𝑋 ) − 0 ) )
229 mulcl ⊢ ( ( ( 1 / 2 ) ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( ( 1 / 2 ) · 𝑋 ) ∈ ℂ )
230 69 229 mpan ⊢ ( 𝑋 ∈ ℂ → ( ( 1 / 2 ) · 𝑋 ) ∈ ℂ )
231 230 subid1d ⊢ ( 𝑋 ∈ ℂ → ( ( ( 1 / 2 ) · 𝑋 ) − 0 ) = ( ( 1 / 2 ) · 𝑋 ) )
232 228 231 eqtrd ⊢ ( 𝑋 ∈ ℂ → ( ( ( ( 3 / 2 ) · 𝑋 ) − 𝑋 ) − 0 ) = ( ( 1 / 2 ) · 𝑋 ) )
233 210 214 232 3eqtr3a ⊢ ( 𝑋 ∈ ℂ → ( ( ( ( 3 / 2 ) · 𝑋 ) + - ( ( 3 / 2 ) · ( 1 / 6 ) ) ) − ( 𝑋 + ( ( 1 / 4 ) − ( 1 / 2 ) ) ) ) = ( ( 1 / 2 ) · 𝑋 ) )
234 174 180 233 3eqtr2d ⊢ ( 𝑋 ∈ ℂ → ( ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) − ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) ) = ( ( 1 / 2 ) · 𝑋 ) )
235 234 negeqd ⊢ ( 𝑋 ∈ ℂ → - ( ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) − ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) ) = - ( ( 1 / 2 ) · 𝑋 ) )
236 169 235 eqtr3d ⊢ ( 𝑋 ∈ ℂ → ( ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) = - ( ( 1 / 2 ) · 𝑋 ) )
237 236 oveq2d ⊢ ( 𝑋 ∈ ℂ → ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) + ( ( ( 1 / 4 ) + ( 𝑋 − ( 1 / 2 ) ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) ) = ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) + - ( ( 1 / 2 ) · 𝑋 ) ) )
238 131 230 negsubd ⊢ ( 𝑋 ∈ ℂ → ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) + - ( ( 1 / 2 ) · 𝑋 ) ) = ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 1 / 2 ) · 𝑋 ) ) )
239 168 237 238 3eqtrd ⊢ ( 𝑋 ∈ ℂ → ( Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) + ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 3 / 2 ) · ( 𝑋 − ( 1 / 6 ) ) ) ) ) = ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 1 / 2 ) · 𝑋 ) ) )
240 141 142 239 3eqtrd ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 1 + 1 ) ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 1 / 2 ) · 𝑋 ) ) )
241 8 240 syl5eq ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 3 − 1 ) ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) = ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 1 / 2 ) · 𝑋 ) ) )
242 241 oveq2d ⊢ ( 𝑋 ∈ ℂ → ( ( 𝑋 ↑ 3 ) − Σ 𝑘 ∈ ( 0 ... ( 3 − 1 ) ) ( ( 3 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 3 − 𝑘 ) + 1 ) ) ) ) = ( ( 𝑋 ↑ 3 ) − ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 1 / 2 ) · 𝑋 ) ) ) )
243 expcl ⊢ ( ( 𝑋 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑋 ↑ 3 ) ∈ ℂ )
244 1 243 mpan2 ⊢ ( 𝑋 ∈ ℂ → ( 𝑋 ↑ 3 ) ∈ ℂ )
245 244 131 230 subsubd ⊢ ( 𝑋 ∈ ℂ → ( ( 𝑋 ↑ 3 ) − ( ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) − ( ( 1 / 2 ) · 𝑋 ) ) ) = ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) )
246 3 242 245 3eqtrd ⊢ ( 𝑋 ∈ ℂ → ( 3 BernPoly 𝑋 ) = ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) )