Step | Hyp | Ref
| Expression |
1 | | 3nn0 12438 |
. . 3
โข 3 โ
โ0 |
2 | | fsumkthpow 15946 |
. . 3
โข ((3
โ โ0 โง ๐ โ โ0) โ
ฮฃ๐ โ (0...๐)(๐โ3) = ((((3 + 1) BernPoly (๐ + 1)) โ ((3 + 1) BernPoly
0)) / (3 + 1))) |
3 | 1, 2 | mpan 689 |
. 2
โข (๐ โ โ0
โ ฮฃ๐ โ
(0...๐)(๐โ3) = ((((3 + 1) BernPoly (๐ + 1)) โ ((3 + 1) BernPoly
0)) / (3 + 1))) |
4 | | df-4 12225 |
. . . . . 6
โข 4 = (3 +
1) |
5 | 4 | oveq1i 7372 |
. . . . 5
โข (4
BernPoly (๐ + 1)) = ((3 +
1) BernPoly (๐ +
1)) |
6 | 4 | oveq1i 7372 |
. . . . 5
โข (4
BernPoly 0) = ((3 + 1) BernPoly 0) |
7 | 5, 6 | oveq12i 7374 |
. . . 4
โข ((4
BernPoly (๐ + 1)) โ
(4 BernPoly 0)) = (((3 + 1) BernPoly (๐ + 1)) โ ((3 + 1) BernPoly
0)) |
8 | 7, 4 | oveq12i 7374 |
. . 3
โข (((4
BernPoly (๐ + 1)) โ
(4 BernPoly 0)) / 4) = ((((3 + 1) BernPoly (๐ + 1)) โ ((3 + 1) BernPoly 0)) / (3 +
1)) |
9 | | nn0cn 12430 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
โ) |
10 | | peano2cn 11334 |
. . . . . . . 8
โข (๐ โ โ โ (๐ + 1) โ
โ) |
11 | 9, 10 | syl 17 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
12 | | bpoly4 15949 |
. . . . . . 7
โข ((๐ + 1) โ โ โ (4
BernPoly (๐ + 1)) =
(((((๐ + 1)โ4) โ
(2 ยท ((๐ +
1)โ3))) + ((๐ +
1)โ2)) โ (1 / ;30))) |
13 | 11, 12 | syl 17 |
. . . . . 6
โข (๐ โ โ0
โ (4 BernPoly (๐ + 1))
= (((((๐ + 1)โ4)
โ (2 ยท ((๐ +
1)โ3))) + ((๐ +
1)โ2)) โ (1 / ;30))) |
14 | | 4nn 12243 |
. . . . . . . . . . . . . 14
โข 4 โ
โ |
15 | | 0exp 14010 |
. . . . . . . . . . . . . 14
โข (4 โ
โ โ (0โ4) = 0) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . . 13
โข
(0โ4) = 0 |
17 | | 3nn 12239 |
. . . . . . . . . . . . . . . 16
โข 3 โ
โ |
18 | | 0exp 14010 |
. . . . . . . . . . . . . . . 16
โข (3 โ
โ โ (0โ3) = 0) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข
(0โ3) = 0 |
20 | 19 | oveq2i 7373 |
. . . . . . . . . . . . . 14
โข (2
ยท (0โ3)) = (2 ยท 0) |
21 | | 2t0e0 12329 |
. . . . . . . . . . . . . 14
โข (2
ยท 0) = 0 |
22 | 20, 21 | eqtri 2765 |
. . . . . . . . . . . . 13
โข (2
ยท (0โ3)) = 0 |
23 | 16, 22 | oveq12i 7374 |
. . . . . . . . . . . 12
โข
((0โ4) โ (2 ยท (0โ3))) = (0 โ
0) |
24 | | 0m0e0 12280 |
. . . . . . . . . . . 12
โข (0
โ 0) = 0 |
25 | 23, 24 | eqtri 2765 |
. . . . . . . . . . 11
โข
((0โ4) โ (2 ยท (0โ3))) = 0 |
26 | | sq0 14103 |
. . . . . . . . . . 11
โข
(0โ2) = 0 |
27 | 25, 26 | oveq12i 7374 |
. . . . . . . . . 10
โข
(((0โ4) โ (2 ยท (0โ3))) + (0โ2)) = (0 +
0) |
28 | | 00id 11337 |
. . . . . . . . . 10
โข (0 + 0) =
0 |
29 | 27, 28 | eqtri 2765 |
. . . . . . . . 9
โข
(((0โ4) โ (2 ยท (0โ3))) + (0โ2)) =
0 |
30 | 29 | oveq1i 7372 |
. . . . . . . 8
โข
((((0โ4) โ (2 ยท (0โ3))) + (0โ2)) โ (1
/ ;30)) = (0 โ (1 / ;30)) |
31 | | 0cn 11154 |
. . . . . . . . 9
โข 0 โ
โ |
32 | | bpoly4 15949 |
. . . . . . . . 9
โข (0 โ
โ โ (4 BernPoly 0) = ((((0โ4) โ (2 ยท (0โ3)))
+ (0โ2)) โ (1 / ;30))) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . 8
โข (4
BernPoly 0) = ((((0โ4) โ (2 ยท (0โ3))) + (0โ2))
โ (1 / ;30)) |
34 | | df-neg 11395 |
. . . . . . . 8
โข -(1 /
;30) = (0 โ (1 / ;30)) |
35 | 30, 33, 34 | 3eqtr4i 2775 |
. . . . . . 7
โข (4
BernPoly 0) = -(1 / ;30) |
36 | 35 | a1i 11 |
. . . . . 6
โข (๐ โ โ0
โ (4 BernPoly 0) = -(1 / ;30)) |
37 | 13, 36 | oveq12d 7380 |
. . . . 5
โข (๐ โ โ0
โ ((4 BernPoly (๐ +
1)) โ (4 BernPoly 0)) = ((((((๐ + 1)โ4) โ (2 ยท ((๐ + 1)โ3))) + ((๐ + 1)โ2)) โ (1 /
;30)) โ -(1 / ;30))) |
38 | | 4nn0 12439 |
. . . . . . . . . . . 12
โข 4 โ
โ0 |
39 | | expcl 13992 |
. . . . . . . . . . . 12
โข (((๐ + 1) โ โ โง 4
โ โ0) โ ((๐ + 1)โ4) โ
โ) |
40 | 38, 39 | mpan2 690 |
. . . . . . . . . . 11
โข ((๐ + 1) โ โ โ
((๐ + 1)โ4) โ
โ) |
41 | | 2cn 12235 |
. . . . . . . . . . . 12
โข 2 โ
โ |
42 | | expcl 13992 |
. . . . . . . . . . . . 13
โข (((๐ + 1) โ โ โง 3
โ โ0) โ ((๐ + 1)โ3) โ
โ) |
43 | 1, 42 | mpan2 690 |
. . . . . . . . . . . 12
โข ((๐ + 1) โ โ โ
((๐ + 1)โ3) โ
โ) |
44 | | mulcl 11142 |
. . . . . . . . . . . 12
โข ((2
โ โ โง ((๐ +
1)โ3) โ โ) โ (2 ยท ((๐ + 1)โ3)) โ
โ) |
45 | 41, 43, 44 | sylancr 588 |
. . . . . . . . . . 11
โข ((๐ + 1) โ โ โ (2
ยท ((๐ + 1)โ3))
โ โ) |
46 | 40, 45 | subcld 11519 |
. . . . . . . . . 10
โข ((๐ + 1) โ โ โ
(((๐ + 1)โ4) โ
(2 ยท ((๐ +
1)โ3))) โ โ) |
47 | | sqcl 14030 |
. . . . . . . . . 10
โข ((๐ + 1) โ โ โ
((๐ + 1)โ2) โ
โ) |
48 | 46, 47 | addcld 11181 |
. . . . . . . . 9
โข ((๐ + 1) โ โ โ
((((๐ + 1)โ4) โ
(2 ยท ((๐ +
1)โ3))) + ((๐ +
1)โ2)) โ โ) |
49 | 10, 48 | syl 17 |
. . . . . . . 8
โข (๐ โ โ โ ((((๐ + 1)โ4) โ (2
ยท ((๐ + 1)โ3)))
+ ((๐ + 1)โ2)) โ
โ) |
50 | 9, 49 | syl 17 |
. . . . . . 7
โข (๐ โ โ0
โ ((((๐ + 1)โ4)
โ (2 ยท ((๐ +
1)โ3))) + ((๐ +
1)โ2)) โ โ) |
51 | | 0nn0 12435 |
. . . . . . . . . 10
โข 0 โ
โ0 |
52 | 1, 51 | deccl 12640 |
. . . . . . . . 9
โข ;30 โ
โ0 |
53 | 52 | nn0cni 12432 |
. . . . . . . 8
โข ;30 โ โ |
54 | 52 | nn0rei 12431 |
. . . . . . . . 9
โข ;30 โ โ |
55 | | 10pos 12642 |
. . . . . . . . . 10
โข 0 <
;10 |
56 | 17, 51, 51, 55 | declti 12663 |
. . . . . . . . 9
โข 0 <
;30 |
57 | 54, 56 | gt0ne0ii 11698 |
. . . . . . . 8
โข ;30 โ 0 |
58 | 53, 57 | reccli 11892 |
. . . . . . 7
โข (1 /
;30) โ
โ |
59 | | subcl 11407 |
. . . . . . 7
โข
((((((๐ + 1)โ4)
โ (2 ยท ((๐ +
1)โ3))) + ((๐ +
1)โ2)) โ โ โง (1 / ;30) โ โ) โ (((((๐ + 1)โ4) โ (2 ยท ((๐ + 1)โ3))) + ((๐ + 1)โ2)) โ (1 /
;30)) โ
โ) |
60 | 50, 58, 59 | sylancl 587 |
. . . . . 6
โข (๐ โ โ0
โ (((((๐ + 1)โ4)
โ (2 ยท ((๐ +
1)โ3))) + ((๐ +
1)โ2)) โ (1 / ;30))
โ โ) |
61 | | subneg 11457 |
. . . . . 6
โข
(((((((๐ +
1)โ4) โ (2 ยท ((๐ + 1)โ3))) + ((๐ + 1)โ2)) โ (1 / ;30)) โ โ โง (1 / ;30) โ โ) โ ((((((๐ + 1)โ4) โ (2
ยท ((๐ + 1)โ3)))
+ ((๐ + 1)โ2)) โ
(1 / ;30)) โ -(1 / ;30)) = ((((((๐ + 1)โ4) โ (2 ยท ((๐ + 1)โ3))) + ((๐ + 1)โ2)) โ (1 /
;30)) + (1 / ;30))) |
62 | 60, 58, 61 | sylancl 587 |
. . . . 5
โข (๐ โ โ0
โ ((((((๐ + 1)โ4)
โ (2 ยท ((๐ +
1)โ3))) + ((๐ +
1)โ2)) โ (1 / ;30))
โ -(1 / ;30)) = ((((((๐ + 1)โ4) โ (2
ยท ((๐ + 1)โ3)))
+ ((๐ + 1)โ2)) โ
(1 / ;30)) + (1 / ;30))) |
63 | | npcan 11417 |
. . . . . . . 8
โข
((((((๐ + 1)โ4)
โ (2 ยท ((๐ +
1)โ3))) + ((๐ +
1)โ2)) โ โ โง (1 / ;30) โ โ) โ ((((((๐ + 1)โ4) โ (2 ยท ((๐ + 1)โ3))) + ((๐ + 1)โ2)) โ (1 /
;30)) + (1 / ;30)) = ((((๐ + 1)โ4) โ (2 ยท ((๐ + 1)โ3))) + ((๐ + 1)โ2))) |
64 | 49, 58, 63 | sylancl 587 |
. . . . . . 7
โข (๐ โ โ โ
((((((๐ + 1)โ4)
โ (2 ยท ((๐ +
1)โ3))) + ((๐ +
1)โ2)) โ (1 / ;30)) +
(1 / ;30)) = ((((๐ + 1)โ4) โ (2 ยท ((๐ + 1)โ3))) + ((๐ + 1)โ2))) |
65 | 9, 64 | syl 17 |
. . . . . 6
โข (๐ โ โ0
โ ((((((๐ + 1)โ4)
โ (2 ยท ((๐ +
1)โ3))) + ((๐ +
1)โ2)) โ (1 / ;30)) +
(1 / ;30)) = ((((๐ + 1)โ4) โ (2 ยท ((๐ + 1)โ3))) + ((๐ + 1)โ2))) |
66 | | 2p2e4 12295 |
. . . . . . . . . . 11
โข (2 + 2) =
4 |
67 | 66 | eqcomi 2746 |
. . . . . . . . . 10
โข 4 = (2 +
2) |
68 | 67 | oveq2i 7373 |
. . . . . . . . 9
โข ((๐ + 1)โ4) = ((๐ + 1)โ(2 +
2)) |
69 | | df-3 12224 |
. . . . . . . . . . 11
โข 3 = (2 +
1) |
70 | 69 | oveq2i 7373 |
. . . . . . . . . 10
โข ((๐ + 1)โ3) = ((๐ + 1)โ(2 +
1)) |
71 | 70 | oveq2i 7373 |
. . . . . . . . 9
โข (2
ยท ((๐ + 1)โ3))
= (2 ยท ((๐ +
1)โ(2 + 1))) |
72 | 68, 71 | oveq12i 7374 |
. . . . . . . 8
โข (((๐ + 1)โ4) โ (2
ยท ((๐ + 1)โ3)))
= (((๐ + 1)โ(2 + 2))
โ (2 ยท ((๐ +
1)โ(2 + 1)))) |
73 | 72 | oveq1i 7372 |
. . . . . . 7
โข ((((๐ + 1)โ4) โ (2
ยท ((๐ + 1)โ3)))
+ ((๐ + 1)โ2)) =
((((๐ + 1)โ(2 + 2))
โ (2 ยท ((๐ +
1)โ(2 + 1)))) + ((๐ +
1)โ2)) |
74 | | 2nn0 12437 |
. . . . . . . . . . . . 13
โข 2 โ
โ0 |
75 | | expadd 14017 |
. . . . . . . . . . . . 13
โข (((๐ + 1) โ โ โง 2
โ โ0 โง 2 โ โ0) โ ((๐ + 1)โ(2 + 2)) = (((๐ + 1)โ2) ยท ((๐ + 1)โ2))) |
76 | 74, 74, 75 | mp3an23 1454 |
. . . . . . . . . . . 12
โข ((๐ + 1) โ โ โ
((๐ + 1)โ(2 + 2)) =
(((๐ + 1)โ2) ยท
((๐ +
1)โ2))) |
77 | | 1nn0 12436 |
. . . . . . . . . . . . . 14
โข 1 โ
โ0 |
78 | | expadd 14017 |
. . . . . . . . . . . . . 14
โข (((๐ + 1) โ โ โง 2
โ โ0 โง 1 โ โ0) โ ((๐ + 1)โ(2 + 1)) = (((๐ + 1)โ2) ยท ((๐ + 1)โ1))) |
79 | 74, 77, 78 | mp3an23 1454 |
. . . . . . . . . . . . 13
โข ((๐ + 1) โ โ โ
((๐ + 1)โ(2 + 1)) =
(((๐ + 1)โ2) ยท
((๐ +
1)โ1))) |
80 | 79 | oveq2d 7378 |
. . . . . . . . . . . 12
โข ((๐ + 1) โ โ โ (2
ยท ((๐ + 1)โ(2 +
1))) = (2 ยท (((๐ +
1)โ2) ยท ((๐ +
1)โ1)))) |
81 | 76, 80 | oveq12d 7380 |
. . . . . . . . . . 11
โข ((๐ + 1) โ โ โ
(((๐ + 1)โ(2 + 2))
โ (2 ยท ((๐ +
1)โ(2 + 1)))) = ((((๐
+ 1)โ2) ยท ((๐ +
1)โ2)) โ (2 ยท (((๐ + 1)โ2) ยท ((๐ + 1)โ1))))) |
82 | 10, 81 | syl 17 |
. . . . . . . . . 10
โข (๐ โ โ โ (((๐ + 1)โ(2 + 2)) โ (2
ยท ((๐ + 1)โ(2 +
1)))) = ((((๐ + 1)โ2)
ยท ((๐ + 1)โ2))
โ (2 ยท (((๐ +
1)โ2) ยท ((๐ +
1)โ1))))) |
83 | 10 | sqcld 14056 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((๐ + 1)โ2) โ
โ) |
84 | 83 | mulid1d 11179 |
. . . . . . . . . . 11
โข (๐ โ โ โ (((๐ + 1)โ2) ยท 1) =
((๐ +
1)โ2)) |
85 | 84 | eqcomd 2743 |
. . . . . . . . . 10
โข (๐ โ โ โ ((๐ + 1)โ2) = (((๐ + 1)โ2) ยท
1)) |
86 | 82, 85 | oveq12d 7380 |
. . . . . . . . 9
โข (๐ โ โ โ ((((๐ + 1)โ(2 + 2)) โ (2
ยท ((๐ + 1)โ(2 +
1)))) + ((๐ + 1)โ2)) =
(((((๐ + 1)โ2)
ยท ((๐ + 1)โ2))
โ (2 ยท (((๐ +
1)โ2) ยท ((๐ +
1)โ1)))) + (((๐ +
1)โ2) ยท 1))) |
87 | 10 | exp1d 14053 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ((๐ + 1)โ1) = (๐ + 1)) |
88 | 87 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (2
ยท ((๐ + 1)โ1))
= (2 ยท (๐ +
1))) |
89 | 88 | oveq2d 7378 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (((๐ + 1)โ2) ยท (2
ยท ((๐ + 1)โ1)))
= (((๐ + 1)โ2)
ยท (2 ยท (๐ +
1)))) |
90 | 89 | oveq2d 7378 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((((๐ + 1)โ2) ยท ((๐ + 1)โ2)) โ (((๐ + 1)โ2) ยท (2
ยท ((๐ +
1)โ1)))) = ((((๐ +
1)โ2) ยท ((๐ +
1)โ2)) โ (((๐ +
1)โ2) ยท (2 ยท (๐ + 1))))) |
91 | 87, 10 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ((๐ + 1)โ1) โ
โ) |
92 | | mul12 11327 |
. . . . . . . . . . . . . . 15
โข ((2
โ โ โง ((๐ +
1)โ2) โ โ โง ((๐ + 1)โ1) โ โ) โ (2
ยท (((๐ + 1)โ2)
ยท ((๐ + 1)โ1)))
= (((๐ + 1)โ2)
ยท (2 ยท ((๐ +
1)โ1)))) |
93 | 41, 83, 91, 92 | mp3an2i 1467 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (2
ยท (((๐ + 1)โ2)
ยท ((๐ + 1)โ1)))
= (((๐ + 1)โ2)
ยท (2 ยท ((๐ +
1)โ1)))) |
94 | 93 | oveq2d 7378 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((((๐ + 1)โ2) ยท ((๐ + 1)โ2)) โ (2
ยท (((๐ + 1)โ2)
ยท ((๐ +
1)โ1)))) = ((((๐ +
1)โ2) ยท ((๐ +
1)โ2)) โ (((๐ +
1)โ2) ยท (2 ยท ((๐ + 1)โ1))))) |
95 | | mulcl 11142 |
. . . . . . . . . . . . . . 15
โข ((2
โ โ โง (๐ +
1) โ โ) โ (2 ยท (๐ + 1)) โ โ) |
96 | 41, 10, 95 | sylancr 588 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (2
ยท (๐ + 1)) โ
โ) |
97 | 83, 83, 96 | subdid 11618 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (((๐ + 1)โ2) ยท (((๐ + 1)โ2) โ (2
ยท (๐ + 1)))) =
((((๐ + 1)โ2) ยท
((๐ + 1)โ2)) โ
(((๐ + 1)โ2) ยท
(2 ยท (๐ +
1))))) |
98 | 90, 94, 97 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((((๐ + 1)โ2) ยท ((๐ + 1)โ2)) โ (2
ยท (((๐ + 1)โ2)
ยท ((๐ +
1)โ1)))) = (((๐ +
1)โ2) ยท (((๐ +
1)โ2) โ (2 ยท (๐ + 1))))) |
99 | 98 | oveq1d 7377 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(((((๐ + 1)โ2)
ยท ((๐ + 1)โ2))
โ (2 ยท (((๐ +
1)โ2) ยท ((๐ +
1)โ1)))) + (((๐ +
1)โ2) ยท 1)) = ((((๐ + 1)โ2) ยท (((๐ + 1)โ2) โ (2 ยท (๐ + 1)))) + (((๐ + 1)โ2) ยท 1))) |
100 | 83, 96 | subcld 11519 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (((๐ + 1)โ2) โ (2
ยท (๐ + 1))) โ
โ) |
101 | | ax-1cn 11116 |
. . . . . . . . . . . . 13
โข 1 โ
โ |
102 | | adddi 11147 |
. . . . . . . . . . . . 13
โข ((((๐ + 1)โ2) โ โ
โง (((๐ + 1)โ2)
โ (2 ยท (๐ +
1))) โ โ โง 1 โ โ) โ (((๐ + 1)โ2) ยท ((((๐ + 1)โ2) โ (2 ยท (๐ + 1))) + 1)) = ((((๐ + 1)โ2) ยท (((๐ + 1)โ2) โ (2
ยท (๐ + 1)))) +
(((๐ + 1)โ2) ยท
1))) |
103 | 101, 102 | mp3an3 1451 |
. . . . . . . . . . . 12
โข ((((๐ + 1)โ2) โ โ
โง (((๐ + 1)โ2)
โ (2 ยท (๐ +
1))) โ โ) โ (((๐ + 1)โ2) ยท ((((๐ + 1)โ2) โ (2 ยท (๐ + 1))) + 1)) = ((((๐ + 1)โ2) ยท (((๐ + 1)โ2) โ (2
ยท (๐ + 1)))) +
(((๐ + 1)โ2) ยท
1))) |
104 | 83, 100, 103 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ โ โ (((๐ + 1)โ2) ยท ((((๐ + 1)โ2) โ (2
ยท (๐ + 1))) + 1)) =
((((๐ + 1)โ2) ยท
(((๐ + 1)โ2) โ
(2 ยท (๐ + 1)))) +
(((๐ + 1)โ2) ยท
1))) |
105 | 99, 104 | eqtr4d 2780 |
. . . . . . . . . 10
โข (๐ โ โ โ
(((((๐ + 1)โ2)
ยท ((๐ + 1)โ2))
โ (2 ยท (((๐ +
1)โ2) ยท ((๐ +
1)โ1)))) + (((๐ +
1)โ2) ยท 1)) = (((๐ + 1)โ2) ยท ((((๐ + 1)โ2) โ (2 ยท (๐ + 1))) + 1))) |
106 | | adddi 11147 |
. . . . . . . . . . . . . . . . 17
โข ((2
โ โ โง ๐
โ โ โง 1 โ โ) โ (2 ยท (๐ + 1)) = ((2 ยท ๐) + (2 ยท 1))) |
107 | 41, 101, 106 | mp3an13 1453 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (2
ยท (๐ + 1)) = ((2
ยท ๐) + (2 ยท
1))) |
108 | | 2t1e2 12323 |
. . . . . . . . . . . . . . . . 17
โข (2
ยท 1) = 2 |
109 | 108 | oveq2i 7373 |
. . . . . . . . . . . . . . . 16
โข ((2
ยท ๐) + (2 ยท
1)) = ((2 ยท ๐) +
2) |
110 | 107, 109 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (2
ยท (๐ + 1)) = ((2
ยท ๐) +
2)) |
111 | 110 | oveq1d 7377 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ((2
ยท (๐ + 1)) โ
1) = (((2 ยท ๐) + 2)
โ 1)) |
112 | | mulcl 11142 |
. . . . . . . . . . . . . . . . 17
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
113 | 41, 112 | mpan 689 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (2
ยท ๐) โ
โ) |
114 | | addsubass 11418 |
. . . . . . . . . . . . . . . . 17
โข (((2
ยท ๐) โ โ
โง 2 โ โ โง 1 โ โ) โ (((2 ยท ๐) + 2) โ 1) = ((2 ยท
๐) + (2 โ
1))) |
115 | 41, 101, 114 | mp3an23 1454 |
. . . . . . . . . . . . . . . 16
โข ((2
ยท ๐) โ โ
โ (((2 ยท ๐) +
2) โ 1) = ((2 ยท ๐) + (2 โ 1))) |
116 | 113, 115 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (((2
ยท ๐) + 2) โ 1)
= ((2 ยท ๐) + (2
โ 1))) |
117 | | 2m1e1 12286 |
. . . . . . . . . . . . . . . 16
โข (2
โ 1) = 1 |
118 | 117 | oveq2i 7373 |
. . . . . . . . . . . . . . 15
โข ((2
ยท ๐) + (2 โ
1)) = ((2 ยท ๐) +
1) |
119 | 116, 118 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (((2
ยท ๐) + 2) โ 1)
= ((2 ยท ๐) +
1)) |
120 | 111, 119 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((2
ยท (๐ + 1)) โ
1) = ((2 ยท ๐) +
1)) |
121 | 120 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (((๐ + 1)โ2) โ ((2
ยท (๐ + 1)) โ
1)) = (((๐ + 1)โ2)
โ ((2 ยท ๐) +
1))) |
122 | | subsub 11438 |
. . . . . . . . . . . . . 14
โข ((((๐ + 1)โ2) โ โ
โง (2 ยท (๐ + 1))
โ โ โง 1 โ โ) โ (((๐ + 1)โ2) โ ((2 ยท (๐ + 1)) โ 1)) = ((((๐ + 1)โ2) โ (2
ยท (๐ + 1))) +
1)) |
123 | 101, 122 | mp3an3 1451 |
. . . . . . . . . . . . 13
โข ((((๐ + 1)โ2) โ โ
โง (2 ยท (๐ + 1))
โ โ) โ (((๐
+ 1)โ2) โ ((2 ยท (๐ + 1)) โ 1)) = ((((๐ + 1)โ2) โ (2 ยท (๐ + 1))) + 1)) |
124 | 83, 96, 123 | syl2anc 585 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (((๐ + 1)โ2) โ ((2
ยท (๐ + 1)) โ
1)) = ((((๐ + 1)โ2)
โ (2 ยท (๐ +
1))) + 1)) |
125 | | sqcl 14030 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐โ2) โ
โ) |
126 | | peano2cn 11334 |
. . . . . . . . . . . . . 14
โข ((2
ยท ๐) โ โ
โ ((2 ยท ๐) + 1)
โ โ) |
127 | 113, 126 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((2
ยท ๐) + 1) โ
โ) |
128 | | binom21 14129 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ((๐ + 1)โ2) = (((๐โ2) + (2 ยท ๐)) + 1)) |
129 | | addass 11145 |
. . . . . . . . . . . . . . . 16
โข (((๐โ2) โ โ โง (2
ยท ๐) โ โ
โง 1 โ โ) โ (((๐โ2) + (2 ยท ๐)) + 1) = ((๐โ2) + ((2 ยท ๐) + 1))) |
130 | 101, 129 | mp3an3 1451 |
. . . . . . . . . . . . . . 15
โข (((๐โ2) โ โ โง (2
ยท ๐) โ โ)
โ (((๐โ2) + (2
ยท ๐)) + 1) = ((๐โ2) + ((2 ยท ๐) + 1))) |
131 | 125, 113,
130 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (((๐โ2) + (2 ยท ๐)) + 1) = ((๐โ2) + ((2 ยท ๐) + 1))) |
132 | 128, 131 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((๐ + 1)โ2) = ((๐โ2) + ((2 ยท ๐) + 1))) |
133 | 125, 127,
132 | mvrraddd 11574 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (((๐ + 1)โ2) โ ((2
ยท ๐) + 1)) = (๐โ2)) |
134 | 121, 124,
133 | 3eqtr3d 2785 |
. . . . . . . . . . 11
โข (๐ โ โ โ ((((๐ + 1)โ2) โ (2
ยท (๐ + 1))) + 1) =
(๐โ2)) |
135 | 134 | oveq2d 7378 |
. . . . . . . . . 10
โข (๐ โ โ โ (((๐ + 1)โ2) ยท ((((๐ + 1)โ2) โ (2
ยท (๐ + 1))) + 1)) =
(((๐ + 1)โ2) ยท
(๐โ2))) |
136 | 83, 125 | mulcomd 11183 |
. . . . . . . . . 10
โข (๐ โ โ โ (((๐ + 1)โ2) ยท (๐โ2)) = ((๐โ2) ยท ((๐ + 1)โ2))) |
137 | 105, 135,
136 | 3eqtrd 2781 |
. . . . . . . . 9
โข (๐ โ โ โ
(((((๐ + 1)โ2)
ยท ((๐ + 1)โ2))
โ (2 ยท (((๐ +
1)โ2) ยท ((๐ +
1)โ1)))) + (((๐ +
1)โ2) ยท 1)) = ((๐โ2) ยท ((๐ + 1)โ2))) |
138 | 86, 137 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ โ โ ((((๐ + 1)โ(2 + 2)) โ (2
ยท ((๐ + 1)โ(2 +
1)))) + ((๐ + 1)โ2)) =
((๐โ2) ยท
((๐ +
1)โ2))) |
139 | 9, 138 | syl 17 |
. . . . . . 7
โข (๐ โ โ0
โ ((((๐ + 1)โ(2 +
2)) โ (2 ยท ((๐
+ 1)โ(2 + 1)))) + ((๐
+ 1)โ2)) = ((๐โ2)
ยท ((๐ +
1)โ2))) |
140 | 73, 139 | eqtrid 2789 |
. . . . . 6
โข (๐ โ โ0
โ ((((๐ + 1)โ4)
โ (2 ยท ((๐ +
1)โ3))) + ((๐ +
1)โ2)) = ((๐โ2)
ยท ((๐ +
1)โ2))) |
141 | 65, 140 | eqtrd 2777 |
. . . . 5
โข (๐ โ โ0
โ ((((((๐ + 1)โ4)
โ (2 ยท ((๐ +
1)โ3))) + ((๐ +
1)โ2)) โ (1 / ;30)) +
(1 / ;30)) = ((๐โ2) ยท ((๐ + 1)โ2))) |
142 | 37, 62, 141 | 3eqtrd 2781 |
. . . 4
โข (๐ โ โ0
โ ((4 BernPoly (๐ +
1)) โ (4 BernPoly 0)) = ((๐โ2) ยท ((๐ + 1)โ2))) |
143 | 142 | oveq1d 7377 |
. . 3
โข (๐ โ โ0
โ (((4 BernPoly (๐ +
1)) โ (4 BernPoly 0)) / 4) = (((๐โ2) ยท ((๐ + 1)โ2)) / 4)) |
144 | 8, 143 | eqtr3id 2791 |
. 2
โข (๐ โ โ0
โ ((((3 + 1) BernPoly (๐ + 1)) โ ((3 + 1) BernPoly 0)) / (3 +
1)) = (((๐โ2) ยท
((๐ + 1)โ2)) /
4)) |
145 | 3, 144 | eqtrd 2777 |
1
โข (๐ โ โ0
โ ฮฃ๐ โ
(0...๐)(๐โ3) = (((๐โ2) ยท ((๐ + 1)โ2)) / 4)) |