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

Theorem bpoly3 15411
 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 11914 . . 3 3 ∈ ℕ0
2 bpolyval 15402 . . 3 ((3 ∈ ℕ0𝑋 ∈ ℂ) → (3 BernPoly 𝑋) = ((𝑋↑3) − Σ𝑘 ∈ (0...(3 − 1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1)))))
31, 2mpan 688 . 2 (𝑋 ∈ ℂ → (3 BernPoly 𝑋) = ((𝑋↑3) − Σ𝑘 ∈ (0...(3 − 1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1)))))
4 3m1e2 11764 . . . . . . 7 (3 − 1) = 2
5 df-2 11699 . . . . . . 7 2 = (1 + 1)
64, 5eqtri 2844 . . . . . 6 (3 − 1) = (1 + 1)
76oveq2i 7166 . . . . 5 (0...(3 − 1)) = (0...(1 + 1))
87sumeq1i 15054 . . . 4 Σ𝑘 ∈ (0...(3 − 1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(1 + 1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1)))
9 1eluzge0 12291 . . . . . . 7 1 ∈ (ℤ‘0)
109a1i 11 . . . . . 6 (𝑋 ∈ ℂ → 1 ∈ (ℤ‘0))
11 0z 11991 . . . . . . . . . . . . 13 0 ∈ ℤ
12 fzpr 12961 . . . . . . . . . . . . 13 (0 ∈ ℤ → (0...(0 + 1)) = {0, (0 + 1)})
1311, 12ax-mp 5 . . . . . . . . . . . 12 (0...(0 + 1)) = {0, (0 + 1)}
14 0p1e1 11758 . . . . . . . . . . . . 13 (0 + 1) = 1
1514oveq2i 7166 . . . . . . . . . . . 12 (0...(0 + 1)) = (0...1)
1614preq2i 4672 . . . . . . . . . . . 12 {0, (0 + 1)} = {0, 1}
1713, 15, 163eqtr3ri 2853 . . . . . . . . . . 11 {0, 1} = (0...1)
185sneqi 4577 . . . . . . . . . . 11 {2} = {(1 + 1)}
1917, 18uneq12i 4136 . . . . . . . . . 10 ({0, 1} ∪ {2}) = ((0...1) ∪ {(1 + 1)})
20 df-tp 4571 . . . . . . . . . 10 {0, 1, 2} = ({0, 1} ∪ {2})
21 fzsuc 12953 . . . . . . . . . . 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 2855 . . . . . . . . 9 (0...(1 + 1)) = {0, 1, 2}
2423eleq2i 2904 . . . . . . . 8 (𝑘 ∈ (0...(1 + 1)) ↔ 𝑘 ∈ {0, 1, 2})
25 vex 3497 . . . . . . . . 9 𝑘 ∈ V
2625eltp 4625 . . . . . . . 8 (𝑘 ∈ {0, 1, 2} ↔ (𝑘 = 0 ∨ 𝑘 = 1 ∨ 𝑘 = 2))
2724, 26bitri 277 . . . . . . 7 (𝑘 ∈ (0...(1 + 1)) ↔ (𝑘 = 0 ∨ 𝑘 = 1 ∨ 𝑘 = 2))
28 oveq2 7163 . . . . . . . . . . . 12 (𝑘 = 0 → (3C𝑘) = (3C0))
29 bcn0 13669 . . . . . . . . . . . . 13 (3 ∈ ℕ0 → (3C0) = 1)
301, 29ax-mp 5 . . . . . . . . . . . 12 (3C0) = 1
3128, 30syl6eq 2872 . . . . . . . . . . 11 (𝑘 = 0 → (3C𝑘) = 1)
32 oveq1 7162 . . . . . . . . . . . 12 (𝑘 = 0 → (𝑘 BernPoly 𝑋) = (0 BernPoly 𝑋))
33 oveq2 7163 . . . . . . . . . . . . . 14 (𝑘 = 0 → (3 − 𝑘) = (3 − 0))
3433oveq1d 7170 . . . . . . . . . . . . 13 (𝑘 = 0 → ((3 − 𝑘) + 1) = ((3 − 0) + 1))
35 3cn 11717 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
3635subid1i 10957 . . . . . . . . . . . . . . 15 (3 − 0) = 3
3736oveq1i 7165 . . . . . . . . . . . . . 14 ((3 − 0) + 1) = (3 + 1)
38 df-4 11701 . . . . . . . . . . . . . 14 4 = (3 + 1)
3937, 38eqtr4i 2847 . . . . . . . . . . . . 13 ((3 − 0) + 1) = 4
4034, 39syl6eq 2872 . . . . . . . . . . . 12 (𝑘 = 0 → ((3 − 𝑘) + 1) = 4)
4132, 40oveq12d 7173 . . . . . . . . . . 11 (𝑘 = 0 → ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1)) = ((0 BernPoly 𝑋) / 4))
4231, 41oveq12d 7173 . . . . . . . . . 10 (𝑘 = 0 → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 4)))
43 bpoly0 15403 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (0 BernPoly 𝑋) = 1)
4443oveq1d 7170 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((0 BernPoly 𝑋) / 4) = (1 / 4))
4544oveq2d 7171 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (1 · ((0 BernPoly 𝑋) / 4)) = (1 · (1 / 4)))
46 4cn 11721 . . . . . . . . . . . . 13 4 ∈ ℂ
47 4ne0 11744 . . . . . . . . . . . . 13 4 ≠ 0
4846, 47reccli 11369 . . . . . . . . . . . 12 (1 / 4) ∈ ℂ
4948mulid2i 10645 . . . . . . . . . . 11 (1 · (1 / 4)) = (1 / 4)
5045, 49syl6eq 2872 . . . . . . . . . 10 (𝑋 ∈ ℂ → (1 · ((0 BernPoly 𝑋) / 4)) = (1 / 4))
5142, 50sylan9eqr 2878 . . . . . . . . 9 ((𝑋 ∈ ℂ ∧ 𝑘 = 0) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (1 / 4))
5251, 48eqeltrdi 2921 . . . . . . . 8 ((𝑋 ∈ ℂ ∧ 𝑘 = 0) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ)
53 oveq2 7163 . . . . . . . . . . . 12 (𝑘 = 1 → (3C𝑘) = (3C1))
54 bcn1 13672 . . . . . . . . . . . . 13 (3 ∈ ℕ0 → (3C1) = 3)
551, 54ax-mp 5 . . . . . . . . . . . 12 (3C1) = 3
5653, 55syl6eq 2872 . . . . . . . . . . 11 (𝑘 = 1 → (3C𝑘) = 3)
57 oveq1 7162 . . . . . . . . . . . 12 (𝑘 = 1 → (𝑘 BernPoly 𝑋) = (1 BernPoly 𝑋))
58 oveq2 7163 . . . . . . . . . . . . . 14 (𝑘 = 1 → (3 − 𝑘) = (3 − 1))
5958oveq1d 7170 . . . . . . . . . . . . 13 (𝑘 = 1 → ((3 − 𝑘) + 1) = ((3 − 1) + 1))
60 ax-1cn 10594 . . . . . . . . . . . . . 14 1 ∈ ℂ
61 npcan 10894 . . . . . . . . . . . . . 14 ((3 ∈ ℂ ∧ 1 ∈ ℂ) → ((3 − 1) + 1) = 3)
6235, 60, 61mp2an 690 . . . . . . . . . . . . 13 ((3 − 1) + 1) = 3
6359, 62syl6eq 2872 . . . . . . . . . . . 12 (𝑘 = 1 → ((3 − 𝑘) + 1) = 3)
6457, 63oveq12d 7173 . . . . . . . . . . 11 (𝑘 = 1 → ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1)) = ((1 BernPoly 𝑋) / 3))
6556, 64oveq12d 7173 . . . . . . . . . 10 (𝑘 = 1 → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (3 · ((1 BernPoly 𝑋) / 3)))
66 bpoly1 15404 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (1 BernPoly 𝑋) = (𝑋 − (1 / 2)))
6766oveq1d 7170 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((1 BernPoly 𝑋) / 3) = ((𝑋 − (1 / 2)) / 3))
6867oveq2d 7171 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (3 · ((1 BernPoly 𝑋) / 3)) = (3 · ((𝑋 − (1 / 2)) / 3)))
69 halfcn 11851 . . . . . . . . . . . . 13 (1 / 2) ∈ ℂ
70 subcl 10884 . . . . . . . . . . . . 13 ((𝑋 ∈ ℂ ∧ (1 / 2) ∈ ℂ) → (𝑋 − (1 / 2)) ∈ ℂ)
7169, 70mpan2 689 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (𝑋 − (1 / 2)) ∈ ℂ)
72 3ne0 11742 . . . . . . . . . . . . 13 3 ≠ 0
73 divcan2 11305 . . . . . . . . . . . . 13 (((𝑋 − (1 / 2)) ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0) → (3 · ((𝑋 − (1 / 2)) / 3)) = (𝑋 − (1 / 2)))
7435, 72, 73mp3an23 1449 . . . . . . . . . . . 12 ((𝑋 − (1 / 2)) ∈ ℂ → (3 · ((𝑋 − (1 / 2)) / 3)) = (𝑋 − (1 / 2)))
7571, 74syl 17 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (3 · ((𝑋 − (1 / 2)) / 3)) = (𝑋 − (1 / 2)))
7668, 75eqtrd 2856 . . . . . . . . . 10 (𝑋 ∈ ℂ → (3 · ((1 BernPoly 𝑋) / 3)) = (𝑋 − (1 / 2)))
7765, 76sylan9eqr 2878 . . . . . . . . 9 ((𝑋 ∈ ℂ ∧ 𝑘 = 1) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (𝑋 − (1 / 2)))
7871adantr 483 . . . . . . . . 9 ((𝑋 ∈ ℂ ∧ 𝑘 = 1) → (𝑋 − (1 / 2)) ∈ ℂ)
7977, 78eqeltrd 2913 . . . . . . . 8 ((𝑋 ∈ ℂ ∧ 𝑘 = 1) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ)
80 oveq2 7163 . . . . . . . . . . . 12 (𝑘 = 2 → (3C𝑘) = (3C2))
81 bcn2 13678 . . . . . . . . . . . . . 14 (3 ∈ ℕ0 → (3C2) = ((3 · (3 − 1)) / 2))
821, 81ax-mp 5 . . . . . . . . . . . . 13 (3C2) = ((3 · (3 − 1)) / 2)
834oveq2i 7166 . . . . . . . . . . . . . . 15 (3 · (3 − 1)) = (3 · 2)
8483oveq1i 7165 . . . . . . . . . . . . . 14 ((3 · (3 − 1)) / 2) = ((3 · 2) / 2)
85 2cn 11711 . . . . . . . . . . . . . . 15 2 ∈ ℂ
86 2ne0 11740 . . . . . . . . . . . . . . 15 2 ≠ 0
8735, 85, 86divcan4i 11386 . . . . . . . . . . . . . 14 ((3 · 2) / 2) = 3
8884, 87eqtri 2844 . . . . . . . . . . . . 13 ((3 · (3 − 1)) / 2) = 3
8982, 88eqtri 2844 . . . . . . . . . . . 12 (3C2) = 3
9080, 89syl6eq 2872 . . . . . . . . . . 11 (𝑘 = 2 → (3C𝑘) = 3)
91 oveq1 7162 . . . . . . . . . . . 12 (𝑘 = 2 → (𝑘 BernPoly 𝑋) = (2 BernPoly 𝑋))
92 oveq2 7163 . . . . . . . . . . . . . 14 (𝑘 = 2 → (3 − 𝑘) = (3 − 2))
9392oveq1d 7170 . . . . . . . . . . . . 13 (𝑘 = 2 → ((3 − 𝑘) + 1) = ((3 − 2) + 1))
94 2p1e3 11778 . . . . . . . . . . . . . . . 16 (2 + 1) = 3
9535, 85, 60, 94subaddrii 10974 . . . . . . . . . . . . . . 15 (3 − 2) = 1
9695oveq1i 7165 . . . . . . . . . . . . . 14 ((3 − 2) + 1) = (1 + 1)
9796, 5eqtr4i 2847 . . . . . . . . . . . . 13 ((3 − 2) + 1) = 2
9893, 97syl6eq 2872 . . . . . . . . . . . 12 (𝑘 = 2 → ((3 − 𝑘) + 1) = 2)
9991, 98oveq12d 7173 . . . . . . . . . . 11 (𝑘 = 2 → ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1)) = ((2 BernPoly 𝑋) / 2))
10090, 99oveq12d 7173 . . . . . . . . . 10 (𝑘 = 2 → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (3 · ((2 BernPoly 𝑋) / 2)))
101 2nn0 11913 . . . . . . . . . . . . 13 2 ∈ ℕ0
102 bpolycl 15405 . . . . . . . . . . . . 13 ((2 ∈ ℕ0𝑋 ∈ ℂ) → (2 BernPoly 𝑋) ∈ ℂ)
103101, 102mpan 688 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (2 BernPoly 𝑋) ∈ ℂ)
104 2cnne0 11846 . . . . . . . . . . . . 13 (2 ∈ ℂ ∧ 2 ≠ 0)
105 div12 11319 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ (2 BernPoly 𝑋) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (3 · ((2 BernPoly 𝑋) / 2)) = ((2 BernPoly 𝑋) · (3 / 2)))
10635, 104, 105mp3an13 1448 . . . . . . . . . . . 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 11381 . . . . . . . . . . . 12 (3 / 2) ∈ ℂ
109 mulcom 10622 . . . . . . . . . . . 12 (((2 BernPoly 𝑋) ∈ ℂ ∧ (3 / 2) ∈ ℂ) → ((2 BernPoly 𝑋) · (3 / 2)) = ((3 / 2) · (2 BernPoly 𝑋)))
110103, 108, 109sylancl 588 . . . . . . . . . . 11 (𝑋 ∈ ℂ → ((2 BernPoly 𝑋) · (3 / 2)) = ((3 / 2) · (2 BernPoly 𝑋)))
111 bpoly2 15410 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (2 BernPoly 𝑋) = (((𝑋↑2) − 𝑋) + (1 / 6)))
112111oveq2d 7171 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((3 / 2) · (2 BernPoly 𝑋)) = ((3 / 2) · (((𝑋↑2) − 𝑋) + (1 / 6))))
113 sqcl 13483 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (𝑋↑2) ∈ ℂ)
114 6cn 11727 . . . . . . . . . . . . . . . 16 6 ∈ ℂ
115 6re 11726 . . . . . . . . . . . . . . . . 17 6 ∈ ℝ
116 6pos 11746 . . . . . . . . . . . . . . . . 17 0 < 6
117115, 116gt0ne0ii 11175 . . . . . . . . . . . . . . . 16 6 ≠ 0
118114, 117reccli 11369 . . . . . . . . . . . . . . 15 (1 / 6) ∈ ℂ
119 subsub 10915 . . . . . . . . . . . . . . 15 (((𝑋↑2) ∈ ℂ ∧ 𝑋 ∈ ℂ ∧ (1 / 6) ∈ ℂ) → ((𝑋↑2) − (𝑋 − (1 / 6))) = (((𝑋↑2) − 𝑋) + (1 / 6)))
120118, 119mp3an3 1446 . . . . . . . . . . . . . 14 (((𝑋↑2) ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((𝑋↑2) − (𝑋 − (1 / 6))) = (((𝑋↑2) − 𝑋) + (1 / 6)))
121113, 120mpancom 686 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → ((𝑋↑2) − (𝑋 − (1 / 6))) = (((𝑋↑2) − 𝑋) + (1 / 6)))
122121oveq2d 7171 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((3 / 2) · ((𝑋↑2) − (𝑋 − (1 / 6)))) = ((3 / 2) · (((𝑋↑2) − 𝑋) + (1 / 6))))
123 subcl 10884 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℂ ∧ (1 / 6) ∈ ℂ) → (𝑋 − (1 / 6)) ∈ ℂ)
124118, 123mpan2 689 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (𝑋 − (1 / 6)) ∈ ℂ)
125 subdi 11072 . . . . . . . . . . . . 13 (((3 / 2) ∈ ℂ ∧ (𝑋↑2) ∈ ℂ ∧ (𝑋 − (1 / 6)) ∈ ℂ) → ((3 / 2) · ((𝑋↑2) − (𝑋 − (1 / 6)))) = (((3 / 2) · (𝑋↑2)) − ((3 / 2) · (𝑋 − (1 / 6)))))
126108, 113, 124, 125mp3an2i 1462 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((3 / 2) · ((𝑋↑2) − (𝑋 − (1 / 6)))) = (((3 / 2) · (𝑋↑2)) − ((3 / 2) · (𝑋 − (1 / 6)))))
127112, 122, 1263eqtr2d 2862 . . . . . . . . . . 11 (𝑋 ∈ ℂ → ((3 / 2) · (2 BernPoly 𝑋)) = (((3 / 2) · (𝑋↑2)) − ((3 / 2) · (𝑋 − (1 / 6)))))
128107, 110, 1273eqtrd 2860 . . . . . . . . . 10 (𝑋 ∈ ℂ → (3 · ((2 BernPoly 𝑋) / 2)) = (((3 / 2) · (𝑋↑2)) − ((3 / 2) · (𝑋 − (1 / 6)))))
129100, 128sylan9eqr 2878 . . . . . . . . 9 ((𝑋 ∈ ℂ ∧ 𝑘 = 2) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (((3 / 2) · (𝑋↑2)) − ((3 / 2) · (𝑋 − (1 / 6)))))
130 mulcl 10620 . . . . . . . . . . . 12 (((3 / 2) ∈ ℂ ∧ (𝑋↑2) ∈ ℂ) → ((3 / 2) · (𝑋↑2)) ∈ ℂ)
131108, 113, 130sylancr 589 . . . . . . . . . . 11 (𝑋 ∈ ℂ → ((3 / 2) · (𝑋↑2)) ∈ ℂ)
132 mulcl 10620 . . . . . . . . . . . 12 (((3 / 2) ∈ ℂ ∧ (𝑋 − (1 / 6)) ∈ ℂ) → ((3 / 2) · (𝑋 − (1 / 6))) ∈ ℂ)
133108, 124, 132sylancr 589 . . . . . . . . . . 11 (𝑋 ∈ ℂ → ((3 / 2) · (𝑋 − (1 / 6))) ∈ ℂ)
134131, 133subcld 10996 . . . . . . . . . 10 (𝑋 ∈ ℂ → (((3 / 2) · (𝑋↑2)) − ((3 / 2) · (𝑋 − (1 / 6)))) ∈ ℂ)
135134adantr 483 . . . . . . . . 9 ((𝑋 ∈ ℂ ∧ 𝑘 = 2) → (((3 / 2) · (𝑋↑2)) − ((3 / 2) · (𝑋 − (1 / 6)))) ∈ ℂ)
136129, 135eqeltrd 2913 . . . . . . . 8 ((𝑋 ∈ ℂ ∧ 𝑘 = 2) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ)
13752, 79, 1363jaodan 1426 . . . . . . 7 ((𝑋 ∈ ℂ ∧ (𝑘 = 0 ∨ 𝑘 = 1 ∨ 𝑘 = 2)) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ)
13827, 137sylan2b 595 . . . . . 6 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(1 + 1))) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ)
1395eqeq2i 2834 . . . . . . 7 (𝑘 = 2 ↔ 𝑘 = (1 + 1))
140139, 100sylbir 237 . . . . . 6 (𝑘 = (1 + 1) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (3 · ((2 BernPoly 𝑋) / 2)))
14110, 138, 140fsump1 15110 . . . . 5 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(1 + 1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...1)((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (3 · ((2 BernPoly 𝑋) / 2))))
142128oveq2d 7171 . . . . 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 15054 . . . . . . . . 9 Σ𝑘 ∈ (0...(0 + 1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = Σ𝑘 ∈ (0...1)((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1)))
144 0nn0 11911 . . . . . . . . . . . . 13 0 ∈ ℕ0
145 nn0uz 12279 . . . . . . . . . . . . 13 0 = (ℤ‘0)
146144, 145eleqtri 2911 . . . . . . . . . . . 12 0 ∈ (ℤ‘0)
147146a1i 11 . . . . . . . . . . 11 (𝑋 ∈ ℂ → 0 ∈ (ℤ‘0))
14813, 16eqtri 2844 . . . . . . . . . . . . . 14 (0...(0 + 1)) = {0, 1}
149148eleq2i 2904 . . . . . . . . . . . . 13 (𝑘 ∈ (0...(0 + 1)) ↔ 𝑘 ∈ {0, 1})
15025elpr 4589 . . . . . . . . . . . . 13 (𝑘 ∈ {0, 1} ↔ (𝑘 = 0 ∨ 𝑘 = 1))
151149, 150bitri 277 . . . . . . . . . . . 12 (𝑘 ∈ (0...(0 + 1)) ↔ (𝑘 = 0 ∨ 𝑘 = 1))
15252, 79jaodan 954 . . . . . . . . . . . 12 ((𝑋 ∈ ℂ ∧ (𝑘 = 0 ∨ 𝑘 = 1)) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ)
153151, 152sylan2b 595 . . . . . . . . . . 11 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(0 + 1))) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ)
15414eqeq2i 2834 . . . . . . . . . . . 12 (𝑘 = (0 + 1) ↔ 𝑘 = 1)
155154, 65sylbi 219 . . . . . . . . . . 11 (𝑘 = (0 + 1) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (3 · ((1 BernPoly 𝑋) / 3)))
156147, 153, 155fsump1 15110 . . . . . . . . . 10 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(0 + 1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...0)((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (3 · ((1 BernPoly 𝑋) / 3))))
15750, 48eqeltrdi 2921 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (1 · ((0 BernPoly 𝑋) / 4)) ∈ ℂ)
15842fsum1 15101 . . . . . . . . . . . . 13 ((0 ∈ ℤ ∧ (1 · ((0 BernPoly 𝑋) / 4)) ∈ ℂ) → Σ𝑘 ∈ (0...0)((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 4)))
15911, 157, 158sylancr 589 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...0)((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 4)))
160159, 50eqtrd 2856 . . . . . . . . . . 11 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...0)((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (1 / 4))
161160, 76oveq12d 7173 . . . . . . . . . 10 (𝑋 ∈ ℂ → (Σ𝑘 ∈ (0...0)((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (3 · ((1 BernPoly 𝑋) / 3))) = ((1 / 4) + (𝑋 − (1 / 2))))
162156, 161eqtrd 2856 . . . . . . . . 9 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(0 + 1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = ((1 / 4) + (𝑋 − (1 / 2))))
163143, 162syl5eqr 2870 . . . . . . . 8 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...1)((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = ((1 / 4) + (𝑋 − (1 / 2))))
164163oveq1d 7170 . . . . . . 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 10618 . . . . . . . . 9 (((1 / 4) ∈ ℂ ∧ (𝑋 − (1 / 2)) ∈ ℂ) → ((1 / 4) + (𝑋 − (1 / 2))) ∈ ℂ)
16648, 71, 165sylancr 589 . . . . . . . 8 (𝑋 ∈ ℂ → ((1 / 4) + (𝑋 − (1 / 2))) ∈ ℂ)
167166, 131, 133addsub12d 11019 . . . . . . 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 2856 . . . . . 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 11012 . . . . . . . 8 (𝑋 ∈ ℂ → -(((3 / 2) · (𝑋 − (1 / 6))) − ((1 / 4) + (𝑋 − (1 / 2)))) = (((1 / 4) + (𝑋 − (1 / 2))) − ((3 / 2) · (𝑋 − (1 / 6)))))
170 subdi 11072 . . . . . . . . . . . 12 (((3 / 2) ∈ ℂ ∧ 𝑋 ∈ ℂ ∧ (1 / 6) ∈ ℂ) → ((3 / 2) · (𝑋 − (1 / 6))) = (((3 / 2) · 𝑋) − ((3 / 2) · (1 / 6))))
171108, 118, 170mp3an13 1448 . . . . . . . . . . 11 (𝑋 ∈ ℂ → ((3 / 2) · (𝑋 − (1 / 6))) = (((3 / 2) · 𝑋) − ((3 / 2) · (1 / 6))))
172 addsub12 10898 . . . . . . . . . . . 12 (((1 / 4) ∈ ℂ ∧ 𝑋 ∈ ℂ ∧ (1 / 2) ∈ ℂ) → ((1 / 4) + (𝑋 − (1 / 2))) = (𝑋 + ((1 / 4) − (1 / 2))))
17348, 69, 172mp3an13 1448 . . . . . . . . . . 11 (𝑋 ∈ ℂ → ((1 / 4) + (𝑋 − (1 / 2))) = (𝑋 + ((1 / 4) − (1 / 2))))
174171, 173oveq12d 7173 . . . . . . . . . 10 (𝑋 ∈ ℂ → (((3 / 2) · (𝑋 − (1 / 6))) − ((1 / 4) + (𝑋 − (1 / 2)))) = ((((3 / 2) · 𝑋) − ((3 / 2) · (1 / 6))) − (𝑋 + ((1 / 4) − (1 / 2)))))
175 mulcl 10620 . . . . . . . . . . . . 13 (((3 / 2) ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((3 / 2) · 𝑋) ∈ ℂ)
176108, 175mpan 688 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((3 / 2) · 𝑋) ∈ ℂ)
177108, 118mulcli 10647 . . . . . . . . . . . 12 ((3 / 2) · (1 / 6)) ∈ ℂ
178 negsub 10933 . . . . . . . . . . . 12 ((((3 / 2) · 𝑋) ∈ ℂ ∧ ((3 / 2) · (1 / 6)) ∈ ℂ) → (((3 / 2) · 𝑋) + -((3 / 2) · (1 / 6))) = (((3 / 2) · 𝑋) − ((3 / 2) · (1 / 6))))
179176, 177, 178sylancl 588 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (((3 / 2) · 𝑋) + -((3 / 2) · (1 / 6))) = (((3 / 2) · 𝑋) − ((3 / 2) · (1 / 6))))
180179oveq1d 7170 . . . . . . . . . 10 (𝑋 ∈ ℂ → ((((3 / 2) · 𝑋) + -((3 / 2) · (1 / 6))) − (𝑋 + ((1 / 4) − (1 / 2)))) = ((((3 / 2) · 𝑋) − ((3 / 2) · (1 / 6))) − (𝑋 + ((1 / 4) − (1 / 2)))))
18169, 48negsubdi2i 10971 . . . . . . . . . . . . . 14 -((1 / 2) − (1 / 4)) = ((1 / 4) − (1 / 2))
18285, 35, 85mul12i 10834 . . . . . . . . . . . . . . . . . . 19 (2 · (3 · 2)) = (3 · (2 · 2))
183 3t2e6 11802 . . . . . . . . . . . . . . . . . . . 20 (3 · 2) = 6
184183oveq2i 7166 . . . . . . . . . . . . . . . . . . 19 (2 · (3 · 2)) = (2 · 6)
185 2t2e4 11800 . . . . . . . . . . . . . . . . . . . 20 (2 · 2) = 4
186185oveq2i 7166 . . . . . . . . . . . . . . . . . . 19 (3 · (2 · 2)) = (3 · 4)
187182, 184, 1863eqtr3i 2852 . . . . . . . . . . . . . . . . . 18 (2 · 6) = (3 · 4)
188187oveq2i 7166 . . . . . . . . . . . . . . . . 17 ((3 · 1) / (2 · 6)) = ((3 · 1) / (3 · 4))
18946, 47pm3.2i 473 . . . . . . . . . . . . . . . . . 18 (4 ∈ ℂ ∧ 4 ≠ 0)
19035, 72pm3.2i 473 . . . . . . . . . . . . . . . . . 18 (3 ∈ ℂ ∧ 3 ≠ 0)
191 divcan5 11341 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → ((3 · 1) / (3 · 4)) = (1 / 4))
19260, 189, 190, 191mp3an 1457 . . . . . . . . . . . . . . . . 17 ((3 · 1) / (3 · 4)) = (1 / 4)
193188, 192eqtri 2844 . . . . . . . . . . . . . . . 16 ((3 · 1) / (2 · 6)) = (1 / 4)
19435, 85, 60, 114, 86, 117divmuldivi 11399 . . . . . . . . . . . . . . . 16 ((3 / 2) · (1 / 6)) = ((3 · 1) / (2 · 6))
195 2t1e2 11799 . . . . . . . . . . . . . . . . . . . 20 (2 · 1) = 2
196195, 5eqtri 2844 . . . . . . . . . . . . . . . . . . 19 (2 · 1) = (1 + 1)
197196, 185oveq12i 7167 . . . . . . . . . . . . . . . . . 18 ((2 · 1) / (2 · 2)) = ((1 + 1) / 4)
198 divcan5 11341 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 1) / (2 · 2)) = (1 / 2))
19960, 104, 104, 198mp3an 1457 . . . . . . . . . . . . . . . . . 18 ((2 · 1) / (2 · 2)) = (1 / 2)
20060, 60, 46, 47divdiri 11396 . . . . . . . . . . . . . . . . . 18 ((1 + 1) / 4) = ((1 / 4) + (1 / 4))
201197, 199, 2003eqtr3ri 2853 . . . . . . . . . . . . . . . . 17 ((1 / 4) + (1 / 4)) = (1 / 2)
20269, 48, 48, 201subaddrii 10974 . . . . . . . . . . . . . . . 16 ((1 / 2) − (1 / 4)) = (1 / 4)
203193, 194, 2023eqtr4ri 2855 . . . . . . . . . . . . . . 15 ((1 / 2) − (1 / 4)) = ((3 / 2) · (1 / 6))
204203negeqi 10878 . . . . . . . . . . . . . 14 -((1 / 2) − (1 / 4)) = -((3 / 2) · (1 / 6))
205181, 204eqtr3i 2846 . . . . . . . . . . . . 13 ((1 / 4) − (1 / 2)) = -((3 / 2) · (1 / 6))
20648, 69subcli 10961 . . . . . . . . . . . . . 14 ((1 / 4) − (1 / 2)) ∈ ℂ
207177negcli 10953 . . . . . . . . . . . . . 14 -((3 / 2) · (1 / 6)) ∈ ℂ
208206, 207subeq0i 10965 . . . . . . . . . . . . 13 ((((1 / 4) − (1 / 2)) − -((3 / 2) · (1 / 6))) = 0 ↔ ((1 / 4) − (1 / 2)) = -((3 / 2) · (1 / 6)))
209205, 208mpbir 233 . . . . . . . . . . . 12 (((1 / 4) − (1 / 2)) − -((3 / 2) · (1 / 6))) = 0
210209oveq2i 7166 . . . . . . . . . . 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 11044 . . . . . . . . . . 11 (𝑋 ∈ ℂ → ((((3 / 2) · 𝑋) − 𝑋) − (((1 / 4) − (1 / 2)) − -((3 / 2) · (1 / 6)))) = ((((3 / 2) · 𝑋) + -((3 / 2) · (1 / 6))) − (𝑋 + ((1 / 4) − (1 / 2)))))
215 subdir 11073 . . . . . . . . . . . . . . 15 (((3 / 2) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (((3 / 2) − 1) · 𝑋) = (((3 / 2) · 𝑋) − (1 · 𝑋)))
216108, 60, 215mp3an12 1447 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (((3 / 2) − 1) · 𝑋) = (((3 / 2) · 𝑋) − (1 · 𝑋)))
217 divsubdir 11333 . . . . . . . . . . . . . . . . . 18 ((3 ∈ ℂ ∧ 2 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((3 − 2) / 2) = ((3 / 2) − (2 / 2)))
21835, 85, 104, 217mp3an 1457 . . . . . . . . . . . . . . . . 17 ((3 − 2) / 2) = ((3 / 2) − (2 / 2))
21995oveq1i 7165 . . . . . . . . . . . . . . . . 17 ((3 − 2) / 2) = (1 / 2)
220 2div2e1 11777 . . . . . . . . . . . . . . . . . 18 (2 / 2) = 1
221220oveq2i 7166 . . . . . . . . . . . . . . . . 17 ((3 / 2) − (2 / 2)) = ((3 / 2) − 1)
222218, 219, 2213eqtr3ri 2853 . . . . . . . . . . . . . . . 16 ((3 / 2) − 1) = (1 / 2)
223222oveq1i 7165 . . . . . . . . . . . . . . 15 (((3 / 2) − 1) · 𝑋) = ((1 / 2) · 𝑋)
224223a1i 11 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (((3 / 2) − 1) · 𝑋) = ((1 / 2) · 𝑋))
225 mulid2 10639 . . . . . . . . . . . . . . 15 (𝑋 ∈ ℂ → (1 · 𝑋) = 𝑋)
226225oveq2d 7171 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (((3 / 2) · 𝑋) − (1 · 𝑋)) = (((3 / 2) · 𝑋) − 𝑋))
227216, 224, 2263eqtr3rd 2865 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (((3 / 2) · 𝑋) − 𝑋) = ((1 / 2) · 𝑋))
228227oveq1d 7170 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((((3 / 2) · 𝑋) − 𝑋) − 0) = (((1 / 2) · 𝑋) − 0))
229 mulcl 10620 . . . . . . . . . . . . . 14 (((1 / 2) ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((1 / 2) · 𝑋) ∈ ℂ)
23069, 229mpan 688 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → ((1 / 2) · 𝑋) ∈ ℂ)
231230subid1d 10985 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (((1 / 2) · 𝑋) − 0) = ((1 / 2) · 𝑋))
232228, 231eqtrd 2856 . . . . . . . . . . 11 (𝑋 ∈ ℂ → ((((3 / 2) · 𝑋) − 𝑋) − 0) = ((1 / 2) · 𝑋))
233210, 214, 2323eqtr3a 2880 . . . . . . . . . 10 (𝑋 ∈ ℂ → ((((3 / 2) · 𝑋) + -((3 / 2) · (1 / 6))) − (𝑋 + ((1 / 4) − (1 / 2)))) = ((1 / 2) · 𝑋))
234174, 180, 2333eqtr2d 2862 . . . . . . . . 9 (𝑋 ∈ ℂ → (((3 / 2) · (𝑋 − (1 / 6))) − ((1 / 4) + (𝑋 − (1 / 2)))) = ((1 / 2) · 𝑋))
235234negeqd 10879 . . . . . . . 8 (𝑋 ∈ ℂ → -(((3 / 2) · (𝑋 − (1 / 6))) − ((1 / 4) + (𝑋 − (1 / 2)))) = -((1 / 2) · 𝑋))
236169, 235eqtr3d 2858 . . . . . . 7 (𝑋 ∈ ℂ → (((1 / 4) + (𝑋 − (1 / 2))) − ((3 / 2) · (𝑋 − (1 / 6)))) = -((1 / 2) · 𝑋))
237236oveq2d 7171 . . . . . 6 (𝑋 ∈ ℂ → (((3 / 2) · (𝑋↑2)) + (((1 / 4) + (𝑋 − (1 / 2))) − ((3 / 2) · (𝑋 − (1 / 6))))) = (((3 / 2) · (𝑋↑2)) + -((1 / 2) · 𝑋)))
238131, 230negsubd 11002 . . . . . 6 (𝑋 ∈ ℂ → (((3 / 2) · (𝑋↑2)) + -((1 / 2) · 𝑋)) = (((3 / 2) · (𝑋↑2)) − ((1 / 2) · 𝑋)))
239168, 237, 2383eqtrd 2860 . . . . 5 (𝑋 ∈ ℂ → (Σ𝑘 ∈ (0...1)((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (((3 / 2) · (𝑋↑2)) − ((3 / 2) · (𝑋 − (1 / 6))))) = (((3 / 2) · (𝑋↑2)) − ((1 / 2) · 𝑋)))
240141, 142, 2393eqtrd 2860 . . . 4 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(1 + 1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (((3 / 2) · (𝑋↑2)) − ((1 / 2) · 𝑋)))
2418, 240syl5eq 2868 . . 3 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(3 − 1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (((3 / 2) · (𝑋↑2)) − ((1 / 2) · 𝑋)))
242241oveq2d 7171 . 2 (𝑋 ∈ ℂ → ((𝑋↑3) − Σ𝑘 ∈ (0...(3 − 1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1)))) = ((𝑋↑3) − (((3 / 2) · (𝑋↑2)) − ((1 / 2) · 𝑋))))
243 expcl 13446 . . . 4 ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑋↑3) ∈ ℂ)
2441, 243mpan2 689 . . 3 (𝑋 ∈ ℂ → (𝑋↑3) ∈ ℂ)
245244, 131, 230subsubd 11024 . 2 (𝑋 ∈ ℂ → ((𝑋↑3) − (((3 / 2) · (𝑋↑2)) − ((1 / 2) · 𝑋))) = (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))
2463, 242, 2453eqtrd 2860 1 (𝑋 ∈ ℂ → (3 BernPoly 𝑋) = (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   ∨ wo 843   ∨ w3o 1082   = wceq 1533   ∈ wcel 2110   ≠ wne 3016   ∪ cun 3933  {csn 4566  {cpr 4568  {ctp 4570  ‘cfv 6354  (class class class)co 7155  ℂcc 10534  0cc0 10536  1c1 10537   + caddc 10539   · cmul 10541   − cmin 10869  -cneg 10870   / cdiv 11296  2c2 11691  3c3 11692  4c4 11693  6c6 11695  ℕ0cn0 11896  ℤcz 11980  ℤ≥cuz 12242  ...cfz 12891  ↑cexp 13428  Ccbc 13661  Σcsu 15041   BernPoly cbp 15399 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5189  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460  ax-inf2 9103  ax-cnex 10592  ax-resscn 10593  ax-1cn 10594  ax-icn 10595  ax-addcl 10596  ax-addrcl 10597  ax-mulcl 10598  ax-mulrcl 10599  ax-mulcom 10600  ax-addass 10601  ax-mulass 10602  ax-distr 10603  ax-i2m1 10604  ax-1ne0 10605  ax-1rid 10606  ax-rnegex 10607  ax-rrecex 10608  ax-cnre 10609  ax-pre-lttri 10610  ax-pre-lttrn 10611  ax-pre-ltadd 10612  ax-pre-mulgt0 10613  ax-pre-sup 10614 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-fal 1546  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4838  df-int 4876  df-iun 4920  df-br 5066  df-opab 5128  df-mpt 5146  df-tr 5172  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-om 7580  df-1st 7688  df-2nd 7689  df-wrecs 7946  df-recs 8007  df-rdg 8045  df-1o 8101  df-oadd 8105  df-er 8288  df-en 8509  df-dom 8510  df-sdom 8511  df-fin 8512  df-sup 8905  df-oi 8973  df-card 9367  df-pnf 10676  df-mnf 10677  df-xr 10678  df-ltxr 10679  df-le 10680  df-sub 10871  df-neg 10872  df-div 11297  df-nn 11638  df-2 11699  df-3 11700  df-4 11701  df-5 11702  df-6 11703  df-n0 11897  df-z 11981  df-uz 12243  df-rp 12389  df-fz 12892  df-fzo 13033  df-seq 13369  df-exp 13429  df-fac 13633  df-bc 13662  df-hash 13690  df-cj 14457  df-re 14458  df-im 14459  df-sqrt 14593  df-abs 14594  df-clim 14844  df-sum 15042  df-bpoly 15400 This theorem is referenced by:  bpoly4  15412
 Copyright terms: Public domain W3C validator