Theorem taylfvallem1

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	taylfvallem1	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 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	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝑆 ∈ { ℝ , ℂ } )
7		cnex	⊢ ℂ ∈ V
8	7	a1i	⊢ ( 𝜑 → ℂ ∈ V )
9		elpm2r	⊢ ( ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
10	8 1 2 3 9	syl22anc	⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
11	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
12		simpr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) )
13	12	elin2d	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝑘 ∈ ℤ )
14	12	elin1d	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝑘 ∈ ( 0 [,] 𝑁 ) )
15		0xr	⊢ 0 ∈ ℝ*
16		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
17	16	rexrd	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ* )
18		id	⊢ ( 𝑁 = +∞ → 𝑁 = +∞ )
19		pnfxr	⊢ +∞ ∈ ℝ*
20	18 19	eqeltrdi	⊢ ( 𝑁 = +∞ → 𝑁 ∈ ℝ* )
21	17 20	jaoi	⊢ ( ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) → 𝑁 ∈ ℝ* )
22	4 21	syl	⊢ ( 𝜑 → 𝑁 ∈ ℝ* )
23	22	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝑁 ∈ ℝ* )
24		elicc1	⊢ ( ( 0 ∈ ℝ* ∧ 𝑁 ∈ ℝ* ) → ( 𝑘 ∈ ( 0 [,] 𝑁 ) ↔ ( 𝑘 ∈ ℝ* ∧ 0 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) )
25	15 23 24	sylancr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( 𝑘 ∈ ( 0 [,] 𝑁 ) ↔ ( 𝑘 ∈ ℝ* ∧ 0 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) ) )
26	14 25	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( 𝑘 ∈ ℝ* ∧ 0 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁 ) )
27	26	simp2d	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 0 ≤ 𝑘 )
28		elnn0z	⊢ ( 𝑘 ∈ ℕ0 ↔ ( 𝑘 ∈ ℤ ∧ 0 ≤ 𝑘 ) )
29	13 27 28	sylanbrc	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝑘 ∈ ℕ0 )
30		dvnf	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ⟶ ℂ )
31	6 11 29 30	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) : dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ⟶ ℂ )
32	5	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
33	31 32	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) ∈ ℂ )
34	29	faccld	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ! ‘ 𝑘 ) ∈ ℕ )
35	34	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ! ‘ 𝑘 ) ∈ ℂ )
36	34	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ! ‘ 𝑘 ) ≠ 0 )
37	33 35 36	divcld	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
38		simplr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝑋 ∈ ℂ )
39	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐹 : 𝐴 ⟶ ℂ )
40		dvnbss	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ⊆ dom 𝐹 )
41	6 11 29 40	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ⊆ dom 𝐹 )
42	39 41	fssdmd	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ⊆ 𝐴 )
43		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
44	1 43	syl	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
45	3 44	sstrd	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
46	45	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐴 ⊆ ℂ )
47	42 46	sstrd	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ⊆ ℂ )
48	47 32	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐵 ∈ ℂ )
49	38 48	subcld	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( 𝑋 − 𝐵 ) ∈ ℂ )
50	49 29	expcld	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ∈ ℂ )
51	37 50	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) ∈ ℂ )