Metamath Proof Explorer


Theorem bpoly4

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

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

Proof

Step Hyp Ref Expression
1 4nn0 4 ∈ ℕ0
2 bpolyval ( ( 4 ∈ ℕ0𝑋 ∈ ℂ ) → ( 4 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 4 ) − Σ 𝑘 ∈ ( 0 ... ( 4 − 1 ) ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) ) )
3 1 2 mpan ( 𝑋 ∈ ℂ → ( 4 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 4 ) − Σ 𝑘 ∈ ( 0 ... ( 4 − 1 ) ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) ) )
4 4m1e3 ( 4 − 1 ) = 3
5 df-3 3 = ( 2 + 1 )
6 4 5 eqtri ( 4 − 1 ) = ( 2 + 1 )
7 6 oveq2i ( 0 ... ( 4 − 1 ) ) = ( 0 ... ( 2 + 1 ) )
8 7 sumeq1i Σ 𝑘 ∈ ( 0 ... ( 4 − 1 ) ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) )
9 2eluzge0 2 ∈ ( ℤ ‘ 0 )
10 9 a1i ( 𝑋 ∈ ℂ → 2 ∈ ( ℤ ‘ 0 ) )
11 elfzelz ( 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) → 𝑘 ∈ ℤ )
12 bccl ( ( 4 ∈ ℕ0𝑘 ∈ ℤ ) → ( 4 C 𝑘 ) ∈ ℕ0 )
13 1 11 12 sylancr ( 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) → ( 4 C 𝑘 ) ∈ ℕ0 )
14 13 nn0cnd ( 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) → ( 4 C 𝑘 ) ∈ ℂ )
15 14 adantl ( ( 𝑋 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) ) → ( 4 C 𝑘 ) ∈ ℂ )
16 elfznn0 ( 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) → 𝑘 ∈ ℕ0 )
17 bpolycl ( ( 𝑘 ∈ ℕ0𝑋 ∈ ℂ ) → ( 𝑘 BernPoly 𝑋 ) ∈ ℂ )
18 16 17 sylan ( ( 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) ∧ 𝑋 ∈ ℂ ) → ( 𝑘 BernPoly 𝑋 ) ∈ ℂ )
19 18 ancoms ( ( 𝑋 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) ) → ( 𝑘 BernPoly 𝑋 ) ∈ ℂ )
20 4re 4 ∈ ℝ
21 20 a1i ( 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) → 4 ∈ ℝ )
22 11 zred ( 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) → 𝑘 ∈ ℝ )
23 21 22 resubcld ( 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) → ( 4 − 𝑘 ) ∈ ℝ )
24 peano2re ( ( 4 − 𝑘 ) ∈ ℝ → ( ( 4 − 𝑘 ) + 1 ) ∈ ℝ )
25 23 24 syl ( 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) → ( ( 4 − 𝑘 ) + 1 ) ∈ ℝ )
26 25 recnd ( 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) → ( ( 4 − 𝑘 ) + 1 ) ∈ ℂ )
27 26 adantl ( ( 𝑋 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) ) → ( ( 4 − 𝑘 ) + 1 ) ∈ ℂ )
28 1red ( 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) → 1 ∈ ℝ )
29 5 oveq2i ( 0 ... 3 ) = ( 0 ... ( 2 + 1 ) )
30 29 eleq2i ( 𝑘 ∈ ( 0 ... 3 ) ↔ 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) )
31 elfzelz ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℤ )
32 31 zred ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℝ )
33 3re 3 ∈ ℝ
34 33 a1i ( 𝑘 ∈ ( 0 ... 3 ) → 3 ∈ ℝ )
35 20 a1i ( 𝑘 ∈ ( 0 ... 3 ) → 4 ∈ ℝ )
36 elfzle2 ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ≤ 3 )
37 3lt4 3 < 4
38 37 a1i ( 𝑘 ∈ ( 0 ... 3 ) → 3 < 4 )
39 32 34 35 36 38 lelttrd ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 < 4 )
40 30 39 sylbir ( 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) → 𝑘 < 4 )
41 22 21 posdifd ( 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) → ( 𝑘 < 4 ↔ 0 < ( 4 − 𝑘 ) ) )
42 40 41 mpbid ( 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) → 0 < ( 4 − 𝑘 ) )
43 0lt1 0 < 1
44 43 a1i ( 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) → 0 < 1 )
45 23 28 42 44 addgt0d ( 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) → 0 < ( ( 4 − 𝑘 ) + 1 ) )
46 45 gt0ne0d ( 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) → ( ( 4 − 𝑘 ) + 1 ) ≠ 0 )
47 46 adantl ( ( 𝑋 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) ) → ( ( 4 − 𝑘 ) + 1 ) ≠ 0 )
48 19 27 47 divcld ( ( 𝑋 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) ) → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ∈ ℂ )
49 15 48 mulcld ( ( 𝑋 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) ) → ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) ∈ ℂ )
50 5 eqeq2i ( 𝑘 = 3 ↔ 𝑘 = ( 2 + 1 ) )
51 oveq2 ( 𝑘 = 3 → ( 4 C 𝑘 ) = ( 4 C 3 ) )
52 4bc3eq4 ( 4 C 3 ) = 4
53 51 52 eqtrdi ( 𝑘 = 3 → ( 4 C 𝑘 ) = 4 )
54 oveq1 ( 𝑘 = 3 → ( 𝑘 BernPoly 𝑋 ) = ( 3 BernPoly 𝑋 ) )
55 oveq2 ( 𝑘 = 3 → ( 4 − 𝑘 ) = ( 4 − 3 ) )
56 55 oveq1d ( 𝑘 = 3 → ( ( 4 − 𝑘 ) + 1 ) = ( ( 4 − 3 ) + 1 ) )
57 4cn 4 ∈ ℂ
58 3cn 3 ∈ ℂ
59 ax-1cn 1 ∈ ℂ
60 3p1e4 ( 3 + 1 ) = 4
61 57 58 59 60 subaddrii ( 4 − 3 ) = 1
62 61 oveq1i ( ( 4 − 3 ) + 1 ) = ( 1 + 1 )
63 df-2 2 = ( 1 + 1 )
64 62 63 eqtr4i ( ( 4 − 3 ) + 1 ) = 2
65 56 64 eqtrdi ( 𝑘 = 3 → ( ( 4 − 𝑘 ) + 1 ) = 2 )
66 54 65 oveq12d ( 𝑘 = 3 → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) = ( ( 3 BernPoly 𝑋 ) / 2 ) )
67 53 66 oveq12d ( 𝑘 = 3 → ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( 4 · ( ( 3 BernPoly 𝑋 ) / 2 ) ) )
68 50 67 sylbir ( 𝑘 = ( 2 + 1 ) → ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( 4 · ( ( 3 BernPoly 𝑋 ) / 2 ) ) )
69 10 49 68 fsump1 ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 2 ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) + ( 4 · ( ( 3 BernPoly 𝑋 ) / 2 ) ) ) )
70 63 oveq2i ( 0 ... 2 ) = ( 0 ... ( 1 + 1 ) )
71 70 sumeq1i Σ 𝑘 ∈ ( 0 ... 2 ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 1 + 1 ) ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) )
72 1eluzge0 1 ∈ ( ℤ ‘ 0 )
73 72 a1i ( 𝑋 ∈ ℂ → 1 ∈ ( ℤ ‘ 0 ) )
74 fzssp1 ( 0 ... ( 1 + 1 ) ) ⊆ ( 0 ... ( ( 1 + 1 ) + 1 ) )
75 63 oveq1i ( 2 + 1 ) = ( ( 1 + 1 ) + 1 )
76 75 oveq2i ( 0 ... ( 2 + 1 ) ) = ( 0 ... ( ( 1 + 1 ) + 1 ) )
77 74 76 sseqtrri ( 0 ... ( 1 + 1 ) ) ⊆ ( 0 ... ( 2 + 1 ) )
78 77 sseli ( 𝑘 ∈ ( 0 ... ( 1 + 1 ) ) → 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) )
79 78 49 sylan2 ( ( 𝑋 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 1 + 1 ) ) ) → ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) ∈ ℂ )
80 63 eqeq2i ( 𝑘 = 2 ↔ 𝑘 = ( 1 + 1 ) )
81 oveq2 ( 𝑘 = 2 → ( 4 C 𝑘 ) = ( 4 C 2 ) )
82 4bc2eq6 ( 4 C 2 ) = 6
83 81 82 eqtrdi ( 𝑘 = 2 → ( 4 C 𝑘 ) = 6 )
84 oveq1 ( 𝑘 = 2 → ( 𝑘 BernPoly 𝑋 ) = ( 2 BernPoly 𝑋 ) )
85 oveq2 ( 𝑘 = 2 → ( 4 − 𝑘 ) = ( 4 − 2 ) )
86 85 oveq1d ( 𝑘 = 2 → ( ( 4 − 𝑘 ) + 1 ) = ( ( 4 − 2 ) + 1 ) )
87 2cn 2 ∈ ℂ
88 2p2e4 ( 2 + 2 ) = 4
89 57 87 87 88 subaddrii ( 4 − 2 ) = 2
90 89 oveq1i ( ( 4 − 2 ) + 1 ) = ( 2 + 1 )
91 90 5 eqtr4i ( ( 4 − 2 ) + 1 ) = 3
92 86 91 eqtrdi ( 𝑘 = 2 → ( ( 4 − 𝑘 ) + 1 ) = 3 )
93 84 92 oveq12d ( 𝑘 = 2 → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) = ( ( 2 BernPoly 𝑋 ) / 3 ) )
94 83 93 oveq12d ( 𝑘 = 2 → ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( 6 · ( ( 2 BernPoly 𝑋 ) / 3 ) ) )
95 80 94 sylbir ( 𝑘 = ( 1 + 1 ) → ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( 6 · ( ( 2 BernPoly 𝑋 ) / 3 ) ) )
96 73 79 95 fsump1 ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 1 + 1 ) ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) + ( 6 · ( ( 2 BernPoly 𝑋 ) / 3 ) ) ) )
97 0p1e1 ( 0 + 1 ) = 1
98 97 oveq2i ( 0 ... ( 0 + 1 ) ) = ( 0 ... 1 )
99 98 sumeq1i Σ 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) )
100 0nn0 0 ∈ ℕ0
101 nn0uz 0 = ( ℤ ‘ 0 )
102 100 101 eleqtri 0 ∈ ( ℤ ‘ 0 )
103 102 a1i ( 𝑋 ∈ ℂ → 0 ∈ ( ℤ ‘ 0 ) )
104 3nn 3 ∈ ℕ
105 nnuz ℕ = ( ℤ ‘ 1 )
106 104 105 eleqtri 3 ∈ ( ℤ ‘ 1 )
107 fzss2 ( 3 ∈ ( ℤ ‘ 1 ) → ( 0 ... 1 ) ⊆ ( 0 ... 3 ) )
108 106 107 ax-mp ( 0 ... 1 ) ⊆ ( 0 ... 3 )
109 2p1e3 ( 2 + 1 ) = 3
110 109 oveq2i ( 0 ... ( 2 + 1 ) ) = ( 0 ... 3 )
111 108 98 110 3sstr4i ( 0 ... ( 0 + 1 ) ) ⊆ ( 0 ... ( 2 + 1 ) )
112 111 sseli ( 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) → 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) )
113 112 49 sylan2 ( ( 𝑋 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ) → ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) ∈ ℂ )
114 97 eqeq2i ( 𝑘 = ( 0 + 1 ) ↔ 𝑘 = 1 )
115 oveq2 ( 𝑘 = 1 → ( 4 C 𝑘 ) = ( 4 C 1 ) )
116 bcn1 ( 4 ∈ ℕ0 → ( 4 C 1 ) = 4 )
117 1 116 ax-mp ( 4 C 1 ) = 4
118 115 117 eqtrdi ( 𝑘 = 1 → ( 4 C 𝑘 ) = 4 )
119 oveq1 ( 𝑘 = 1 → ( 𝑘 BernPoly 𝑋 ) = ( 1 BernPoly 𝑋 ) )
120 oveq2 ( 𝑘 = 1 → ( 4 − 𝑘 ) = ( 4 − 1 ) )
121 120 oveq1d ( 𝑘 = 1 → ( ( 4 − 𝑘 ) + 1 ) = ( ( 4 − 1 ) + 1 ) )
122 4 oveq1i ( ( 4 − 1 ) + 1 ) = ( 3 + 1 )
123 df-4 4 = ( 3 + 1 )
124 122 123 eqtr4i ( ( 4 − 1 ) + 1 ) = 4
125 121 124 eqtrdi ( 𝑘 = 1 → ( ( 4 − 𝑘 ) + 1 ) = 4 )
126 119 125 oveq12d ( 𝑘 = 1 → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) = ( ( 1 BernPoly 𝑋 ) / 4 ) )
127 118 126 oveq12d ( 𝑘 = 1 → ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( 4 · ( ( 1 BernPoly 𝑋 ) / 4 ) ) )
128 114 127 sylbi ( 𝑘 = ( 0 + 1 ) → ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( 4 · ( ( 1 BernPoly 𝑋 ) / 4 ) ) )
129 103 113 128 fsump1 ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) + ( 4 · ( ( 1 BernPoly 𝑋 ) / 4 ) ) ) )
130 0z 0 ∈ ℤ
131 59 a1i ( 𝑋 ∈ ℂ → 1 ∈ ℂ )
132 bpolycl ( ( 0 ∈ ℕ0𝑋 ∈ ℂ ) → ( 0 BernPoly 𝑋 ) ∈ ℂ )
133 100 132 mpan ( 𝑋 ∈ ℂ → ( 0 BernPoly 𝑋 ) ∈ ℂ )
134 5cn 5 ∈ ℂ
135 134 a1i ( 𝑋 ∈ ℂ → 5 ∈ ℂ )
136 0re 0 ∈ ℝ
137 5pos 0 < 5
138 136 137 gtneii 5 ≠ 0
139 138 a1i ( 𝑋 ∈ ℂ → 5 ≠ 0 )
140 133 135 139 divcld ( 𝑋 ∈ ℂ → ( ( 0 BernPoly 𝑋 ) / 5 ) ∈ ℂ )
141 131 140 mulcld ( 𝑋 ∈ ℂ → ( 1 · ( ( 0 BernPoly 𝑋 ) / 5 ) ) ∈ ℂ )
142 oveq2 ( 𝑘 = 0 → ( 4 C 𝑘 ) = ( 4 C 0 ) )
143 bcn0 ( 4 ∈ ℕ0 → ( 4 C 0 ) = 1 )
144 1 143 ax-mp ( 4 C 0 ) = 1
145 142 144 eqtrdi ( 𝑘 = 0 → ( 4 C 𝑘 ) = 1 )
146 oveq1 ( 𝑘 = 0 → ( 𝑘 BernPoly 𝑋 ) = ( 0 BernPoly 𝑋 ) )
147 oveq2 ( 𝑘 = 0 → ( 4 − 𝑘 ) = ( 4 − 0 ) )
148 147 oveq1d ( 𝑘 = 0 → ( ( 4 − 𝑘 ) + 1 ) = ( ( 4 − 0 ) + 1 ) )
149 57 subid1i ( 4 − 0 ) = 4
150 149 oveq1i ( ( 4 − 0 ) + 1 ) = ( 4 + 1 )
151 4p1e5 ( 4 + 1 ) = 5
152 150 151 eqtri ( ( 4 − 0 ) + 1 ) = 5
153 148 152 eqtrdi ( 𝑘 = 0 → ( ( 4 − 𝑘 ) + 1 ) = 5 )
154 146 153 oveq12d ( 𝑘 = 0 → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) = ( ( 0 BernPoly 𝑋 ) / 5 ) )
155 145 154 oveq12d ( 𝑘 = 0 → ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( 1 · ( ( 0 BernPoly 𝑋 ) / 5 ) ) )
156 155 fsum1 ( ( 0 ∈ ℤ ∧ ( 1 · ( ( 0 BernPoly 𝑋 ) / 5 ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( 1 · ( ( 0 BernPoly 𝑋 ) / 5 ) ) )
157 130 141 156 sylancr ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( 1 · ( ( 0 BernPoly 𝑋 ) / 5 ) ) )
158 bpoly0 ( 𝑋 ∈ ℂ → ( 0 BernPoly 𝑋 ) = 1 )
159 158 oveq1d ( 𝑋 ∈ ℂ → ( ( 0 BernPoly 𝑋 ) / 5 ) = ( 1 / 5 ) )
160 159 oveq2d ( 𝑋 ∈ ℂ → ( 1 · ( ( 0 BernPoly 𝑋 ) / 5 ) ) = ( 1 · ( 1 / 5 ) ) )
161 134 138 reccli ( 1 / 5 ) ∈ ℂ
162 161 mulid2i ( 1 · ( 1 / 5 ) ) = ( 1 / 5 )
163 160 162 eqtrdi ( 𝑋 ∈ ℂ → ( 1 · ( ( 0 BernPoly 𝑋 ) / 5 ) ) = ( 1 / 5 ) )
164 157 163 eqtrd ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( 1 / 5 ) )
165 1nn0 1 ∈ ℕ0
166 bpolycl ( ( 1 ∈ ℕ0𝑋 ∈ ℂ ) → ( 1 BernPoly 𝑋 ) ∈ ℂ )
167 165 166 mpan ( 𝑋 ∈ ℂ → ( 1 BernPoly 𝑋 ) ∈ ℂ )
168 nn0cn ( 4 ∈ ℕ0 → 4 ∈ ℂ )
169 1 168 mp1i ( 𝑋 ∈ ℂ → 4 ∈ ℂ )
170 4ne0 4 ≠ 0
171 170 a1i ( 𝑋 ∈ ℂ → 4 ≠ 0 )
172 167 169 171 divcan2d ( 𝑋 ∈ ℂ → ( 4 · ( ( 1 BernPoly 𝑋 ) / 4 ) ) = ( 1 BernPoly 𝑋 ) )
173 bpoly1 ( 𝑋 ∈ ℂ → ( 1 BernPoly 𝑋 ) = ( 𝑋 − ( 1 / 2 ) ) )
174 172 173 eqtrd ( 𝑋 ∈ ℂ → ( 4 · ( ( 1 BernPoly 𝑋 ) / 4 ) ) = ( 𝑋 − ( 1 / 2 ) ) )
175 164 174 oveq12d ( 𝑋 ∈ ℂ → ( Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) + ( 4 · ( ( 1 BernPoly 𝑋 ) / 4 ) ) ) = ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) )
176 129 175 eqtrd ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) )
177 99 176 eqtr3id ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) )
178 6cn 6 ∈ ℂ
179 178 a1i ( 𝑋 ∈ ℂ → 6 ∈ ℂ )
180 2nn0 2 ∈ ℕ0
181 bpolycl ( ( 2 ∈ ℕ0𝑋 ∈ ℂ ) → ( 2 BernPoly 𝑋 ) ∈ ℂ )
182 180 181 mpan ( 𝑋 ∈ ℂ → ( 2 BernPoly 𝑋 ) ∈ ℂ )
183 58 a1i ( 𝑋 ∈ ℂ → 3 ∈ ℂ )
184 3ne0 3 ≠ 0
185 184 a1i ( 𝑋 ∈ ℂ → 3 ≠ 0 )
186 179 182 183 185 div12d ( 𝑋 ∈ ℂ → ( 6 · ( ( 2 BernPoly 𝑋 ) / 3 ) ) = ( ( 2 BernPoly 𝑋 ) · ( 6 / 3 ) ) )
187 3t2e6 ( 3 · 2 ) = 6
188 178 58 87 184 divmuli ( ( 6 / 3 ) = 2 ↔ ( 3 · 2 ) = 6 )
189 187 188 mpbir ( 6 / 3 ) = 2
190 189 oveq2i ( ( 2 BernPoly 𝑋 ) · ( 6 / 3 ) ) = ( ( 2 BernPoly 𝑋 ) · 2 )
191 87 a1i ( 𝑋 ∈ ℂ → 2 ∈ ℂ )
192 182 191 mulcomd ( 𝑋 ∈ ℂ → ( ( 2 BernPoly 𝑋 ) · 2 ) = ( 2 · ( 2 BernPoly 𝑋 ) ) )
193 bpoly2 ( 𝑋 ∈ ℂ → ( 2 BernPoly 𝑋 ) = ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) )
194 193 oveq2d ( 𝑋 ∈ ℂ → ( 2 · ( 2 BernPoly 𝑋 ) ) = ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) )
195 192 194 eqtrd ( 𝑋 ∈ ℂ → ( ( 2 BernPoly 𝑋 ) · 2 ) = ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) )
196 190 195 eqtrid ( 𝑋 ∈ ℂ → ( ( 2 BernPoly 𝑋 ) · ( 6 / 3 ) ) = ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) )
197 186 196 eqtrd ( 𝑋 ∈ ℂ → ( 6 · ( ( 2 BernPoly 𝑋 ) / 3 ) ) = ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) )
198 177 197 oveq12d ( 𝑋 ∈ ℂ → ( Σ 𝑘 ∈ ( 0 ... 1 ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) + ( 6 · ( ( 2 BernPoly 𝑋 ) / 3 ) ) ) = ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) )
199 96 198 eqtrd ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 1 + 1 ) ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) )
200 71 199 eqtrid ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... 2 ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) )
201 3nn0 3 ∈ ℕ0
202 bpolycl ( ( 3 ∈ ℕ0𝑋 ∈ ℂ ) → ( 3 BernPoly 𝑋 ) ∈ ℂ )
203 201 202 mpan ( 𝑋 ∈ ℂ → ( 3 BernPoly 𝑋 ) ∈ ℂ )
204 2ne0 2 ≠ 0
205 204 a1i ( 𝑋 ∈ ℂ → 2 ≠ 0 )
206 169 203 191 205 div12d ( 𝑋 ∈ ℂ → ( 4 · ( ( 3 BernPoly 𝑋 ) / 2 ) ) = ( ( 3 BernPoly 𝑋 ) · ( 4 / 2 ) ) )
207 4d2e2 ( 4 / 2 ) = 2
208 207 oveq2i ( ( 3 BernPoly 𝑋 ) · ( 4 / 2 ) ) = ( ( 3 BernPoly 𝑋 ) · 2 )
209 203 191 mulcomd ( 𝑋 ∈ ℂ → ( ( 3 BernPoly 𝑋 ) · 2 ) = ( 2 · ( 3 BernPoly 𝑋 ) ) )
210 bpoly3 ( 𝑋 ∈ ℂ → ( 3 BernPoly 𝑋 ) = ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) )
211 210 oveq2d ( 𝑋 ∈ ℂ → ( 2 · ( 3 BernPoly 𝑋 ) ) = ( 2 · ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ) )
212 209 211 eqtrd ( 𝑋 ∈ ℂ → ( ( 3 BernPoly 𝑋 ) · 2 ) = ( 2 · ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ) )
213 208 212 eqtrid ( 𝑋 ∈ ℂ → ( ( 3 BernPoly 𝑋 ) · ( 4 / 2 ) ) = ( 2 · ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ) )
214 206 213 eqtrd ( 𝑋 ∈ ℂ → ( 4 · ( ( 3 BernPoly 𝑋 ) / 2 ) ) = ( 2 · ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ) )
215 200 214 oveq12d ( 𝑋 ∈ ℂ → ( Σ 𝑘 ∈ ( 0 ... 2 ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) + ( 4 · ( ( 3 BernPoly 𝑋 ) / 2 ) ) ) = ( ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ) ) )
216 69 215 eqtrd ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 2 + 1 ) ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ) ) )
217 8 216 eqtrid ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 4 − 1 ) ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) = ( ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ) ) )
218 217 oveq2d ( 𝑋 ∈ ℂ → ( ( 𝑋 ↑ 4 ) − Σ 𝑘 ∈ ( 0 ... ( 4 − 1 ) ) ( ( 4 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 4 − 𝑘 ) + 1 ) ) ) ) = ( ( 𝑋 ↑ 4 ) − ( ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ) ) ) )
219 expcl ( ( 𝑋 ∈ ℂ ∧ 4 ∈ ℕ0 ) → ( 𝑋 ↑ 4 ) ∈ ℂ )
220 1 219 mpan2 ( 𝑋 ∈ ℂ → ( 𝑋 ↑ 4 ) ∈ ℂ )
221 expcl ( ( 𝑋 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑋 ↑ 3 ) ∈ ℂ )
222 201 221 mpan2 ( 𝑋 ∈ ℂ → ( 𝑋 ↑ 3 ) ∈ ℂ )
223 191 222 mulcld ( 𝑋 ∈ ℂ → ( 2 · ( 𝑋 ↑ 3 ) ) ∈ ℂ )
224 sqcl ( 𝑋 ∈ ℂ → ( 𝑋 ↑ 2 ) ∈ ℂ )
225 201 100 deccl 3 0 ∈ ℕ0
226 225 nn0cni 3 0 ∈ ℂ
227 dfdec10 3 0 = ( ( 1 0 · 3 ) + 0 )
228 10re 1 0 ∈ ℝ
229 228 recni 1 0 ∈ ℂ
230 229 58 mulcli ( 1 0 · 3 ) ∈ ℂ
231 230 addid1i ( ( 1 0 · 3 ) + 0 ) = ( 1 0 · 3 )
232 227 231 eqtri 3 0 = ( 1 0 · 3 )
233 10pos 0 < 1 0
234 136 233 gtneii 1 0 ≠ 0
235 229 58 234 184 mulne0i ( 1 0 · 3 ) ≠ 0
236 232 235 eqnetri 3 0 ≠ 0
237 226 236 reccli ( 1 / 3 0 ) ∈ ℂ
238 237 a1i ( 𝑋 ∈ ℂ → ( 1 / 3 0 ) ∈ ℂ )
239 224 238 subcld ( 𝑋 ∈ ℂ → ( ( 𝑋 ↑ 2 ) − ( 1 / 3 0 ) ) ∈ ℂ )
240 220 223 239 subsubd ( 𝑋 ∈ ℂ → ( ( 𝑋 ↑ 4 ) − ( ( 2 · ( 𝑋 ↑ 3 ) ) − ( ( 𝑋 ↑ 2 ) − ( 1 / 3 0 ) ) ) ) = ( ( ( 𝑋 ↑ 4 ) − ( 2 · ( 𝑋 ↑ 3 ) ) ) + ( ( 𝑋 ↑ 2 ) − ( 1 / 3 0 ) ) ) )
241 161 a1i ( 𝑋 ∈ ℂ → ( 1 / 5 ) ∈ ℂ )
242 id ( 𝑋 ∈ ℂ → 𝑋 ∈ ℂ )
243 87 204 reccli ( 1 / 2 ) ∈ ℂ
244 243 a1i ( 𝑋 ∈ ℂ → ( 1 / 2 ) ∈ ℂ )
245 242 244 subcld ( 𝑋 ∈ ℂ → ( 𝑋 − ( 1 / 2 ) ) ∈ ℂ )
246 241 245 addcld ( 𝑋 ∈ ℂ → ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) ∈ ℂ )
247 224 242 subcld ( 𝑋 ∈ ℂ → ( ( 𝑋 ↑ 2 ) − 𝑋 ) ∈ ℂ )
248 6pos 0 < 6
249 136 248 gtneii 6 ≠ 0
250 178 249 reccli ( 1 / 6 ) ∈ ℂ
251 250 a1i ( 𝑋 ∈ ℂ → ( 1 / 6 ) ∈ ℂ )
252 247 251 addcld ( 𝑋 ∈ ℂ → ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ∈ ℂ )
253 191 252 mulcld ( 𝑋 ∈ ℂ → ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ∈ ℂ )
254 246 253 addcld ( 𝑋 ∈ ℂ → ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ∈ ℂ )
255 58 87 204 divcli ( 3 / 2 ) ∈ ℂ
256 255 a1i ( 𝑋 ∈ ℂ → ( 3 / 2 ) ∈ ℂ )
257 256 224 mulcld ( 𝑋 ∈ ℂ → ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ∈ ℂ )
258 222 257 subcld ( 𝑋 ∈ ℂ → ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) ∈ ℂ )
259 244 242 mulcld ( 𝑋 ∈ ℂ → ( ( 1 / 2 ) · 𝑋 ) ∈ ℂ )
260 258 259 addcld ( 𝑋 ∈ ℂ → ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ∈ ℂ )
261 191 260 mulcld ( 𝑋 ∈ ℂ → ( 2 · ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ) ∈ ℂ )
262 254 261 addcomd ( 𝑋 ∈ ℂ → ( ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ) ) = ( ( 2 · ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ) + ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) )
263 191 258 259 adddid ( 𝑋 ∈ ℂ → ( 2 · ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ) = ( ( 2 · ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) ) + ( 2 · ( ( 1 / 2 ) · 𝑋 ) ) ) )
264 191 222 257 subdid ( 𝑋 ∈ ℂ → ( 2 · ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) ) = ( ( 2 · ( 𝑋 ↑ 3 ) ) − ( 2 · ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) ) )
265 87 204 recidi ( 2 · ( 1 / 2 ) ) = 1
266 265 oveq1i ( ( 2 · ( 1 / 2 ) ) · 𝑋 ) = ( 1 · 𝑋 )
267 191 244 242 mulassd ( 𝑋 ∈ ℂ → ( ( 2 · ( 1 / 2 ) ) · 𝑋 ) = ( 2 · ( ( 1 / 2 ) · 𝑋 ) ) )
268 mulid2 ( 𝑋 ∈ ℂ → ( 1 · 𝑋 ) = 𝑋 )
269 266 267 268 3eqtr3a ( 𝑋 ∈ ℂ → ( 2 · ( ( 1 / 2 ) · 𝑋 ) ) = 𝑋 )
270 264 269 oveq12d ( 𝑋 ∈ ℂ → ( ( 2 · ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) ) + ( 2 · ( ( 1 / 2 ) · 𝑋 ) ) ) = ( ( ( 2 · ( 𝑋 ↑ 3 ) ) − ( 2 · ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) ) + 𝑋 ) )
271 263 270 eqtrd ( 𝑋 ∈ ℂ → ( 2 · ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ) = ( ( ( 2 · ( 𝑋 ↑ 3 ) ) − ( 2 · ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) ) + 𝑋 ) )
272 271 oveq1d ( 𝑋 ∈ ℂ → ( ( 2 · ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ) + ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) = ( ( ( ( 2 · ( 𝑋 ↑ 3 ) ) − ( 2 · ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) ) + 𝑋 ) + ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) )
273 191 257 mulcld ( 𝑋 ∈ ℂ → ( 2 · ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) ∈ ℂ )
274 223 273 subcld ( 𝑋 ∈ ℂ → ( ( 2 · ( 𝑋 ↑ 3 ) ) − ( 2 · ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) ) ∈ ℂ )
275 274 242 254 addassd ( 𝑋 ∈ ℂ → ( ( ( ( 2 · ( 𝑋 ↑ 3 ) ) − ( 2 · ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) ) + 𝑋 ) + ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) = ( ( ( 2 · ( 𝑋 ↑ 3 ) ) − ( 2 · ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) ) + ( 𝑋 + ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) ) )
276 242 254 addcld ( 𝑋 ∈ ℂ → ( 𝑋 + ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) ∈ ℂ )
277 223 273 276 subsubd ( 𝑋 ∈ ℂ → ( ( 2 · ( 𝑋 ↑ 3 ) ) − ( ( 2 · ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) − ( 𝑋 + ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) ) ) = ( ( ( 2 · ( 𝑋 ↑ 3 ) ) − ( 2 · ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) ) + ( 𝑋 + ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) ) )
278 191 256 224 mulassd ( 𝑋 ∈ ℂ → ( ( 2 · ( 3 / 2 ) ) · ( 𝑋 ↑ 2 ) ) = ( 2 · ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) )
279 58 87 204 divcan2i ( 2 · ( 3 / 2 ) ) = 3
280 279 oveq1i ( ( 2 · ( 3 / 2 ) ) · ( 𝑋 ↑ 2 ) ) = ( 3 · ( 𝑋 ↑ 2 ) )
281 278 280 eqtr3di ( 𝑋 ∈ ℂ → ( 2 · ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) = ( 3 · ( 𝑋 ↑ 2 ) ) )
282 281 oveq1d ( 𝑋 ∈ ℂ → ( ( 2 · ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) − ( 𝑋 + ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) ) = ( ( 3 · ( 𝑋 ↑ 2 ) ) − ( 𝑋 + ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) ) )
283 242 246 253 add12d ( 𝑋 ∈ ℂ → ( 𝑋 + ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) = ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 𝑋 + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) )
284 191 247 251 adddid ( 𝑋 ∈ ℂ → ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) = ( ( 2 · ( ( 𝑋 ↑ 2 ) − 𝑋 ) ) + ( 2 · ( 1 / 6 ) ) ) )
285 191 224 242 subdid ( 𝑋 ∈ ℂ → ( 2 · ( ( 𝑋 ↑ 2 ) − 𝑋 ) ) = ( ( 2 · ( 𝑋 ↑ 2 ) ) − ( 2 · 𝑋 ) ) )
286 187 oveq2i ( 2 / ( 3 · 2 ) ) = ( 2 / 6 )
287 58 184 reccli ( 1 / 3 ) ∈ ℂ
288 58 87 287 mul32i ( ( 3 · 2 ) · ( 1 / 3 ) ) = ( ( 3 · ( 1 / 3 ) ) · 2 )
289 58 184 recidi ( 3 · ( 1 / 3 ) ) = 1
290 289 oveq1i ( ( 3 · ( 1 / 3 ) ) · 2 ) = ( 1 · 2 )
291 87 mulid2i ( 1 · 2 ) = 2
292 290 291 eqtri ( ( 3 · ( 1 / 3 ) ) · 2 ) = 2
293 288 292 eqtri ( ( 3 · 2 ) · ( 1 / 3 ) ) = 2
294 187 178 eqeltri ( 3 · 2 ) ∈ ℂ
295 187 249 eqnetri ( 3 · 2 ) ≠ 0
296 87 294 287 295 divmuli ( ( 2 / ( 3 · 2 ) ) = ( 1 / 3 ) ↔ ( ( 3 · 2 ) · ( 1 / 3 ) ) = 2 )
297 293 296 mpbir ( 2 / ( 3 · 2 ) ) = ( 1 / 3 )
298 87 178 249 divreci ( 2 / 6 ) = ( 2 · ( 1 / 6 ) )
299 286 297 298 3eqtr3ri ( 2 · ( 1 / 6 ) ) = ( 1 / 3 )
300 299 a1i ( 𝑋 ∈ ℂ → ( 2 · ( 1 / 6 ) ) = ( 1 / 3 ) )
301 285 300 oveq12d ( 𝑋 ∈ ℂ → ( ( 2 · ( ( 𝑋 ↑ 2 ) − 𝑋 ) ) + ( 2 · ( 1 / 6 ) ) ) = ( ( ( 2 · ( 𝑋 ↑ 2 ) ) − ( 2 · 𝑋 ) ) + ( 1 / 3 ) ) )
302 284 301 eqtrd ( 𝑋 ∈ ℂ → ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) = ( ( ( 2 · ( 𝑋 ↑ 2 ) ) − ( 2 · 𝑋 ) ) + ( 1 / 3 ) ) )
303 302 oveq2d ( 𝑋 ∈ ℂ → ( 𝑋 + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) = ( 𝑋 + ( ( ( 2 · ( 𝑋 ↑ 2 ) ) − ( 2 · 𝑋 ) ) + ( 1 / 3 ) ) ) )
304 191 224 mulcld ( 𝑋 ∈ ℂ → ( 2 · ( 𝑋 ↑ 2 ) ) ∈ ℂ )
305 191 242 mulcld ( 𝑋 ∈ ℂ → ( 2 · 𝑋 ) ∈ ℂ )
306 304 305 subcld ( 𝑋 ∈ ℂ → ( ( 2 · ( 𝑋 ↑ 2 ) ) − ( 2 · 𝑋 ) ) ∈ ℂ )
307 287 a1i ( 𝑋 ∈ ℂ → ( 1 / 3 ) ∈ ℂ )
308 242 306 307 addassd ( 𝑋 ∈ ℂ → ( ( 𝑋 + ( ( 2 · ( 𝑋 ↑ 2 ) ) − ( 2 · 𝑋 ) ) ) + ( 1 / 3 ) ) = ( 𝑋 + ( ( ( 2 · ( 𝑋 ↑ 2 ) ) − ( 2 · 𝑋 ) ) + ( 1 / 3 ) ) ) )
309 242 304 305 addsub12d ( 𝑋 ∈ ℂ → ( 𝑋 + ( ( 2 · ( 𝑋 ↑ 2 ) ) − ( 2 · 𝑋 ) ) ) = ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) )
310 309 oveq1d ( 𝑋 ∈ ℂ → ( ( 𝑋 + ( ( 2 · ( 𝑋 ↑ 2 ) ) − ( 2 · 𝑋 ) ) ) + ( 1 / 3 ) ) = ( ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( 1 / 3 ) ) )
311 303 308 310 3eqtr2d ( 𝑋 ∈ ℂ → ( 𝑋 + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) = ( ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( 1 / 3 ) ) )
312 311 oveq2d ( 𝑋 ∈ ℂ → ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 𝑋 + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) = ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( 1 / 3 ) ) ) )
313 283 312 eqtrd ( 𝑋 ∈ ℂ → ( 𝑋 + ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) = ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( 1 / 3 ) ) ) )
314 313 oveq2d ( 𝑋 ∈ ℂ → ( ( 3 · ( 𝑋 ↑ 2 ) ) − ( 𝑋 + ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) ) = ( ( 3 · ( 𝑋 ↑ 2 ) ) − ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( 1 / 3 ) ) ) ) )
315 242 305 subcld ( 𝑋 ∈ ℂ → ( 𝑋 − ( 2 · 𝑋 ) ) ∈ ℂ )
316 304 315 addcld ( 𝑋 ∈ ℂ → ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) ∈ ℂ )
317 241 245 316 307 add4d ( 𝑋 ∈ ℂ → ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( 1 / 3 ) ) ) = ( ( ( 1 / 5 ) + ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) ) + ( ( 𝑋 − ( 1 / 2 ) ) + ( 1 / 3 ) ) ) )
318 241 304 315 add12d ( 𝑋 ∈ ℂ → ( ( 1 / 5 ) + ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) ) = ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( ( 1 / 5 ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) ) )
319 318 oveq1d ( 𝑋 ∈ ℂ → ( ( ( 1 / 5 ) + ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) ) + ( ( 𝑋 − ( 1 / 2 ) ) + ( 1 / 3 ) ) ) = ( ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( ( 1 / 5 ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) ) + ( ( 𝑋 − ( 1 / 2 ) ) + ( 1 / 3 ) ) ) )
320 241 315 addcld ( 𝑋 ∈ ℂ → ( ( 1 / 5 ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) ∈ ℂ )
321 245 307 addcld ( 𝑋 ∈ ℂ → ( ( 𝑋 − ( 1 / 2 ) ) + ( 1 / 3 ) ) ∈ ℂ )
322 304 320 321 addassd ( 𝑋 ∈ ℂ → ( ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( ( 1 / 5 ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) ) + ( ( 𝑋 − ( 1 / 2 ) ) + ( 1 / 3 ) ) ) = ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( ( ( 1 / 5 ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( ( 𝑋 − ( 1 / 2 ) ) + ( 1 / 3 ) ) ) ) )
323 317 319 322 3eqtrd ( 𝑋 ∈ ℂ → ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( 1 / 3 ) ) ) = ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( ( ( 1 / 5 ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( ( 𝑋 − ( 1 / 2 ) ) + ( 1 / 3 ) ) ) ) )
324 323 oveq2d ( 𝑋 ∈ ℂ → ( ( 3 · ( 𝑋 ↑ 2 ) ) − ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( 1 / 3 ) ) ) ) = ( ( 3 · ( 𝑋 ↑ 2 ) ) − ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( ( ( 1 / 5 ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( ( 𝑋 − ( 1 / 2 ) ) + ( 1 / 3 ) ) ) ) ) )
325 183 224 mulcld ( 𝑋 ∈ ℂ → ( 3 · ( 𝑋 ↑ 2 ) ) ∈ ℂ )
326 320 321 addcld ( 𝑋 ∈ ℂ → ( ( ( 1 / 5 ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( ( 𝑋 − ( 1 / 2 ) ) + ( 1 / 3 ) ) ) ∈ ℂ )
327 325 304 326 subsub4d ( 𝑋 ∈ ℂ → ( ( ( 3 · ( 𝑋 ↑ 2 ) ) − ( 2 · ( 𝑋 ↑ 2 ) ) ) − ( ( ( 1 / 5 ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( ( 𝑋 − ( 1 / 2 ) ) + ( 1 / 3 ) ) ) ) = ( ( 3 · ( 𝑋 ↑ 2 ) ) − ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( ( ( 1 / 5 ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( ( 𝑋 − ( 1 / 2 ) ) + ( 1 / 3 ) ) ) ) ) )
328 58 87 59 109 subaddrii ( 3 − 2 ) = 1
329 328 oveq1i ( ( 3 − 2 ) · ( 𝑋 ↑ 2 ) ) = ( 1 · ( 𝑋 ↑ 2 ) )
330 183 191 224 subdird ( 𝑋 ∈ ℂ → ( ( 3 − 2 ) · ( 𝑋 ↑ 2 ) ) = ( ( 3 · ( 𝑋 ↑ 2 ) ) − ( 2 · ( 𝑋 ↑ 2 ) ) ) )
331 224 mulid2d ( 𝑋 ∈ ℂ → ( 1 · ( 𝑋 ↑ 2 ) ) = ( 𝑋 ↑ 2 ) )
332 329 330 331 3eqtr3a ( 𝑋 ∈ ℂ → ( ( 3 · ( 𝑋 ↑ 2 ) ) − ( 2 · ( 𝑋 ↑ 2 ) ) ) = ( 𝑋 ↑ 2 ) )
333 241 305 242 subsubd ( 𝑋 ∈ ℂ → ( ( 1 / 5 ) − ( ( 2 · 𝑋 ) − 𝑋 ) ) = ( ( ( 1 / 5 ) − ( 2 · 𝑋 ) ) + 𝑋 ) )
334 2txmxeqx ( 𝑋 ∈ ℂ → ( ( 2 · 𝑋 ) − 𝑋 ) = 𝑋 )
335 334 oveq2d ( 𝑋 ∈ ℂ → ( ( 1 / 5 ) − ( ( 2 · 𝑋 ) − 𝑋 ) ) = ( ( 1 / 5 ) − 𝑋 ) )
336 241 305 242 subadd23d ( 𝑋 ∈ ℂ → ( ( ( 1 / 5 ) − ( 2 · 𝑋 ) ) + 𝑋 ) = ( ( 1 / 5 ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) )
337 333 335 336 3eqtr3d ( 𝑋 ∈ ℂ → ( ( 1 / 5 ) − 𝑋 ) = ( ( 1 / 5 ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) )
338 242 244 307 subsubd ( 𝑋 ∈ ℂ → ( 𝑋 − ( ( 1 / 2 ) − ( 1 / 3 ) ) ) = ( ( 𝑋 − ( 1 / 2 ) ) + ( 1 / 3 ) ) )
339 337 338 oveq12d ( 𝑋 ∈ ℂ → ( ( ( 1 / 5 ) − 𝑋 ) + ( 𝑋 − ( ( 1 / 2 ) − ( 1 / 3 ) ) ) ) = ( ( ( 1 / 5 ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( ( 𝑋 − ( 1 / 2 ) ) + ( 1 / 3 ) ) ) )
340 243 287 subcli ( ( 1 / 2 ) − ( 1 / 3 ) ) ∈ ℂ
341 340 a1i ( 𝑋 ∈ ℂ → ( ( 1 / 2 ) − ( 1 / 3 ) ) ∈ ℂ )
342 241 242 341 npncand ( 𝑋 ∈ ℂ → ( ( ( 1 / 5 ) − 𝑋 ) + ( 𝑋 − ( ( 1 / 2 ) − ( 1 / 3 ) ) ) ) = ( ( 1 / 5 ) − ( ( 1 / 2 ) − ( 1 / 3 ) ) ) )
343 halfthird ( ( 1 / 2 ) − ( 1 / 3 ) ) = ( 1 / 6 )
344 343 oveq2i ( ( 1 / 5 ) − ( ( 1 / 2 ) − ( 1 / 3 ) ) ) = ( ( 1 / 5 ) − ( 1 / 6 ) )
345 5recm6rec ( ( 1 / 5 ) − ( 1 / 6 ) ) = ( 1 / 3 0 )
346 344 345 eqtri ( ( 1 / 5 ) − ( ( 1 / 2 ) − ( 1 / 3 ) ) ) = ( 1 / 3 0 )
347 342 346 eqtrdi ( 𝑋 ∈ ℂ → ( ( ( 1 / 5 ) − 𝑋 ) + ( 𝑋 − ( ( 1 / 2 ) − ( 1 / 3 ) ) ) ) = ( 1 / 3 0 ) )
348 339 347 eqtr3d ( 𝑋 ∈ ℂ → ( ( ( 1 / 5 ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( ( 𝑋 − ( 1 / 2 ) ) + ( 1 / 3 ) ) ) = ( 1 / 3 0 ) )
349 332 348 oveq12d ( 𝑋 ∈ ℂ → ( ( ( 3 · ( 𝑋 ↑ 2 ) ) − ( 2 · ( 𝑋 ↑ 2 ) ) ) − ( ( ( 1 / 5 ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( ( 𝑋 − ( 1 / 2 ) ) + ( 1 / 3 ) ) ) ) = ( ( 𝑋 ↑ 2 ) − ( 1 / 3 0 ) ) )
350 324 327 349 3eqtr2d ( 𝑋 ∈ ℂ → ( ( 3 · ( 𝑋 ↑ 2 ) ) − ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( ( ( 2 · ( 𝑋 ↑ 2 ) ) + ( 𝑋 − ( 2 · 𝑋 ) ) ) + ( 1 / 3 ) ) ) ) = ( ( 𝑋 ↑ 2 ) − ( 1 / 3 0 ) ) )
351 282 314 350 3eqtrd ( 𝑋 ∈ ℂ → ( ( 2 · ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) − ( 𝑋 + ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) ) = ( ( 𝑋 ↑ 2 ) − ( 1 / 3 0 ) ) )
352 351 oveq2d ( 𝑋 ∈ ℂ → ( ( 2 · ( 𝑋 ↑ 3 ) ) − ( ( 2 · ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) − ( 𝑋 + ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) ) ) = ( ( 2 · ( 𝑋 ↑ 3 ) ) − ( ( 𝑋 ↑ 2 ) − ( 1 / 3 0 ) ) ) )
353 275 277 352 3eqtr2d ( 𝑋 ∈ ℂ → ( ( ( ( 2 · ( 𝑋 ↑ 3 ) ) − ( 2 · ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) ) + 𝑋 ) + ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) ) = ( ( 2 · ( 𝑋 ↑ 3 ) ) − ( ( 𝑋 ↑ 2 ) − ( 1 / 3 0 ) ) ) )
354 262 272 353 3eqtrd ( 𝑋 ∈ ℂ → ( ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ) ) = ( ( 2 · ( 𝑋 ↑ 3 ) ) − ( ( 𝑋 ↑ 2 ) − ( 1 / 3 0 ) ) ) )
355 354 oveq2d ( 𝑋 ∈ ℂ → ( ( 𝑋 ↑ 4 ) − ( ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ) ) ) = ( ( 𝑋 ↑ 4 ) − ( ( 2 · ( 𝑋 ↑ 3 ) ) − ( ( 𝑋 ↑ 2 ) − ( 1 / 3 0 ) ) ) ) )
356 220 223 subcld ( 𝑋 ∈ ℂ → ( ( 𝑋 ↑ 4 ) − ( 2 · ( 𝑋 ↑ 3 ) ) ) ∈ ℂ )
357 356 224 238 addsubassd ( 𝑋 ∈ ℂ → ( ( ( ( 𝑋 ↑ 4 ) − ( 2 · ( 𝑋 ↑ 3 ) ) ) + ( 𝑋 ↑ 2 ) ) − ( 1 / 3 0 ) ) = ( ( ( 𝑋 ↑ 4 ) − ( 2 · ( 𝑋 ↑ 3 ) ) ) + ( ( 𝑋 ↑ 2 ) − ( 1 / 3 0 ) ) ) )
358 240 355 357 3eqtr4d ( 𝑋 ∈ ℂ → ( ( 𝑋 ↑ 4 ) − ( ( ( ( 1 / 5 ) + ( 𝑋 − ( 1 / 2 ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) ) ) + ( 2 · ( ( ( 𝑋 ↑ 3 ) − ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) + ( ( 1 / 2 ) · 𝑋 ) ) ) ) ) = ( ( ( ( 𝑋 ↑ 4 ) − ( 2 · ( 𝑋 ↑ 3 ) ) ) + ( 𝑋 ↑ 2 ) ) − ( 1 / 3 0 ) ) )
359 3 218 358 3eqtrd ( 𝑋 ∈ ℂ → ( 4 BernPoly 𝑋 ) = ( ( ( ( 𝑋 ↑ 4 ) − ( 2 · ( 𝑋 ↑ 3 ) ) ) + ( 𝑋 ↑ 2 ) ) − ( 1 / 3 0 ) ) )