bpolylem - Metamath Proof Explorer

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

Theorem bpolylem 15260

Description: Lemma for bpolyval 15261. (Contributed by Scott Fenton, 22-May-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)

**Hypotheses**
Ref	Expression
bpoly.1	⊢ 𝐺 = (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))
bpoly.2	⊢ 𝐹 = wrecs( < , ℕ₀, 𝐺)

**Assertion**
Ref	Expression
bpolylem	⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝑁 BernPoly 𝑋) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))

Distinct variable groups: 𝑔,𝑘,𝑛,𝐹 𝑔,𝑁,𝑘,𝑛 𝑔,𝑋,𝑘,𝑛 Allowed substitution hints: 𝐺(𝑔,𝑘,𝑛)

Proof of Theorem bpolylem Dummy variables 𝑚 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 6981	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝑥↑𝑛) = (𝑋↑𝑛))
2	1	oveq1d 6989	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))
3	2	csbeq2dv 4250	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))
4	3	mpteq2dv 5019	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) = (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))
5		bpoly.1	. . . . . . . 8 ⊢ 𝐺 = (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))
6	4, 5	syl6eqr 2825	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) = 𝐺)
7		wrecseq3 7753	. . . . . . 7 ⊢ ((𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) = 𝐺 → wrecs( < , ℕ₀, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))) = wrecs( < , ℕ₀, 𝐺))
8	6, 7	syl 17	. . . . . 6 ⊢ (𝑥 = 𝑋 → wrecs( < , ℕ₀, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))) = wrecs( < , ℕ₀, 𝐺))
9		bpoly.2	. . . . . 6 ⊢ 𝐹 = wrecs( < , ℕ₀, 𝐺)
10	8, 9	syl6eqr 2825	. . . . 5 ⊢ (𝑥 = 𝑋 → wrecs( < , ℕ₀, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))) = 𝐹)
11	10	fveq1d 6498	. . . 4 ⊢ (𝑥 = 𝑋 → (wrecs( < , ℕ₀, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚) = (𝐹‘𝑚))
12		fveq2 6496	. . . 4 ⊢ (𝑚 = 𝑁 → (𝐹‘𝑚) = (𝐹‘𝑁))
13	11, 12	sylan9eqr 2829	. . 3 ⊢ ((𝑚 = 𝑁 ∧ 𝑥 = 𝑋) → (wrecs( < , ℕ₀, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚) = (𝐹‘𝑁))
14		df-bpoly 15259	. . 3 ⊢ BernPoly = (𝑚 ∈ ℕ₀, 𝑥 ∈ ℂ ↦ (wrecs( < , ℕ₀, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚))
15		fvex 6509	. . 3 ⊢ (𝐹‘𝑁) ∈ V
16	13, 14, 15	ovmpoa 7119	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝑁 BernPoly 𝑋) = (𝐹‘𝑁))
17		ltweuz 13142	. . . . 5 ⊢ < We (ℤ_≥‘0)
18		nn0uz 12092	. . . . . 6 ⊢ ℕ₀ = (ℤ_≥‘0)
19		weeq2 5392	. . . . . 6 ⊢ (ℕ₀ = (ℤ_≥‘0) → ( < We ℕ₀ ↔ < We (ℤ_≥‘0)))
20	18, 19	ax-mp 5	. . . . 5 ⊢ ( < We ℕ₀ ↔ < We (ℤ_≥‘0))
21	17, 20	mpbir 223	. . . 4 ⊢ < We ℕ₀
22		nn0ex 11712	. . . . 5 ⊢ ℕ₀ ∈ V
23		exse 5367	. . . . 5 ⊢ (ℕ₀ ∈ V → < Se ℕ₀)
24	22, 23	ax-mp 5	. . . 4 ⊢ < Se ℕ₀
25	21, 24, 9	wfr2 7776	. . 3 ⊢ (𝑁 ∈ ℕ₀ → (𝐹‘𝑁) = (𝐺‘(𝐹 ↾ Pred( < , ℕ₀, 𝑁))))
26	25	adantr 473	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝐹‘𝑁) = (𝐺‘(𝐹 ↾ Pred( < , ℕ₀, 𝑁))))
27		prednn0 12845	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → Pred( < , ℕ₀, 𝑁) = (0...(𝑁 − 1)))
28	27	adantr 473	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → Pred( < , ℕ₀, 𝑁) = (0...(𝑁 − 1)))
29	28	reseq2d 5692	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝐹 ↾ Pred( < , ℕ₀, 𝑁)) = (𝐹 ↾ (0...(𝑁 − 1))))
30	29	fveq2d 6500	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝐺‘(𝐹 ↾ Pred( < , ℕ₀, 𝑁))) = (𝐺‘(𝐹 ↾ (0...(𝑁 − 1)))))
31	21, 24, 9	wfrfun 7767	. . . . . 6 ⊢ Fun 𝐹
32		ovex 7006	. . . . . 6 ⊢ (0...(𝑁 − 1)) ∈ V
33		resfunexg 6802	. . . . . 6 ⊢ ((Fun 𝐹 ∧ (0...(𝑁 − 1)) ∈ V) → (𝐹 ↾ (0...(𝑁 − 1))) ∈ V)
34	31, 32, 33	mp2an 680	. . . . 5 ⊢ (𝐹 ↾ (0...(𝑁 − 1))) ∈ V
35		dmeq 5618	. . . . . . . . . . 11 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → dom 𝑔 = dom (𝐹 ↾ (0...(𝑁 − 1))))
36	21, 24, 9	wfr1 7775	. . . . . . . . . . . . 13 ⊢ 𝐹 Fn ℕ₀
37		fz0ssnn0 12816	. . . . . . . . . . . . 13 ⊢ (0...(𝑁 − 1)) ⊆ ℕ₀
38		fnssres 6300	. . . . . . . . . . . . 13 ⊢ ((𝐹 Fn ℕ₀ ∧ (0...(𝑁 − 1)) ⊆ ℕ₀) → (𝐹 ↾ (0...(𝑁 − 1))) Fn (0...(𝑁 − 1)))
39	36, 37, 38	mp2an 680	. . . . . . . . . . . 12 ⊢ (𝐹 ↾ (0...(𝑁 − 1))) Fn (0...(𝑁 − 1))
40		fndm 6285	. . . . . . . . . . . 12 ⊢ ((𝐹 ↾ (0...(𝑁 − 1))) Fn (0...(𝑁 − 1)) → dom (𝐹 ↾ (0...(𝑁 − 1))) = (0...(𝑁 − 1)))
41	39, 40	ax-mp 5	. . . . . . . . . . 11 ⊢ dom (𝐹 ↾ (0...(𝑁 − 1))) = (0...(𝑁 − 1))
42	35, 41	syl6eq 2823	. . . . . . . . . 10 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → dom 𝑔 = (0...(𝑁 − 1)))
43		fveq1 6495	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → (𝑔‘𝑘) = ((𝐹 ↾ (0...(𝑁 − 1)))‘𝑘))
44		fvres 6515	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝐹 ↾ (0...(𝑁 − 1)))‘𝑘) = (𝐹‘𝑘))
45	43, 44	sylan9eq 2827	. . . . . . . . . . . 12 ⊢ ((𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑔‘𝑘) = (𝐹‘𝑘))
46	45	oveq1d 6989	. . . . . . . . . . 11 ⊢ ((𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)) = ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))
47	46	oveq2d 6990	. . . . . . . . . 10 ⊢ ((𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))) = ((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))
48	42, 47	sumeq12rdv 14922	. . . . . . . . 9 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))
49	48	oveq2d 6990	. . . . . . . 8 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → ((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))))
50	49	csbeq2dv 4250	. . . . . . 7 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))))
51	42	fveq2d 6500	. . . . . . . 8 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → (♯‘dom 𝑔) = (♯‘(0...(𝑁 − 1))))
52	51	csbeq1d 3786	. . . . . . 7 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))))
53	50, 52	eqtrd 2807	. . . . . 6 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))))
54		ovex 7006	. . . . . . 7 ⊢ ((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) ∈ V
55	54	csbex 5068	. . . . . 6 ⊢ ⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) ∈ V
56	53, 5, 55	fvmpt 6593	. . . . 5 ⊢ ((𝐹 ↾ (0...(𝑁 − 1))) ∈ V → (𝐺‘(𝐹 ↾ (0...(𝑁 − 1)))) = ⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))))
57	34, 56	ax-mp 5	. . . 4 ⊢ (𝐺‘(𝐹 ↾ (0...(𝑁 − 1)))) = ⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))
58		nfcvd 2926	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → Ⅎ𝑛((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))))
59		oveq2 6982	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → (𝑋↑𝑛) = (𝑋↑𝑁))
60		oveq1 6981	. . . . . . . . . 10 ⊢ (𝑛 = 𝑁 → (𝑛C𝑘) = (𝑁C𝑘))
61		oveq1 6981	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑁 → (𝑛 − 𝑘) = (𝑁 − 𝑘))
62	61	oveq1d 6989	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑁 → ((𝑛 − 𝑘) + 1) = ((𝑁 − 𝑘) + 1))
63	62	oveq2d 6990	. . . . . . . . . 10 ⊢ (𝑛 = 𝑁 → ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)) = ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))
64	60, 63	oveq12d 6992	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → ((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))) = ((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))
65	64	sumeq2sdv 14919	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))
66	59, 65	oveq12d 6992	. . . . . . 7 ⊢ (𝑛 = 𝑁 → ((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))))
67	58, 66	csbiegf 3805	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ⦋𝑁 / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))))
68	67	adantr 473	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → ⦋𝑁 / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))))
69		nn0z 11816	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
70		fz01en 12749	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℤ → (0...(𝑁 − 1)) ≈ (1...𝑁))
71	69, 70	syl 17	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (0...(𝑁 − 1)) ≈ (1...𝑁))
72		fzfi 13153	. . . . . . . . . 10 ⊢ (0...(𝑁 − 1)) ∈ Fin
73		fzfi 13153	. . . . . . . . . 10 ⊢ (1...𝑁) ∈ Fin
74		hashen 13520	. . . . . . . . . 10 ⊢ (((0...(𝑁 − 1)) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((♯‘(0...(𝑁 − 1))) = (♯‘(1...𝑁)) ↔ (0...(𝑁 − 1)) ≈ (1...𝑁)))
75	72, 73, 74	mp2an 680	. . . . . . . . 9 ⊢ ((♯‘(0...(𝑁 − 1))) = (♯‘(1...𝑁)) ↔ (0...(𝑁 − 1)) ≈ (1...𝑁))
76	71, 75	sylibr 226	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(0...(𝑁 − 1))) = (♯‘(1...𝑁)))
77		hashfz1 13519	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(1...𝑁)) = 𝑁)
78	76, 77	eqtrd 2807	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(0...(𝑁 − 1))) = 𝑁)
79	78	adantr 473	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (♯‘(0...(𝑁 − 1))) = 𝑁)
80	79	csbeq1d 3786	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → ⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋𝑁 / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))))
81		elfznn0 12814	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ₀)
82		simpr 477	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → 𝑋 ∈ ℂ)
83		fveq2 6496	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘))
84	11, 83	sylan9eqr 2829	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑘 ∧ 𝑥 = 𝑋) → (wrecs( < , ℕ₀, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚) = (𝐹‘𝑘))
85		fvex 6509	. . . . . . . . . . 11 ⊢ (𝐹‘𝑘) ∈ V
86	84, 14, 85	ovmpoa 7119	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝑘 BernPoly 𝑋) = (𝐹‘𝑘))
87	81, 82, 86	syl2anr 588	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑘 BernPoly 𝑋) = (𝐹‘𝑘))
88	87	oveq1d 6989	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)) = ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))
89	88	oveq2d 6990	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = ((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))
90	89	sumeq2dv 14918	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))
91	90	oveq2d 6990	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))))
92	68, 80, 91	3eqtr4d 2817	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → ⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))
93	57, 92	syl5eq 2819	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝐺‘(𝐹 ↾ (0...(𝑁 − 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))
94	30, 93	eqtrd 2807	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝐺‘(𝐹 ↾ Pred( < , ℕ₀, 𝑁))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))
95	16, 26, 94	3eqtrd 2811	1 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝑁 BernPoly 𝑋) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1508 ∈ wcel 2051 Vcvv 3408 ⦋csb 3779 ⊆ wss 3822 class class class wbr 4925 ↦ cmpt 5004 Se wse 5360 We wwe 5361 dom cdm 5403 ↾ cres 5405 Predcpred 5982 Fun wfun 6179 Fn wfn 6180 ‘cfv 6185 (class class class)co 6974 wrecscwrecs 7747 ≈ cen 8301 Fincfn 8304 ℂcc 10331 0cc0 10333 1c1 10334 + caddc 10336 · cmul 10338 < clt 10472 − cmin 10668 / cdiv 11096 ℕ₀cn0 11705 ℤcz 11791 ℤ_≥cuz 12056 ...cfz 12706 ↑cexp 13242 Ccbc 13475 ♯chash 13503 Σcsu 14901 BernPoly cbp 15258

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2743 ax-rep 5045 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 ax-inf2 8896 ax-cnex 10389 ax-resscn 10390 ax-1cn 10391 ax-icn 10392 ax-addcl 10393 ax-addrcl 10394 ax-mulcl 10395 ax-mulrcl 10396 ax-mulcom 10397 ax-addass 10398 ax-mulass 10399 ax-distr 10400 ax-i2m1 10401 ax-1ne0 10402 ax-1rid 10403 ax-rnegex 10404 ax-rrecex 10405 ax-cnre 10406 ax-pre-lttri 10407 ax-pre-lttrn 10408 ax-pre-ltadd 10409 ax-pre-mulgt0 10410

