Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  taylplem1 Structured version   Unicode version

Theorem taylplem1 20279
 Description: Lemma for taylpfval 20281 and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016.)
Hypotheses
Ref Expression
taylpfval.s
taylpfval.f
taylpfval.a
taylpfval.n
taylpfval.b
Assertion
Ref Expression
taylplem1
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem taylplem1
StepHypRef Expression
1 0z 10293 . . . . 5
2 taylpfval.n . . . . . 6
32nn0zd 10373 . . . . 5
4 fzval2 11046 . . . . 5
51, 3, 4sylancr 645 . . . 4
65eleq2d 2503 . . 3
76biimpar 472 . 2
8 taylpfval.s . . . . 5
9 cnex 9071 . . . . . . 7
109a1i 11 . . . . . 6
11 taylpfval.f . . . . . 6
12 taylpfval.a . . . . . 6
13 elpm2r 7034 . . . . . 6
1410, 8, 11, 12, 13syl22anc 1185 . . . . 5
158, 14jca 519 . . . 4
16 dvn2bss 19816 . . . . 5
17163expa 1153 . . . 4
1815, 17sylan 458 . . 3
19 taylpfval.b . . . 4