Step | Hyp | Ref
| Expression |
1 | | 3nn0 12436 |
. . 3
โข 3 โ
โ0 |
2 | | bpolyval 15937 |
. . 3
โข ((3
โ โ0 โง ๐ โ โ) โ (3 BernPoly ๐) = ((๐โ3) โ ฮฃ๐ โ (0...(3 โ 1))((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))))) |
3 | 1, 2 | mpan 689 |
. 2
โข (๐ โ โ โ (3
BernPoly ๐) = ((๐โ3) โ ฮฃ๐ โ (0...(3 โ
1))((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))))) |
4 | | 3m1e2 12286 |
. . . . . . 7
โข (3
โ 1) = 2 |
5 | | df-2 12221 |
. . . . . . 7
โข 2 = (1 +
1) |
6 | 4, 5 | eqtri 2761 |
. . . . . 6
โข (3
โ 1) = (1 + 1) |
7 | 6 | oveq2i 7369 |
. . . . 5
โข (0...(3
โ 1)) = (0...(1 + 1)) |
8 | 7 | sumeq1i 15588 |
. . . 4
โข
ฮฃ๐ โ
(0...(3 โ 1))((3C๐)
ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = ฮฃ๐ โ (0...(1 + 1))((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) |
9 | | 1eluzge0 12822 |
. . . . . . 7
โข 1 โ
(โคโฅโ0) |
10 | 9 | a1i 11 |
. . . . . 6
โข (๐ โ โ โ 1 โ
(โคโฅโ0)) |
11 | | 0z 12515 |
. . . . . . . . . . . . 13
โข 0 โ
โค |
12 | | fzpr 13502 |
. . . . . . . . . . . . 13
โข (0 โ
โค โ (0...(0 + 1)) = {0, (0 + 1)}) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . . . . 12
โข (0...(0 +
1)) = {0, (0 + 1)} |
14 | | 0p1e1 12280 |
. . . . . . . . . . . . 13
โข (0 + 1) =
1 |
15 | 14 | oveq2i 7369 |
. . . . . . . . . . . 12
โข (0...(0 +
1)) = (0...1) |
16 | 14 | preq2i 4699 |
. . . . . . . . . . . 12
โข {0, (0 +
1)} = {0, 1} |
17 | 13, 15, 16 | 3eqtr3ri 2770 |
. . . . . . . . . . 11
โข {0, 1} =
(0...1) |
18 | 5 | sneqi 4598 |
. . . . . . . . . . 11
โข {2} = {(1
+ 1)} |
19 | 17, 18 | uneq12i 4122 |
. . . . . . . . . 10
โข ({0, 1}
โช {2}) = ((0...1) โช {(1 + 1)}) |
20 | | df-tp 4592 |
. . . . . . . . . 10
โข {0, 1, 2}
= ({0, 1} โช {2}) |
21 | | fzsuc 13494 |
. . . . . . . . . . 11
โข (1 โ
(โคโฅโ0) โ (0...(1 + 1)) = ((0...1) โช {(1 +
1)})) |
22 | 9, 21 | ax-mp 5 |
. . . . . . . . . 10
โข (0...(1 +
1)) = ((0...1) โช {(1 + 1)}) |
23 | 19, 20, 22 | 3eqtr4ri 2772 |
. . . . . . . . 9
โข (0...(1 +
1)) = {0, 1, 2} |
24 | 23 | eleq2i 2826 |
. . . . . . . 8
โข (๐ โ (0...(1 + 1)) โ
๐ โ {0, 1,
2}) |
25 | | vex 3448 |
. . . . . . . . 9
โข ๐ โ V |
26 | 25 | eltp 4650 |
. . . . . . . 8
โข (๐ โ {0, 1, 2} โ (๐ = 0 โจ ๐ = 1 โจ ๐ = 2)) |
27 | 24, 26 | bitri 275 |
. . . . . . 7
โข (๐ โ (0...(1 + 1)) โ
(๐ = 0 โจ ๐ = 1 โจ ๐ = 2)) |
28 | | oveq2 7366 |
. . . . . . . . . . . 12
โข (๐ = 0 โ (3C๐) = (3C0)) |
29 | | bcn0 14216 |
. . . . . . . . . . . . 13
โข (3 โ
โ0 โ (3C0) = 1) |
30 | 1, 29 | ax-mp 5 |
. . . . . . . . . . . 12
โข (3C0) =
1 |
31 | 28, 30 | eqtrdi 2789 |
. . . . . . . . . . 11
โข (๐ = 0 โ (3C๐) = 1) |
32 | | oveq1 7365 |
. . . . . . . . . . . 12
โข (๐ = 0 โ (๐ BernPoly ๐) = (0 BernPoly ๐)) |
33 | | oveq2 7366 |
. . . . . . . . . . . . . 14
โข (๐ = 0 โ (3 โ ๐) = (3 โ
0)) |
34 | 33 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ = 0 โ ((3 โ ๐) + 1) = ((3 โ 0) +
1)) |
35 | | 3cn 12239 |
. . . . . . . . . . . . . . . 16
โข 3 โ
โ |
36 | 35 | subid1i 11478 |
. . . . . . . . . . . . . . 15
โข (3
โ 0) = 3 |
37 | 36 | oveq1i 7368 |
. . . . . . . . . . . . . 14
โข ((3
โ 0) + 1) = (3 + 1) |
38 | | df-4 12223 |
. . . . . . . . . . . . . 14
โข 4 = (3 +
1) |
39 | 37, 38 | eqtr4i 2764 |
. . . . . . . . . . . . 13
โข ((3
โ 0) + 1) = 4 |
40 | 34, 39 | eqtrdi 2789 |
. . . . . . . . . . . 12
โข (๐ = 0 โ ((3 โ ๐) + 1) = 4) |
41 | 32, 40 | oveq12d 7376 |
. . . . . . . . . . 11
โข (๐ = 0 โ ((๐ BernPoly ๐) / ((3 โ ๐) + 1)) = ((0 BernPoly ๐) / 4)) |
42 | 31, 41 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ = 0 โ ((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = (1 ยท ((0 BernPoly ๐) / 4))) |
43 | | bpoly0 15938 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (0
BernPoly ๐) =
1) |
44 | 43 | oveq1d 7373 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((0
BernPoly ๐) / 4) = (1 /
4)) |
45 | 44 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ โ โ โ (1
ยท ((0 BernPoly ๐) /
4)) = (1 ยท (1 / 4))) |
46 | | 4cn 12243 |
. . . . . . . . . . . . 13
โข 4 โ
โ |
47 | | 4ne0 12266 |
. . . . . . . . . . . . 13
โข 4 โ
0 |
48 | 46, 47 | reccli 11890 |
. . . . . . . . . . . 12
โข (1 / 4)
โ โ |
49 | 48 | mulid2i 11165 |
. . . . . . . . . . 11
โข (1
ยท (1 / 4)) = (1 / 4) |
50 | 45, 49 | eqtrdi 2789 |
. . . . . . . . . 10
โข (๐ โ โ โ (1
ยท ((0 BernPoly ๐) /
4)) = (1 / 4)) |
51 | 42, 50 | sylan9eqr 2795 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ = 0) โ ((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = (1 / 4)) |
52 | 51, 48 | eqeltrdi 2842 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ = 0) โ ((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) โ โ) |
53 | | oveq2 7366 |
. . . . . . . . . . . 12
โข (๐ = 1 โ (3C๐) = (3C1)) |
54 | | bcn1 14219 |
. . . . . . . . . . . . 13
โข (3 โ
โ0 โ (3C1) = 3) |
55 | 1, 54 | ax-mp 5 |
. . . . . . . . . . . 12
โข (3C1) =
3 |
56 | 53, 55 | eqtrdi 2789 |
. . . . . . . . . . 11
โข (๐ = 1 โ (3C๐) = 3) |
57 | | oveq1 7365 |
. . . . . . . . . . . 12
โข (๐ = 1 โ (๐ BernPoly ๐) = (1 BernPoly ๐)) |
58 | | oveq2 7366 |
. . . . . . . . . . . . . 14
โข (๐ = 1 โ (3 โ ๐) = (3 โ
1)) |
59 | 58 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ = 1 โ ((3 โ ๐) + 1) = ((3 โ 1) +
1)) |
60 | | ax-1cn 11114 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
61 | | npcan 11415 |
. . . . . . . . . . . . . 14
โข ((3
โ โ โง 1 โ โ) โ ((3 โ 1) + 1) =
3) |
62 | 35, 60, 61 | mp2an 691 |
. . . . . . . . . . . . 13
โข ((3
โ 1) + 1) = 3 |
63 | 59, 62 | eqtrdi 2789 |
. . . . . . . . . . . 12
โข (๐ = 1 โ ((3 โ ๐) + 1) = 3) |
64 | 57, 63 | oveq12d 7376 |
. . . . . . . . . . 11
โข (๐ = 1 โ ((๐ BernPoly ๐) / ((3 โ ๐) + 1)) = ((1 BernPoly ๐) / 3)) |
65 | 56, 64 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ = 1 โ ((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = (3 ยท ((1 BernPoly ๐) / 3))) |
66 | | bpoly1 15939 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (1
BernPoly ๐) = (๐ โ (1 /
2))) |
67 | 66 | oveq1d 7373 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((1
BernPoly ๐) / 3) = ((๐ โ (1 / 2)) /
3)) |
68 | 67 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ โ โ โ (3
ยท ((1 BernPoly ๐) /
3)) = (3 ยท ((๐
โ (1 / 2)) / 3))) |
69 | | halfcn 12373 |
. . . . . . . . . . . . 13
โข (1 / 2)
โ โ |
70 | | subcl 11405 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง (1 / 2)
โ โ) โ (๐
โ (1 / 2)) โ โ) |
71 | 69, 70 | mpan2 690 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (๐ โ (1 / 2)) โ
โ) |
72 | | 3ne0 12264 |
. . . . . . . . . . . . 13
โข 3 โ
0 |
73 | | divcan2 11826 |
. . . . . . . . . . . . 13
โข (((๐ โ (1 / 2)) โ โ
โง 3 โ โ โง 3 โ 0) โ (3 ยท ((๐ โ (1 / 2)) / 3)) = (๐ โ (1 / 2))) |
74 | 35, 72, 73 | mp3an23 1454 |
. . . . . . . . . . . 12
โข ((๐ โ (1 / 2)) โ โ
โ (3 ยท ((๐
โ (1 / 2)) / 3)) = (๐
โ (1 / 2))) |
75 | 71, 74 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ โ โ (3
ยท ((๐ โ (1 /
2)) / 3)) = (๐ โ (1 /
2))) |
76 | 68, 75 | eqtrd 2773 |
. . . . . . . . . 10
โข (๐ โ โ โ (3
ยท ((1 BernPoly ๐) /
3)) = (๐ โ (1 /
2))) |
77 | 65, 76 | sylan9eqr 2795 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ = 1) โ ((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = (๐ โ (1 / 2))) |
78 | 71 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ = 1) โ (๐ โ (1 / 2)) โ
โ) |
79 | 77, 78 | eqeltrd 2834 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ = 1) โ ((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) โ โ) |
80 | | oveq2 7366 |
. . . . . . . . . . . 12
โข (๐ = 2 โ (3C๐) = (3C2)) |
81 | | bcn2 14225 |
. . . . . . . . . . . . . 14
โข (3 โ
โ0 โ (3C2) = ((3 ยท (3 โ 1)) /
2)) |
82 | 1, 81 | ax-mp 5 |
. . . . . . . . . . . . 13
โข (3C2) =
((3 ยท (3 โ 1)) / 2) |
83 | 4 | oveq2i 7369 |
. . . . . . . . . . . . . . 15
โข (3
ยท (3 โ 1)) = (3 ยท 2) |
84 | 83 | oveq1i 7368 |
. . . . . . . . . . . . . 14
โข ((3
ยท (3 โ 1)) / 2) = ((3 ยท 2) / 2) |
85 | | 2cn 12233 |
. . . . . . . . . . . . . . 15
โข 2 โ
โ |
86 | | 2ne0 12262 |
. . . . . . . . . . . . . . 15
โข 2 โ
0 |
87 | 35, 85, 86 | divcan4i 11907 |
. . . . . . . . . . . . . 14
โข ((3
ยท 2) / 2) = 3 |
88 | 84, 87 | eqtri 2761 |
. . . . . . . . . . . . 13
โข ((3
ยท (3 โ 1)) / 2) = 3 |
89 | 82, 88 | eqtri 2761 |
. . . . . . . . . . . 12
โข (3C2) =
3 |
90 | 80, 89 | eqtrdi 2789 |
. . . . . . . . . . 11
โข (๐ = 2 โ (3C๐) = 3) |
91 | | oveq1 7365 |
. . . . . . . . . . . 12
โข (๐ = 2 โ (๐ BernPoly ๐) = (2 BernPoly ๐)) |
92 | | oveq2 7366 |
. . . . . . . . . . . . . 14
โข (๐ = 2 โ (3 โ ๐) = (3 โ
2)) |
93 | 92 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ = 2 โ ((3 โ ๐) + 1) = ((3 โ 2) +
1)) |
94 | | 2p1e3 12300 |
. . . . . . . . . . . . . . . 16
โข (2 + 1) =
3 |
95 | 35, 85, 60, 94 | subaddrii 11495 |
. . . . . . . . . . . . . . 15
โข (3
โ 2) = 1 |
96 | 95 | oveq1i 7368 |
. . . . . . . . . . . . . 14
โข ((3
โ 2) + 1) = (1 + 1) |
97 | 96, 5 | eqtr4i 2764 |
. . . . . . . . . . . . 13
โข ((3
โ 2) + 1) = 2 |
98 | 93, 97 | eqtrdi 2789 |
. . . . . . . . . . . 12
โข (๐ = 2 โ ((3 โ ๐) + 1) = 2) |
99 | 91, 98 | oveq12d 7376 |
. . . . . . . . . . 11
โข (๐ = 2 โ ((๐ BernPoly ๐) / ((3 โ ๐) + 1)) = ((2 BernPoly ๐) / 2)) |
100 | 90, 99 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ = 2 โ ((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = (3 ยท ((2 BernPoly ๐) / 2))) |
101 | | 2nn0 12435 |
. . . . . . . . . . . . 13
โข 2 โ
โ0 |
102 | | bpolycl 15940 |
. . . . . . . . . . . . 13
โข ((2
โ โ0 โง ๐ โ โ) โ (2 BernPoly ๐) โ
โ) |
103 | 101, 102 | mpan 689 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (2
BernPoly ๐) โ
โ) |
104 | | 2cnne0 12368 |
. . . . . . . . . . . . 13
โข (2 โ
โ โง 2 โ 0) |
105 | | div12 11840 |
. . . . . . . . . . . . 13
โข ((3
โ โ โง (2 BernPoly ๐) โ โ โง (2 โ โ
โง 2 โ 0)) โ (3 ยท ((2 BernPoly ๐) / 2)) = ((2 BernPoly ๐) ยท (3 / 2))) |
106 | 35, 104, 105 | mp3an13 1453 |
. . . . . . . . . . . 12
โข ((2
BernPoly ๐) โ โ
โ (3 ยท ((2 BernPoly ๐) / 2)) = ((2 BernPoly ๐) ยท (3 / 2))) |
107 | 103, 106 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ โ โ (3
ยท ((2 BernPoly ๐) /
2)) = ((2 BernPoly ๐)
ยท (3 / 2))) |
108 | 35, 85, 86 | divcli 11902 |
. . . . . . . . . . . 12
โข (3 / 2)
โ โ |
109 | | mulcom 11142 |
. . . . . . . . . . . 12
โข (((2
BernPoly ๐) โ โ
โง (3 / 2) โ โ) โ ((2 BernPoly ๐) ยท (3 / 2)) = ((3 / 2) ยท (2
BernPoly ๐))) |
110 | 103, 108,
109 | sylancl 587 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((2
BernPoly ๐) ยท (3 /
2)) = ((3 / 2) ยท (2 BernPoly ๐))) |
111 | | bpoly2 15945 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (2
BernPoly ๐) = (((๐โ2) โ ๐) + (1 / 6))) |
112 | 111 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((3 / 2)
ยท (2 BernPoly ๐)) =
((3 / 2) ยท (((๐โ2) โ ๐) + (1 / 6)))) |
113 | | sqcl 14029 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐โ2) โ
โ) |
114 | | 6cn 12249 |
. . . . . . . . . . . . . . . 16
โข 6 โ
โ |
115 | | 6re 12248 |
. . . . . . . . . . . . . . . . 17
โข 6 โ
โ |
116 | | 6pos 12268 |
. . . . . . . . . . . . . . . . 17
โข 0 <
6 |
117 | 115, 116 | gt0ne0ii 11696 |
. . . . . . . . . . . . . . . 16
โข 6 โ
0 |
118 | 114, 117 | reccli 11890 |
. . . . . . . . . . . . . . 15
โข (1 / 6)
โ โ |
119 | | subsub 11436 |
. . . . . . . . . . . . . . 15
โข (((๐โ2) โ โ โง
๐ โ โ โง (1 /
6) โ โ) โ ((๐โ2) โ (๐ โ (1 / 6))) = (((๐โ2) โ ๐) + (1 / 6))) |
120 | 118, 119 | mp3an3 1451 |
. . . . . . . . . . . . . 14
โข (((๐โ2) โ โ โง
๐ โ โ) โ
((๐โ2) โ (๐ โ (1 / 6))) = (((๐โ2) โ ๐) + (1 / 6))) |
121 | 113, 120 | mpancom 687 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((๐โ2) โ (๐ โ (1 / 6))) = (((๐โ2) โ ๐) + (1 / 6))) |
122 | 121 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((3 / 2)
ยท ((๐โ2)
โ (๐ โ (1 /
6)))) = ((3 / 2) ยท (((๐โ2) โ ๐) + (1 / 6)))) |
123 | | subcl 11405 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง (1 / 6)
โ โ) โ (๐
โ (1 / 6)) โ โ) |
124 | 118, 123 | mpan2 690 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ โ (1 / 6)) โ
โ) |
125 | | subdi 11593 |
. . . . . . . . . . . . 13
โข (((3 / 2)
โ โ โง (๐โ2) โ โ โง (๐ โ (1 / 6)) โ
โ) โ ((3 / 2) ยท ((๐โ2) โ (๐ โ (1 / 6)))) = (((3 / 2) ยท
(๐โ2)) โ ((3 /
2) ยท (๐ โ (1 /
6))))) |
126 | 108, 113,
124, 125 | mp3an2i 1467 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((3 / 2)
ยท ((๐โ2)
โ (๐ โ (1 /
6)))) = (((3 / 2) ยท (๐โ2)) โ ((3 / 2) ยท (๐ โ (1 /
6))))) |
127 | 112, 122,
126 | 3eqtr2d 2779 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((3 / 2)
ยท (2 BernPoly ๐)) =
(((3 / 2) ยท (๐โ2)) โ ((3 / 2) ยท (๐ โ (1 /
6))))) |
128 | 107, 110,
127 | 3eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ โ โ (3
ยท ((2 BernPoly ๐) /
2)) = (((3 / 2) ยท (๐โ2)) โ ((3 / 2) ยท (๐ โ (1 /
6))))) |
129 | 100, 128 | sylan9eqr 2795 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ = 2) โ ((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = (((3 / 2) ยท (๐โ2)) โ ((3 / 2)
ยท (๐ โ (1 /
6))))) |
130 | | mulcl 11140 |
. . . . . . . . . . . 12
โข (((3 / 2)
โ โ โง (๐โ2) โ โ) โ ((3 / 2)
ยท (๐โ2)) โ
โ) |
131 | 108, 113,
130 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((3 / 2)
ยท (๐โ2)) โ
โ) |
132 | | mulcl 11140 |
. . . . . . . . . . . 12
โข (((3 / 2)
โ โ โง (๐
โ (1 / 6)) โ โ) โ ((3 / 2) ยท (๐ โ (1 / 6))) โ
โ) |
133 | 108, 124,
132 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((3 / 2)
ยท (๐ โ (1 /
6))) โ โ) |
134 | 131, 133 | subcld 11517 |
. . . . . . . . . 10
โข (๐ โ โ โ (((3 / 2)
ยท (๐โ2))
โ ((3 / 2) ยท (๐ โ (1 / 6)))) โ
โ) |
135 | 134 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ = 2) โ (((3 / 2) ยท
(๐โ2)) โ ((3 /
2) ยท (๐ โ (1 /
6)))) โ โ) |
136 | 129, 135 | eqeltrd 2834 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ = 2) โ ((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) โ โ) |
137 | 52, 79, 136 | 3jaodan 1431 |
. . . . . . 7
โข ((๐ โ โ โง (๐ = 0 โจ ๐ = 1 โจ ๐ = 2)) โ ((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) โ โ) |
138 | 27, 137 | sylan2b 595 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (0...(1 + 1))) โ
((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) โ โ) |
139 | 5 | eqeq2i 2746 |
. . . . . . 7
โข (๐ = 2 โ ๐ = (1 + 1)) |
140 | 139, 100 | sylbir 234 |
. . . . . 6
โข (๐ = (1 + 1) โ ((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = (3 ยท ((2 BernPoly ๐) / 2))) |
141 | 10, 138, 140 | fsump1 15646 |
. . . . 5
โข (๐ โ โ โ
ฮฃ๐ โ (0...(1 +
1))((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = (ฮฃ๐ โ (0...1)((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) + (3 ยท ((2 BernPoly ๐) / 2)))) |
142 | 128 | oveq2d 7374 |
. . . . 5
โข (๐ โ โ โ
(ฮฃ๐ โ
(0...1)((3C๐) ยท
((๐ BernPoly ๐) / ((3 โ ๐) + 1))) + (3 ยท ((2
BernPoly ๐) / 2))) =
(ฮฃ๐ โ
(0...1)((3C๐) ยท
((๐ BernPoly ๐) / ((3 โ ๐) + 1))) + (((3 / 2) ยท
(๐โ2)) โ ((3 /
2) ยท (๐ โ (1 /
6)))))) |
143 | 15 | sumeq1i 15588 |
. . . . . . . . 9
โข
ฮฃ๐ โ
(0...(0 + 1))((3C๐)
ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = ฮฃ๐ โ (0...1)((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) |
144 | | 0nn0 12433 |
. . . . . . . . . . . . 13
โข 0 โ
โ0 |
145 | | nn0uz 12810 |
. . . . . . . . . . . . 13
โข
โ0 = (โคโฅโ0) |
146 | 144, 145 | eleqtri 2832 |
. . . . . . . . . . . 12
โข 0 โ
(โคโฅโ0) |
147 | 146 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โ โ 0 โ
(โคโฅโ0)) |
148 | 13, 16 | eqtri 2761 |
. . . . . . . . . . . . . 14
โข (0...(0 +
1)) = {0, 1} |
149 | 148 | eleq2i 2826 |
. . . . . . . . . . . . 13
โข (๐ โ (0...(0 + 1)) โ
๐ โ {0,
1}) |
150 | 25 | elpr 4610 |
. . . . . . . . . . . . 13
โข (๐ โ {0, 1} โ (๐ = 0 โจ ๐ = 1)) |
151 | 149, 150 | bitri 275 |
. . . . . . . . . . . 12
โข (๐ โ (0...(0 + 1)) โ
(๐ = 0 โจ ๐ = 1)) |
152 | 52, 79 | jaodan 957 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง (๐ = 0 โจ ๐ = 1)) โ ((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) โ โ) |
153 | 151, 152 | sylan2b 595 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ (0...(0 + 1))) โ
((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) โ โ) |
154 | 14 | eqeq2i 2746 |
. . . . . . . . . . . 12
โข (๐ = (0 + 1) โ ๐ = 1) |
155 | 154, 65 | sylbi 216 |
. . . . . . . . . . 11
โข (๐ = (0 + 1) โ ((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = (3 ยท ((1 BernPoly ๐) / 3))) |
156 | 147, 153,
155 | fsump1 15646 |
. . . . . . . . . 10
โข (๐ โ โ โ
ฮฃ๐ โ (0...(0 +
1))((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = (ฮฃ๐ โ (0...0)((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) + (3 ยท ((1 BernPoly ๐) / 3)))) |
157 | 50, 48 | eqeltrdi 2842 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (1
ยท ((0 BernPoly ๐) /
4)) โ โ) |
158 | 42 | fsum1 15637 |
. . . . . . . . . . . . 13
โข ((0
โ โค โง (1 ยท ((0 BernPoly ๐) / 4)) โ โ) โ ฮฃ๐ โ (0...0)((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = (1 ยท ((0 BernPoly ๐) / 4))) |
159 | 11, 157, 158 | sylancr 588 |
. . . . . . . . . . . 12
โข (๐ โ โ โ
ฮฃ๐ โ
(0...0)((3C๐) ยท
((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = (1 ยท ((0
BernPoly ๐) /
4))) |
160 | 159, 50 | eqtrd 2773 |
. . . . . . . . . . 11
โข (๐ โ โ โ
ฮฃ๐ โ
(0...0)((3C๐) ยท
((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = (1 /
4)) |
161 | 160, 76 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ โ โ โ
(ฮฃ๐ โ
(0...0)((3C๐) ยท
((๐ BernPoly ๐) / ((3 โ ๐) + 1))) + (3 ยท ((1
BernPoly ๐) / 3))) = ((1 /
4) + (๐ โ (1 /
2)))) |
162 | 156, 161 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ โ โ โ
ฮฃ๐ โ (0...(0 +
1))((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = ((1 / 4) + (๐ โ (1 / 2)))) |
163 | 143, 162 | eqtr3id 2787 |
. . . . . . . 8
โข (๐ โ โ โ
ฮฃ๐ โ
(0...1)((3C๐) ยท
((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = ((1 / 4) + (๐ โ (1 /
2)))) |
164 | 163 | oveq1d 7373 |
. . . . . . 7
โข (๐ โ โ โ
(ฮฃ๐ โ
(0...1)((3C๐) ยท
((๐ BernPoly ๐) / ((3 โ ๐) + 1))) + (((3 / 2) ยท
(๐โ2)) โ ((3 /
2) ยท (๐ โ (1 /
6))))) = (((1 / 4) + (๐
โ (1 / 2))) + (((3 / 2) ยท (๐โ2)) โ ((3 / 2) ยท (๐ โ (1 /
6)))))) |
165 | | addcl 11138 |
. . . . . . . . 9
โข (((1 / 4)
โ โ โง (๐
โ (1 / 2)) โ โ) โ ((1 / 4) + (๐ โ (1 / 2))) โ
โ) |
166 | 48, 71, 165 | sylancr 588 |
. . . . . . . 8
โข (๐ โ โ โ ((1 / 4)
+ (๐ โ (1 / 2)))
โ โ) |
167 | 166, 131,
133 | addsub12d 11540 |
. . . . . . 7
โข (๐ โ โ โ (((1 / 4)
+ (๐ โ (1 / 2))) +
(((3 / 2) ยท (๐โ2)) โ ((3 / 2) ยท (๐ โ (1 / 6))))) = (((3 / 2)
ยท (๐โ2)) + (((1
/ 4) + (๐ โ (1 / 2)))
โ ((3 / 2) ยท (๐ โ (1 / 6)))))) |
168 | 164, 167 | eqtrd 2773 |
. . . . . 6
โข (๐ โ โ โ
(ฮฃ๐ โ
(0...1)((3C๐) ยท
((๐ BernPoly ๐) / ((3 โ ๐) + 1))) + (((3 / 2) ยท
(๐โ2)) โ ((3 /
2) ยท (๐ โ (1 /
6))))) = (((3 / 2) ยท (๐โ2)) + (((1 / 4) + (๐ โ (1 / 2))) โ ((3 / 2) ยท
(๐ โ (1 /
6)))))) |
169 | 133, 166 | negsubdi2d 11533 |
. . . . . . . 8
โข (๐ โ โ โ -(((3 /
2) ยท (๐ โ (1 /
6))) โ ((1 / 4) + (๐
โ (1 / 2)))) = (((1 / 4) + (๐ โ (1 / 2))) โ ((3 / 2) ยท
(๐ โ (1 /
6))))) |
170 | | subdi 11593 |
. . . . . . . . . . . 12
โข (((3 / 2)
โ โ โง ๐
โ โ โง (1 / 6) โ โ) โ ((3 / 2) ยท (๐ โ (1 / 6))) = (((3 / 2)
ยท ๐) โ ((3 /
2) ยท (1 / 6)))) |
171 | 108, 118,
170 | mp3an13 1453 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((3 / 2)
ยท (๐ โ (1 /
6))) = (((3 / 2) ยท ๐) โ ((3 / 2) ยท (1 /
6)))) |
172 | | addsub12 11419 |
. . . . . . . . . . . 12
โข (((1 / 4)
โ โ โง ๐
โ โ โง (1 / 2) โ โ) โ ((1 / 4) + (๐ โ (1 / 2))) = (๐ + ((1 / 4) โ (1 /
2)))) |
173 | 48, 69, 172 | mp3an13 1453 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((1 / 4)
+ (๐ โ (1 / 2))) =
(๐ + ((1 / 4) โ (1 /
2)))) |
174 | 171, 173 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ โ โ โ (((3 / 2)
ยท (๐ โ (1 /
6))) โ ((1 / 4) + (๐
โ (1 / 2)))) = ((((3 / 2) ยท ๐) โ ((3 / 2) ยท (1 / 6)))
โ (๐ + ((1 / 4)
โ (1 / 2))))) |
175 | | mulcl 11140 |
. . . . . . . . . . . . 13
โข (((3 / 2)
โ โ โง ๐
โ โ) โ ((3 / 2) ยท ๐) โ โ) |
176 | 108, 175 | mpan 689 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((3 / 2)
ยท ๐) โ
โ) |
177 | 108, 118 | mulcli 11167 |
. . . . . . . . . . . 12
โข ((3 / 2)
ยท (1 / 6)) โ โ |
178 | | negsub 11454 |
. . . . . . . . . . . 12
โข ((((3 /
2) ยท ๐) โ
โ โง ((3 / 2) ยท (1 / 6)) โ โ) โ (((3 / 2)
ยท ๐) + -((3 / 2)
ยท (1 / 6))) = (((3 / 2) ยท ๐) โ ((3 / 2) ยท (1 /
6)))) |
179 | 176, 177,
178 | sylancl 587 |
. . . . . . . . . . 11
โข (๐ โ โ โ (((3 / 2)
ยท ๐) + -((3 / 2)
ยท (1 / 6))) = (((3 / 2) ยท ๐) โ ((3 / 2) ยท (1 /
6)))) |
180 | 179 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐ โ โ โ ((((3 /
2) ยท ๐) + -((3 / 2)
ยท (1 / 6))) โ (๐ + ((1 / 4) โ (1 / 2)))) = ((((3 / 2)
ยท ๐) โ ((3 /
2) ยท (1 / 6))) โ (๐ + ((1 / 4) โ (1 /
2))))) |
181 | 69, 48 | negsubdi2i 11492 |
. . . . . . . . . . . . . 14
โข -((1 / 2)
โ (1 / 4)) = ((1 / 4) โ (1 / 2)) |
182 | 85, 35, 85 | mul12i 11355 |
. . . . . . . . . . . . . . . . . . 19
โข (2
ยท (3 ยท 2)) = (3 ยท (2 ยท 2)) |
183 | | 3t2e6 12324 |
. . . . . . . . . . . . . . . . . . . 20
โข (3
ยท 2) = 6 |
184 | 183 | oveq2i 7369 |
. . . . . . . . . . . . . . . . . . 19
โข (2
ยท (3 ยท 2)) = (2 ยท 6) |
185 | | 2t2e4 12322 |
. . . . . . . . . . . . . . . . . . . 20
โข (2
ยท 2) = 4 |
186 | 185 | oveq2i 7369 |
. . . . . . . . . . . . . . . . . . 19
โข (3
ยท (2 ยท 2)) = (3 ยท 4) |
187 | 182, 184,
186 | 3eqtr3i 2769 |
. . . . . . . . . . . . . . . . . 18
โข (2
ยท 6) = (3 ยท 4) |
188 | 187 | oveq2i 7369 |
. . . . . . . . . . . . . . . . 17
โข ((3
ยท 1) / (2 ยท 6)) = ((3 ยท 1) / (3 ยท
4)) |
189 | 46, 47 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . 18
โข (4 โ
โ โง 4 โ 0) |
190 | 35, 72 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . 18
โข (3 โ
โ โง 3 โ 0) |
191 | | divcan5 11862 |
. . . . . . . . . . . . . . . . . 18
โข ((1
โ โ โง (4 โ โ โง 4 โ 0) โง (3 โ โ
โง 3 โ 0)) โ ((3 ยท 1) / (3 ยท 4)) = (1 /
4)) |
192 | 60, 189, 190, 191 | mp3an 1462 |
. . . . . . . . . . . . . . . . 17
โข ((3
ยท 1) / (3 ยท 4)) = (1 / 4) |
193 | 188, 192 | eqtri 2761 |
. . . . . . . . . . . . . . . 16
โข ((3
ยท 1) / (2 ยท 6)) = (1 / 4) |
194 | 35, 85, 60, 114, 86, 117 | divmuldivi 11920 |
. . . . . . . . . . . . . . . 16
โข ((3 / 2)
ยท (1 / 6)) = ((3 ยท 1) / (2 ยท 6)) |
195 | | 2t1e2 12321 |
. . . . . . . . . . . . . . . . . . . 20
โข (2
ยท 1) = 2 |
196 | 195, 5 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . 19
โข (2
ยท 1) = (1 + 1) |
197 | 196, 185 | oveq12i 7370 |
. . . . . . . . . . . . . . . . . 18
โข ((2
ยท 1) / (2 ยท 2)) = ((1 + 1) / 4) |
198 | | divcan5 11862 |
. . . . . . . . . . . . . . . . . . 19
โข ((1
โ โ โง (2 โ โ โง 2 โ 0) โง (2 โ โ
โง 2 โ 0)) โ ((2 ยท 1) / (2 ยท 2)) = (1 /
2)) |
199 | 60, 104, 104, 198 | mp3an 1462 |
. . . . . . . . . . . . . . . . . 18
โข ((2
ยท 1) / (2 ยท 2)) = (1 / 2) |
200 | 60, 60, 46, 47 | divdiri 11917 |
. . . . . . . . . . . . . . . . . 18
โข ((1 + 1)
/ 4) = ((1 / 4) + (1 / 4)) |
201 | 197, 199,
200 | 3eqtr3ri 2770 |
. . . . . . . . . . . . . . . . 17
โข ((1 / 4)
+ (1 / 4)) = (1 / 2) |
202 | 69, 48, 48, 201 | subaddrii 11495 |
. . . . . . . . . . . . . . . 16
โข ((1 / 2)
โ (1 / 4)) = (1 / 4) |
203 | 193, 194,
202 | 3eqtr4ri 2772 |
. . . . . . . . . . . . . . 15
โข ((1 / 2)
โ (1 / 4)) = ((3 / 2) ยท (1 / 6)) |
204 | 203 | negeqi 11399 |
. . . . . . . . . . . . . 14
โข -((1 / 2)
โ (1 / 4)) = -((3 / 2) ยท (1 / 6)) |
205 | 181, 204 | eqtr3i 2763 |
. . . . . . . . . . . . 13
โข ((1 / 4)
โ (1 / 2)) = -((3 / 2) ยท (1 / 6)) |
206 | 48, 69 | subcli 11482 |
. . . . . . . . . . . . . 14
โข ((1 / 4)
โ (1 / 2)) โ โ |
207 | 177 | negcli 11474 |
. . . . . . . . . . . . . 14
โข -((3 / 2)
ยท (1 / 6)) โ โ |
208 | 206, 207 | subeq0i 11486 |
. . . . . . . . . . . . 13
โข ((((1 /
4) โ (1 / 2)) โ -((3 / 2) ยท (1 / 6))) = 0 โ ((1 / 4)
โ (1 / 2)) = -((3 / 2) ยท (1 / 6))) |
209 | 205, 208 | mpbir 230 |
. . . . . . . . . . . 12
โข (((1 / 4)
โ (1 / 2)) โ -((3 / 2) ยท (1 / 6))) = 0 |
210 | 209 | oveq2i 7369 |
. . . . . . . . . . 11
โข ((((3 /
2) ยท ๐) โ
๐) โ (((1 / 4)
โ (1 / 2)) โ -((3 / 2) ยท (1 / 6)))) = ((((3 / 2) ยท
๐) โ ๐) โ 0) |
211 | | id 22 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
212 | 206 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((1 / 4)
โ (1 / 2)) โ โ) |
213 | 207 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ โ โ -((3 / 2)
ยท (1 / 6)) โ โ) |
214 | 176, 211,
212, 213 | subadd4d 11565 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((((3 /
2) ยท ๐) โ
๐) โ (((1 / 4)
โ (1 / 2)) โ -((3 / 2) ยท (1 / 6)))) = ((((3 / 2) ยท
๐) + -((3 / 2) ยท (1
/ 6))) โ (๐ + ((1 /
4) โ (1 / 2))))) |
215 | | subdir 11594 |
. . . . . . . . . . . . . . 15
โข (((3 / 2)
โ โ โง 1 โ โ โง ๐ โ โ) โ (((3 / 2) โ 1)
ยท ๐) = (((3 / 2)
ยท ๐) โ (1
ยท ๐))) |
216 | 108, 60, 215 | mp3an12 1452 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (((3 / 2)
โ 1) ยท ๐) =
(((3 / 2) ยท ๐)
โ (1 ยท ๐))) |
217 | | divsubdir 11854 |
. . . . . . . . . . . . . . . . . 18
โข ((3
โ โ โง 2 โ โ โง (2 โ โ โง 2 โ 0))
โ ((3 โ 2) / 2) = ((3 / 2) โ (2 / 2))) |
218 | 35, 85, 104, 217 | mp3an 1462 |
. . . . . . . . . . . . . . . . 17
โข ((3
โ 2) / 2) = ((3 / 2) โ (2 / 2)) |
219 | 95 | oveq1i 7368 |
. . . . . . . . . . . . . . . . 17
โข ((3
โ 2) / 2) = (1 / 2) |
220 | | 2div2e1 12299 |
. . . . . . . . . . . . . . . . . 18
โข (2 / 2) =
1 |
221 | 220 | oveq2i 7369 |
. . . . . . . . . . . . . . . . 17
โข ((3 / 2)
โ (2 / 2)) = ((3 / 2) โ 1) |
222 | 218, 219,
221 | 3eqtr3ri 2770 |
. . . . . . . . . . . . . . . 16
โข ((3 / 2)
โ 1) = (1 / 2) |
223 | 222 | oveq1i 7368 |
. . . . . . . . . . . . . . 15
โข (((3 / 2)
โ 1) ยท ๐) =
((1 / 2) ยท ๐) |
224 | 223 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (((3 / 2)
โ 1) ยท ๐) =
((1 / 2) ยท ๐)) |
225 | | mulid2 11159 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (1
ยท ๐) = ๐) |
226 | 225 | oveq2d 7374 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (((3 / 2)
ยท ๐) โ (1
ยท ๐)) = (((3 / 2)
ยท ๐) โ ๐)) |
227 | 216, 224,
226 | 3eqtr3rd 2782 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (((3 / 2)
ยท ๐) โ ๐) = ((1 / 2) ยท ๐)) |
228 | 227 | oveq1d 7373 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((((3 /
2) ยท ๐) โ
๐) โ 0) = (((1 / 2)
ยท ๐) โ
0)) |
229 | | mulcl 11140 |
. . . . . . . . . . . . . 14
โข (((1 / 2)
โ โ โง ๐
โ โ) โ ((1 / 2) ยท ๐) โ โ) |
230 | 69, 229 | mpan 689 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((1 / 2)
ยท ๐) โ
โ) |
231 | 230 | subid1d 11506 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (((1 / 2)
ยท ๐) โ 0) =
((1 / 2) ยท ๐)) |
232 | 228, 231 | eqtrd 2773 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((((3 /
2) ยท ๐) โ
๐) โ 0) = ((1 / 2)
ยท ๐)) |
233 | 210, 214,
232 | 3eqtr3a 2797 |
. . . . . . . . . 10
โข (๐ โ โ โ ((((3 /
2) ยท ๐) + -((3 / 2)
ยท (1 / 6))) โ (๐ + ((1 / 4) โ (1 / 2)))) = ((1 / 2)
ยท ๐)) |
234 | 174, 180,
233 | 3eqtr2d 2779 |
. . . . . . . . 9
โข (๐ โ โ โ (((3 / 2)
ยท (๐ โ (1 /
6))) โ ((1 / 4) + (๐
โ (1 / 2)))) = ((1 / 2) ยท ๐)) |
235 | 234 | negeqd 11400 |
. . . . . . . 8
โข (๐ โ โ โ -(((3 /
2) ยท (๐ โ (1 /
6))) โ ((1 / 4) + (๐
โ (1 / 2)))) = -((1 / 2) ยท ๐)) |
236 | 169, 235 | eqtr3d 2775 |
. . . . . . 7
โข (๐ โ โ โ (((1 / 4)
+ (๐ โ (1 / 2)))
โ ((3 / 2) ยท (๐ โ (1 / 6)))) = -((1 / 2) ยท
๐)) |
237 | 236 | oveq2d 7374 |
. . . . . 6
โข (๐ โ โ โ (((3 / 2)
ยท (๐โ2)) + (((1
/ 4) + (๐ โ (1 / 2)))
โ ((3 / 2) ยท (๐ โ (1 / 6))))) = (((3 / 2) ยท
(๐โ2)) + -((1 / 2)
ยท ๐))) |
238 | 131, 230 | negsubd 11523 |
. . . . . 6
โข (๐ โ โ โ (((3 / 2)
ยท (๐โ2)) + -((1
/ 2) ยท ๐)) = (((3 /
2) ยท (๐โ2))
โ ((1 / 2) ยท ๐))) |
239 | 168, 237,
238 | 3eqtrd 2777 |
. . . . 5
โข (๐ โ โ โ
(ฮฃ๐ โ
(0...1)((3C๐) ยท
((๐ BernPoly ๐) / ((3 โ ๐) + 1))) + (((3 / 2) ยท
(๐โ2)) โ ((3 /
2) ยท (๐ โ (1 /
6))))) = (((3 / 2) ยท (๐โ2)) โ ((1 / 2) ยท ๐))) |
240 | 141, 142,
239 | 3eqtrd 2777 |
. . . 4
โข (๐ โ โ โ
ฮฃ๐ โ (0...(1 +
1))((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = (((3 / 2) ยท (๐โ2)) โ ((1 / 2)
ยท ๐))) |
241 | 8, 240 | eqtrid 2785 |
. . 3
โข (๐ โ โ โ
ฮฃ๐ โ (0...(3
โ 1))((3C๐) ยท
((๐ BernPoly ๐) / ((3 โ ๐) + 1))) = (((3 / 2) ยท
(๐โ2)) โ ((1 /
2) ยท ๐))) |
242 | 241 | oveq2d 7374 |
. 2
โข (๐ โ โ โ ((๐โ3) โ ฮฃ๐ โ (0...(3 โ
1))((3C๐) ยท ((๐ BernPoly ๐) / ((3 โ ๐) + 1)))) = ((๐โ3) โ (((3 / 2) ยท (๐โ2)) โ ((1 / 2)
ยท ๐)))) |
243 | | expcl 13991 |
. . . 4
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
244 | 1, 243 | mpan2 690 |
. . 3
โข (๐ โ โ โ (๐โ3) โ
โ) |
245 | 244, 131,
230 | subsubd 11545 |
. 2
โข (๐ โ โ โ ((๐โ3) โ (((3 / 2)
ยท (๐โ2))
โ ((1 / 2) ยท ๐))) = (((๐โ3) โ ((3 / 2) ยท (๐โ2))) + ((1 / 2) ยท
๐))) |
246 | 3, 242, 245 | 3eqtrd 2777 |
1
โข (๐ โ โ โ (3
BernPoly ๐) = (((๐โ3) โ ((3 / 2)
ยท (๐โ2))) + ((1
/ 2) ยท ๐))) |