This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-fal 1521 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-ne 2961 df-nel 3067 df-ral 3086 df-rex 3087 df-reu 3088 df-rmo 3089 df-rab 3090 df-v 3410 df-sbc 3675 df-csb 3780 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-pss 3838 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4709 df-int 4746 df-iun 4790 df-br 4926 df-opab 4988 df-mpt 5005 df-tr 5027 df-id 5308 df-eprel 5313 df-po 5322 df-so 5323 df-fr 5362 df-se 5363 df-we 5364 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-pred 5983 df-ord 6029 df-on 6030 df-lim 6031 df-suc 6032 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-isom 6194 df-riota 6935 df-ov 6977 df-oprab 6978 df-mpo 6979 df-om 7395 df-1st 7499 df-2nd 7500 df-wrecs 7748 df-recs 7810 df-rdg 7848 df-1o 7903 df-er 8087 df-en 8305 df-dom 8306 df-sdom 8307 df-fin 8308 df-card 9160 df-pnf 10474 df-mnf 10475 df-xr 10476 df-ltxr 10477 df-le 10478 df-sub 10670 df-neg 10671 df-nn 11438 df-n0 11706 df-z 11792 df-uz 12057 df-fz 12707 df-seq 13183 df-hash 13504 df-sum 14902 df-bpoly 15259

This theorem is referenced by: bpolyval 15261

W3C validator