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	mullidi	⊢ ( 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	eqtrid	⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 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 ) ) )