Metamath Proof Explorer


Theorem taylplem2

Description: Lemma for taylpfval and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016)

Ref Expression
Hypotheses taylpfval.s φS
taylpfval.f φF:A
taylpfval.a φAS
taylpfval.n φN0
taylpfval.b φBdomSDnFN
Assertion taylplem2 φXk0NSDnFkBk!XBk

Proof

Step Hyp Ref Expression
1 taylpfval.s φS
2 taylpfval.f φF:A
3 taylpfval.a φAS
4 taylpfval.n φN0
5 taylpfval.b φBdomSDnFN
6 0z 0
7 4 nn0zd φN
8 fzval2 0N0N=0N
9 6 7 8 sylancr φ0N=0N
10 9 eleq2d φk0Nk0N
11 10 adantr φXk0Nk0N
12 11 biimpa φXk0Nk0N
13 4 orcd φN0N=+∞
14 1 2 3 4 5 taylplem1 φk0NBdomSDnFk
15 1 2 3 13 14 taylfvallem1 φXk0NSDnFkBk!XBk
16 12 15 syldan φXk0NSDnFkBk!XBk