Step | Hyp | Ref
| Expression |
1 | | 2nn0 12435 |
. . 3
โข 2 โ
โ0 |
2 | | bpolyval 15937 |
. . 3
โข ((2
โ โ0 โง ๐ โ โ) โ (2 BernPoly ๐) = ((๐โ2) โ ฮฃ๐ โ (0...(2 โ 1))((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))))) |
3 | 1, 2 | mpan 689 |
. 2
โข (๐ โ โ โ (2
BernPoly ๐) = ((๐โ2) โ ฮฃ๐ โ (0...(2 โ
1))((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))))) |
4 | | 2m1e1 12284 |
. . . . . . 7
โข (2
โ 1) = 1 |
5 | | 0p1e1 12280 |
. . . . . . 7
โข (0 + 1) =
1 |
6 | 4, 5 | eqtr4i 2764 |
. . . . . 6
โข (2
โ 1) = (0 + 1) |
7 | 6 | oveq2i 7369 |
. . . . 5
โข (0...(2
โ 1)) = (0...(0 + 1)) |
8 | 7 | sumeq1i 15588 |
. . . 4
โข
ฮฃ๐ โ
(0...(2 โ 1))((2C๐)
ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))) = ฮฃ๐ โ (0...(0 + 1))((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))) |
9 | | 0nn0 12433 |
. . . . . . . . 9
โข 0 โ
โ0 |
10 | | nn0uz 12810 |
. . . . . . . . 9
โข
โ0 = (โคโฅโ0) |
11 | 9, 10 | eleqtri 2832 |
. . . . . . . 8
โข 0 โ
(โคโฅโ0) |
12 | 11 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ 0 โ
(โคโฅโ0)) |
13 | | 0z 12515 |
. . . . . . . . . . 11
โข 0 โ
โค |
14 | | fzpr 13502 |
. . . . . . . . . . 11
โข (0 โ
โค โ (0...(0 + 1)) = {0, (0 + 1)}) |
15 | 13, 14 | ax-mp 5 |
. . . . . . . . . 10
โข (0...(0 +
1)) = {0, (0 + 1)} |
16 | 15 | eleq2i 2826 |
. . . . . . . . 9
โข (๐ โ (0...(0 + 1)) โ
๐ โ {0, (0 +
1)}) |
17 | | vex 3448 |
. . . . . . . . . 10
โข ๐ โ V |
18 | 17 | elpr 4610 |
. . . . . . . . 9
โข (๐ โ {0, (0 + 1)} โ
(๐ = 0 โจ ๐ = (0 + 1))) |
19 | 16, 18 | bitri 275 |
. . . . . . . 8
โข (๐ โ (0...(0 + 1)) โ
(๐ = 0 โจ ๐ = (0 + 1))) |
20 | | oveq2 7366 |
. . . . . . . . . . . . 13
โข (๐ = 0 โ (2C๐) = (2C0)) |
21 | | bcn0 14216 |
. . . . . . . . . . . . . 14
โข (2 โ
โ0 โ (2C0) = 1) |
22 | 1, 21 | ax-mp 5 |
. . . . . . . . . . . . 13
โข (2C0) =
1 |
23 | 20, 22 | eqtrdi 2789 |
. . . . . . . . . . . 12
โข (๐ = 0 โ (2C๐) = 1) |
24 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (๐ = 0 โ (๐ BernPoly ๐) = (0 BernPoly ๐)) |
25 | | oveq2 7366 |
. . . . . . . . . . . . . . 15
โข (๐ = 0 โ (2 โ ๐) = (2 โ
0)) |
26 | 25 | oveq1d 7373 |
. . . . . . . . . . . . . 14
โข (๐ = 0 โ ((2 โ ๐) + 1) = ((2 โ 0) +
1)) |
27 | | 2cn 12233 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
โ |
28 | 27 | subid1i 11478 |
. . . . . . . . . . . . . . . 16
โข (2
โ 0) = 2 |
29 | 28 | oveq1i 7368 |
. . . . . . . . . . . . . . 15
โข ((2
โ 0) + 1) = (2 + 1) |
30 | | df-3 12222 |
. . . . . . . . . . . . . . 15
โข 3 = (2 +
1) |
31 | 29, 30 | eqtr4i 2764 |
. . . . . . . . . . . . . 14
โข ((2
โ 0) + 1) = 3 |
32 | 26, 31 | eqtrdi 2789 |
. . . . . . . . . . . . 13
โข (๐ = 0 โ ((2 โ ๐) + 1) = 3) |
33 | 24, 32 | oveq12d 7376 |
. . . . . . . . . . . 12
โข (๐ = 0 โ ((๐ BernPoly ๐) / ((2 โ ๐) + 1)) = ((0 BernPoly ๐) / 3)) |
34 | 23, 33 | oveq12d 7376 |
. . . . . . . . . . 11
โข (๐ = 0 โ ((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))) = (1 ยท ((0 BernPoly ๐) / 3))) |
35 | | bpoly0 15938 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (0
BernPoly ๐) =
1) |
36 | 35 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((0
BernPoly ๐) / 3) = (1 /
3)) |
37 | 36 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (1
ยท ((0 BernPoly ๐) /
3)) = (1 ยท (1 / 3))) |
38 | | 3cn 12239 |
. . . . . . . . . . . . . 14
โข 3 โ
โ |
39 | | 3ne0 12264 |
. . . . . . . . . . . . . 14
โข 3 โ
0 |
40 | 38, 39 | reccli 11890 |
. . . . . . . . . . . . 13
โข (1 / 3)
โ โ |
41 | 40 | mulid2i 11165 |
. . . . . . . . . . . 12
โข (1
ยท (1 / 3)) = (1 / 3) |
42 | 37, 41 | eqtrdi 2789 |
. . . . . . . . . . 11
โข (๐ โ โ โ (1
ยท ((0 BernPoly ๐) /
3)) = (1 / 3)) |
43 | 34, 42 | sylan9eqr 2795 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ = 0) โ ((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))) = (1 / 3)) |
44 | 43, 40 | eqeltrdi 2842 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ = 0) โ ((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))) โ โ) |
45 | 5 | eqeq2i 2746 |
. . . . . . . . . . . 12
โข (๐ = (0 + 1) โ ๐ = 1) |
46 | | oveq2 7366 |
. . . . . . . . . . . . . 14
โข (๐ = 1 โ (2C๐) = (2C1)) |
47 | | bcn1 14219 |
. . . . . . . . . . . . . . 15
โข (2 โ
โ0 โ (2C1) = 2) |
48 | 1, 47 | ax-mp 5 |
. . . . . . . . . . . . . 14
โข (2C1) =
2 |
49 | 46, 48 | eqtrdi 2789 |
. . . . . . . . . . . . 13
โข (๐ = 1 โ (2C๐) = 2) |
50 | | oveq1 7365 |
. . . . . . . . . . . . . 14
โข (๐ = 1 โ (๐ BernPoly ๐) = (1 BernPoly ๐)) |
51 | | oveq2 7366 |
. . . . . . . . . . . . . . . 16
โข (๐ = 1 โ (2 โ ๐) = (2 โ
1)) |
52 | 51 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
โข (๐ = 1 โ ((2 โ ๐) + 1) = ((2 โ 1) +
1)) |
53 | | ax-1cn 11114 |
. . . . . . . . . . . . . . . 16
โข 1 โ
โ |
54 | | npcan 11415 |
. . . . . . . . . . . . . . . 16
โข ((2
โ โ โง 1 โ โ) โ ((2 โ 1) + 1) =
2) |
55 | 27, 53, 54 | mp2an 691 |
. . . . . . . . . . . . . . 15
โข ((2
โ 1) + 1) = 2 |
56 | 52, 55 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
โข (๐ = 1 โ ((2 โ ๐) + 1) = 2) |
57 | 50, 56 | oveq12d 7376 |
. . . . . . . . . . . . 13
โข (๐ = 1 โ ((๐ BernPoly ๐) / ((2 โ ๐) + 1)) = ((1 BernPoly ๐) / 2)) |
58 | 49, 57 | oveq12d 7376 |
. . . . . . . . . . . 12
โข (๐ = 1 โ ((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))) = (2 ยท ((1 BernPoly ๐) / 2))) |
59 | 45, 58 | sylbi 216 |
. . . . . . . . . . 11
โข (๐ = (0 + 1) โ ((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))) = (2 ยท ((1 BernPoly ๐) / 2))) |
60 | | bpoly1 15939 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (1
BernPoly ๐) = (๐ โ (1 /
2))) |
61 | 60 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((1
BernPoly ๐) / 2) = ((๐ โ (1 / 2)) /
2)) |
62 | 61 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (2
ยท ((1 BernPoly ๐) /
2)) = (2 ยท ((๐
โ (1 / 2)) / 2))) |
63 | | halfcn 12373 |
. . . . . . . . . . . . . 14
โข (1 / 2)
โ โ |
64 | | subcl 11405 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง (1 / 2)
โ โ) โ (๐
โ (1 / 2)) โ โ) |
65 | 63, 64 | mpan2 690 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ โ (1 / 2)) โ
โ) |
66 | | 2ne0 12262 |
. . . . . . . . . . . . . 14
โข 2 โ
0 |
67 | | divcan2 11826 |
. . . . . . . . . . . . . 14
โข (((๐ โ (1 / 2)) โ โ
โง 2 โ โ โง 2 โ 0) โ (2 ยท ((๐ โ (1 / 2)) / 2)) = (๐ โ (1 / 2))) |
68 | 27, 66, 67 | mp3an23 1454 |
. . . . . . . . . . . . 13
โข ((๐ โ (1 / 2)) โ โ
โ (2 ยท ((๐
โ (1 / 2)) / 2)) = (๐
โ (1 / 2))) |
69 | 65, 68 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (2
ยท ((๐ โ (1 /
2)) / 2)) = (๐ โ (1 /
2))) |
70 | 62, 69 | eqtrd 2773 |
. . . . . . . . . . 11
โข (๐ โ โ โ (2
ยท ((1 BernPoly ๐) /
2)) = (๐ โ (1 /
2))) |
71 | 59, 70 | sylan9eqr 2795 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ = (0 + 1)) โ ((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))) = (๐ โ (1 / 2))) |
72 | 65 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ = (0 + 1)) โ (๐ โ (1 / 2)) โ
โ) |
73 | 71, 72 | eqeltrd 2834 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ = (0 + 1)) โ ((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))) โ โ) |
74 | 44, 73 | jaodan 957 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ = 0 โจ ๐ = (0 + 1))) โ ((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))) โ โ) |
75 | 19, 74 | sylan2b 595 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (0...(0 + 1))) โ
((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))) โ โ) |
76 | 12, 75, 59 | fsump1 15646 |
. . . . . 6
โข (๐ โ โ โ
ฮฃ๐ โ (0...(0 +
1))((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))) = (ฮฃ๐ โ (0...0)((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))) + (2 ยท ((1 BernPoly ๐) / 2)))) |
77 | 42, 40 | eqeltrdi 2842 |
. . . . . . . . 9
โข (๐ โ โ โ (1
ยท ((0 BernPoly ๐) /
3)) โ โ) |
78 | 34 | fsum1 15637 |
. . . . . . . . 9
โข ((0
โ โค โง (1 ยท ((0 BernPoly ๐) / 3)) โ โ) โ ฮฃ๐ โ (0...0)((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))) = (1 ยท ((0 BernPoly ๐) / 3))) |
79 | 13, 77, 78 | sylancr 588 |
. . . . . . . 8
โข (๐ โ โ โ
ฮฃ๐ โ
(0...0)((2C๐) ยท
((๐ BernPoly ๐) / ((2 โ ๐) + 1))) = (1 ยท ((0
BernPoly ๐) /
3))) |
80 | 79, 42 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ โ โ
ฮฃ๐ โ
(0...0)((2C๐) ยท
((๐ BernPoly ๐) / ((2 โ ๐) + 1))) = (1 /
3)) |
81 | 80, 70 | oveq12d 7376 |
. . . . . 6
โข (๐ โ โ โ
(ฮฃ๐ โ
(0...0)((2C๐) ยท
((๐ BernPoly ๐) / ((2 โ ๐) + 1))) + (2 ยท ((1
BernPoly ๐) / 2))) = ((1 /
3) + (๐ โ (1 /
2)))) |
82 | 76, 81 | eqtrd 2773 |
. . . . 5
โข (๐ โ โ โ
ฮฃ๐ โ (0...(0 +
1))((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))) = ((1 / 3) + (๐ โ (1 / 2)))) |
83 | | addsub12 11419 |
. . . . . . 7
โข (((1 / 3)
โ โ โง ๐
โ โ โง (1 / 2) โ โ) โ ((1 / 3) + (๐ โ (1 / 2))) = (๐ + ((1 / 3) โ (1 /
2)))) |
84 | 40, 63, 83 | mp3an13 1453 |
. . . . . 6
โข (๐ โ โ โ ((1 / 3)
+ (๐ โ (1 / 2))) =
(๐ + ((1 / 3) โ (1 /
2)))) |
85 | 63, 40 | negsubdi2i 11492 |
. . . . . . . 8
โข -((1 / 2)
โ (1 / 3)) = ((1 / 3) โ (1 / 2)) |
86 | | halfthird 12766 |
. . . . . . . . 9
โข ((1 / 2)
โ (1 / 3)) = (1 / 6) |
87 | 86 | negeqi 11399 |
. . . . . . . 8
โข -((1 / 2)
โ (1 / 3)) = -(1 / 6) |
88 | 85, 87 | eqtr3i 2763 |
. . . . . . 7
โข ((1 / 3)
โ (1 / 2)) = -(1 / 6) |
89 | 88 | oveq2i 7369 |
. . . . . 6
โข (๐ + ((1 / 3) โ (1 / 2))) =
(๐ + -(1 /
6)) |
90 | 84, 89 | eqtrdi 2789 |
. . . . 5
โข (๐ โ โ โ ((1 / 3)
+ (๐ โ (1 / 2))) =
(๐ + -(1 /
6))) |
91 | | 6cn 12249 |
. . . . . . 7
โข 6 โ
โ |
92 | | 6re 12248 |
. . . . . . . 8
โข 6 โ
โ |
93 | | 6pos 12268 |
. . . . . . . 8
โข 0 <
6 |
94 | 92, 93 | gt0ne0ii 11696 |
. . . . . . 7
โข 6 โ
0 |
95 | 91, 94 | reccli 11890 |
. . . . . 6
โข (1 / 6)
โ โ |
96 | | negsub 11454 |
. . . . . 6
โข ((๐ โ โ โง (1 / 6)
โ โ) โ (๐ +
-(1 / 6)) = (๐ โ (1 /
6))) |
97 | 95, 96 | mpan2 690 |
. . . . 5
โข (๐ โ โ โ (๐ + -(1 / 6)) = (๐ โ (1 /
6))) |
98 | 82, 90, 97 | 3eqtrd 2777 |
. . . 4
โข (๐ โ โ โ
ฮฃ๐ โ (0...(0 +
1))((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1))) = (๐ โ (1 / 6))) |
99 | 8, 98 | eqtrid 2785 |
. . 3
โข (๐ โ โ โ
ฮฃ๐ โ (0...(2
โ 1))((2C๐) ยท
((๐ BernPoly ๐) / ((2 โ ๐) + 1))) = (๐ โ (1 / 6))) |
100 | 99 | oveq2d 7374 |
. 2
โข (๐ โ โ โ ((๐โ2) โ ฮฃ๐ โ (0...(2 โ
1))((2C๐) ยท ((๐ BernPoly ๐) / ((2 โ ๐) + 1)))) = ((๐โ2) โ (๐ โ (1 / 6)))) |
101 | | sqcl 14029 |
. . 3
โข (๐ โ โ โ (๐โ2) โ
โ) |
102 | | subsub 11436 |
. . . 4
โข (((๐โ2) โ โ โง
๐ โ โ โง (1 /
6) โ โ) โ ((๐โ2) โ (๐ โ (1 / 6))) = (((๐โ2) โ ๐) + (1 / 6))) |
103 | 95, 102 | mp3an3 1451 |
. . 3
โข (((๐โ2) โ โ โง
๐ โ โ) โ
((๐โ2) โ (๐ โ (1 / 6))) = (((๐โ2) โ ๐) + (1 / 6))) |
104 | 101, 103 | mpancom 687 |
. 2
โข (๐ โ โ โ ((๐โ2) โ (๐ โ (1 / 6))) = (((๐โ2) โ ๐) + (1 / 6))) |
105 | 3, 100, 104 | 3eqtrd 2777 |
1
โข (๐ โ โ โ (2
BernPoly ๐) = (((๐โ2) โ ๐) + (1 / 6))) |