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 ) ) ) |