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 14779

Description: Lemma for bpolyval 14780. (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 6657	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝑥↑𝑛) = (𝑋↑𝑛))
2	1	oveq1d 6665	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))
3	2	csbeq2dv 3992	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → ⦋(#‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋(#‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))
4	3	mpteq2dv 4745	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑔 ∈ V ↦ ⦋(#‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) = (𝑔 ∈ V ↦ ⦋(#‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))
5		bpoly.1	. . . . . . . 8 ⊢ 𝐺 = (𝑔 ∈ V ↦ ⦋(#‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))
6	4, 5	syl6eqr 2674	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑔 ∈ V ↦ ⦋(#‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) = 𝐺)
7		wrecseq3 7412	. . . . . . 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 2674	. . . . 5 ⊢ (𝑥 = 𝑋 → wrecs( < , ℕ₀, (𝑔 ∈ V ↦ ⦋(#‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))) = 𝐹)
11	10	fveq1d 6193	. . . 4 ⊢ (𝑥 = 𝑋 → (wrecs( < , ℕ₀, (𝑔 ∈ V ↦ ⦋(#‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚) = (𝐹‘𝑚))
12		fveq2 6191	. . . 4 ⊢ (𝑚 = 𝑁 → (𝐹‘𝑚) = (𝐹‘𝑁))
13	11, 12	sylan9eqr 2678	. . 3 ⊢ ((𝑚 = 𝑁 ∧ 𝑥 = 𝑋) → (wrecs( < , ℕ₀, (𝑔 ∈ V ↦ ⦋(#‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚) = (𝐹‘𝑁))
14		df-bpoly 14778	. . 3 ⊢ BernPoly = (𝑚 ∈ ℕ₀, 𝑥 ∈ ℂ ↦ (wrecs( < , ℕ₀, (𝑔 ∈ V ↦ ⦋(#‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚))
15		fvex 6201	. . 3 ⊢ (𝐹‘𝑁) ∈ V
16	13, 14, 15	ovmpt2a 6791	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝑁 BernPoly 𝑋) = (𝐹‘𝑁))
17		ltweuz 12760	. . . . 5 ⊢ < We (ℤ_≥‘0)
18		nn0uz 11722	. . . . . 6 ⊢ ℕ₀ = (ℤ_≥‘0)
19		weeq2 5103	. . . . . 6 ⊢ (ℕ₀ = (ℤ_≥‘0) → ( < We ℕ₀ ↔ < We (ℤ_≥‘0)))
20	18, 19	ax-mp 5	. . . . 5 ⊢ ( < We ℕ₀ ↔ < We (ℤ_≥‘0))
21	17, 20	mpbir 221	. . . 4 ⊢ < We ℕ₀
22		nn0ex 11298	. . . . 5 ⊢ ℕ₀ ∈ V
23		exse 5078	. . . . 5 ⊢ (ℕ₀ ∈ V → < Se ℕ₀)
24	22, 23	ax-mp 5	. . . 4 ⊢ < Se ℕ₀
25	21, 24, 9	wfr2 7434	. . 3 ⊢ (𝑁 ∈ ℕ₀ → (𝐹‘𝑁) = (𝐺‘(𝐹 ↾ Pred( < , ℕ₀, 𝑁))))
26	25	adantr 481	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝐹‘𝑁) = (𝐺‘(𝐹 ↾ Pred( < , ℕ₀, 𝑁))))
27		prednn0 12463	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → Pred( < , ℕ₀, 𝑁) = (0...(𝑁 − 1)))
28	27	adantr 481	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → Pred( < , ℕ₀, 𝑁) = (0...(𝑁 − 1)))
29	28	reseq2d 5396	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝐹 ↾ Pred( < , ℕ₀, 𝑁)) = (𝐹 ↾ (0...(𝑁 − 1))))
30	29	fveq2d 6195	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝐺‘(𝐹 ↾ Pred( < , ℕ₀, 𝑁))) = (𝐺‘(𝐹 ↾ (0...(𝑁 − 1)))))
31	21, 24, 9	wfrfun 7425	. . . . . 6 ⊢ Fun 𝐹
32		ovex 6678	. . . . . 6 ⊢ (0...(𝑁 − 1)) ∈ V
33		resfunexg 6479	. . . . . 6 ⊢ ((Fun 𝐹 ∧ (0...(𝑁 − 1)) ∈ V) → (𝐹 ↾ (0...(𝑁 − 1))) ∈ V)
34	31, 32, 33	mp2an 708	. . . . 5 ⊢ (𝐹 ↾ (0...(𝑁 − 1))) ∈ V
35		dmeq 5324	. . . . . . . . . . 11 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → dom 𝑔 = dom (𝐹 ↾ (0...(𝑁 − 1))))
36	21, 24, 9	wfr1 7433	. . . . . . . . . . . . 13 ⊢ 𝐹 Fn ℕ₀
37		fz0ssnn0 12435	. . . . . . . . . . . . 13 ⊢ (0...(𝑁 − 1)) ⊆ ℕ₀
38		fnssres 6004	. . . . . . . . . . . . 13 ⊢ ((𝐹 Fn ℕ₀ ∧ (0...(𝑁 − 1)) ⊆ ℕ₀) → (𝐹 ↾ (0...(𝑁 − 1))) Fn (0...(𝑁 − 1)))
39	36, 37, 38	mp2an 708	. . . . . . . . . . . 12 ⊢ (𝐹 ↾ (0...(𝑁 − 1))) Fn (0...(𝑁 − 1))
40		fndm 5990	. . . . . . . . . . . 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 2672	. . . . . . . . . 10 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → dom 𝑔 = (0...(𝑁 − 1)))
43		fveq1 6190	. . . . . . . . . . . . 13 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → (𝑔‘𝑘) = ((𝐹 ↾ (0...(𝑁 − 1)))‘𝑘))
44		fvres 6207	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝐹 ↾ (0...(𝑁 − 1)))‘𝑘) = (𝐹‘𝑘))
45	43, 44	sylan9eq 2676	. . . . . . . . . . . 12 ⊢ ((𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑔‘𝑘) = (𝐹‘𝑘))
46	45	oveq1d 6665	. . . . . . . . . . 11 ⊢ ((𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)) = ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))
47	46	oveq2d 6666	. . . . . . . . . 10 ⊢ ((𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))) = ((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))
48	42, 47	sumeq12rdv 14438	. . . . . . . . 9 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))
49	48	oveq2d 6666	. . . . . . . 8 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → ((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))))
50	49	csbeq2dv 3992	. . . . . . 7 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → ⦋(#‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋(#‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))))
51	42	fveq2d 6195	. . . . . . . 8 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → (#‘dom 𝑔) = (#‘(0...(𝑁 − 1))))
52	51	csbeq1d 3540	. . . . . . 7 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → ⦋(#‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋(#‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))))
53	50, 52	eqtrd 2656	. . . . . 6 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → ⦋(#‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋(#‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))))
54		ovex 6678	. . . . . . 7 ⊢ ((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) ∈ V
55	54	csbex 4793	. . . . . 6 ⊢ ⦋(#‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) ∈ V
56	53, 5, 55	fvmpt 6282	. . . . 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 2765	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → Ⅎ𝑛((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))))
59		oveq2 6658	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → (𝑋↑𝑛) = (𝑋↑𝑁))
60		oveq1 6657	. . . . . . . . . 10 ⊢ (𝑛 = 𝑁 → (𝑛C𝑘) = (𝑁C𝑘))
61		oveq1 6657	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑁 → (𝑛 − 𝑘) = (𝑁 − 𝑘))
62	61	oveq1d 6665	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑁 → ((𝑛 − 𝑘) + 1) = ((𝑁 − 𝑘) + 1))
63	62	oveq2d 6666	. . . . . . . . . 10 ⊢ (𝑛 = 𝑁 → ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)) = ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))
64	60, 63	oveq12d 6668	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → ((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))) = ((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))
65	64	sumeq2sdv 14435	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))
66	59, 65	oveq12d 6668	. . . . . . 7 ⊢ (𝑛 = 𝑁 → ((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))))
67	58, 66	csbiegf 3557	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ⦋𝑁 / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))))
68	67	adantr 481	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → ⦋𝑁 / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))))
69		nn0z 11400	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
70		fz01en 12369	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℤ → (0...(𝑁 − 1)) ≈ (1...𝑁))
71	69, 70	syl 17	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (0...(𝑁 − 1)) ≈ (1...𝑁))
72		fzfi 12771	. . . . . . . . . 10 ⊢ (0...(𝑁 − 1)) ∈ Fin
73		fzfi 12771	. . . . . . . . . 10 ⊢ (1...𝑁) ∈ Fin
74		hashen 13135	. . . . . . . . . 10 ⊢ (((0...(𝑁 − 1)) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((#‘(0...(𝑁 − 1))) = (#‘(1...𝑁)) ↔ (0...(𝑁 − 1)) ≈ (1...𝑁)))
75	72, 73, 74	mp2an 708	. . . . . . . . 9 ⊢ ((#‘(0...(𝑁 − 1))) = (#‘(1...𝑁)) ↔ (0...(𝑁 − 1)) ≈ (1...𝑁))
76	71, 75	sylibr 224	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → (#‘(0...(𝑁 − 1))) = (#‘(1...𝑁)))
77		hashfz1 13134	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → (#‘(1...𝑁)) = 𝑁)
78	76, 77	eqtrd 2656	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → (#‘(0...(𝑁 − 1))) = 𝑁)
79	78	adantr 481	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (#‘(0...(𝑁 − 1))) = 𝑁)
80	79	csbeq1d 3540	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → ⦋(#‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋𝑁 / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))))
81		elfznn0 12433	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ₀)
82		simpr 477	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → 𝑋 ∈ ℂ)
83		fveq2 6191	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘))
84	11, 83	sylan9eqr 2678	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑘 ∧ 𝑥 = 𝑋) → (wrecs( < , ℕ₀, (𝑔 ∈ V ↦ ⦋(#‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚) = (𝐹‘𝑘))
85		fvex 6201	. . . . . . . . . . 11 ⊢ (𝐹‘𝑘) ∈ V
86	84, 14, 85	ovmpt2a 6791	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝑘 BernPoly 𝑋) = (𝐹‘𝑘))
87	81, 82, 86	syl2anr 495	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑘 BernPoly 𝑋) = (𝐹‘𝑘))
88	87	oveq1d 6665	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)) = ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))
89	88	oveq2d 6666	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = ((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))
90	89	sumeq2dv 14433	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))
91	90	oveq2d 6666	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))))
92	68, 80, 91	3eqtr4d 2666	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → ⦋(#‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))
93	57, 92	syl5eq 2668	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝐺‘(𝐹 ↾ (0...(𝑁 − 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))
94	30, 93	eqtrd 2656	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝐺‘(𝐹 ↾ Pred( < , ℕ₀, 𝑁))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))
95	16, 26, 94	3eqtrd 2660	1 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝑁 BernPoly 𝑋) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 ∈ wcel 1990 Vcvv 3200 ⦋csb 3533 ⊆ wss 3574 class class class wbr 4653 ↦ cmpt 4729 Se wse 5071 We wwe 5072 dom cdm 5114 ↾ cres 5116 Predcpred 5679 Fun wfun 5882 Fn wfn 5883 ‘cfv 5888 (class class class)co 6650 wrecscwrecs 7406 ≈ cen 7952 Fincfn 7955 ℂcc 9934 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 − cmin 10266 / cdiv 10684 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ...cfz 12326 ↑cexp 12860 Ccbc 13089 #chash 13117 Σcsu 14416 BernPoly cbp 14777

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327 df-seq 12802 df-hash 13118 df-sum 14417 df-bpoly 14778

This theorem is referenced by: bpolyval 14780

W3C validator