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 15988

Description: Lemma for bpolyval 15989. (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 7412	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (𝑥↑𝑛) = (𝑋↑𝑛))
2	1	oveq1d 7420	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))
3	2	csbeq2dv 3899	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))
4	3	mpteq2dv 5249	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) = (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))
5		bpoly.1	. . . . . . . 8 ⊢ 𝐺 = (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))
6	4, 5	eqtr4di 2790	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) = 𝐺)
7		wrecseq3 8301	. . . . . . 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	eqtr4di 2790	. . . . 5 ⊢ (𝑥 = 𝑋 → wrecs( < , ℕ₀, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))) = 𝐹)
11	10	fveq1d 6890	. . . 4 ⊢ (𝑥 = 𝑋 → (wrecs( < , ℕ₀, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚) = (𝐹‘𝑚))
12		fveq2 6888	. . . 4 ⊢ (𝑚 = 𝑁 → (𝐹‘𝑚) = (𝐹‘𝑁))
13	11, 12	sylan9eqr 2794	. . 3 ⊢ ((𝑚 = 𝑁 ∧ 𝑥 = 𝑋) → (wrecs( < , ℕ₀, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚) = (𝐹‘𝑁))
14		df-bpoly 15987	. . 3 ⊢ BernPoly = (𝑚 ∈ ℕ₀, 𝑥 ∈ ℂ ↦ (wrecs( < , ℕ₀, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚))
15		fvex 6901	. . 3 ⊢ (𝐹‘𝑁) ∈ V
16	13, 14, 15	ovmpoa 7559	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝑁 BernPoly 𝑋) = (𝐹‘𝑁))
17		ltweuz 13922	. . . . 5 ⊢ < We (ℤ_≥‘0)
18		nn0uz 12860	. . . . . 6 ⊢ ℕ₀ = (ℤ_≥‘0)
19		weeq2 5664	. . . . . 6 ⊢ (ℕ₀ = (ℤ_≥‘0) → ( < We ℕ₀ ↔ < We (ℤ_≥‘0)))
20	18, 19	ax-mp 5	. . . . 5 ⊢ ( < We ℕ₀ ↔ < We (ℤ_≥‘0))
21	17, 20	mpbir 230	. . . 4 ⊢ < We ℕ₀
22		nn0ex 12474	. . . . 5 ⊢ ℕ₀ ∈ V
23		exse 5638	. . . . 5 ⊢ (ℕ₀ ∈ V → < Se ℕ₀)
24	22, 23	ax-mp 5	. . . 4 ⊢ < Se ℕ₀
25	9	wfr2 8332	. . . 4 ⊢ ((( < We ℕ₀ ∧ < Se ℕ₀) ∧ 𝑁 ∈ ℕ₀) → (𝐹‘𝑁) = (𝐺‘(𝐹 ↾ Pred( < , ℕ₀, 𝑁))))
26	21, 24, 25	mpanl12 700	. . 3 ⊢ (𝑁 ∈ ℕ₀ → (𝐹‘𝑁) = (𝐺‘(𝐹 ↾ Pred( < , ℕ₀, 𝑁))))
27	26	adantr 481	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝐹‘𝑁) = (𝐺‘(𝐹 ↾ Pred( < , ℕ₀, 𝑁))))
28		prednn0 13621	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → Pred( < , ℕ₀, 𝑁) = (0...(𝑁 − 1)))
29	28	adantr 481	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → Pred( < , ℕ₀, 𝑁) = (0...(𝑁 − 1)))
30	29	reseq2d 5979	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝐹 ↾ Pred( < , ℕ₀, 𝑁)) = (𝐹 ↾ (0...(𝑁 − 1))))
31	30	fveq2d 6892	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝐺‘(𝐹 ↾ Pred( < , ℕ₀, 𝑁))) = (𝐺‘(𝐹 ↾ (0...(𝑁 − 1)))))
32	9	wfrfun 8328	. . . . . . 7 ⊢ (( < We ℕ₀ ∧ < Se ℕ₀) → Fun 𝐹)
33	21, 24, 32	mp2an 690	. . . . . 6 ⊢ Fun 𝐹
34		ovex 7438	. . . . . 6 ⊢ (0...(𝑁 − 1)) ∈ V
35		resfunexg 7213	. . . . . 6 ⊢ ((Fun 𝐹 ∧ (0...(𝑁 − 1)) ∈ V) → (𝐹 ↾ (0...(𝑁 − 1))) ∈ V)
36	33, 34, 35	mp2an 690	. . . . 5 ⊢ (𝐹 ↾ (0...(𝑁 − 1))) ∈ V
37		dmeq 5901	. . . . . . . . 9 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → dom 𝑔 = dom (𝐹 ↾ (0...(𝑁 − 1))))
38	9	wfr1 8331	. . . . . . . . . . . 12 ⊢ (( < We ℕ₀ ∧ < Se ℕ₀) → 𝐹 Fn ℕ₀)
39	21, 24, 38	mp2an 690	. . . . . . . . . . 11 ⊢ 𝐹 Fn ℕ₀
40		fz0ssnn0 13592	. . . . . . . . . . 11 ⊢ (0...(𝑁 − 1)) ⊆ ℕ₀
41		fnssres 6670	. . . . . . . . . . 11 ⊢ ((𝐹 Fn ℕ₀ ∧ (0...(𝑁 − 1)) ⊆ ℕ₀) → (𝐹 ↾ (0...(𝑁 − 1))) Fn (0...(𝑁 − 1)))
42	39, 40, 41	mp2an 690	. . . . . . . . . 10 ⊢ (𝐹 ↾ (0...(𝑁 − 1))) Fn (0...(𝑁 − 1))
43	42	fndmi 6650	. . . . . . . . 9 ⊢ dom (𝐹 ↾ (0...(𝑁 − 1))) = (0...(𝑁 − 1))
44	37, 43	eqtrdi 2788	. . . . . . . 8 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → dom 𝑔 = (0...(𝑁 − 1)))
45	44	fveq2d 6892	. . . . . . 7 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → (♯‘dom 𝑔) = (♯‘(0...(𝑁 − 1))))
46		fveq1 6887	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → (𝑔‘𝑘) = ((𝐹 ↾ (0...(𝑁 − 1)))‘𝑘))
47		fvres 6907	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝐹 ↾ (0...(𝑁 − 1)))‘𝑘) = (𝐹‘𝑘))
48	46, 47	sylan9eq 2792	. . . . . . . . . . 11 ⊢ ((𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑔‘𝑘) = (𝐹‘𝑘))
49	48	oveq1d 7420	. . . . . . . . . 10 ⊢ ((𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)) = ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))
50	49	oveq2d 7421	. . . . . . . . 9 ⊢ ((𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))) = ((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))
51	44, 50	sumeq12rdv 15649	. . . . . . . 8 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))
52	51	oveq2d 7421	. . . . . . 7 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → ((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))))
53	45, 52	csbeq12dv 3901	. . . . . 6 ⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))))
54		ovex 7438	. . . . . . 7 ⊢ ((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) ∈ V
55	54	csbex 5310	. . . . . 6 ⊢ ⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) ∈ V
56	53, 5, 55	fvmpt 6995	. . . . 5 ⊢ ((𝐹 ↾ (0...(𝑁 − 1))) ∈ V → (𝐺‘(𝐹 ↾ (0...(𝑁 − 1)))) = ⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))))
57	36, 56	ax-mp 5	. . . 4 ⊢ (𝐺‘(𝐹 ↾ (0...(𝑁 − 1)))) = ⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))
58		nfcvd 2904	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → Ⅎ𝑛((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))))
59		oveq2 7413	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → (𝑋↑𝑛) = (𝑋↑𝑁))
60		oveq1 7412	. . . . . . . . . 10 ⊢ (𝑛 = 𝑁 → (𝑛C𝑘) = (𝑁C𝑘))
61		oveq1 7412	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑁 → (𝑛 − 𝑘) = (𝑁 − 𝑘))
62	61	oveq1d 7420	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑁 → ((𝑛 − 𝑘) + 1) = ((𝑁 − 𝑘) + 1))
63	62	oveq2d 7421	. . . . . . . . . 10 ⊢ (𝑛 = 𝑁 → ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)) = ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))
64	60, 63	oveq12d 7423	. . . . . . . . 9 ⊢ (𝑛 = 𝑁 → ((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))) = ((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))
65	64	sumeq2sdv 15646	. . . . . . . 8 ⊢ (𝑛 = 𝑁 → Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))
66	59, 65	oveq12d 7423	. . . . . . 7 ⊢ (𝑛 = 𝑁 → ((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))))
67	58, 66	csbiegf 3926	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ⦋𝑁 / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))))
68	67	adantr 481	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → ⦋𝑁 / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))))
69		nn0z 12579	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
70		fz01en 13525	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℤ → (0...(𝑁 − 1)) ≈ (1...𝑁))
71	69, 70	syl 17	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (0...(𝑁 − 1)) ≈ (1...𝑁))
72		fzfi 13933	. . . . . . . . . 10 ⊢ (0...(𝑁 − 1)) ∈ Fin
73		fzfi 13933	. . . . . . . . . 10 ⊢ (1...𝑁) ∈ Fin
74		hashen 14303	. . . . . . . . . 10 ⊢ (((0...(𝑁 − 1)) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((♯‘(0...(𝑁 − 1))) = (♯‘(1...𝑁)) ↔ (0...(𝑁 − 1)) ≈ (1...𝑁)))
75	72, 73, 74	mp2an 690	. . . . . . . . 9 ⊢ ((♯‘(0...(𝑁 − 1))) = (♯‘(1...𝑁)) ↔ (0...(𝑁 − 1)) ≈ (1...𝑁))
76	71, 75	sylibr 233	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(0...(𝑁 − 1))) = (♯‘(1...𝑁)))
77		hashfz1 14302	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(1...𝑁)) = 𝑁)
78	76, 77	eqtrd 2772	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(0...(𝑁 − 1))) = 𝑁)
79	78	adantr 481	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (♯‘(0...(𝑁 − 1))) = 𝑁)
80	79	csbeq1d 3896	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → ⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋𝑁 / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))))
81		elfznn0 13590	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ₀)
82		simpr 485	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → 𝑋 ∈ ℂ)
83		fveq2 6888	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘))
84	11, 83	sylan9eqr 2794	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑘 ∧ 𝑥 = 𝑋) → (wrecs( < , ℕ₀, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚) = (𝐹‘𝑘))
85		fvex 6901	. . . . . . . . . . 11 ⊢ (𝐹‘𝑘) ∈ V
86	84, 14, 85	ovmpoa 7559	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝑘 BernPoly 𝑋) = (𝐹‘𝑘))
87	81, 82, 86	syl2anr 597	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑘 BernPoly 𝑋) = (𝐹‘𝑘))
88	87	oveq1d 7420	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)) = ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))
89	88	oveq2d 7421	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = ((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))
90	89	sumeq2dv 15645	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))
91	90	oveq2d 7421	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))))
92	68, 80, 91	3eqtr4d 2782	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → ⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))
93	57, 92	eqtrid 2784	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝐺‘(𝐹 ↾ (0...(𝑁 − 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))
94	31, 93	eqtrd 2772	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝐺‘(𝐹 ↾ Pred( < , ℕ₀, 𝑁))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))
95	16, 27, 94	3eqtrd 2776	1 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝑁 BernPoly 𝑋) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 Vcvv 3474 ⦋csb 3892 ⊆ wss 3947 class class class wbr 5147 ↦ cmpt 5230 Se wse 5628 We wwe 5629 dom cdm 5675 ↾ cres 5677 Predcpred 6296 Fun wfun 6534 Fn wfn 6535 ‘cfv 6540 (class class class)co 7405 wrecscwrecs 8292 ≈ cen 8932 Fincfn 8935 ℂcc 11104 0cc0 11106 1c1 11107 + caddc 11109 · cmul 11111 < clt 11244 − cmin 11440 / cdiv 11867 ℕ₀cn0 12468 ℤcz 12554 ℤ_≥cuz 12818 ...cfz 13480 ↑cexp 14023 Ccbc 14258 ♯chash 14286 Σcsu 15628 BernPoly cbp 15986

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-inf2 9632 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7852 df-1st 7971 df-2nd 7972 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-1o 8462 df-er 8699 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-card 9930 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-nn 12209 df-n0 12469 df-z 12555 df-uz 12819 df-fz 13481 df-seq 13963 df-hash 14287 df-sum 15629 df-bpoly 15987

This theorem is referenced by: bpolyval 15989

W3C validator