| Step | Hyp | Ref
| Expression |
|---|
| 1 | | taylfval.s |
. . . . . 6
β’ (π β π β {β, β}) |
| 2 | 1 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π β {β, β}) |
| 3 | | cnex 11205 |
. . . . . . . 8
β’ β
β V |
| 4 | 3 | a1i 11 |
. . . . . . 7
β’ (π β β β
V) |
| 5 | | taylfval.f |
. . . . . . 7
β’ (π β πΉ:π΄βΆβ) |
| 6 | | taylfval.a |
. . . . . . 7
β’ (π β π΄ β π) |
| 7 | | elpm2r 8853 |
. . . . . . 7
β’
(((β β V β§ π β {β, β}) β§ (πΉ:π΄βΆβ β§ π΄ β π)) β πΉ β (β βpm π)) |
| 8 | 4, 1, 5, 6, 7 | syl22anc 838 |
. . . . . 6
β’ (π β πΉ β (β βpm π)) |
| 9 | 8 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β πΉ β (β βpm π)) |
| 10 | | simpr 484 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π β ((0[,]π) β© β€)) |
| 11 | 10 | elin2d 4195 |
. . . . . 6
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π β β€) |
| 12 | 10 | elin1d 4194 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π β (0[,]π)) |
| 13 | | 0xr 11277 |
. . . . . . . . 9
β’ 0 β
β* |
| 14 | | taylfval.n |
. . . . . . . . . . 11
β’ (π β (π β β0 β¨ π = +β)) |
| 15 | | nn0re 12497 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β) |
| 16 | 15 | rexrd 11280 |
. . . . . . . . . . . 12
β’ (π β β0
β π β
β*) |
| 17 | | id 22 |
. . . . . . . . . . . . 13
β’ (π = +β β π = +β) |
| 18 | | pnfxr 11284 |
. . . . . . . . . . . . 13
β’ +β
β β* |
| 19 | 17, 18 | eqeltrdi 2836 |
. . . . . . . . . . . 12
β’ (π = +β β π β
β*) |
| 20 | 16, 19 | jaoi 856 |
. . . . . . . . . . 11
β’ ((π β β0 β¨
π = +β) β π β
β*) |
| 21 | 14, 20 | syl 17 |
. . . . . . . . . 10
β’ (π β π β
β*) |
| 22 | 21 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π β
β*) |
| 23 | | elicc1 13386 |
. . . . . . . . 9
β’ ((0
β β* β§ π β β*) β (π β (0[,]π) β (π β β* β§ 0 β€
π β§ π β€ π))) |
| 24 | 13, 22, 23 | sylancr 586 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (π β (0[,]π) β (π β β* β§ 0 β€
π β§ π β€ π))) |
| 25 | 12, 24 | mpbid 231 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (π β β* β§ 0 β€
π β§ π β€ π)) |
| 26 | 25 | simp2d 1141 |
. . . . . 6
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β 0 β€ π) |
| 27 | | elnn0z 12587 |
. . . . . 6
β’ (π β β0
β (π β β€
β§ 0 β€ π)) |
| 28 | 11, 26, 27 | sylanbrc 582 |
. . . . 5
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π β β0) |
| 29 | | dvnf 25831 |
. . . . 5
β’ ((π β {β, β} β§
πΉ β (β
βpm π)
β§ π β
β0) β ((π Dπ πΉ)βπ):dom ((π Dπ πΉ)βπ)βΆβ) |
| 30 | 2, 9, 28, 29 | syl3anc 1369 |
. . . 4
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β ((π Dπ πΉ)βπ):dom ((π Dπ πΉ)βπ)βΆβ) |
| 31 | | taylfval.b |
. . . . 5
β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) |
| 32 | 31 | adantlr 714 |
. . . 4
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) |
| 33 | 30, 32 | ffvelcdmd 7089 |
. . 3
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (((π Dπ πΉ)βπ)βπ΅) β β) |
| 34 | 28 | faccld 14261 |
. . . 4
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (!βπ) β
β) |
| 35 | 34 | nncnd 12244 |
. . 3
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (!βπ) β
β) |
| 36 | 34 | nnne0d 12278 |
. . 3
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (!βπ) β 0) |
| 37 | 33, 35, 36 | divcld 12006 |
. 2
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β ((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) β β) |
| 38 | | simplr 768 |
. . . 4
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π β β) |
| 39 | 5 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β πΉ:π΄βΆβ) |
| 40 | | dvnbss 25832 |
. . . . . . . 8
β’ ((π β {β, β} β§
πΉ β (β
βpm π)
β§ π β
β0) β dom ((π Dπ πΉ)βπ) β dom πΉ) |
| 41 | 2, 9, 28, 40 | syl3anc 1369 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β dom ((π Dπ πΉ)βπ) β dom πΉ) |
| 42 | 39, 41 | fssdmd 6735 |
. . . . . 6
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β dom ((π Dπ πΉ)βπ) β π΄) |
| 43 | | recnprss 25807 |
. . . . . . . . 9
β’ (π β {β, β}
β π β
β) |
| 44 | 1, 43 | syl 17 |
. . . . . . . 8
β’ (π β π β β) |
| 45 | 6, 44 | sstrd 3988 |
. . . . . . 7
β’ (π β π΄ β β) |
| 46 | 45 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π΄ β β) |
| 47 | 42, 46 | sstrd 3988 |
. . . . 5
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β dom ((π Dπ πΉ)βπ) β β) |
| 48 | 47, 32 | sseldd 3979 |
. . . 4
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β π΅ β β) |
| 49 | 38, 48 | subcld 11587 |
. . 3
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (π β π΅) β β) |
| 50 | 49, 28 | expcld 14128 |
. 2
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β ((π β π΅)βπ) β β) |
| 51 | 37, 50 | mulcld 11250 |
1
β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π β π΅)βπ)) β β) |
