Metamath Proof Explorer

Theorem bpoly2

Description: The Bernoulli polynomials at two. (Contributed by Scott Fenton, 8-Jul-2015)

Ref Expression
Assertion bpoly2 ( 𝑋 ∈ ℂ → ( 2 BernPoly 𝑋 ) = ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) )

Proof

Step Hyp Ref Expression
1 2nn0 ⊢ 2 ∈ ℕ0
2 bpolyval ⊢ ( ( 2 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 2 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 2 ) − Σ 𝑘 ∈ ( 0 ... ( 2 − 1 ) ) ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) ) )
3 1 2 mpan ⊢ ( 𝑋 ∈ ℂ → ( 2 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 2 ) − Σ 𝑘 ∈ ( 0 ... ( 2 − 1 ) ) ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) ) )
4 2m1e1 ⊢ ( 2 − 1 ) = 1
5 0p1e1 ⊢ ( 0 + 1 ) = 1
6 4 5 eqtr4i ⊢ ( 2 − 1 ) = ( 0 + 1 )
7 6 oveq2i ⊢ ( 0 ... ( 2 − 1 ) ) = ( 0 ... ( 0 + 1 ) )
8 7 sumeq1i ⊢ Σ 𝑘 ∈ ( 0 ... ( 2 − 1 ) ) ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) )
9 0nn0 ⊢ 0 ∈ ℕ0
10 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
11 9 10 eleqtri ⊢ 0 ∈ ( ℤ≥ ‘ 0 )
12 11 a1i ⊢ ( 𝑋 ∈ ℂ → 0 ∈ ( ℤ≥ ‘ 0 ) )
13 0z ⊢ 0 ∈ ℤ
14 fzpr ⊢ ( 0 ∈ ℤ → ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) } )
15 13 14 ax-mp ⊢ ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) }
16 15 eleq2i ⊢ ( 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ↔ 𝑘 ∈ { 0 , ( 0 + 1 ) } )
17 vex ⊢ 𝑘 ∈ V
18 17 elpr ⊢ ( 𝑘 ∈ { 0 , ( 0 + 1 ) } ↔ ( 𝑘 = 0 ∨ 𝑘 = ( 0 + 1 ) ) )
19 16 18 bitri ⊢ ( 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ↔ ( 𝑘 = 0 ∨ 𝑘 = ( 0 + 1 ) ) )
20 oveq2 ⊢ ( 𝑘 = 0 → ( 2 C 𝑘 ) = ( 2 C 0 ) )
21 bcn0 ⊢ ( 2 ∈ ℕ0 → ( 2 C 0 ) = 1 )
22 1 21 ax-mp ⊢ ( 2 C 0 ) = 1
23 20 22 eqtrdi ⊢ ( 𝑘 = 0 → ( 2 C 𝑘 ) = 1 )
24 oveq1 ⊢ ( 𝑘 = 0 → ( 𝑘 BernPoly 𝑋 ) = ( 0 BernPoly 𝑋 ) )
25 oveq2 ⊢ ( 𝑘 = 0 → ( 2 − 𝑘 ) = ( 2 − 0 ) )
26 25 oveq1d ⊢ ( 𝑘 = 0 → ( ( 2 − 𝑘 ) + 1 ) = ( ( 2 − 0 ) + 1 ) )
27 2cn ⊢ 2 ∈ ℂ
28 27 subid1i ⊢ ( 2 − 0 ) = 2
29 28 oveq1i ⊢ ( ( 2 − 0 ) + 1 ) = ( 2 + 1 )
30 df-3 ⊢ 3 = ( 2 + 1 )
31 29 30 eqtr4i ⊢ ( ( 2 − 0 ) + 1 ) = 3
32 26 31 eqtrdi ⊢ ( 𝑘 = 0 → ( ( 2 − 𝑘 ) + 1 ) = 3 )
33 24 32 oveq12d ⊢ ( 𝑘 = 0 → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) = ( ( 0 BernPoly 𝑋 ) / 3 ) )
34 23 33 oveq12d ⊢ ( 𝑘 = 0 → ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) = ( 1 · ( ( 0 BernPoly 𝑋 ) / 3 ) ) )
35 bpoly0 ⊢ ( 𝑋 ∈ ℂ → ( 0 BernPoly 𝑋 ) = 1 )
36 35 oveq1d ⊢ ( 𝑋 ∈ ℂ → ( ( 0 BernPoly 𝑋 ) / 3 ) = ( 1 / 3 ) )
37 36 oveq2d ⊢ ( 𝑋 ∈ ℂ → ( 1 · ( ( 0 BernPoly 𝑋 ) / 3 ) ) = ( 1 · ( 1 / 3 ) ) )
38 3cn ⊢ 3 ∈ ℂ
39 3ne0 ⊢ 3 ≠ 0
40 38 39 reccli ⊢ ( 1 / 3 ) ∈ ℂ
41 40 mulid2i ⊢ ( 1 · ( 1 / 3 ) ) = ( 1 / 3 )
42 37 41 eqtrdi ⊢ ( 𝑋 ∈ ℂ → ( 1 · ( ( 0 BernPoly 𝑋 ) / 3 ) ) = ( 1 / 3 ) )
43 34 42 sylan9eqr ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑘 = 0 ) → ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) = ( 1 / 3 ) )
44 43 40 eqeltrdi ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑘 = 0 ) → ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) ∈ ℂ )
45 5 eqeq2i ⊢ ( 𝑘 = ( 0 + 1 ) ↔ 𝑘 = 1 )
46 oveq2 ⊢ ( 𝑘 = 1 → ( 2 C 𝑘 ) = ( 2 C 1 ) )
47 bcn1 ⊢ ( 2 ∈ ℕ0 → ( 2 C 1 ) = 2 )
48 1 47 ax-mp ⊢ ( 2 C 1 ) = 2
49 46 48 eqtrdi ⊢ ( 𝑘 = 1 → ( 2 C 𝑘 ) = 2 )
50 oveq1 ⊢ ( 𝑘 = 1 → ( 𝑘 BernPoly 𝑋 ) = ( 1 BernPoly 𝑋 ) )
51 oveq2 ⊢ ( 𝑘 = 1 → ( 2 − 𝑘 ) = ( 2 − 1 ) )
52 51 oveq1d ⊢ ( 𝑘 = 1 → ( ( 2 − 𝑘 ) + 1 ) = ( ( 2 − 1 ) + 1 ) )
53 ax-1cn ⊢ 1 ∈ ℂ
54 npcan ⊢ ( ( 2 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 2 − 1 ) + 1 ) = 2 )
55 27 53 54 mp2an ⊢ ( ( 2 − 1 ) + 1 ) = 2
56 52 55 eqtrdi ⊢ ( 𝑘 = 1 → ( ( 2 − 𝑘 ) + 1 ) = 2 )
57 50 56 oveq12d ⊢ ( 𝑘 = 1 → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) = ( ( 1 BernPoly 𝑋 ) / 2 ) )
58 49 57 oveq12d ⊢ ( 𝑘 = 1 → ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) = ( 2 · ( ( 1 BernPoly 𝑋 ) / 2 ) ) )
59 45 58 sylbi ⊢ ( 𝑘 = ( 0 + 1 ) → ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) = ( 2 · ( ( 1 BernPoly 𝑋 ) / 2 ) ) )
60 bpoly1 ⊢ ( 𝑋 ∈ ℂ → ( 1 BernPoly 𝑋 ) = ( 𝑋 − ( 1 / 2 ) ) )
61 60 oveq1d ⊢ ( 𝑋 ∈ ℂ → ( ( 1 BernPoly 𝑋 ) / 2 ) = ( ( 𝑋 − ( 1 / 2 ) ) / 2 ) )
62 61 oveq2d ⊢ ( 𝑋 ∈ ℂ → ( 2 · ( ( 1 BernPoly 𝑋 ) / 2 ) ) = ( 2 · ( ( 𝑋 − ( 1 / 2 ) ) / 2 ) ) )
63 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
64 subcl ⊢ ( ( 𝑋 ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) → ( 𝑋 − ( 1 / 2 ) ) ∈ ℂ )
65 63 64 mpan2 ⊢ ( 𝑋 ∈ ℂ → ( 𝑋 − ( 1 / 2 ) ) ∈ ℂ )
66 2ne0 ⊢ 2 ≠ 0
67 divcan2 ⊢ ( ( ( 𝑋 − ( 1 / 2 ) ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 2 · ( ( 𝑋 − ( 1 / 2 ) ) / 2 ) ) = ( 𝑋 − ( 1 / 2 ) ) )
68 27 66 67 mp3an23 ⊢ ( ( 𝑋 − ( 1 / 2 ) ) ∈ ℂ → ( 2 · ( ( 𝑋 − ( 1 / 2 ) ) / 2 ) ) = ( 𝑋 − ( 1 / 2 ) ) )
69 65 68 syl ⊢ ( 𝑋 ∈ ℂ → ( 2 · ( ( 𝑋 − ( 1 / 2 ) ) / 2 ) ) = ( 𝑋 − ( 1 / 2 ) ) )
70 62 69 eqtrd ⊢ ( 𝑋 ∈ ℂ → ( 2 · ( ( 1 BernPoly 𝑋 ) / 2 ) ) = ( 𝑋 − ( 1 / 2 ) ) )
71 59 70 sylan9eqr ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑘 = ( 0 + 1 ) ) → ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) = ( 𝑋 − ( 1 / 2 ) ) )
72 65 adantr ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑘 = ( 0 + 1 ) ) → ( 𝑋 − ( 1 / 2 ) ) ∈ ℂ )
73 71 72 eqeltrd ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑘 = ( 0 + 1 ) ) → ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) ∈ ℂ )
74 44 73 jaodan ⊢ ( ( 𝑋 ∈ ℂ ∧ ( 𝑘 = 0 ∨ 𝑘 = ( 0 + 1 ) ) ) → ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) ∈ ℂ )
75 19 74 sylan2b ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ) → ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) ∈ ℂ )
76 12 75 59 fsump1 ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) + ( 2 · ( ( 1 BernPoly 𝑋 ) / 2 ) ) ) )
77 42 40 eqeltrdi ⊢ ( 𝑋 ∈ ℂ → ( 1 · ( ( 0 BernPoly 𝑋 ) / 3 ) ) ∈ ℂ )
78 34 fsum1 ⊢ ( ( 0 ∈ ℤ ∧ ( 1 · ( ( 0 BernPoly 𝑋 ) / 3 ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) = ( 1 · ( ( 0 BernPoly 𝑋 ) / 3 ) ) )
79 13 77 78 sylancr ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) = ( 1 · ( ( 0 BernPoly 𝑋 ) / 3 ) ) )
80 79 42 eqtrd ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) = ( 1 / 3 ) )
81 80 70 oveq12d ⊢ ( 𝑋 ∈ ℂ → ( Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) + ( 2 · ( ( 1 BernPoly 𝑋 ) / 2 ) ) ) = ( ( 1 / 3 ) + ( 𝑋 − ( 1 / 2 ) ) ) )
82 76 81 eqtrd ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) = ( ( 1 / 3 ) + ( 𝑋 − ( 1 / 2 ) ) ) )
83 addsub12 ⊢ ( ( ( 1 / 3 ) ∈ ℂ ∧ 𝑋 ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) → ( ( 1 / 3 ) + ( 𝑋 − ( 1 / 2 ) ) ) = ( 𝑋 + ( ( 1 / 3 ) − ( 1 / 2 ) ) ) )
84 40 63 83 mp3an13 ⊢ ( 𝑋 ∈ ℂ → ( ( 1 / 3 ) + ( 𝑋 − ( 1 / 2 ) ) ) = ( 𝑋 + ( ( 1 / 3 ) − ( 1 / 2 ) ) ) )
85 63 40 negsubdi2i ⊢ - ( ( 1 / 2 ) − ( 1 / 3 ) ) = ( ( 1 / 3 ) − ( 1 / 2 ) )
86 halfthird ⊢ ( ( 1 / 2 ) − ( 1 / 3 ) ) = ( 1 / 6 )
87 86 negeqi ⊢ - ( ( 1 / 2 ) − ( 1 / 3 ) ) = - ( 1 / 6 )
88 85 87 eqtr3i ⊢ ( ( 1 / 3 ) − ( 1 / 2 ) ) = - ( 1 / 6 )
89 88 oveq2i ⊢ ( 𝑋 + ( ( 1 / 3 ) − ( 1 / 2 ) ) ) = ( 𝑋 + - ( 1 / 6 ) )
90 84 89 eqtrdi ⊢ ( 𝑋 ∈ ℂ → ( ( 1 / 3 ) + ( 𝑋 − ( 1 / 2 ) ) ) = ( 𝑋 + - ( 1 / 6 ) ) )
91 6cn ⊢ 6 ∈ ℂ
92 6re ⊢ 6 ∈ ℝ
93 6pos ⊢ 0 < 6
94 92 93 gt0ne0ii ⊢ 6 ≠ 0
95 91 94 reccli ⊢ ( 1 / 6 ) ∈ ℂ
96 negsub ⊢ ( ( 𝑋 ∈ ℂ ∧ ( 1 / 6 ) ∈ ℂ ) → ( 𝑋 + - ( 1 / 6 ) ) = ( 𝑋 − ( 1 / 6 ) ) )
97 95 96 mpan2 ⊢ ( 𝑋 ∈ ℂ → ( 𝑋 + - ( 1 / 6 ) ) = ( 𝑋 − ( 1 / 6 ) ) )
98 82 90 97 3eqtrd ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) = ( 𝑋 − ( 1 / 6 ) ) )
99 8 98 syl5eq ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 2 − 1 ) ) ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) = ( 𝑋 − ( 1 / 6 ) ) )
100 99 oveq2d ⊢ ( 𝑋 ∈ ℂ → ( ( 𝑋 ↑ 2 ) − Σ 𝑘 ∈ ( 0 ... ( 2 − 1 ) ) ( ( 2 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 2 − 𝑘 ) + 1 ) ) ) ) = ( ( 𝑋 ↑ 2 ) − ( 𝑋 − ( 1 / 6 ) ) ) )
101 sqcl ⊢ ( 𝑋 ∈ ℂ → ( 𝑋 ↑ 2 ) ∈ ℂ )
102 subsub ⊢ ( ( ( 𝑋 ↑ 2 ) ∈ ℂ ∧ 𝑋 ∈ ℂ ∧ ( 1 / 6 ) ∈ ℂ ) → ( ( 𝑋 ↑ 2 ) − ( 𝑋 − ( 1 / 6 ) ) ) = ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) )
103 95 102 mp3an3 ⊢ ( ( ( 𝑋 ↑ 2 ) ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( ( 𝑋 ↑ 2 ) − ( 𝑋 − ( 1 / 6 ) ) ) = ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) )
104 101 103 mpancom ⊢ ( 𝑋 ∈ ℂ → ( ( 𝑋 ↑ 2 ) − ( 𝑋 − ( 1 / 6 ) ) ) = ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) )
105 3 100 104 3eqtrd ⊢ ( 𝑋 ∈ ℂ → ( 2 BernPoly 𝑋 ) = ( ( ( 𝑋 ↑ 2 ) − 𝑋 ) + ( 1 / 6 ) ) )