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 syl5eqr ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 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 syl5eq ⊢ ( 𝑋 ∈ ℂ → ( ( 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 syl5eq ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 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 syl5eq ⊢ ( 𝑋 ∈ ℂ → ( ( 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 syl5eq ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 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 58 87 204 divcan2i ⊢ ( 2 · ( 3 / 2 ) ) = 3
279 278 oveq1i ⊢ ( ( 2 · ( 3 / 2 ) ) · ( 𝑋 ↑ 2 ) ) = ( 3 · ( 𝑋 ↑ 2 ) )
280 191 256 224 mulassd ⊢ ( 𝑋 ∈ ℂ → ( ( 2 · ( 3 / 2 ) ) · ( 𝑋 ↑ 2 ) ) = ( 2 · ( ( 3 / 2 ) · ( 𝑋 ↑ 2 ) ) ) )
281 279 280 syl5reqr ⊢ ( 𝑋 ∈ ℂ → ( 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 ) ) )