MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bpoly3 Structured version   Visualization version   GIF version

Theorem bpoly3 16002
Description: The Bernoulli polynomials at three. (Contributed by Scott Fenton, 8-Jul-2015.)
Assertion
Ref Expression
bpoly3 (๐‘‹ โˆˆ โ„‚ โ†’ (3 BernPoly ๐‘‹) = (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹)))

Proof of Theorem bpoly3
Dummy variable ๐‘˜ is distinct from all other variables.
StepHypRef Expression
1 3nn0 12490 . . 3 3 โˆˆ โ„•0
2 bpolyval 15993 . . 3 ((3 โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ โ„‚) โ†’ (3 BernPoly ๐‘‹) = ((๐‘‹โ†‘3) โˆ’ ฮฃ๐‘˜ โˆˆ (0...(3 โˆ’ 1))((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1)))))
31, 2mpan 689 . 2 (๐‘‹ โˆˆ โ„‚ โ†’ (3 BernPoly ๐‘‹) = ((๐‘‹โ†‘3) โˆ’ ฮฃ๐‘˜ โˆˆ (0...(3 โˆ’ 1))((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1)))))
4 3m1e2 12340 . . . . . . 7 (3 โˆ’ 1) = 2
5 df-2 12275 . . . . . . 7 2 = (1 + 1)
64, 5eqtri 2761 . . . . . 6 (3 โˆ’ 1) = (1 + 1)
76oveq2i 7420 . . . . 5 (0...(3 โˆ’ 1)) = (0...(1 + 1))
87sumeq1i 15644 . . . 4 ฮฃ๐‘˜ โˆˆ (0...(3 โˆ’ 1))((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = ฮฃ๐‘˜ โˆˆ (0...(1 + 1))((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1)))
9 1eluzge0 12876 . . . . . . 7 1 โˆˆ (โ„คโ‰ฅโ€˜0)
109a1i 11 . . . . . 6 (๐‘‹ โˆˆ โ„‚ โ†’ 1 โˆˆ (โ„คโ‰ฅโ€˜0))
11 0z 12569 . . . . . . . . . . . . 13 0 โˆˆ โ„ค
12 fzpr 13556 . . . . . . . . . . . . 13 (0 โˆˆ โ„ค โ†’ (0...(0 + 1)) = {0, (0 + 1)})
1311, 12ax-mp 5 . . . . . . . . . . . 12 (0...(0 + 1)) = {0, (0 + 1)}
14 0p1e1 12334 . . . . . . . . . . . . 13 (0 + 1) = 1
1514oveq2i 7420 . . . . . . . . . . . 12 (0...(0 + 1)) = (0...1)
1614preq2i 4742 . . . . . . . . . . . 12 {0, (0 + 1)} = {0, 1}
1713, 15, 163eqtr3ri 2770 . . . . . . . . . . 11 {0, 1} = (0...1)
185sneqi 4640 . . . . . . . . . . 11 {2} = {(1 + 1)}
1917, 18uneq12i 4162 . . . . . . . . . 10 ({0, 1} โˆช {2}) = ((0...1) โˆช {(1 + 1)})
20 df-tp 4634 . . . . . . . . . 10 {0, 1, 2} = ({0, 1} โˆช {2})
21 fzsuc 13548 . . . . . . . . . . 11 (1 โˆˆ (โ„คโ‰ฅโ€˜0) โ†’ (0...(1 + 1)) = ((0...1) โˆช {(1 + 1)}))
229, 21ax-mp 5 . . . . . . . . . 10 (0...(1 + 1)) = ((0...1) โˆช {(1 + 1)})
2319, 20, 223eqtr4ri 2772 . . . . . . . . 9 (0...(1 + 1)) = {0, 1, 2}
2423eleq2i 2826 . . . . . . . 8 (๐‘˜ โˆˆ (0...(1 + 1)) โ†” ๐‘˜ โˆˆ {0, 1, 2})
25 vex 3479 . . . . . . . . 9 ๐‘˜ โˆˆ V
2625eltp 4693 . . . . . . . 8 (๐‘˜ โˆˆ {0, 1, 2} โ†” (๐‘˜ = 0 โˆจ ๐‘˜ = 1 โˆจ ๐‘˜ = 2))
2724, 26bitri 275 . . . . . . 7 (๐‘˜ โˆˆ (0...(1 + 1)) โ†” (๐‘˜ = 0 โˆจ ๐‘˜ = 1 โˆจ ๐‘˜ = 2))
28 oveq2 7417 . . . . . . . . . . . 12 (๐‘˜ = 0 โ†’ (3C๐‘˜) = (3C0))
29 bcn0 14270 . . . . . . . . . . . . 13 (3 โˆˆ โ„•0 โ†’ (3C0) = 1)
301, 29ax-mp 5 . . . . . . . . . . . 12 (3C0) = 1
3128, 30eqtrdi 2789 . . . . . . . . . . 11 (๐‘˜ = 0 โ†’ (3C๐‘˜) = 1)
32 oveq1 7416 . . . . . . . . . . . 12 (๐‘˜ = 0 โ†’ (๐‘˜ BernPoly ๐‘‹) = (0 BernPoly ๐‘‹))
33 oveq2 7417 . . . . . . . . . . . . . 14 (๐‘˜ = 0 โ†’ (3 โˆ’ ๐‘˜) = (3 โˆ’ 0))
3433oveq1d 7424 . . . . . . . . . . . . 13 (๐‘˜ = 0 โ†’ ((3 โˆ’ ๐‘˜) + 1) = ((3 โˆ’ 0) + 1))
35 3cn 12293 . . . . . . . . . . . . . . . 16 3 โˆˆ โ„‚
3635subid1i 11532 . . . . . . . . . . . . . . 15 (3 โˆ’ 0) = 3
3736oveq1i 7419 . . . . . . . . . . . . . 14 ((3 โˆ’ 0) + 1) = (3 + 1)
38 df-4 12277 . . . . . . . . . . . . . 14 4 = (3 + 1)
3937, 38eqtr4i 2764 . . . . . . . . . . . . 13 ((3 โˆ’ 0) + 1) = 4
4034, 39eqtrdi 2789 . . . . . . . . . . . 12 (๐‘˜ = 0 โ†’ ((3 โˆ’ ๐‘˜) + 1) = 4)
4132, 40oveq12d 7427 . . . . . . . . . . 11 (๐‘˜ = 0 โ†’ ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1)) = ((0 BernPoly ๐‘‹) / 4))
4231, 41oveq12d 7427 . . . . . . . . . 10 (๐‘˜ = 0 โ†’ ((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = (1 ยท ((0 BernPoly ๐‘‹) / 4)))
43 bpoly0 15994 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ (0 BernPoly ๐‘‹) = 1)
4443oveq1d 7424 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ((0 BernPoly ๐‘‹) / 4) = (1 / 4))
4544oveq2d 7425 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ (1 ยท ((0 BernPoly ๐‘‹) / 4)) = (1 ยท (1 / 4)))
46 4cn 12297 . . . . . . . . . . . . 13 4 โˆˆ โ„‚
47 4ne0 12320 . . . . . . . . . . . . 13 4 โ‰  0
4846, 47reccli 11944 . . . . . . . . . . . 12 (1 / 4) โˆˆ โ„‚
4948mullidi 11219 . . . . . . . . . . 11 (1 ยท (1 / 4)) = (1 / 4)
5045, 49eqtrdi 2789 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ (1 ยท ((0 BernPoly ๐‘‹) / 4)) = (1 / 4))
5142, 50sylan9eqr 2795 . . . . . . . . 9 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ = 0) โ†’ ((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = (1 / 4))
5251, 48eqeltrdi 2842 . . . . . . . 8 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ = 0) โ†’ ((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) โˆˆ โ„‚)
53 oveq2 7417 . . . . . . . . . . . 12 (๐‘˜ = 1 โ†’ (3C๐‘˜) = (3C1))
54 bcn1 14273 . . . . . . . . . . . . 13 (3 โˆˆ โ„•0 โ†’ (3C1) = 3)
551, 54ax-mp 5 . . . . . . . . . . . 12 (3C1) = 3
5653, 55eqtrdi 2789 . . . . . . . . . . 11 (๐‘˜ = 1 โ†’ (3C๐‘˜) = 3)
57 oveq1 7416 . . . . . . . . . . . 12 (๐‘˜ = 1 โ†’ (๐‘˜ BernPoly ๐‘‹) = (1 BernPoly ๐‘‹))
58 oveq2 7417 . . . . . . . . . . . . . 14 (๐‘˜ = 1 โ†’ (3 โˆ’ ๐‘˜) = (3 โˆ’ 1))
5958oveq1d 7424 . . . . . . . . . . . . 13 (๐‘˜ = 1 โ†’ ((3 โˆ’ ๐‘˜) + 1) = ((3 โˆ’ 1) + 1))
60 ax-1cn 11168 . . . . . . . . . . . . . 14 1 โˆˆ โ„‚
61 npcan 11469 . . . . . . . . . . . . . 14 ((3 โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((3 โˆ’ 1) + 1) = 3)
6235, 60, 61mp2an 691 . . . . . . . . . . . . 13 ((3 โˆ’ 1) + 1) = 3
6359, 62eqtrdi 2789 . . . . . . . . . . . 12 (๐‘˜ = 1 โ†’ ((3 โˆ’ ๐‘˜) + 1) = 3)
6457, 63oveq12d 7427 . . . . . . . . . . 11 (๐‘˜ = 1 โ†’ ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1)) = ((1 BernPoly ๐‘‹) / 3))
6556, 64oveq12d 7427 . . . . . . . . . 10 (๐‘˜ = 1 โ†’ ((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = (3 ยท ((1 BernPoly ๐‘‹) / 3)))
66 bpoly1 15995 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ (1 BernPoly ๐‘‹) = (๐‘‹ โˆ’ (1 / 2)))
6766oveq1d 7424 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ((1 BernPoly ๐‘‹) / 3) = ((๐‘‹ โˆ’ (1 / 2)) / 3))
6867oveq2d 7425 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ (3 ยท ((1 BernPoly ๐‘‹) / 3)) = (3 ยท ((๐‘‹ โˆ’ (1 / 2)) / 3)))
69 halfcn 12427 . . . . . . . . . . . . 13 (1 / 2) โˆˆ โ„‚
70 subcl 11459 . . . . . . . . . . . . 13 ((๐‘‹ โˆˆ โ„‚ โˆง (1 / 2) โˆˆ โ„‚) โ†’ (๐‘‹ โˆ’ (1 / 2)) โˆˆ โ„‚)
7169, 70mpan2 690 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ (๐‘‹ โˆ’ (1 / 2)) โˆˆ โ„‚)
72 3ne0 12318 . . . . . . . . . . . . 13 3 โ‰  0
73 divcan2 11880 . . . . . . . . . . . . 13 (((๐‘‹ โˆ’ (1 / 2)) โˆˆ โ„‚ โˆง 3 โˆˆ โ„‚ โˆง 3 โ‰  0) โ†’ (3 ยท ((๐‘‹ โˆ’ (1 / 2)) / 3)) = (๐‘‹ โˆ’ (1 / 2)))
7435, 72, 73mp3an23 1454 . . . . . . . . . . . 12 ((๐‘‹ โˆ’ (1 / 2)) โˆˆ โ„‚ โ†’ (3 ยท ((๐‘‹ โˆ’ (1 / 2)) / 3)) = (๐‘‹ โˆ’ (1 / 2)))
7571, 74syl 17 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ (3 ยท ((๐‘‹ โˆ’ (1 / 2)) / 3)) = (๐‘‹ โˆ’ (1 / 2)))
7668, 75eqtrd 2773 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ (3 ยท ((1 BernPoly ๐‘‹) / 3)) = (๐‘‹ โˆ’ (1 / 2)))
7765, 76sylan9eqr 2795 . . . . . . . . 9 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ = 1) โ†’ ((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = (๐‘‹ โˆ’ (1 / 2)))
7871adantr 482 . . . . . . . . 9 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ = 1) โ†’ (๐‘‹ โˆ’ (1 / 2)) โˆˆ โ„‚)
7977, 78eqeltrd 2834 . . . . . . . 8 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ = 1) โ†’ ((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) โˆˆ โ„‚)
80 oveq2 7417 . . . . . . . . . . . 12 (๐‘˜ = 2 โ†’ (3C๐‘˜) = (3C2))
81 bcn2 14279 . . . . . . . . . . . . . 14 (3 โˆˆ โ„•0 โ†’ (3C2) = ((3 ยท (3 โˆ’ 1)) / 2))
821, 81ax-mp 5 . . . . . . . . . . . . 13 (3C2) = ((3 ยท (3 โˆ’ 1)) / 2)
834oveq2i 7420 . . . . . . . . . . . . . . 15 (3 ยท (3 โˆ’ 1)) = (3 ยท 2)
8483oveq1i 7419 . . . . . . . . . . . . . 14 ((3 ยท (3 โˆ’ 1)) / 2) = ((3 ยท 2) / 2)
85 2cn 12287 . . . . . . . . . . . . . . 15 2 โˆˆ โ„‚
86 2ne0 12316 . . . . . . . . . . . . . . 15 2 โ‰  0
8735, 85, 86divcan4i 11961 . . . . . . . . . . . . . 14 ((3 ยท 2) / 2) = 3
8884, 87eqtri 2761 . . . . . . . . . . . . 13 ((3 ยท (3 โˆ’ 1)) / 2) = 3
8982, 88eqtri 2761 . . . . . . . . . . . 12 (3C2) = 3
9080, 89eqtrdi 2789 . . . . . . . . . . 11 (๐‘˜ = 2 โ†’ (3C๐‘˜) = 3)
91 oveq1 7416 . . . . . . . . . . . 12 (๐‘˜ = 2 โ†’ (๐‘˜ BernPoly ๐‘‹) = (2 BernPoly ๐‘‹))
92 oveq2 7417 . . . . . . . . . . . . . 14 (๐‘˜ = 2 โ†’ (3 โˆ’ ๐‘˜) = (3 โˆ’ 2))
9392oveq1d 7424 . . . . . . . . . . . . 13 (๐‘˜ = 2 โ†’ ((3 โˆ’ ๐‘˜) + 1) = ((3 โˆ’ 2) + 1))
94 2p1e3 12354 . . . . . . . . . . . . . . . 16 (2 + 1) = 3
9535, 85, 60, 94subaddrii 11549 . . . . . . . . . . . . . . 15 (3 โˆ’ 2) = 1
9695oveq1i 7419 . . . . . . . . . . . . . 14 ((3 โˆ’ 2) + 1) = (1 + 1)
9796, 5eqtr4i 2764 . . . . . . . . . . . . 13 ((3 โˆ’ 2) + 1) = 2
9893, 97eqtrdi 2789 . . . . . . . . . . . 12 (๐‘˜ = 2 โ†’ ((3 โˆ’ ๐‘˜) + 1) = 2)
9991, 98oveq12d 7427 . . . . . . . . . . 11 (๐‘˜ = 2 โ†’ ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1)) = ((2 BernPoly ๐‘‹) / 2))
10090, 99oveq12d 7427 . . . . . . . . . 10 (๐‘˜ = 2 โ†’ ((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = (3 ยท ((2 BernPoly ๐‘‹) / 2)))
101 2nn0 12489 . . . . . . . . . . . . 13 2 โˆˆ โ„•0
102 bpolycl 15996 . . . . . . . . . . . . 13 ((2 โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ โ„‚) โ†’ (2 BernPoly ๐‘‹) โˆˆ โ„‚)
103101, 102mpan 689 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ (2 BernPoly ๐‘‹) โˆˆ โ„‚)
104 2cnne0 12422 . . . . . . . . . . . . 13 (2 โˆˆ โ„‚ โˆง 2 โ‰  0)
105 div12 11894 . . . . . . . . . . . . 13 ((3 โˆˆ โ„‚ โˆง (2 BernPoly ๐‘‹) โˆˆ โ„‚ โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0)) โ†’ (3 ยท ((2 BernPoly ๐‘‹) / 2)) = ((2 BernPoly ๐‘‹) ยท (3 / 2)))
10635, 104, 105mp3an13 1453 . . . . . . . . . . . 12 ((2 BernPoly ๐‘‹) โˆˆ โ„‚ โ†’ (3 ยท ((2 BernPoly ๐‘‹) / 2)) = ((2 BernPoly ๐‘‹) ยท (3 / 2)))
107103, 106syl 17 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ (3 ยท ((2 BernPoly ๐‘‹) / 2)) = ((2 BernPoly ๐‘‹) ยท (3 / 2)))
10835, 85, 86divcli 11956 . . . . . . . . . . . 12 (3 / 2) โˆˆ โ„‚
109 mulcom 11196 . . . . . . . . . . . 12 (((2 BernPoly ๐‘‹) โˆˆ โ„‚ โˆง (3 / 2) โˆˆ โ„‚) โ†’ ((2 BernPoly ๐‘‹) ยท (3 / 2)) = ((3 / 2) ยท (2 BernPoly ๐‘‹)))
110103, 108, 109sylancl 587 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ ((2 BernPoly ๐‘‹) ยท (3 / 2)) = ((3 / 2) ยท (2 BernPoly ๐‘‹)))
111 bpoly2 16001 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ (2 BernPoly ๐‘‹) = (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))
112111oveq2d 7425 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ((3 / 2) ยท (2 BernPoly ๐‘‹)) = ((3 / 2) ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6))))
113 sqcl 14083 . . . . . . . . . . . . . 14 (๐‘‹ โˆˆ โ„‚ โ†’ (๐‘‹โ†‘2) โˆˆ โ„‚)
114 6cn 12303 . . . . . . . . . . . . . . . 16 6 โˆˆ โ„‚
115 6re 12302 . . . . . . . . . . . . . . . . 17 6 โˆˆ โ„
116 6pos 12322 . . . . . . . . . . . . . . . . 17 0 < 6
117115, 116gt0ne0ii 11750 . . . . . . . . . . . . . . . 16 6 โ‰  0
118114, 117reccli 11944 . . . . . . . . . . . . . . 15 (1 / 6) โˆˆ โ„‚
119 subsub 11490 . . . . . . . . . . . . . . 15 (((๐‘‹โ†‘2) โˆˆ โ„‚ โˆง ๐‘‹ โˆˆ โ„‚ โˆง (1 / 6) โˆˆ โ„‚) โ†’ ((๐‘‹โ†‘2) โˆ’ (๐‘‹ โˆ’ (1 / 6))) = (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))
120118, 119mp3an3 1451 . . . . . . . . . . . . . 14 (((๐‘‹โ†‘2) โˆˆ โ„‚ โˆง ๐‘‹ โˆˆ โ„‚) โ†’ ((๐‘‹โ†‘2) โˆ’ (๐‘‹ โˆ’ (1 / 6))) = (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))
121113, 120mpancom 687 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ ((๐‘‹โ†‘2) โˆ’ (๐‘‹ โˆ’ (1 / 6))) = (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))
122121oveq2d 7425 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ((3 / 2) ยท ((๐‘‹โ†‘2) โˆ’ (๐‘‹ โˆ’ (1 / 6)))) = ((3 / 2) ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6))))
123 subcl 11459 . . . . . . . . . . . . . 14 ((๐‘‹ โˆˆ โ„‚ โˆง (1 / 6) โˆˆ โ„‚) โ†’ (๐‘‹ โˆ’ (1 / 6)) โˆˆ โ„‚)
124118, 123mpan2 690 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ (๐‘‹ โˆ’ (1 / 6)) โˆˆ โ„‚)
125 subdi 11647 . . . . . . . . . . . . 13 (((3 / 2) โˆˆ โ„‚ โˆง (๐‘‹โ†‘2) โˆˆ โ„‚ โˆง (๐‘‹ โˆ’ (1 / 6)) โˆˆ โ„‚) โ†’ ((3 / 2) ยท ((๐‘‹โ†‘2) โˆ’ (๐‘‹ โˆ’ (1 / 6)))) = (((3 / 2) ยท (๐‘‹โ†‘2)) โˆ’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6)))))
126108, 113, 124, 125mp3an2i 1467 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ((3 / 2) ยท ((๐‘‹โ†‘2) โˆ’ (๐‘‹ โˆ’ (1 / 6)))) = (((3 / 2) ยท (๐‘‹โ†‘2)) โˆ’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6)))))
127112, 122, 1263eqtr2d 2779 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ ((3 / 2) ยท (2 BernPoly ๐‘‹)) = (((3 / 2) ยท (๐‘‹โ†‘2)) โˆ’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6)))))
128107, 110, 1273eqtrd 2777 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ (3 ยท ((2 BernPoly ๐‘‹) / 2)) = (((3 / 2) ยท (๐‘‹โ†‘2)) โˆ’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6)))))
129100, 128sylan9eqr 2795 . . . . . . . . 9 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ = 2) โ†’ ((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = (((3 / 2) ยท (๐‘‹โ†‘2)) โˆ’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6)))))
130 mulcl 11194 . . . . . . . . . . . 12 (((3 / 2) โˆˆ โ„‚ โˆง (๐‘‹โ†‘2) โˆˆ โ„‚) โ†’ ((3 / 2) ยท (๐‘‹โ†‘2)) โˆˆ โ„‚)
131108, 113, 130sylancr 588 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ ((3 / 2) ยท (๐‘‹โ†‘2)) โˆˆ โ„‚)
132 mulcl 11194 . . . . . . . . . . . 12 (((3 / 2) โˆˆ โ„‚ โˆง (๐‘‹ โˆ’ (1 / 6)) โˆˆ โ„‚) โ†’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6))) โˆˆ โ„‚)
133108, 124, 132sylancr 588 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6))) โˆˆ โ„‚)
134131, 133subcld 11571 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ (((3 / 2) ยท (๐‘‹โ†‘2)) โˆ’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6)))) โˆˆ โ„‚)
135134adantr 482 . . . . . . . . 9 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ = 2) โ†’ (((3 / 2) ยท (๐‘‹โ†‘2)) โˆ’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6)))) โˆˆ โ„‚)
136129, 135eqeltrd 2834 . . . . . . . 8 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ = 2) โ†’ ((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) โˆˆ โ„‚)
13752, 79, 1363jaodan 1431 . . . . . . 7 ((๐‘‹ โˆˆ โ„‚ โˆง (๐‘˜ = 0 โˆจ ๐‘˜ = 1 โˆจ ๐‘˜ = 2)) โ†’ ((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) โˆˆ โ„‚)
13827, 137sylan2b 595 . . . . . 6 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ (0...(1 + 1))) โ†’ ((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) โˆˆ โ„‚)
1395eqeq2i 2746 . . . . . . 7 (๐‘˜ = 2 โ†” ๐‘˜ = (1 + 1))
140139, 100sylbir 234 . . . . . 6 (๐‘˜ = (1 + 1) โ†’ ((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = (3 ยท ((2 BernPoly ๐‘‹) / 2)))
14110, 138, 140fsump1 15702 . . . . 5 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...(1 + 1))((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = (ฮฃ๐‘˜ โˆˆ (0...1)((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) + (3 ยท ((2 BernPoly ๐‘‹) / 2))))
142128oveq2d 7425 . . . . 5 (๐‘‹ โˆˆ โ„‚ โ†’ (ฮฃ๐‘˜ โˆˆ (0...1)((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) + (3 ยท ((2 BernPoly ๐‘‹) / 2))) = (ฮฃ๐‘˜ โˆˆ (0...1)((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) + (((3 / 2) ยท (๐‘‹โ†‘2)) โˆ’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6))))))
14315sumeq1i 15644 . . . . . . . . 9 ฮฃ๐‘˜ โˆˆ (0...(0 + 1))((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = ฮฃ๐‘˜ โˆˆ (0...1)((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1)))
144 0nn0 12487 . . . . . . . . . . . . 13 0 โˆˆ โ„•0
145 nn0uz 12864 . . . . . . . . . . . . 13 โ„•0 = (โ„คโ‰ฅโ€˜0)
146144, 145eleqtri 2832 . . . . . . . . . . . 12 0 โˆˆ (โ„คโ‰ฅโ€˜0)
147146a1i 11 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ 0 โˆˆ (โ„คโ‰ฅโ€˜0))
14813, 16eqtri 2761 . . . . . . . . . . . . . 14 (0...(0 + 1)) = {0, 1}
149148eleq2i 2826 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ (0...(0 + 1)) โ†” ๐‘˜ โˆˆ {0, 1})
15025elpr 4652 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ {0, 1} โ†” (๐‘˜ = 0 โˆจ ๐‘˜ = 1))
151149, 150bitri 275 . . . . . . . . . . . 12 (๐‘˜ โˆˆ (0...(0 + 1)) โ†” (๐‘˜ = 0 โˆจ ๐‘˜ = 1))
15252, 79jaodan 957 . . . . . . . . . . . 12 ((๐‘‹ โˆˆ โ„‚ โˆง (๐‘˜ = 0 โˆจ ๐‘˜ = 1)) โ†’ ((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) โˆˆ โ„‚)
153151, 152sylan2b 595 . . . . . . . . . . 11 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ (0...(0 + 1))) โ†’ ((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) โˆˆ โ„‚)
15414eqeq2i 2746 . . . . . . . . . . . 12 (๐‘˜ = (0 + 1) โ†” ๐‘˜ = 1)
155154, 65sylbi 216 . . . . . . . . . . 11 (๐‘˜ = (0 + 1) โ†’ ((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = (3 ยท ((1 BernPoly ๐‘‹) / 3)))
156147, 153, 155fsump1 15702 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...(0 + 1))((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = (ฮฃ๐‘˜ โˆˆ (0...0)((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) + (3 ยท ((1 BernPoly ๐‘‹) / 3))))
15750, 48eqeltrdi 2842 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ (1 ยท ((0 BernPoly ๐‘‹) / 4)) โˆˆ โ„‚)
15842fsum1 15693 . . . . . . . . . . . . 13 ((0 โˆˆ โ„ค โˆง (1 ยท ((0 BernPoly ๐‘‹) / 4)) โˆˆ โ„‚) โ†’ ฮฃ๐‘˜ โˆˆ (0...0)((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = (1 ยท ((0 BernPoly ๐‘‹) / 4)))
15911, 157, 158sylancr 588 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...0)((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = (1 ยท ((0 BernPoly ๐‘‹) / 4)))
160159, 50eqtrd 2773 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...0)((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = (1 / 4))
161160, 76oveq12d 7427 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ (ฮฃ๐‘˜ โˆˆ (0...0)((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) + (3 ยท ((1 BernPoly ๐‘‹) / 3))) = ((1 / 4) + (๐‘‹ โˆ’ (1 / 2))))
162156, 161eqtrd 2773 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...(0 + 1))((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = ((1 / 4) + (๐‘‹ โˆ’ (1 / 2))))
163143, 162eqtr3id 2787 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...1)((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = ((1 / 4) + (๐‘‹ โˆ’ (1 / 2))))
164163oveq1d 7424 . . . . . . 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 11192 . . . . . . . . 9 (((1 / 4) โˆˆ โ„‚ โˆง (๐‘‹ โˆ’ (1 / 2)) โˆˆ โ„‚) โ†’ ((1 / 4) + (๐‘‹ โˆ’ (1 / 2))) โˆˆ โ„‚)
16648, 71, 165sylancr 588 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ ((1 / 4) + (๐‘‹ โˆ’ (1 / 2))) โˆˆ โ„‚)
167166, 131, 133addsub12d 11594 . . . . . . 7 (๐‘‹ โˆˆ โ„‚ โ†’ (((1 / 4) + (๐‘‹ โˆ’ (1 / 2))) + (((3 / 2) ยท (๐‘‹โ†‘2)) โˆ’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6))))) = (((3 / 2) ยท (๐‘‹โ†‘2)) + (((1 / 4) + (๐‘‹ โˆ’ (1 / 2))) โˆ’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6))))))
168164, 167eqtrd 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))))))
169133, 166negsubdi2d 11587 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ -(((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6))) โˆ’ ((1 / 4) + (๐‘‹ โˆ’ (1 / 2)))) = (((1 / 4) + (๐‘‹ โˆ’ (1 / 2))) โˆ’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6)))))
170 subdi 11647 . . . . . . . . . . . 12 (((3 / 2) โˆˆ โ„‚ โˆง ๐‘‹ โˆˆ โ„‚ โˆง (1 / 6) โˆˆ โ„‚) โ†’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6))) = (((3 / 2) ยท ๐‘‹) โˆ’ ((3 / 2) ยท (1 / 6))))
171108, 118, 170mp3an13 1453 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6))) = (((3 / 2) ยท ๐‘‹) โˆ’ ((3 / 2) ยท (1 / 6))))
172 addsub12 11473 . . . . . . . . . . . 12 (((1 / 4) โˆˆ โ„‚ โˆง ๐‘‹ โˆˆ โ„‚ โˆง (1 / 2) โˆˆ โ„‚) โ†’ ((1 / 4) + (๐‘‹ โˆ’ (1 / 2))) = (๐‘‹ + ((1 / 4) โˆ’ (1 / 2))))
17348, 69, 172mp3an13 1453 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ ((1 / 4) + (๐‘‹ โˆ’ (1 / 2))) = (๐‘‹ + ((1 / 4) โˆ’ (1 / 2))))
174171, 173oveq12d 7427 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ (((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6))) โˆ’ ((1 / 4) + (๐‘‹ โˆ’ (1 / 2)))) = ((((3 / 2) ยท ๐‘‹) โˆ’ ((3 / 2) ยท (1 / 6))) โˆ’ (๐‘‹ + ((1 / 4) โˆ’ (1 / 2)))))
175 mulcl 11194 . . . . . . . . . . . . 13 (((3 / 2) โˆˆ โ„‚ โˆง ๐‘‹ โˆˆ โ„‚) โ†’ ((3 / 2) ยท ๐‘‹) โˆˆ โ„‚)
176108, 175mpan 689 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ((3 / 2) ยท ๐‘‹) โˆˆ โ„‚)
177108, 118mulcli 11221 . . . . . . . . . . . 12 ((3 / 2) ยท (1 / 6)) โˆˆ โ„‚
178 negsub 11508 . . . . . . . . . . . 12 ((((3 / 2) ยท ๐‘‹) โˆˆ โ„‚ โˆง ((3 / 2) ยท (1 / 6)) โˆˆ โ„‚) โ†’ (((3 / 2) ยท ๐‘‹) + -((3 / 2) ยท (1 / 6))) = (((3 / 2) ยท ๐‘‹) โˆ’ ((3 / 2) ยท (1 / 6))))
179176, 177, 178sylancl 587 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ (((3 / 2) ยท ๐‘‹) + -((3 / 2) ยท (1 / 6))) = (((3 / 2) ยท ๐‘‹) โˆ’ ((3 / 2) ยท (1 / 6))))
180179oveq1d 7424 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ ((((3 / 2) ยท ๐‘‹) + -((3 / 2) ยท (1 / 6))) โˆ’ (๐‘‹ + ((1 / 4) โˆ’ (1 / 2)))) = ((((3 / 2) ยท ๐‘‹) โˆ’ ((3 / 2) ยท (1 / 6))) โˆ’ (๐‘‹ + ((1 / 4) โˆ’ (1 / 2)))))
18169, 48negsubdi2i 11546 . . . . . . . . . . . . . 14 -((1 / 2) โˆ’ (1 / 4)) = ((1 / 4) โˆ’ (1 / 2))
18285, 35, 85mul12i 11409 . . . . . . . . . . . . . . . . . . 19 (2 ยท (3 ยท 2)) = (3 ยท (2 ยท 2))
183 3t2e6 12378 . . . . . . . . . . . . . . . . . . . 20 (3 ยท 2) = 6
184183oveq2i 7420 . . . . . . . . . . . . . . . . . . 19 (2 ยท (3 ยท 2)) = (2 ยท 6)
185 2t2e4 12376 . . . . . . . . . . . . . . . . . . . 20 (2 ยท 2) = 4
186185oveq2i 7420 . . . . . . . . . . . . . . . . . . 19 (3 ยท (2 ยท 2)) = (3 ยท 4)
187182, 184, 1863eqtr3i 2769 . . . . . . . . . . . . . . . . . 18 (2 ยท 6) = (3 ยท 4)
188187oveq2i 7420 . . . . . . . . . . . . . . . . 17 ((3 ยท 1) / (2 ยท 6)) = ((3 ยท 1) / (3 ยท 4))
18946, 47pm3.2i 472 . . . . . . . . . . . . . . . . . 18 (4 โˆˆ โ„‚ โˆง 4 โ‰  0)
19035, 72pm3.2i 472 . . . . . . . . . . . . . . . . . 18 (3 โˆˆ โ„‚ โˆง 3 โ‰  0)
191 divcan5 11916 . . . . . . . . . . . . . . . . . 18 ((1 โˆˆ โ„‚ โˆง (4 โˆˆ โ„‚ โˆง 4 โ‰  0) โˆง (3 โˆˆ โ„‚ โˆง 3 โ‰  0)) โ†’ ((3 ยท 1) / (3 ยท 4)) = (1 / 4))
19260, 189, 190, 191mp3an 1462 . . . . . . . . . . . . . . . . 17 ((3 ยท 1) / (3 ยท 4)) = (1 / 4)
193188, 192eqtri 2761 . . . . . . . . . . . . . . . 16 ((3 ยท 1) / (2 ยท 6)) = (1 / 4)
19435, 85, 60, 114, 86, 117divmuldivi 11974 . . . . . . . . . . . . . . . 16 ((3 / 2) ยท (1 / 6)) = ((3 ยท 1) / (2 ยท 6))
195 2t1e2 12375 . . . . . . . . . . . . . . . . . . . 20 (2 ยท 1) = 2
196195, 5eqtri 2761 . . . . . . . . . . . . . . . . . . 19 (2 ยท 1) = (1 + 1)
197196, 185oveq12i 7421 . . . . . . . . . . . . . . . . . 18 ((2 ยท 1) / (2 ยท 2)) = ((1 + 1) / 4)
198 divcan5 11916 . . . . . . . . . . . . . . . . . . 19 ((1 โˆˆ โ„‚ โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0) โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0)) โ†’ ((2 ยท 1) / (2 ยท 2)) = (1 / 2))
19960, 104, 104, 198mp3an 1462 . . . . . . . . . . . . . . . . . 18 ((2 ยท 1) / (2 ยท 2)) = (1 / 2)
20060, 60, 46, 47divdiri 11971 . . . . . . . . . . . . . . . . . 18 ((1 + 1) / 4) = ((1 / 4) + (1 / 4))
201197, 199, 2003eqtr3ri 2770 . . . . . . . . . . . . . . . . 17 ((1 / 4) + (1 / 4)) = (1 / 2)
20269, 48, 48, 201subaddrii 11549 . . . . . . . . . . . . . . . 16 ((1 / 2) โˆ’ (1 / 4)) = (1 / 4)
203193, 194, 2023eqtr4ri 2772 . . . . . . . . . . . . . . 15 ((1 / 2) โˆ’ (1 / 4)) = ((3 / 2) ยท (1 / 6))
204203negeqi 11453 . . . . . . . . . . . . . 14 -((1 / 2) โˆ’ (1 / 4)) = -((3 / 2) ยท (1 / 6))
205181, 204eqtr3i 2763 . . . . . . . . . . . . 13 ((1 / 4) โˆ’ (1 / 2)) = -((3 / 2) ยท (1 / 6))
20648, 69subcli 11536 . . . . . . . . . . . . . 14 ((1 / 4) โˆ’ (1 / 2)) โˆˆ โ„‚
207177negcli 11528 . . . . . . . . . . . . . 14 -((3 / 2) ยท (1 / 6)) โˆˆ โ„‚
208206, 207subeq0i 11540 . . . . . . . . . . . . 13 ((((1 / 4) โˆ’ (1 / 2)) โˆ’ -((3 / 2) ยท (1 / 6))) = 0 โ†” ((1 / 4) โˆ’ (1 / 2)) = -((3 / 2) ยท (1 / 6)))
209205, 208mpbir 230 . . . . . . . . . . . 12 (((1 / 4) โˆ’ (1 / 2)) โˆ’ -((3 / 2) ยท (1 / 6))) = 0
210209oveq2i 7420 . . . . . . . . . . 11 ((((3 / 2) ยท ๐‘‹) โˆ’ ๐‘‹) โˆ’ (((1 / 4) โˆ’ (1 / 2)) โˆ’ -((3 / 2) ยท (1 / 6)))) = ((((3 / 2) ยท ๐‘‹) โˆ’ ๐‘‹) โˆ’ 0)
211 id 22 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ๐‘‹ โˆˆ โ„‚)
212206a1i 11 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ((1 / 4) โˆ’ (1 / 2)) โˆˆ โ„‚)
213207a1i 11 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ -((3 / 2) ยท (1 / 6)) โˆˆ โ„‚)
214176, 211, 212, 213subadd4d 11619 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ ((((3 / 2) ยท ๐‘‹) โˆ’ ๐‘‹) โˆ’ (((1 / 4) โˆ’ (1 / 2)) โˆ’ -((3 / 2) ยท (1 / 6)))) = ((((3 / 2) ยท ๐‘‹) + -((3 / 2) ยท (1 / 6))) โˆ’ (๐‘‹ + ((1 / 4) โˆ’ (1 / 2)))))
215 subdir 11648 . . . . . . . . . . . . . . 15 (((3 / 2) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ โˆง ๐‘‹ โˆˆ โ„‚) โ†’ (((3 / 2) โˆ’ 1) ยท ๐‘‹) = (((3 / 2) ยท ๐‘‹) โˆ’ (1 ยท ๐‘‹)))
216108, 60, 215mp3an12 1452 . . . . . . . . . . . . . 14 (๐‘‹ โˆˆ โ„‚ โ†’ (((3 / 2) โˆ’ 1) ยท ๐‘‹) = (((3 / 2) ยท ๐‘‹) โˆ’ (1 ยท ๐‘‹)))
217 divsubdir 11908 . . . . . . . . . . . . . . . . . 18 ((3 โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0)) โ†’ ((3 โˆ’ 2) / 2) = ((3 / 2) โˆ’ (2 / 2)))
21835, 85, 104, 217mp3an 1462 . . . . . . . . . . . . . . . . 17 ((3 โˆ’ 2) / 2) = ((3 / 2) โˆ’ (2 / 2))
21995oveq1i 7419 . . . . . . . . . . . . . . . . 17 ((3 โˆ’ 2) / 2) = (1 / 2)
220 2div2e1 12353 . . . . . . . . . . . . . . . . . 18 (2 / 2) = 1
221220oveq2i 7420 . . . . . . . . . . . . . . . . 17 ((3 / 2) โˆ’ (2 / 2)) = ((3 / 2) โˆ’ 1)
222218, 219, 2213eqtr3ri 2770 . . . . . . . . . . . . . . . 16 ((3 / 2) โˆ’ 1) = (1 / 2)
223222oveq1i 7419 . . . . . . . . . . . . . . 15 (((3 / 2) โˆ’ 1) ยท ๐‘‹) = ((1 / 2) ยท ๐‘‹)
224223a1i 11 . . . . . . . . . . . . . 14 (๐‘‹ โˆˆ โ„‚ โ†’ (((3 / 2) โˆ’ 1) ยท ๐‘‹) = ((1 / 2) ยท ๐‘‹))
225 mullid 11213 . . . . . . . . . . . . . . 15 (๐‘‹ โˆˆ โ„‚ โ†’ (1 ยท ๐‘‹) = ๐‘‹)
226225oveq2d 7425 . . . . . . . . . . . . . 14 (๐‘‹ โˆˆ โ„‚ โ†’ (((3 / 2) ยท ๐‘‹) โˆ’ (1 ยท ๐‘‹)) = (((3 / 2) ยท ๐‘‹) โˆ’ ๐‘‹))
227216, 224, 2263eqtr3rd 2782 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ (((3 / 2) ยท ๐‘‹) โˆ’ ๐‘‹) = ((1 / 2) ยท ๐‘‹))
228227oveq1d 7424 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ((((3 / 2) ยท ๐‘‹) โˆ’ ๐‘‹) โˆ’ 0) = (((1 / 2) ยท ๐‘‹) โˆ’ 0))
229 mulcl 11194 . . . . . . . . . . . . . 14 (((1 / 2) โˆˆ โ„‚ โˆง ๐‘‹ โˆˆ โ„‚) โ†’ ((1 / 2) ยท ๐‘‹) โˆˆ โ„‚)
23069, 229mpan 689 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ ((1 / 2) ยท ๐‘‹) โˆˆ โ„‚)
231230subid1d 11560 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ (((1 / 2) ยท ๐‘‹) โˆ’ 0) = ((1 / 2) ยท ๐‘‹))
232228, 231eqtrd 2773 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ ((((3 / 2) ยท ๐‘‹) โˆ’ ๐‘‹) โˆ’ 0) = ((1 / 2) ยท ๐‘‹))
233210, 214, 2323eqtr3a 2797 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ ((((3 / 2) ยท ๐‘‹) + -((3 / 2) ยท (1 / 6))) โˆ’ (๐‘‹ + ((1 / 4) โˆ’ (1 / 2)))) = ((1 / 2) ยท ๐‘‹))
234174, 180, 2333eqtr2d 2779 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ (((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6))) โˆ’ ((1 / 4) + (๐‘‹ โˆ’ (1 / 2)))) = ((1 / 2) ยท ๐‘‹))
235234negeqd 11454 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ -(((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6))) โˆ’ ((1 / 4) + (๐‘‹ โˆ’ (1 / 2)))) = -((1 / 2) ยท ๐‘‹))
236169, 235eqtr3d 2775 . . . . . . 7 (๐‘‹ โˆˆ โ„‚ โ†’ (((1 / 4) + (๐‘‹ โˆ’ (1 / 2))) โˆ’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6)))) = -((1 / 2) ยท ๐‘‹))
237236oveq2d 7425 . . . . . 6 (๐‘‹ โˆˆ โ„‚ โ†’ (((3 / 2) ยท (๐‘‹โ†‘2)) + (((1 / 4) + (๐‘‹ โˆ’ (1 / 2))) โˆ’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6))))) = (((3 / 2) ยท (๐‘‹โ†‘2)) + -((1 / 2) ยท ๐‘‹)))
238131, 230negsubd 11577 . . . . . 6 (๐‘‹ โˆˆ โ„‚ โ†’ (((3 / 2) ยท (๐‘‹โ†‘2)) + -((1 / 2) ยท ๐‘‹)) = (((3 / 2) ยท (๐‘‹โ†‘2)) โˆ’ ((1 / 2) ยท ๐‘‹)))
239168, 237, 2383eqtrd 2777 . . . . 5 (๐‘‹ โˆˆ โ„‚ โ†’ (ฮฃ๐‘˜ โˆˆ (0...1)((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) + (((3 / 2) ยท (๐‘‹โ†‘2)) โˆ’ ((3 / 2) ยท (๐‘‹ โˆ’ (1 / 6))))) = (((3 / 2) ยท (๐‘‹โ†‘2)) โˆ’ ((1 / 2) ยท ๐‘‹)))
240141, 142, 2393eqtrd 2777 . . . 4 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...(1 + 1))((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = (((3 / 2) ยท (๐‘‹โ†‘2)) โˆ’ ((1 / 2) ยท ๐‘‹)))
2418, 240eqtrid 2785 . . 3 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...(3 โˆ’ 1))((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1))) = (((3 / 2) ยท (๐‘‹โ†‘2)) โˆ’ ((1 / 2) ยท ๐‘‹)))
242241oveq2d 7425 . 2 (๐‘‹ โˆˆ โ„‚ โ†’ ((๐‘‹โ†‘3) โˆ’ ฮฃ๐‘˜ โˆˆ (0...(3 โˆ’ 1))((3C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((3 โˆ’ ๐‘˜) + 1)))) = ((๐‘‹โ†‘3) โˆ’ (((3 / 2) ยท (๐‘‹โ†‘2)) โˆ’ ((1 / 2) ยท ๐‘‹))))
243 expcl 14045 . . . 4 ((๐‘‹ โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0) โ†’ (๐‘‹โ†‘3) โˆˆ โ„‚)
2441, 243mpan2 690 . . 3 (๐‘‹ โˆˆ โ„‚ โ†’ (๐‘‹โ†‘3) โˆˆ โ„‚)
245244, 131, 230subsubd 11599 . 2 (๐‘‹ โˆˆ โ„‚ โ†’ ((๐‘‹โ†‘3) โˆ’ (((3 / 2) ยท (๐‘‹โ†‘2)) โˆ’ ((1 / 2) ยท ๐‘‹))) = (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹)))
2463, 242, 2453eqtrd 2777 1 (๐‘‹ โˆˆ โ„‚ โ†’ (3 BernPoly ๐‘‹) = (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 397   โˆจ wo 846   โˆจ w3o 1087   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2941   โˆช cun 3947  {csn 4629  {cpr 4631  {ctp 4633  โ€˜cfv 6544  (class class class)co 7409  โ„‚cc 11108  0cc0 11110  1c1 11111   + caddc 11113   ยท cmul 11115   โˆ’ cmin 11444  -cneg 11445   / cdiv 11871  2c2 12267  3c3 12268  4c4 12269  6c6 12271  โ„•0cn0 12472  โ„คcz 12558  โ„คโ‰ฅcuz 12822  ...cfz 13484  โ†‘cexp 14027  Ccbc 14262  ฮฃcsu 15632   BernPoly cbp 15990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-sup 9437  df-oi 9505  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-n0 12473  df-z 12559  df-uz 12823  df-rp 12975  df-fz 13485  df-fzo 13628  df-seq 13967  df-exp 14028  df-fac 14234  df-bc 14263  df-hash 14291  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-clim 15432  df-sum 15633  df-bpoly 15991
This theorem is referenced by:  bpoly4  16003
  Copyright terms: Public domain W3C validator