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

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

Proof of Theorem bpoly4
Dummy variable ๐‘˜ is distinct from all other variables.
StepHypRef Expression
1 4nn0 12491 . . 3 4 โˆˆ โ„•0
2 bpolyval 15993 . . 3 ((4 โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ โ„‚) โ†’ (4 BernPoly ๐‘‹) = ((๐‘‹โ†‘4) โˆ’ ฮฃ๐‘˜ โˆˆ (0...(4 โˆ’ 1))((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1)))))
31, 2mpan 689 . 2 (๐‘‹ โˆˆ โ„‚ โ†’ (4 BernPoly ๐‘‹) = ((๐‘‹โ†‘4) โˆ’ ฮฃ๐‘˜ โˆˆ (0...(4 โˆ’ 1))((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1)))))
4 4m1e3 12341 . . . . . . 7 (4 โˆ’ 1) = 3
5 df-3 12276 . . . . . . 7 3 = (2 + 1)
64, 5eqtri 2761 . . . . . 6 (4 โˆ’ 1) = (2 + 1)
76oveq2i 7420 . . . . 5 (0...(4 โˆ’ 1)) = (0...(2 + 1))
87sumeq1i 15644 . . . 4 ฮฃ๐‘˜ โˆˆ (0...(4 โˆ’ 1))((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = ฮฃ๐‘˜ โˆˆ (0...(2 + 1))((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1)))
9 2eluzge0 12877 . . . . . . 7 2 โˆˆ (โ„คโ‰ฅโ€˜0)
109a1i 11 . . . . . 6 (๐‘‹ โˆˆ โ„‚ โ†’ 2 โˆˆ (โ„คโ‰ฅโ€˜0))
11 elfzelz 13501 . . . . . . . . . 10 (๐‘˜ โˆˆ (0...(2 + 1)) โ†’ ๐‘˜ โˆˆ โ„ค)
12 bccl 14282 . . . . . . . . . 10 ((4 โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„ค) โ†’ (4C๐‘˜) โˆˆ โ„•0)
131, 11, 12sylancr 588 . . . . . . . . 9 (๐‘˜ โˆˆ (0...(2 + 1)) โ†’ (4C๐‘˜) โˆˆ โ„•0)
1413nn0cnd 12534 . . . . . . . 8 (๐‘˜ โˆˆ (0...(2 + 1)) โ†’ (4C๐‘˜) โˆˆ โ„‚)
1514adantl 483 . . . . . . 7 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ (0...(2 + 1))) โ†’ (4C๐‘˜) โˆˆ โ„‚)
16 elfznn0 13594 . . . . . . . . . 10 (๐‘˜ โˆˆ (0...(2 + 1)) โ†’ ๐‘˜ โˆˆ โ„•0)
17 bpolycl 15996 . . . . . . . . . 10 ((๐‘˜ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ โ„‚) โ†’ (๐‘˜ BernPoly ๐‘‹) โˆˆ โ„‚)
1816, 17sylan 581 . . . . . . . . 9 ((๐‘˜ โˆˆ (0...(2 + 1)) โˆง ๐‘‹ โˆˆ โ„‚) โ†’ (๐‘˜ BernPoly ๐‘‹) โˆˆ โ„‚)
1918ancoms 460 . . . . . . . 8 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ (0...(2 + 1))) โ†’ (๐‘˜ BernPoly ๐‘‹) โˆˆ โ„‚)
20 4re 12296 . . . . . . . . . . . . 13 4 โˆˆ โ„
2120a1i 11 . . . . . . . . . . . 12 (๐‘˜ โˆˆ (0...(2 + 1)) โ†’ 4 โˆˆ โ„)
2211zred 12666 . . . . . . . . . . . 12 (๐‘˜ โˆˆ (0...(2 + 1)) โ†’ ๐‘˜ โˆˆ โ„)
2321, 22resubcld 11642 . . . . . . . . . . 11 (๐‘˜ โˆˆ (0...(2 + 1)) โ†’ (4 โˆ’ ๐‘˜) โˆˆ โ„)
24 peano2re 11387 . . . . . . . . . . 11 ((4 โˆ’ ๐‘˜) โˆˆ โ„ โ†’ ((4 โˆ’ ๐‘˜) + 1) โˆˆ โ„)
2523, 24syl 17 . . . . . . . . . 10 (๐‘˜ โˆˆ (0...(2 + 1)) โ†’ ((4 โˆ’ ๐‘˜) + 1) โˆˆ โ„)
2625recnd 11242 . . . . . . . . 9 (๐‘˜ โˆˆ (0...(2 + 1)) โ†’ ((4 โˆ’ ๐‘˜) + 1) โˆˆ โ„‚)
2726adantl 483 . . . . . . . 8 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ (0...(2 + 1))) โ†’ ((4 โˆ’ ๐‘˜) + 1) โˆˆ โ„‚)
28 1red 11215 . . . . . . . . . . 11 (๐‘˜ โˆˆ (0...(2 + 1)) โ†’ 1 โˆˆ โ„)
295oveq2i 7420 . . . . . . . . . . . . . 14 (0...3) = (0...(2 + 1))
3029eleq2i 2826 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ (0...3) โ†” ๐‘˜ โˆˆ (0...(2 + 1)))
31 elfzelz 13501 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ (0...3) โ†’ ๐‘˜ โˆˆ โ„ค)
3231zred 12666 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ (0...3) โ†’ ๐‘˜ โˆˆ โ„)
33 3re 12292 . . . . . . . . . . . . . . 15 3 โˆˆ โ„
3433a1i 11 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ (0...3) โ†’ 3 โˆˆ โ„)
3520a1i 11 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ (0...3) โ†’ 4 โˆˆ โ„)
36 elfzle2 13505 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ (0...3) โ†’ ๐‘˜ โ‰ค 3)
37 3lt4 12386 . . . . . . . . . . . . . . 15 3 < 4
3837a1i 11 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ (0...3) โ†’ 3 < 4)
3932, 34, 35, 36, 38lelttrd 11372 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ (0...3) โ†’ ๐‘˜ < 4)
4030, 39sylbir 234 . . . . . . . . . . . 12 (๐‘˜ โˆˆ (0...(2 + 1)) โ†’ ๐‘˜ < 4)
4122, 21posdifd 11801 . . . . . . . . . . . 12 (๐‘˜ โˆˆ (0...(2 + 1)) โ†’ (๐‘˜ < 4 โ†” 0 < (4 โˆ’ ๐‘˜)))
4240, 41mpbid 231 . . . . . . . . . . 11 (๐‘˜ โˆˆ (0...(2 + 1)) โ†’ 0 < (4 โˆ’ ๐‘˜))
43 0lt1 11736 . . . . . . . . . . . 12 0 < 1
4443a1i 11 . . . . . . . . . . 11 (๐‘˜ โˆˆ (0...(2 + 1)) โ†’ 0 < 1)
4523, 28, 42, 44addgt0d 11789 . . . . . . . . . 10 (๐‘˜ โˆˆ (0...(2 + 1)) โ†’ 0 < ((4 โˆ’ ๐‘˜) + 1))
4645gt0ne0d 11778 . . . . . . . . 9 (๐‘˜ โˆˆ (0...(2 + 1)) โ†’ ((4 โˆ’ ๐‘˜) + 1) โ‰  0)
4746adantl 483 . . . . . . . 8 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ (0...(2 + 1))) โ†’ ((4 โˆ’ ๐‘˜) + 1) โ‰  0)
4819, 27, 47divcld 11990 . . . . . . 7 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ (0...(2 + 1))) โ†’ ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1)) โˆˆ โ„‚)
4915, 48mulcld 11234 . . . . . 6 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ (0...(2 + 1))) โ†’ ((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) โˆˆ โ„‚)
505eqeq2i 2746 . . . . . . 7 (๐‘˜ = 3 โ†” ๐‘˜ = (2 + 1))
51 oveq2 7417 . . . . . . . . 9 (๐‘˜ = 3 โ†’ (4C๐‘˜) = (4C3))
52 4bc3eq4 14288 . . . . . . . . 9 (4C3) = 4
5351, 52eqtrdi 2789 . . . . . . . 8 (๐‘˜ = 3 โ†’ (4C๐‘˜) = 4)
54 oveq1 7416 . . . . . . . . 9 (๐‘˜ = 3 โ†’ (๐‘˜ BernPoly ๐‘‹) = (3 BernPoly ๐‘‹))
55 oveq2 7417 . . . . . . . . . . 11 (๐‘˜ = 3 โ†’ (4 โˆ’ ๐‘˜) = (4 โˆ’ 3))
5655oveq1d 7424 . . . . . . . . . 10 (๐‘˜ = 3 โ†’ ((4 โˆ’ ๐‘˜) + 1) = ((4 โˆ’ 3) + 1))
57 4cn 12297 . . . . . . . . . . . . 13 4 โˆˆ โ„‚
58 3cn 12293 . . . . . . . . . . . . 13 3 โˆˆ โ„‚
59 ax-1cn 11168 . . . . . . . . . . . . 13 1 โˆˆ โ„‚
60 3p1e4 12357 . . . . . . . . . . . . 13 (3 + 1) = 4
6157, 58, 59, 60subaddrii 11549 . . . . . . . . . . . 12 (4 โˆ’ 3) = 1
6261oveq1i 7419 . . . . . . . . . . 11 ((4 โˆ’ 3) + 1) = (1 + 1)
63 df-2 12275 . . . . . . . . . . 11 2 = (1 + 1)
6462, 63eqtr4i 2764 . . . . . . . . . 10 ((4 โˆ’ 3) + 1) = 2
6556, 64eqtrdi 2789 . . . . . . . . 9 (๐‘˜ = 3 โ†’ ((4 โˆ’ ๐‘˜) + 1) = 2)
6654, 65oveq12d 7427 . . . . . . . 8 (๐‘˜ = 3 โ†’ ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1)) = ((3 BernPoly ๐‘‹) / 2))
6753, 66oveq12d 7427 . . . . . . 7 (๐‘˜ = 3 โ†’ ((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = (4 ยท ((3 BernPoly ๐‘‹) / 2)))
6850, 67sylbir 234 . . . . . 6 (๐‘˜ = (2 + 1) โ†’ ((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = (4 ยท ((3 BernPoly ๐‘‹) / 2)))
6910, 49, 68fsump1 15702 . . . . 5 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...(2 + 1))((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = (ฮฃ๐‘˜ โˆˆ (0...2)((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) + (4 ยท ((3 BernPoly ๐‘‹) / 2))))
7063oveq2i 7420 . . . . . . . 8 (0...2) = (0...(1 + 1))
7170sumeq1i 15644 . . . . . . 7 ฮฃ๐‘˜ โˆˆ (0...2)((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = ฮฃ๐‘˜ โˆˆ (0...(1 + 1))((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1)))
72 1eluzge0 12876 . . . . . . . . . 10 1 โˆˆ (โ„คโ‰ฅโ€˜0)
7372a1i 11 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ 1 โˆˆ (โ„คโ‰ฅโ€˜0))
74 fzssp1 13544 . . . . . . . . . . . 12 (0...(1 + 1)) โŠ† (0...((1 + 1) + 1))
7563oveq1i 7419 . . . . . . . . . . . . 13 (2 + 1) = ((1 + 1) + 1)
7675oveq2i 7420 . . . . . . . . . . . 12 (0...(2 + 1)) = (0...((1 + 1) + 1))
7774, 76sseqtrri 4020 . . . . . . . . . . 11 (0...(1 + 1)) โŠ† (0...(2 + 1))
7877sseli 3979 . . . . . . . . . 10 (๐‘˜ โˆˆ (0...(1 + 1)) โ†’ ๐‘˜ โˆˆ (0...(2 + 1)))
7978, 49sylan2 594 . . . . . . . . 9 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ (0...(1 + 1))) โ†’ ((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) โˆˆ โ„‚)
8063eqeq2i 2746 . . . . . . . . . 10 (๐‘˜ = 2 โ†” ๐‘˜ = (1 + 1))
81 oveq2 7417 . . . . . . . . . . . 12 (๐‘˜ = 2 โ†’ (4C๐‘˜) = (4C2))
82 4bc2eq6 14289 . . . . . . . . . . . 12 (4C2) = 6
8381, 82eqtrdi 2789 . . . . . . . . . . 11 (๐‘˜ = 2 โ†’ (4C๐‘˜) = 6)
84 oveq1 7416 . . . . . . . . . . . 12 (๐‘˜ = 2 โ†’ (๐‘˜ BernPoly ๐‘‹) = (2 BernPoly ๐‘‹))
85 oveq2 7417 . . . . . . . . . . . . . 14 (๐‘˜ = 2 โ†’ (4 โˆ’ ๐‘˜) = (4 โˆ’ 2))
8685oveq1d 7424 . . . . . . . . . . . . 13 (๐‘˜ = 2 โ†’ ((4 โˆ’ ๐‘˜) + 1) = ((4 โˆ’ 2) + 1))
87 2cn 12287 . . . . . . . . . . . . . . . 16 2 โˆˆ โ„‚
88 2p2e4 12347 . . . . . . . . . . . . . . . 16 (2 + 2) = 4
8957, 87, 87, 88subaddrii 11549 . . . . . . . . . . . . . . 15 (4 โˆ’ 2) = 2
9089oveq1i 7419 . . . . . . . . . . . . . 14 ((4 โˆ’ 2) + 1) = (2 + 1)
9190, 5eqtr4i 2764 . . . . . . . . . . . . 13 ((4 โˆ’ 2) + 1) = 3
9286, 91eqtrdi 2789 . . . . . . . . . . . 12 (๐‘˜ = 2 โ†’ ((4 โˆ’ ๐‘˜) + 1) = 3)
9384, 92oveq12d 7427 . . . . . . . . . . 11 (๐‘˜ = 2 โ†’ ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1)) = ((2 BernPoly ๐‘‹) / 3))
9483, 93oveq12d 7427 . . . . . . . . . 10 (๐‘˜ = 2 โ†’ ((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = (6 ยท ((2 BernPoly ๐‘‹) / 3)))
9580, 94sylbir 234 . . . . . . . . 9 (๐‘˜ = (1 + 1) โ†’ ((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = (6 ยท ((2 BernPoly ๐‘‹) / 3)))
9673, 79, 95fsump1 15702 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...(1 + 1))((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = (ฮฃ๐‘˜ โˆˆ (0...1)((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) + (6 ยท ((2 BernPoly ๐‘‹) / 3))))
97 0p1e1 12334 . . . . . . . . . . . 12 (0 + 1) = 1
9897oveq2i 7420 . . . . . . . . . . 11 (0...(0 + 1)) = (0...1)
9998sumeq1i 15644 . . . . . . . . . 10 ฮฃ๐‘˜ โˆˆ (0...(0 + 1))((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = ฮฃ๐‘˜ โˆˆ (0...1)((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1)))
100 0nn0 12487 . . . . . . . . . . . . . 14 0 โˆˆ โ„•0
101 nn0uz 12864 . . . . . . . . . . . . . 14 โ„•0 = (โ„คโ‰ฅโ€˜0)
102100, 101eleqtri 2832 . . . . . . . . . . . . 13 0 โˆˆ (โ„คโ‰ฅโ€˜0)
103102a1i 11 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ 0 โˆˆ (โ„คโ‰ฅโ€˜0))
104 3nn 12291 . . . . . . . . . . . . . . . . 17 3 โˆˆ โ„•
105 nnuz 12865 . . . . . . . . . . . . . . . . 17 โ„• = (โ„คโ‰ฅโ€˜1)
106104, 105eleqtri 2832 . . . . . . . . . . . . . . . 16 3 โˆˆ (โ„คโ‰ฅโ€˜1)
107 fzss2 13541 . . . . . . . . . . . . . . . 16 (3 โˆˆ (โ„คโ‰ฅโ€˜1) โ†’ (0...1) โŠ† (0...3))
108106, 107ax-mp 5 . . . . . . . . . . . . . . 15 (0...1) โŠ† (0...3)
109 2p1e3 12354 . . . . . . . . . . . . . . . 16 (2 + 1) = 3
110109oveq2i 7420 . . . . . . . . . . . . . . 15 (0...(2 + 1)) = (0...3)
111108, 98, 1103sstr4i 4026 . . . . . . . . . . . . . 14 (0...(0 + 1)) โŠ† (0...(2 + 1))
112111sseli 3979 . . . . . . . . . . . . 13 (๐‘˜ โˆˆ (0...(0 + 1)) โ†’ ๐‘˜ โˆˆ (0...(2 + 1)))
113112, 49sylan2 594 . . . . . . . . . . . 12 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ (0...(0 + 1))) โ†’ ((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) โˆˆ โ„‚)
11497eqeq2i 2746 . . . . . . . . . . . . 13 (๐‘˜ = (0 + 1) โ†” ๐‘˜ = 1)
115 oveq2 7417 . . . . . . . . . . . . . . 15 (๐‘˜ = 1 โ†’ (4C๐‘˜) = (4C1))
116 bcn1 14273 . . . . . . . . . . . . . . . 16 (4 โˆˆ โ„•0 โ†’ (4C1) = 4)
1171, 116ax-mp 5 . . . . . . . . . . . . . . 15 (4C1) = 4
118115, 117eqtrdi 2789 . . . . . . . . . . . . . 14 (๐‘˜ = 1 โ†’ (4C๐‘˜) = 4)
119 oveq1 7416 . . . . . . . . . . . . . . 15 (๐‘˜ = 1 โ†’ (๐‘˜ BernPoly ๐‘‹) = (1 BernPoly ๐‘‹))
120 oveq2 7417 . . . . . . . . . . . . . . . . 17 (๐‘˜ = 1 โ†’ (4 โˆ’ ๐‘˜) = (4 โˆ’ 1))
121120oveq1d 7424 . . . . . . . . . . . . . . . 16 (๐‘˜ = 1 โ†’ ((4 โˆ’ ๐‘˜) + 1) = ((4 โˆ’ 1) + 1))
1224oveq1i 7419 . . . . . . . . . . . . . . . . 17 ((4 โˆ’ 1) + 1) = (3 + 1)
123 df-4 12277 . . . . . . . . . . . . . . . . 17 4 = (3 + 1)
124122, 123eqtr4i 2764 . . . . . . . . . . . . . . . 16 ((4 โˆ’ 1) + 1) = 4
125121, 124eqtrdi 2789 . . . . . . . . . . . . . . 15 (๐‘˜ = 1 โ†’ ((4 โˆ’ ๐‘˜) + 1) = 4)
126119, 125oveq12d 7427 . . . . . . . . . . . . . 14 (๐‘˜ = 1 โ†’ ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1)) = ((1 BernPoly ๐‘‹) / 4))
127118, 126oveq12d 7427 . . . . . . . . . . . . 13 (๐‘˜ = 1 โ†’ ((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = (4 ยท ((1 BernPoly ๐‘‹) / 4)))
128114, 127sylbi 216 . . . . . . . . . . . 12 (๐‘˜ = (0 + 1) โ†’ ((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = (4 ยท ((1 BernPoly ๐‘‹) / 4)))
129103, 113, 128fsump1 15702 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...(0 + 1))((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = (ฮฃ๐‘˜ โˆˆ (0...0)((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) + (4 ยท ((1 BernPoly ๐‘‹) / 4))))
130 0z 12569 . . . . . . . . . . . . . 14 0 โˆˆ โ„ค
13159a1i 11 . . . . . . . . . . . . . . 15 (๐‘‹ โˆˆ โ„‚ โ†’ 1 โˆˆ โ„‚)
132 bpolycl 15996 . . . . . . . . . . . . . . . . 17 ((0 โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ โ„‚) โ†’ (0 BernPoly ๐‘‹) โˆˆ โ„‚)
133100, 132mpan 689 . . . . . . . . . . . . . . . 16 (๐‘‹ โˆˆ โ„‚ โ†’ (0 BernPoly ๐‘‹) โˆˆ โ„‚)
134 5cn 12300 . . . . . . . . . . . . . . . . 17 5 โˆˆ โ„‚
135134a1i 11 . . . . . . . . . . . . . . . 16 (๐‘‹ โˆˆ โ„‚ โ†’ 5 โˆˆ โ„‚)
136 0re 11216 . . . . . . . . . . . . . . . . . 18 0 โˆˆ โ„
137 5pos 12321 . . . . . . . . . . . . . . . . . 18 0 < 5
138136, 137gtneii 11326 . . . . . . . . . . . . . . . . 17 5 โ‰  0
139138a1i 11 . . . . . . . . . . . . . . . 16 (๐‘‹ โˆˆ โ„‚ โ†’ 5 โ‰  0)
140133, 135, 139divcld 11990 . . . . . . . . . . . . . . 15 (๐‘‹ โˆˆ โ„‚ โ†’ ((0 BernPoly ๐‘‹) / 5) โˆˆ โ„‚)
141131, 140mulcld 11234 . . . . . . . . . . . . . 14 (๐‘‹ โˆˆ โ„‚ โ†’ (1 ยท ((0 BernPoly ๐‘‹) / 5)) โˆˆ โ„‚)
142 oveq2 7417 . . . . . . . . . . . . . . . . 17 (๐‘˜ = 0 โ†’ (4C๐‘˜) = (4C0))
143 bcn0 14270 . . . . . . . . . . . . . . . . . 18 (4 โˆˆ โ„•0 โ†’ (4C0) = 1)
1441, 143ax-mp 5 . . . . . . . . . . . . . . . . 17 (4C0) = 1
145142, 144eqtrdi 2789 . . . . . . . . . . . . . . . 16 (๐‘˜ = 0 โ†’ (4C๐‘˜) = 1)
146 oveq1 7416 . . . . . . . . . . . . . . . . 17 (๐‘˜ = 0 โ†’ (๐‘˜ BernPoly ๐‘‹) = (0 BernPoly ๐‘‹))
147 oveq2 7417 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ = 0 โ†’ (4 โˆ’ ๐‘˜) = (4 โˆ’ 0))
148147oveq1d 7424 . . . . . . . . . . . . . . . . . 18 (๐‘˜ = 0 โ†’ ((4 โˆ’ ๐‘˜) + 1) = ((4 โˆ’ 0) + 1))
14957subid1i 11532 . . . . . . . . . . . . . . . . . . . 20 (4 โˆ’ 0) = 4
150149oveq1i 7419 . . . . . . . . . . . . . . . . . . 19 ((4 โˆ’ 0) + 1) = (4 + 1)
151 4p1e5 12358 . . . . . . . . . . . . . . . . . . 19 (4 + 1) = 5
152150, 151eqtri 2761 . . . . . . . . . . . . . . . . . 18 ((4 โˆ’ 0) + 1) = 5
153148, 152eqtrdi 2789 . . . . . . . . . . . . . . . . 17 (๐‘˜ = 0 โ†’ ((4 โˆ’ ๐‘˜) + 1) = 5)
154146, 153oveq12d 7427 . . . . . . . . . . . . . . . 16 (๐‘˜ = 0 โ†’ ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1)) = ((0 BernPoly ๐‘‹) / 5))
155145, 154oveq12d 7427 . . . . . . . . . . . . . . 15 (๐‘˜ = 0 โ†’ ((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = (1 ยท ((0 BernPoly ๐‘‹) / 5)))
156155fsum1 15693 . . . . . . . . . . . . . 14 ((0 โˆˆ โ„ค โˆง (1 ยท ((0 BernPoly ๐‘‹) / 5)) โˆˆ โ„‚) โ†’ ฮฃ๐‘˜ โˆˆ (0...0)((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = (1 ยท ((0 BernPoly ๐‘‹) / 5)))
157130, 141, 156sylancr 588 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...0)((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = (1 ยท ((0 BernPoly ๐‘‹) / 5)))
158 bpoly0 15994 . . . . . . . . . . . . . . . 16 (๐‘‹ โˆˆ โ„‚ โ†’ (0 BernPoly ๐‘‹) = 1)
159158oveq1d 7424 . . . . . . . . . . . . . . 15 (๐‘‹ โˆˆ โ„‚ โ†’ ((0 BernPoly ๐‘‹) / 5) = (1 / 5))
160159oveq2d 7425 . . . . . . . . . . . . . 14 (๐‘‹ โˆˆ โ„‚ โ†’ (1 ยท ((0 BernPoly ๐‘‹) / 5)) = (1 ยท (1 / 5)))
161134, 138reccli 11944 . . . . . . . . . . . . . . 15 (1 / 5) โˆˆ โ„‚
162161mullidi 11219 . . . . . . . . . . . . . 14 (1 ยท (1 / 5)) = (1 / 5)
163160, 162eqtrdi 2789 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ (1 ยท ((0 BernPoly ๐‘‹) / 5)) = (1 / 5))
164157, 163eqtrd 2773 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...0)((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = (1 / 5))
165 1nn0 12488 . . . . . . . . . . . . . . 15 1 โˆˆ โ„•0
166 bpolycl 15996 . . . . . . . . . . . . . . 15 ((1 โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ โ„‚) โ†’ (1 BernPoly ๐‘‹) โˆˆ โ„‚)
167165, 166mpan 689 . . . . . . . . . . . . . 14 (๐‘‹ โˆˆ โ„‚ โ†’ (1 BernPoly ๐‘‹) โˆˆ โ„‚)
168 nn0cn 12482 . . . . . . . . . . . . . . 15 (4 โˆˆ โ„•0 โ†’ 4 โˆˆ โ„‚)
1691, 168mp1i 13 . . . . . . . . . . . . . 14 (๐‘‹ โˆˆ โ„‚ โ†’ 4 โˆˆ โ„‚)
170 4ne0 12320 . . . . . . . . . . . . . . 15 4 โ‰  0
171170a1i 11 . . . . . . . . . . . . . 14 (๐‘‹ โˆˆ โ„‚ โ†’ 4 โ‰  0)
172167, 169, 171divcan2d 11992 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ (4 ยท ((1 BernPoly ๐‘‹) / 4)) = (1 BernPoly ๐‘‹))
173 bpoly1 15995 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ (1 BernPoly ๐‘‹) = (๐‘‹ โˆ’ (1 / 2)))
174172, 173eqtrd 2773 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ (4 ยท ((1 BernPoly ๐‘‹) / 4)) = (๐‘‹ โˆ’ (1 / 2)))
175164, 174oveq12d 7427 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ (ฮฃ๐‘˜ โˆˆ (0...0)((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) + (4 ยท ((1 BernPoly ๐‘‹) / 4))) = ((1 / 5) + (๐‘‹ โˆ’ (1 / 2))))
176129, 175eqtrd 2773 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...(0 + 1))((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = ((1 / 5) + (๐‘‹ โˆ’ (1 / 2))))
17799, 176eqtr3id 2787 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...1)((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = ((1 / 5) + (๐‘‹ โˆ’ (1 / 2))))
178 6cn 12303 . . . . . . . . . . . 12 6 โˆˆ โ„‚
179178a1i 11 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ 6 โˆˆ โ„‚)
180 2nn0 12489 . . . . . . . . . . . 12 2 โˆˆ โ„•0
181 bpolycl 15996 . . . . . . . . . . . 12 ((2 โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ โ„‚) โ†’ (2 BernPoly ๐‘‹) โˆˆ โ„‚)
182180, 181mpan 689 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ (2 BernPoly ๐‘‹) โˆˆ โ„‚)
18358a1i 11 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ 3 โˆˆ โ„‚)
184 3ne0 12318 . . . . . . . . . . . 12 3 โ‰  0
185184a1i 11 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ 3 โ‰  0)
186179, 182, 183, 185div12d 12026 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ (6 ยท ((2 BernPoly ๐‘‹) / 3)) = ((2 BernPoly ๐‘‹) ยท (6 / 3)))
187 3t2e6 12378 . . . . . . . . . . . . 13 (3 ยท 2) = 6
188178, 58, 87, 184divmuli 11968 . . . . . . . . . . . . 13 ((6 / 3) = 2 โ†” (3 ยท 2) = 6)
189187, 188mpbir 230 . . . . . . . . . . . 12 (6 / 3) = 2
190189oveq2i 7420 . . . . . . . . . . 11 ((2 BernPoly ๐‘‹) ยท (6 / 3)) = ((2 BernPoly ๐‘‹) ยท 2)
19187a1i 11 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ 2 โˆˆ โ„‚)
192182, 191mulcomd 11235 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ((2 BernPoly ๐‘‹) ยท 2) = (2 ยท (2 BernPoly ๐‘‹)))
193 bpoly2 16001 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ (2 BernPoly ๐‘‹) = (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))
194193oveq2d 7425 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ (2 ยท (2 BernPoly ๐‘‹)) = (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6))))
195192, 194eqtrd 2773 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ ((2 BernPoly ๐‘‹) ยท 2) = (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6))))
196190, 195eqtrid 2785 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ ((2 BernPoly ๐‘‹) ยท (6 / 3)) = (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6))))
197186, 196eqtrd 2773 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ (6 ยท ((2 BernPoly ๐‘‹) / 3)) = (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6))))
198177, 197oveq12d 7427 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ (ฮฃ๐‘˜ โˆˆ (0...1)((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) + (6 ยท ((2 BernPoly ๐‘‹) / 3))) = (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))))
19996, 198eqtrd 2773 . . . . . . 7 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...(1 + 1))((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))))
20071, 199eqtrid 2785 . . . . . 6 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...2)((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))))
201 3nn0 12490 . . . . . . . . 9 3 โˆˆ โ„•0
202 bpolycl 15996 . . . . . . . . 9 ((3 โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ โ„‚) โ†’ (3 BernPoly ๐‘‹) โˆˆ โ„‚)
203201, 202mpan 689 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ (3 BernPoly ๐‘‹) โˆˆ โ„‚)
204 2ne0 12316 . . . . . . . . 9 2 โ‰  0
205204a1i 11 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ 2 โ‰  0)
206169, 203, 191, 205div12d 12026 . . . . . . 7 (๐‘‹ โˆˆ โ„‚ โ†’ (4 ยท ((3 BernPoly ๐‘‹) / 2)) = ((3 BernPoly ๐‘‹) ยท (4 / 2)))
207 4d2e2 12382 . . . . . . . . 9 (4 / 2) = 2
208207oveq2i 7420 . . . . . . . 8 ((3 BernPoly ๐‘‹) ยท (4 / 2)) = ((3 BernPoly ๐‘‹) ยท 2)
209203, 191mulcomd 11235 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ ((3 BernPoly ๐‘‹) ยท 2) = (2 ยท (3 BernPoly ๐‘‹)))
210 bpoly3 16002 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ (3 BernPoly ๐‘‹) = (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹)))
211210oveq2d 7425 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ (2 ยท (3 BernPoly ๐‘‹)) = (2 ยท (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹))))
212209, 211eqtrd 2773 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ ((3 BernPoly ๐‘‹) ยท 2) = (2 ยท (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹))))
213208, 212eqtrid 2785 . . . . . . 7 (๐‘‹ โˆˆ โ„‚ โ†’ ((3 BernPoly ๐‘‹) ยท (4 / 2)) = (2 ยท (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹))))
214206, 213eqtrd 2773 . . . . . 6 (๐‘‹ โˆˆ โ„‚ โ†’ (4 ยท ((3 BernPoly ๐‘‹) / 2)) = (2 ยท (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹))))
215200, 214oveq12d 7427 . . . . 5 (๐‘‹ โˆˆ โ„‚ โ†’ (ฮฃ๐‘˜ โˆˆ (0...2)((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) + (4 ยท ((3 BernPoly ๐‘‹) / 2))) = ((((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))) + (2 ยท (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹)))))
21669, 215eqtrd 2773 . . . 4 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...(2 + 1))((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = ((((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))) + (2 ยท (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹)))))
2178, 216eqtrid 2785 . . 3 (๐‘‹ โˆˆ โ„‚ โ†’ ฮฃ๐‘˜ โˆˆ (0...(4 โˆ’ 1))((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1))) = ((((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))) + (2 ยท (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹)))))
218217oveq2d 7425 . 2 (๐‘‹ โˆˆ โ„‚ โ†’ ((๐‘‹โ†‘4) โˆ’ ฮฃ๐‘˜ โˆˆ (0...(4 โˆ’ 1))((4C๐‘˜) ยท ((๐‘˜ BernPoly ๐‘‹) / ((4 โˆ’ ๐‘˜) + 1)))) = ((๐‘‹โ†‘4) โˆ’ ((((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))) + (2 ยท (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹))))))
219 expcl 14045 . . . . 5 ((๐‘‹ โˆˆ โ„‚ โˆง 4 โˆˆ โ„•0) โ†’ (๐‘‹โ†‘4) โˆˆ โ„‚)
2201, 219mpan2 690 . . . 4 (๐‘‹ โˆˆ โ„‚ โ†’ (๐‘‹โ†‘4) โˆˆ โ„‚)
221 expcl 14045 . . . . . 6 ((๐‘‹ โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0) โ†’ (๐‘‹โ†‘3) โˆˆ โ„‚)
222201, 221mpan2 690 . . . . 5 (๐‘‹ โˆˆ โ„‚ โ†’ (๐‘‹โ†‘3) โˆˆ โ„‚)
223191, 222mulcld 11234 . . . 4 (๐‘‹ โˆˆ โ„‚ โ†’ (2 ยท (๐‘‹โ†‘3)) โˆˆ โ„‚)
224 sqcl 14083 . . . . 5 (๐‘‹ โˆˆ โ„‚ โ†’ (๐‘‹โ†‘2) โˆˆ โ„‚)
225201, 100deccl 12692 . . . . . . . 8 30 โˆˆ โ„•0
226225nn0cni 12484 . . . . . . 7 30 โˆˆ โ„‚
227 dfdec10 12680 . . . . . . . . 9 30 = ((10 ยท 3) + 0)
228 10re 12696 . . . . . . . . . . . 12 10 โˆˆ โ„
229228recni 11228 . . . . . . . . . . 11 10 โˆˆ โ„‚
230229, 58mulcli 11221 . . . . . . . . . 10 (10 ยท 3) โˆˆ โ„‚
231230addridi 11401 . . . . . . . . 9 ((10 ยท 3) + 0) = (10 ยท 3)
232227, 231eqtri 2761 . . . . . . . 8 30 = (10 ยท 3)
233 10pos 12694 . . . . . . . . . 10 0 < 10
234136, 233gtneii 11326 . . . . . . . . 9 10 โ‰  0
235229, 58, 234, 184mulne0i 11857 . . . . . . . 8 (10 ยท 3) โ‰  0
236232, 235eqnetri 3012 . . . . . . 7 30 โ‰  0
237226, 236reccli 11944 . . . . . 6 (1 / 30) โˆˆ โ„‚
238237a1i 11 . . . . 5 (๐‘‹ โˆˆ โ„‚ โ†’ (1 / 30) โˆˆ โ„‚)
239224, 238subcld 11571 . . . 4 (๐‘‹ โˆˆ โ„‚ โ†’ ((๐‘‹โ†‘2) โˆ’ (1 / 30)) โˆˆ โ„‚)
240220, 223, 239subsubd 11599 . . 3 (๐‘‹ โˆˆ โ„‚ โ†’ ((๐‘‹โ†‘4) โˆ’ ((2 ยท (๐‘‹โ†‘3)) โˆ’ ((๐‘‹โ†‘2) โˆ’ (1 / 30)))) = (((๐‘‹โ†‘4) โˆ’ (2 ยท (๐‘‹โ†‘3))) + ((๐‘‹โ†‘2) โˆ’ (1 / 30))))
241161a1i 11 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ (1 / 5) โˆˆ โ„‚)
242 id 22 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ ๐‘‹ โˆˆ โ„‚)
24387, 204reccli 11944 . . . . . . . . . 10 (1 / 2) โˆˆ โ„‚
244243a1i 11 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ (1 / 2) โˆˆ โ„‚)
245242, 244subcld 11571 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ (๐‘‹ โˆ’ (1 / 2)) โˆˆ โ„‚)
246241, 245addcld 11233 . . . . . . 7 (๐‘‹ โˆˆ โ„‚ โ†’ ((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) โˆˆ โ„‚)
247224, 242subcld 11571 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ ((๐‘‹โ†‘2) โˆ’ ๐‘‹) โˆˆ โ„‚)
248 6pos 12322 . . . . . . . . . . . 12 0 < 6
249136, 248gtneii 11326 . . . . . . . . . . 11 6 โ‰  0
250178, 249reccli 11944 . . . . . . . . . 10 (1 / 6) โˆˆ โ„‚
251250a1i 11 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ (1 / 6) โˆˆ โ„‚)
252247, 251addcld 11233 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)) โˆˆ โ„‚)
253191, 252mulcld 11234 . . . . . . 7 (๐‘‹ โˆˆ โ„‚ โ†’ (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6))) โˆˆ โ„‚)
254246, 253addcld 11233 . . . . . 6 (๐‘‹ โˆˆ โ„‚ โ†’ (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))) โˆˆ โ„‚)
25558, 87, 204divcli 11956 . . . . . . . . . . 11 (3 / 2) โˆˆ โ„‚
256255a1i 11 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ (3 / 2) โˆˆ โ„‚)
257256, 224mulcld 11234 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ ((3 / 2) ยท (๐‘‹โ†‘2)) โˆˆ โ„‚)
258222, 257subcld 11571 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ ((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) โˆˆ โ„‚)
259244, 242mulcld 11234 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ ((1 / 2) ยท ๐‘‹) โˆˆ โ„‚)
260258, 259addcld 11233 . . . . . . 7 (๐‘‹ โˆˆ โ„‚ โ†’ (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹)) โˆˆ โ„‚)
261191, 260mulcld 11234 . . . . . 6 (๐‘‹ โˆˆ โ„‚ โ†’ (2 ยท (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹))) โˆˆ โ„‚)
262254, 261addcomd 11416 . . . . 5 (๐‘‹ โˆˆ โ„‚ โ†’ ((((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))))))
263191, 258, 259adddid 11238 . . . . . . 7 (๐‘‹ โˆˆ โ„‚ โ†’ (2 ยท (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹))) = ((2 ยท ((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2)))) + (2 ยท ((1 / 2) ยท ๐‘‹))))
264191, 222, 257subdid 11670 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ (2 ยท ((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2)))) = ((2 ยท (๐‘‹โ†‘3)) โˆ’ (2 ยท ((3 / 2) ยท (๐‘‹โ†‘2)))))
26587, 204recidi 11945 . . . . . . . . . 10 (2 ยท (1 / 2)) = 1
266265oveq1i 7419 . . . . . . . . 9 ((2 ยท (1 / 2)) ยท ๐‘‹) = (1 ยท ๐‘‹)
267191, 244, 242mulassd 11237 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ ((2 ยท (1 / 2)) ยท ๐‘‹) = (2 ยท ((1 / 2) ยท ๐‘‹)))
268 mullid 11213 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ (1 ยท ๐‘‹) = ๐‘‹)
269266, 267, 2683eqtr3a 2797 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ (2 ยท ((1 / 2) ยท ๐‘‹)) = ๐‘‹)
270264, 269oveq12d 7427 . . . . . . 7 (๐‘‹ โˆˆ โ„‚ โ†’ ((2 ยท ((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2)))) + (2 ยท ((1 / 2) ยท ๐‘‹))) = (((2 ยท (๐‘‹โ†‘3)) โˆ’ (2 ยท ((3 / 2) ยท (๐‘‹โ†‘2)))) + ๐‘‹))
271263, 270eqtrd 2773 . . . . . 6 (๐‘‹ โˆˆ โ„‚ โ†’ (2 ยท (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹))) = (((2 ยท (๐‘‹โ†‘3)) โˆ’ (2 ยท ((3 / 2) ยท (๐‘‹โ†‘2)))) + ๐‘‹))
272271oveq1d 7424 . . . . 5 (๐‘‹ โˆˆ โ„‚ โ†’ ((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))))))
273191, 257mulcld 11234 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ (2 ยท ((3 / 2) ยท (๐‘‹โ†‘2))) โˆˆ โ„‚)
274223, 273subcld 11571 . . . . . . 7 (๐‘‹ โˆˆ โ„‚ โ†’ ((2 ยท (๐‘‹โ†‘3)) โˆ’ (2 ยท ((3 / 2) ยท (๐‘‹โ†‘2)))) โˆˆ โ„‚)
275274, 242, 254addassd 11236 . . . . . 6 (๐‘‹ โˆˆ โ„‚ โ†’ ((((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)))))))
276242, 254addcld 11233 . . . . . . 7 (๐‘‹ โˆˆ โ„‚ โ†’ (๐‘‹ + (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6))))) โˆˆ โ„‚)
277223, 273, 276subsubd 11599 . . . . . 6 (๐‘‹ โˆˆ โ„‚ โ†’ ((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)))))))
278191, 256, 224mulassd 11237 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ ((2 ยท (3 / 2)) ยท (๐‘‹โ†‘2)) = (2 ยท ((3 / 2) ยท (๐‘‹โ†‘2))))
27958, 87, 204divcan2i 11957 . . . . . . . . . . 11 (2 ยท (3 / 2)) = 3
280279oveq1i 7419 . . . . . . . . . 10 ((2 ยท (3 / 2)) ยท (๐‘‹โ†‘2)) = (3 ยท (๐‘‹โ†‘2))
281278, 280eqtr3di 2788 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ (2 ยท ((3 / 2) ยท (๐‘‹โ†‘2))) = (3 ยท (๐‘‹โ†‘2)))
282281oveq1d 7424 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ ((2 ยท ((3 / 2) ยท (๐‘‹โ†‘2))) โˆ’ (๐‘‹ + (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))))) = ((3 ยท (๐‘‹โ†‘2)) โˆ’ (๐‘‹ + (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))))))
283242, 246, 253add12d 11440 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ (๐‘‹ + (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6))))) = (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (๐‘‹ + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6))))))
284191, 247, 251adddid 11238 . . . . . . . . . . . . . 14 (๐‘‹ โˆˆ โ„‚ โ†’ (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6))) = ((2 ยท ((๐‘‹โ†‘2) โˆ’ ๐‘‹)) + (2 ยท (1 / 6))))
285191, 224, 242subdid 11670 . . . . . . . . . . . . . . 15 (๐‘‹ โˆˆ โ„‚ โ†’ (2 ยท ((๐‘‹โ†‘2) โˆ’ ๐‘‹)) = ((2 ยท (๐‘‹โ†‘2)) โˆ’ (2 ยท ๐‘‹)))
286187oveq2i 7420 . . . . . . . . . . . . . . . . 17 (2 / (3 ยท 2)) = (2 / 6)
28758, 184reccli 11944 . . . . . . . . . . . . . . . . . . . 20 (1 / 3) โˆˆ โ„‚
28858, 87, 287mul32i 11410 . . . . . . . . . . . . . . . . . . 19 ((3 ยท 2) ยท (1 / 3)) = ((3 ยท (1 / 3)) ยท 2)
28958, 184recidi 11945 . . . . . . . . . . . . . . . . . . . . 21 (3 ยท (1 / 3)) = 1
290289oveq1i 7419 . . . . . . . . . . . . . . . . . . . 20 ((3 ยท (1 / 3)) ยท 2) = (1 ยท 2)
29187mullidi 11219 . . . . . . . . . . . . . . . . . . . 20 (1 ยท 2) = 2
292290, 291eqtri 2761 . . . . . . . . . . . . . . . . . . 19 ((3 ยท (1 / 3)) ยท 2) = 2
293288, 292eqtri 2761 . . . . . . . . . . . . . . . . . 18 ((3 ยท 2) ยท (1 / 3)) = 2
294187, 178eqeltri 2830 . . . . . . . . . . . . . . . . . . 19 (3 ยท 2) โˆˆ โ„‚
295187, 249eqnetri 3012 . . . . . . . . . . . . . . . . . . 19 (3 ยท 2) โ‰  0
29687, 294, 287, 295divmuli 11968 . . . . . . . . . . . . . . . . . 18 ((2 / (3 ยท 2)) = (1 / 3) โ†” ((3 ยท 2) ยท (1 / 3)) = 2)
297293, 296mpbir 230 . . . . . . . . . . . . . . . . 17 (2 / (3 ยท 2)) = (1 / 3)
29887, 178, 249divreci 11959 . . . . . . . . . . . . . . . . 17 (2 / 6) = (2 ยท (1 / 6))
299286, 297, 2983eqtr3ri 2770 . . . . . . . . . . . . . . . 16 (2 ยท (1 / 6)) = (1 / 3)
300299a1i 11 . . . . . . . . . . . . . . 15 (๐‘‹ โˆˆ โ„‚ โ†’ (2 ยท (1 / 6)) = (1 / 3))
301285, 300oveq12d 7427 . . . . . . . . . . . . . 14 (๐‘‹ โˆˆ โ„‚ โ†’ ((2 ยท ((๐‘‹โ†‘2) โˆ’ ๐‘‹)) + (2 ยท (1 / 6))) = (((2 ยท (๐‘‹โ†‘2)) โˆ’ (2 ยท ๐‘‹)) + (1 / 3)))
302284, 301eqtrd 2773 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6))) = (((2 ยท (๐‘‹โ†‘2)) โˆ’ (2 ยท ๐‘‹)) + (1 / 3)))
303302oveq2d 7425 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ (๐‘‹ + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))) = (๐‘‹ + (((2 ยท (๐‘‹โ†‘2)) โˆ’ (2 ยท ๐‘‹)) + (1 / 3))))
304191, 224mulcld 11234 . . . . . . . . . . . . . 14 (๐‘‹ โˆˆ โ„‚ โ†’ (2 ยท (๐‘‹โ†‘2)) โˆˆ โ„‚)
305191, 242mulcld 11234 . . . . . . . . . . . . . 14 (๐‘‹ โˆˆ โ„‚ โ†’ (2 ยท ๐‘‹) โˆˆ โ„‚)
306304, 305subcld 11571 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ ((2 ยท (๐‘‹โ†‘2)) โˆ’ (2 ยท ๐‘‹)) โˆˆ โ„‚)
307287a1i 11 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ (1 / 3) โˆˆ โ„‚)
308242, 306, 307addassd 11236 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ((๐‘‹ + ((2 ยท (๐‘‹โ†‘2)) โˆ’ (2 ยท ๐‘‹))) + (1 / 3)) = (๐‘‹ + (((2 ยท (๐‘‹โ†‘2)) โˆ’ (2 ยท ๐‘‹)) + (1 / 3))))
309242, 304, 305addsub12d 11594 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ (๐‘‹ + ((2 ยท (๐‘‹โ†‘2)) โˆ’ (2 ยท ๐‘‹))) = ((2 ยท (๐‘‹โ†‘2)) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))))
310309oveq1d 7424 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ((๐‘‹ + ((2 ยท (๐‘‹โ†‘2)) โˆ’ (2 ยท ๐‘‹))) + (1 / 3)) = (((2 ยท (๐‘‹โ†‘2)) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + (1 / 3)))
311303, 308, 3103eqtr2d 2779 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ (๐‘‹ + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))) = (((2 ยท (๐‘‹โ†‘2)) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + (1 / 3)))
312311oveq2d 7425 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (๐‘‹ + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6))))) = (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (((2 ยท (๐‘‹โ†‘2)) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + (1 / 3))))
313283, 312eqtrd 2773 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ (๐‘‹ + (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6))))) = (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (((2 ยท (๐‘‹โ†‘2)) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + (1 / 3))))
314313oveq2d 7425 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ ((3 ยท (๐‘‹โ†‘2)) โˆ’ (๐‘‹ + (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))))) = ((3 ยท (๐‘‹โ†‘2)) โˆ’ (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (((2 ยท (๐‘‹โ†‘2)) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + (1 / 3)))))
315242, 305subcld 11571 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ (๐‘‹ โˆ’ (2 ยท ๐‘‹)) โˆˆ โ„‚)
316304, 315addcld 11233 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ((2 ยท (๐‘‹โ†‘2)) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) โˆˆ โ„‚)
317241, 245, 316, 307add4d 11442 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (((2 ยท (๐‘‹โ†‘2)) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + (1 / 3))) = (((1 / 5) + ((2 ยท (๐‘‹โ†‘2)) + (๐‘‹ โˆ’ (2 ยท ๐‘‹)))) + ((๐‘‹ โˆ’ (1 / 2)) + (1 / 3))))
318241, 304, 315add12d 11440 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ((1 / 5) + ((2 ยท (๐‘‹โ†‘2)) + (๐‘‹ โˆ’ (2 ยท ๐‘‹)))) = ((2 ยท (๐‘‹โ†‘2)) + ((1 / 5) + (๐‘‹ โˆ’ (2 ยท ๐‘‹)))))
319318oveq1d 7424 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ (((1 / 5) + ((2 ยท (๐‘‹โ†‘2)) + (๐‘‹ โˆ’ (2 ยท ๐‘‹)))) + ((๐‘‹ โˆ’ (1 / 2)) + (1 / 3))) = (((2 ยท (๐‘‹โ†‘2)) + ((1 / 5) + (๐‘‹ โˆ’ (2 ยท ๐‘‹)))) + ((๐‘‹ โˆ’ (1 / 2)) + (1 / 3))))
320241, 315addcld 11233 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ((1 / 5) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) โˆˆ โ„‚)
321245, 307addcld 11233 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ((๐‘‹ โˆ’ (1 / 2)) + (1 / 3)) โˆˆ โ„‚)
322304, 320, 321addassd 11236 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ (((2 ยท (๐‘‹โ†‘2)) + ((1 / 5) + (๐‘‹ โˆ’ (2 ยท ๐‘‹)))) + ((๐‘‹ โˆ’ (1 / 2)) + (1 / 3))) = ((2 ยท (๐‘‹โ†‘2)) + (((1 / 5) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + ((๐‘‹ โˆ’ (1 / 2)) + (1 / 3)))))
323317, 319, 3223eqtrd 2777 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (((2 ยท (๐‘‹โ†‘2)) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + (1 / 3))) = ((2 ยท (๐‘‹โ†‘2)) + (((1 / 5) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + ((๐‘‹ โˆ’ (1 / 2)) + (1 / 3)))))
324323oveq2d 7425 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ ((3 ยท (๐‘‹โ†‘2)) โˆ’ (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (((2 ยท (๐‘‹โ†‘2)) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + (1 / 3)))) = ((3 ยท (๐‘‹โ†‘2)) โˆ’ ((2 ยท (๐‘‹โ†‘2)) + (((1 / 5) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + ((๐‘‹ โˆ’ (1 / 2)) + (1 / 3))))))
325183, 224mulcld 11234 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ (3 ยท (๐‘‹โ†‘2)) โˆˆ โ„‚)
326320, 321addcld 11233 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ (((1 / 5) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + ((๐‘‹ โˆ’ (1 / 2)) + (1 / 3))) โˆˆ โ„‚)
327325, 304, 326subsub4d 11602 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ (((3 ยท (๐‘‹โ†‘2)) โˆ’ (2 ยท (๐‘‹โ†‘2))) โˆ’ (((1 / 5) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + ((๐‘‹ โˆ’ (1 / 2)) + (1 / 3)))) = ((3 ยท (๐‘‹โ†‘2)) โˆ’ ((2 ยท (๐‘‹โ†‘2)) + (((1 / 5) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + ((๐‘‹ โˆ’ (1 / 2)) + (1 / 3))))))
32858, 87, 59, 109subaddrii 11549 . . . . . . . . . . . 12 (3 โˆ’ 2) = 1
329328oveq1i 7419 . . . . . . . . . . 11 ((3 โˆ’ 2) ยท (๐‘‹โ†‘2)) = (1 ยท (๐‘‹โ†‘2))
330183, 191, 224subdird 11671 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ ((3 โˆ’ 2) ยท (๐‘‹โ†‘2)) = ((3 ยท (๐‘‹โ†‘2)) โˆ’ (2 ยท (๐‘‹โ†‘2))))
331224mullidd 11232 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ (1 ยท (๐‘‹โ†‘2)) = (๐‘‹โ†‘2))
332329, 330, 3313eqtr3a 2797 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ ((3 ยท (๐‘‹โ†‘2)) โˆ’ (2 ยท (๐‘‹โ†‘2))) = (๐‘‹โ†‘2))
333241, 305, 242subsubd 11599 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ ((1 / 5) โˆ’ ((2 ยท ๐‘‹) โˆ’ ๐‘‹)) = (((1 / 5) โˆ’ (2 ยท ๐‘‹)) + ๐‘‹))
334 2txmxeqx 12352 . . . . . . . . . . . . . 14 (๐‘‹ โˆˆ โ„‚ โ†’ ((2 ยท ๐‘‹) โˆ’ ๐‘‹) = ๐‘‹)
335334oveq2d 7425 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ ((1 / 5) โˆ’ ((2 ยท ๐‘‹) โˆ’ ๐‘‹)) = ((1 / 5) โˆ’ ๐‘‹))
336241, 305, 242subadd23d 11593 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ (((1 / 5) โˆ’ (2 ยท ๐‘‹)) + ๐‘‹) = ((1 / 5) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))))
337333, 335, 3363eqtr3d 2781 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ ((1 / 5) โˆ’ ๐‘‹) = ((1 / 5) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))))
338242, 244, 307subsubd 11599 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ (๐‘‹ โˆ’ ((1 / 2) โˆ’ (1 / 3))) = ((๐‘‹ โˆ’ (1 / 2)) + (1 / 3)))
339337, 338oveq12d 7427 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ (((1 / 5) โˆ’ ๐‘‹) + (๐‘‹ โˆ’ ((1 / 2) โˆ’ (1 / 3)))) = (((1 / 5) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + ((๐‘‹ โˆ’ (1 / 2)) + (1 / 3))))
340243, 287subcli 11536 . . . . . . . . . . . . . 14 ((1 / 2) โˆ’ (1 / 3)) โˆˆ โ„‚
341340a1i 11 . . . . . . . . . . . . 13 (๐‘‹ โˆˆ โ„‚ โ†’ ((1 / 2) โˆ’ (1 / 3)) โˆˆ โ„‚)
342241, 242, 341npncand 11595 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„‚ โ†’ (((1 / 5) โˆ’ ๐‘‹) + (๐‘‹ โˆ’ ((1 / 2) โˆ’ (1 / 3)))) = ((1 / 5) โˆ’ ((1 / 2) โˆ’ (1 / 3))))
343 halfthird 12820 . . . . . . . . . . . . . 14 ((1 / 2) โˆ’ (1 / 3)) = (1 / 6)
344343oveq2i 7420 . . . . . . . . . . . . 13 ((1 / 5) โˆ’ ((1 / 2) โˆ’ (1 / 3))) = ((1 / 5) โˆ’ (1 / 6))
345 5recm6rec 12821 . . . . . . . . . . . . 13 ((1 / 5) โˆ’ (1 / 6)) = (1 / 30)
346344, 345eqtri 2761 . . . . . . . . . . . 12 ((1 / 5) โˆ’ ((1 / 2) โˆ’ (1 / 3))) = (1 / 30)
347342, 346eqtrdi 2789 . . . . . . . . . . 11 (๐‘‹ โˆˆ โ„‚ โ†’ (((1 / 5) โˆ’ ๐‘‹) + (๐‘‹ โˆ’ ((1 / 2) โˆ’ (1 / 3)))) = (1 / 30))
348339, 347eqtr3d 2775 . . . . . . . . . 10 (๐‘‹ โˆˆ โ„‚ โ†’ (((1 / 5) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + ((๐‘‹ โˆ’ (1 / 2)) + (1 / 3))) = (1 / 30))
349332, 348oveq12d 7427 . . . . . . . . 9 (๐‘‹ โˆˆ โ„‚ โ†’ (((3 ยท (๐‘‹โ†‘2)) โˆ’ (2 ยท (๐‘‹โ†‘2))) โˆ’ (((1 / 5) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + ((๐‘‹ โˆ’ (1 / 2)) + (1 / 3)))) = ((๐‘‹โ†‘2) โˆ’ (1 / 30)))
350324, 327, 3493eqtr2d 2779 . . . . . . . 8 (๐‘‹ โˆˆ โ„‚ โ†’ ((3 ยท (๐‘‹โ†‘2)) โˆ’ (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (((2 ยท (๐‘‹โ†‘2)) + (๐‘‹ โˆ’ (2 ยท ๐‘‹))) + (1 / 3)))) = ((๐‘‹โ†‘2) โˆ’ (1 / 30)))
351282, 314, 3503eqtrd 2777 . . . . . . 7 (๐‘‹ โˆˆ โ„‚ โ†’ ((2 ยท ((3 / 2) ยท (๐‘‹โ†‘2))) โˆ’ (๐‘‹ + (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))))) = ((๐‘‹โ†‘2) โˆ’ (1 / 30)))
352351oveq2d 7425 . . . . . 6 (๐‘‹ โˆˆ โ„‚ โ†’ ((2 ยท (๐‘‹โ†‘3)) โˆ’ ((2 ยท ((3 / 2) ยท (๐‘‹โ†‘2))) โˆ’ (๐‘‹ + (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6))))))) = ((2 ยท (๐‘‹โ†‘3)) โˆ’ ((๐‘‹โ†‘2) โˆ’ (1 / 30))))
353275, 277, 3523eqtr2d 2779 . . . . 5 (๐‘‹ โˆˆ โ„‚ โ†’ ((((2 ยท (๐‘‹โ†‘3)) โˆ’ (2 ยท ((3 / 2) ยท (๐‘‹โ†‘2)))) + ๐‘‹) + (((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6))))) = ((2 ยท (๐‘‹โ†‘3)) โˆ’ ((๐‘‹โ†‘2) โˆ’ (1 / 30))))
354262, 272, 3533eqtrd 2777 . . . 4 (๐‘‹ โˆˆ โ„‚ โ†’ ((((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))) + (2 ยท (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹)))) = ((2 ยท (๐‘‹โ†‘3)) โˆ’ ((๐‘‹โ†‘2) โˆ’ (1 / 30))))
355354oveq2d 7425 . . 3 (๐‘‹ โˆˆ โ„‚ โ†’ ((๐‘‹โ†‘4) โˆ’ ((((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))) + (2 ยท (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹))))) = ((๐‘‹โ†‘4) โˆ’ ((2 ยท (๐‘‹โ†‘3)) โˆ’ ((๐‘‹โ†‘2) โˆ’ (1 / 30)))))
356220, 223subcld 11571 . . . 4 (๐‘‹ โˆˆ โ„‚ โ†’ ((๐‘‹โ†‘4) โˆ’ (2 ยท (๐‘‹โ†‘3))) โˆˆ โ„‚)
357356, 224, 238addsubassd 11591 . . 3 (๐‘‹ โˆˆ โ„‚ โ†’ ((((๐‘‹โ†‘4) โˆ’ (2 ยท (๐‘‹โ†‘3))) + (๐‘‹โ†‘2)) โˆ’ (1 / 30)) = (((๐‘‹โ†‘4) โˆ’ (2 ยท (๐‘‹โ†‘3))) + ((๐‘‹โ†‘2) โˆ’ (1 / 30))))
358240, 355, 3573eqtr4d 2783 . 2 (๐‘‹ โˆˆ โ„‚ โ†’ ((๐‘‹โ†‘4) โˆ’ ((((1 / 5) + (๐‘‹ โˆ’ (1 / 2))) + (2 ยท (((๐‘‹โ†‘2) โˆ’ ๐‘‹) + (1 / 6)))) + (2 ยท (((๐‘‹โ†‘3) โˆ’ ((3 / 2) ยท (๐‘‹โ†‘2))) + ((1 / 2) ยท ๐‘‹))))) = ((((๐‘‹โ†‘4) โˆ’ (2 ยท (๐‘‹โ†‘3))) + (๐‘‹โ†‘2)) โˆ’ (1 / 30)))
3593, 218, 3583eqtrd 2777 1 (๐‘‹ โˆˆ โ„‚ โ†’ (4 BernPoly ๐‘‹) = ((((๐‘‹โ†‘4) โˆ’ (2 ยท (๐‘‹โ†‘3))) + (๐‘‹โ†‘2)) โˆ’ (1 / 30)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2941   โŠ† wss 3949   class class class wbr 5149  โ€˜cfv 6544  (class class class)co 7409  โ„‚cc 11108  โ„cr 11109  0cc0 11110  1c1 11111   + caddc 11113   ยท cmul 11115   < clt 11248   โˆ’ cmin 11444   / cdiv 11871  โ„•cn 12212  2c2 12267  3c3 12268  4c4 12269  5c5 12270  6c6 12271  โ„•0cn0 12472  โ„คcz 12558  cdc 12677  โ„คโ‰ฅ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-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-z 12559  df-dec 12678  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:  fsumcube  16004
  Copyright terms: Public domain W3C validator