Theorem taylfvallem

Description: Lemma for taylfval . (Contributed by Mario Carneiro, 30-Dec-2016)

	Ref	Expression
Hypotheses	taylfval.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	taylfval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	taylfval.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
	taylfval.n	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) )
	taylfval.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
Assertion	taylfvallem	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) → ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) ) ) ⊆ ℂ )

Proof

Step	Hyp	Ref	Expression
1		taylfval.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		taylfval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
3		taylfval.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
4		taylfval.n	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) )
5		taylfval.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
6		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
7		cnring	⊢ ℂfld ∈ Ring
8		ringcmn	⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
9	7 8	mp1i	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) → ℂfld ∈ CMnd )
10		cnfldtps	⊢ ℂfld ∈ TopSp
11	10	a1i	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) → ℂfld ∈ TopSp )
12		ovex	⊢ ( 0 [,] 𝑁 ) ∈ V
13	12	inex1	⊢ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∈ V
14	13	a1i	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) → ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∈ V )
15	1 2 3 4 5	taylfvallem1	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) ∈ ℂ )
16	15	fmpttd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) → ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) ) : ( ( 0 [,] 𝑁 ) ∩ ℤ ) ⟶ ℂ )
17	6 9 11 14 16	tsmscl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) → ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) ) ) ⊆ ℂ )