Step | Hyp | Ref
| Expression |
1 | | dvntaylp0.m |
. . . . . . . . . . 11
β’ (π β π β (0...π)) |
2 | | elfz3nn0 13542 |
. . . . . . . . . . 11
β’ (π β (0...π) β π β
β0) |
3 | 1, 2 | syl 17 |
. . . . . . . . . 10
β’ (π β π β
β0) |
4 | 3 | nn0cnd 12482 |
. . . . . . . . 9
β’ (π β π β β) |
5 | | elfznn0 13541 |
. . . . . . . . . . 11
β’ (π β (0...π) β π β
β0) |
6 | 1, 5 | syl 17 |
. . . . . . . . . 10
β’ (π β π β
β0) |
7 | 6 | nn0cnd 12482 |
. . . . . . . . 9
β’ (π β π β β) |
8 | 4, 7 | npcand 11523 |
. . . . . . . 8
β’ (π β ((π β π) + π) = π) |
9 | 8 | oveq1d 7377 |
. . . . . . 7
β’ (π β (((π β π) + π)(π Tayl πΉ)π΅) = (π(π Tayl πΉ)π΅)) |
10 | | dvntaylp0.t |
. . . . . . 7
β’ π = (π(π Tayl πΉ)π΅) |
11 | 9, 10 | eqtr4di 2795 |
. . . . . 6
β’ (π β (((π β π) + π)(π Tayl πΉ)π΅) = π) |
12 | 11 | oveq2d 7378 |
. . . . 5
β’ (π β (β
Dπ (((π
β π) + π)(π Tayl πΉ)π΅)) = (β Dπ π)) |
13 | 12 | fveq1d 6849 |
. . . 4
β’ (π β ((β
Dπ (((π
β π) + π)(π Tayl πΉ)π΅))βπ) = ((β Dπ π)βπ)) |
14 | | dvntaylp0.s |
. . . . 5
β’ (π β π β {β, β}) |
15 | | dvntaylp0.f |
. . . . 5
β’ (π β πΉ:π΄βΆβ) |
16 | | dvntaylp0.a |
. . . . 5
β’ (π β π΄ β π) |
17 | | fznn0sub 13480 |
. . . . . 6
β’ (π β (0...π) β (π β π) β
β0) |
18 | 1, 17 | syl 17 |
. . . . 5
β’ (π β (π β π) β
β0) |
19 | | dvntaylp0.b |
. . . . . 6
β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) |
20 | 8 | fveq2d 6851 |
. . . . . . 7
β’ (π β ((π Dπ πΉ)β((π β π) + π)) = ((π Dπ πΉ)βπ)) |
21 | 20 | dmeqd 5866 |
. . . . . 6
β’ (π β dom ((π Dπ πΉ)β((π β π) + π)) = dom ((π Dπ πΉ)βπ)) |
22 | 19, 21 | eleqtrrd 2841 |
. . . . 5
β’ (π β π΅ β dom ((π Dπ πΉ)β((π β π) + π))) |
23 | 14, 15, 16, 6, 18, 22 | dvntaylp 25746 |
. . . 4
β’ (π β ((β
Dπ (((π
β π) + π)(π Tayl πΉ)π΅))βπ) = ((π β π)(π Tayl ((π Dπ πΉ)βπ))π΅)) |
24 | 13, 23 | eqtr3d 2779 |
. . 3
β’ (π β ((β
Dπ π)βπ) = ((π β π)(π Tayl ((π Dπ πΉ)βπ))π΅)) |
25 | 24 | fveq1d 6849 |
. 2
β’ (π β (((β
Dπ π)βπ)βπ΅) = (((π β π)(π Tayl ((π Dπ πΉ)βπ))π΅)βπ΅)) |
26 | | cnex 11139 |
. . . . . . 7
β’ β
β V |
27 | 26 | a1i 11 |
. . . . . 6
β’ (π β β β
V) |
28 | | elpm2r 8790 |
. . . . . 6
β’
(((β β V β§ π β {β, β}) β§ (πΉ:π΄βΆβ β§ π΄ β π)) β πΉ β (β βpm π)) |
29 | 27, 14, 15, 16, 28 | syl22anc 838 |
. . . . 5
β’ (π β πΉ β (β βpm π)) |
30 | | dvnf 25307 |
. . . . 5
β’ ((π β {β, β} β§
πΉ β (β
βpm π)
β§ π β
β0) β ((π Dπ πΉ)βπ):dom ((π Dπ πΉ)βπ)βΆβ) |
31 | 14, 29, 6, 30 | syl3anc 1372 |
. . . 4
β’ (π β ((π Dπ πΉ)βπ):dom ((π Dπ πΉ)βπ)βΆβ) |
32 | | dvnbss 25308 |
. . . . . . 7
β’ ((π β {β, β} β§
πΉ β (β
βpm π)
β§ π β
β0) β dom ((π Dπ πΉ)βπ) β dom πΉ) |
33 | 14, 29, 6, 32 | syl3anc 1372 |
. . . . . 6
β’ (π β dom ((π Dπ πΉ)βπ) β dom πΉ) |
34 | 15, 33 | fssdmd 6692 |
. . . . 5
β’ (π β dom ((π Dπ πΉ)βπ) β π΄) |
35 | 34, 16 | sstrd 3959 |
. . . 4
β’ (π β dom ((π Dπ πΉ)βπ) β π) |
36 | 18 | orcd 872 |
. . . 4
β’ (π β ((π β π) β β0 β¨ (π β π) = +β)) |
37 | | dvnadd 25309 |
. . . . . . . . 9
β’ (((π β {β, β} β§
πΉ β (β
βpm π))
β§ (π β
β0 β§ (π β π) β β0)) β
((π Dπ
((π Dπ
πΉ)βπ))β(π β π)) = ((π Dπ πΉ)β(π + (π β π)))) |
38 | 14, 29, 6, 18, 37 | syl22anc 838 |
. . . . . . . 8
β’ (π β ((π Dπ ((π Dπ πΉ)βπ))β(π β π)) = ((π Dπ πΉ)β(π + (π β π)))) |
39 | 7, 4 | pncan3d 11522 |
. . . . . . . . 9
β’ (π β (π + (π β π)) = π) |
40 | 39 | fveq2d 6851 |
. . . . . . . 8
β’ (π β ((π Dπ πΉ)β(π + (π β π))) = ((π Dπ πΉ)βπ)) |
41 | 38, 40 | eqtrd 2777 |
. . . . . . 7
β’ (π β ((π Dπ ((π Dπ πΉ)βπ))β(π β π)) = ((π Dπ πΉ)βπ)) |
42 | 41 | dmeqd 5866 |
. . . . . 6
β’ (π β dom ((π Dπ ((π Dπ πΉ)βπ))β(π β π)) = dom ((π Dπ πΉ)βπ)) |
43 | 19, 42 | eleqtrrd 2841 |
. . . . 5
β’ (π β π΅ β dom ((π Dπ ((π Dπ πΉ)βπ))β(π β π))) |
44 | 14, 31, 35, 18, 43 | taylplem1 25738 |
. . . 4
β’ ((π β§ π β ((0[,](π β π)) β© β€)) β π΅ β dom ((π Dπ ((π Dπ πΉ)βπ))βπ)) |
45 | | eqid 2737 |
. . . 4
β’ ((π β π)(π Tayl ((π Dπ πΉ)βπ))π΅) = ((π β π)(π Tayl ((π Dπ πΉ)βπ))π΅) |
46 | 14, 31, 35, 36, 44, 45 | tayl0 25737 |
. . 3
β’ (π β (π΅ β dom ((π β π)(π Tayl ((π Dπ πΉ)βπ))π΅) β§ (((π β π)(π Tayl ((π Dπ πΉ)βπ))π΅)βπ΅) = (((π Dπ πΉ)βπ)βπ΅))) |
47 | 46 | simprd 497 |
. 2
β’ (π β (((π β π)(π Tayl ((π Dπ πΉ)βπ))π΅)βπ΅) = (((π Dπ πΉ)βπ)βπ΅)) |
48 | 25, 47 | eqtrd 2777 |
1
β’ (π β (((β
Dπ π)βπ)βπ΅) = (((π Dπ πΉ)βπ)βπ΅)) |