Step | Hyp | Ref
| Expression |
1 | | taylfval.s |
. . . . . 6
β’ (π β π β {β, β}) |
2 | 1 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π β {β, β}) |
3 | | cnex 11139 |
. . . . . . . 8
β’ β
β V |
4 | 3 | a1i 11 |
. . . . . . 7
β’ (π β β β
V) |
5 | | taylfval.f |
. . . . . . 7
β’ (π β πΉ:π΄βΆβ) |
6 | | taylfval.a |
. . . . . . 7
β’ (π β π΄ β π) |
7 | | elpm2r 8790 |
. . . . . . 7
β’
(((β β V β§ π β {β, β}) β§ (πΉ:π΄βΆβ β§ π΄ β π)) β πΉ β (β βpm π)) |
8 | 4, 1, 5, 6, 7 | syl22anc 838 |
. . . . . 6
β’ (π β πΉ β (β βpm π)) |
9 | 8 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β πΉ β (β βpm π)) |
10 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π β ((0[,]π) β© β€)) |
11 | 10 | elin2d 4164 |
. . . . . 6
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π β β€) |
12 | 10 | elin1d 4163 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π β (0[,]π)) |
13 | | 0xr 11209 |
. . . . . . . . 9
β’ 0 β
β* |
14 | | taylfval.n |
. . . . . . . . . . 11
β’ (π β (π β β0 β¨ π = +β)) |
15 | | nn0re 12429 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β) |
16 | 15 | rexrd 11212 |
. . . . . . . . . . . 12
β’ (π β β0
β π β
β*) |
17 | | id 22 |
. . . . . . . . . . . . 13
β’ (π = +β β π = +β) |
18 | | pnfxr 11216 |
. . . . . . . . . . . . 13
β’ +β
β β* |
19 | 17, 18 | eqeltrdi 2846 |
. . . . . . . . . . . 12
β’ (π = +β β π β
β*) |
20 | 16, 19 | jaoi 856 |
. . . . . . . . . . 11
β’ ((π β β0 β¨
π = +β) β π β
β*) |
21 | 14, 20 | syl 17 |
. . . . . . . . . 10
β’ (π β π β
β*) |
22 | 21 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π β
β*) |
23 | | elicc1 13315 |
. . . . . . . . 9
β’ ((0
β β* β§ π β β*) β (π β (0[,]π) β (π β β* β§ 0 β€
π β§ π β€ π))) |
24 | 13, 22, 23 | sylancr 588 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (π β (0[,]π) β (π β β* β§ 0 β€
π β§ π β€ π))) |
25 | 12, 24 | mpbid 231 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (π β β* β§ 0 β€
π β§ π β€ π)) |
26 | 25 | simp2d 1144 |
. . . . . 6
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β 0 β€ π) |
27 | | elnn0z 12519 |
. . . . . 6
β’ (π β β0
β (π β β€
β§ 0 β€ π)) |
28 | 11, 26, 27 | sylanbrc 584 |
. . . . 5
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π β β0) |
29 | | dvnf 25307 |
. . . . 5
β’ ((π β {β, β} β§
πΉ β (β
βpm π)
β§ π β
β0) β ((π Dπ πΉ)βπ):dom ((π Dπ πΉ)βπ)βΆβ) |
30 | 2, 9, 28, 29 | syl3anc 1372 |
. . . 4
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β ((π Dπ πΉ)βπ):dom ((π Dπ πΉ)βπ)βΆβ) |
31 | | taylfval.b |
. . . . 5
β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) |
32 | 31 | adantlr 714 |
. . . 4
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) |
33 | 30, 32 | ffvelcdmd 7041 |
. . 3
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (((π Dπ πΉ)βπ)βπ΅) β β) |
34 | 28 | faccld 14191 |
. . . 4
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (!βπ) β
β) |
35 | 34 | nncnd 12176 |
. . 3
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (!βπ) β
β) |
36 | 34 | nnne0d 12210 |
. . 3
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (!βπ) β 0) |
37 | 33, 35, 36 | divcld 11938 |
. 2
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β ((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) β β) |
38 | | simplr 768 |
. . . 4
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π β β) |
39 | 5 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β πΉ:π΄βΆβ) |
40 | | dvnbss 25308 |
. . . . . . . 8
β’ ((π β {β, β} β§
πΉ β (β
βpm π)
β§ π β
β0) β dom ((π Dπ πΉ)βπ) β dom πΉ) |
41 | 2, 9, 28, 40 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β dom ((π Dπ πΉ)βπ) β dom πΉ) |
42 | 39, 41 | fssdmd 6692 |
. . . . . 6
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β dom ((π Dπ πΉ)βπ) β π΄) |
43 | | recnprss 25284 |
. . . . . . . . 9
β’ (π β {β, β}
β π β
β) |
44 | 1, 43 | syl 17 |
. . . . . . . 8
β’ (π β π β β) |
45 | 6, 44 | sstrd 3959 |
. . . . . . 7
β’ (π β π΄ β β) |
46 | 45 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π΄ β β) |
47 | 42, 46 | sstrd 3959 |
. . . . 5
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β dom ((π Dπ πΉ)βπ) β β) |
48 | 47, 32 | sseldd 3950 |
. . . 4
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π΅ β β) |
49 | 38, 48 | subcld 11519 |
. . 3
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (π β π΅) β β) |
50 | 49, 28 | expcld 14058 |
. 2
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β ((π β π΅)βπ) β β) |
51 | 37, 50 | mulcld 11182 |
1
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π β π΅)βπ)) β β) |