Step | Hyp | Ref
| Expression |
1 | | dvntaylp.m |
. . . . 5
β’ (π β π β
β0) |
2 | | nn0uz 12812 |
. . . . 5
β’
β0 = (β€β₯β0) |
3 | 1, 2 | eleqtrdi 2848 |
. . . 4
β’ (π β π β
(β€β₯β0)) |
4 | | eluzfz2b 13457 |
. . . 4
β’ (π β
(β€β₯β0) β π β (0...π)) |
5 | 3, 4 | sylib 217 |
. . 3
β’ (π β π β (0...π)) |
6 | | fveq2 6847 |
. . . . . 6
β’ (π = 0 β ((β
Dπ ((π +
π)(π Tayl πΉ)π΅))βπ) = ((β Dπ ((π + π)(π Tayl πΉ)π΅))β0)) |
7 | | fveq2 6847 |
. . . . . . . 8
β’ (π = 0 β ((π Dπ πΉ)βπ) = ((π Dπ πΉ)β0)) |
8 | 7 | oveq2d 7378 |
. . . . . . 7
β’ (π = 0 β (π Tayl ((π Dπ πΉ)βπ)) = (π Tayl ((π Dπ πΉ)β0))) |
9 | | oveq2 7370 |
. . . . . . . 8
β’ (π = 0 β (π β π) = (π β 0)) |
10 | 9 | oveq2d 7378 |
. . . . . . 7
β’ (π = 0 β (π + (π β π)) = (π + (π β 0))) |
11 | | eqidd 2738 |
. . . . . . 7
β’ (π = 0 β π΅ = π΅) |
12 | 8, 10, 11 | oveq123d 7383 |
. . . . . 6
β’ (π = 0 β ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅) = ((π + (π β 0))(π Tayl ((π Dπ πΉ)β0))π΅)) |
13 | 6, 12 | eqeq12d 2753 |
. . . . 5
β’ (π = 0 β (((β
Dπ ((π +
π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅) β ((β Dπ
((π + π)(π Tayl πΉ)π΅))β0) = ((π + (π β 0))(π Tayl ((π Dπ πΉ)β0))π΅))) |
14 | 13 | imbi2d 341 |
. . . 4
β’ (π = 0 β ((π β ((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅)) β (π β ((β Dπ
((π + π)(π Tayl πΉ)π΅))β0) = ((π + (π β 0))(π Tayl ((π Dπ πΉ)β0))π΅)))) |
15 | | fveq2 6847 |
. . . . . 6
β’ (π = π β ((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((β Dπ ((π + π)(π Tayl πΉ)π΅))βπ)) |
16 | | fveq2 6847 |
. . . . . . . 8
β’ (π = π β ((π Dπ πΉ)βπ) = ((π Dπ πΉ)βπ)) |
17 | 16 | oveq2d 7378 |
. . . . . . 7
β’ (π = π β (π Tayl ((π Dπ πΉ)βπ)) = (π Tayl ((π Dπ πΉ)βπ))) |
18 | | oveq2 7370 |
. . . . . . . 8
β’ (π = π β (π β π) = (π β π)) |
19 | 18 | oveq2d 7378 |
. . . . . . 7
β’ (π = π β (π + (π β π)) = (π + (π β π))) |
20 | | eqidd 2738 |
. . . . . . 7
β’ (π = π β π΅ = π΅) |
21 | 17, 19, 20 | oveq123d 7383 |
. . . . . 6
β’ (π = π β ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅)) |
22 | 15, 21 | eqeq12d 2753 |
. . . . 5
β’ (π = π β (((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅) β ((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅))) |
23 | 22 | imbi2d 341 |
. . . 4
β’ (π = π β ((π β ((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅)) β (π β ((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅)))) |
24 | | fveq2 6847 |
. . . . . 6
β’ (π = (π + 1) β ((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((β Dπ ((π + π)(π Tayl πΉ)π΅))β(π + 1))) |
25 | | fveq2 6847 |
. . . . . . . 8
β’ (π = (π + 1) β ((π Dπ πΉ)βπ) = ((π Dπ πΉ)β(π + 1))) |
26 | 25 | oveq2d 7378 |
. . . . . . 7
β’ (π = (π + 1) β (π Tayl ((π Dπ πΉ)βπ)) = (π Tayl ((π Dπ πΉ)β(π + 1)))) |
27 | | oveq2 7370 |
. . . . . . . 8
β’ (π = (π + 1) β (π β π) = (π β (π + 1))) |
28 | 27 | oveq2d 7378 |
. . . . . . 7
β’ (π = (π + 1) β (π + (π β π)) = (π + (π β (π + 1)))) |
29 | | eqidd 2738 |
. . . . . . 7
β’ (π = (π + 1) β π΅ = π΅) |
30 | 26, 28, 29 | oveq123d 7383 |
. . . . . 6
β’ (π = (π + 1) β ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅) = ((π + (π β (π + 1)))(π Tayl ((π Dπ πΉ)β(π + 1)))π΅)) |
31 | 24, 30 | eqeq12d 2753 |
. . . . 5
β’ (π = (π + 1) β (((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅) β ((β Dπ
((π + π)(π Tayl πΉ)π΅))β(π + 1)) = ((π + (π β (π + 1)))(π Tayl ((π Dπ πΉ)β(π + 1)))π΅))) |
32 | 31 | imbi2d 341 |
. . . 4
β’ (π = (π + 1) β ((π β ((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅)) β (π β ((β Dπ
((π + π)(π Tayl πΉ)π΅))β(π + 1)) = ((π + (π β (π + 1)))(π Tayl ((π Dπ πΉ)β(π + 1)))π΅)))) |
33 | | fveq2 6847 |
. . . . . 6
β’ (π = π β ((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((β Dπ ((π + π)(π Tayl πΉ)π΅))βπ)) |
34 | | fveq2 6847 |
. . . . . . . 8
β’ (π = π β ((π Dπ πΉ)βπ) = ((π Dπ πΉ)βπ)) |
35 | 34 | oveq2d 7378 |
. . . . . . 7
β’ (π = π β (π Tayl ((π Dπ πΉ)βπ)) = (π Tayl ((π Dπ πΉ)βπ))) |
36 | | oveq2 7370 |
. . . . . . . 8
β’ (π = π β (π β π) = (π β π)) |
37 | 36 | oveq2d 7378 |
. . . . . . 7
β’ (π = π β (π + (π β π)) = (π + (π β π))) |
38 | | eqidd 2738 |
. . . . . . 7
β’ (π = π β π΅ = π΅) |
39 | 35, 37, 38 | oveq123d 7383 |
. . . . . 6
β’ (π = π β ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅)) |
40 | 33, 39 | eqeq12d 2753 |
. . . . 5
β’ (π = π β (((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅) β ((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅))) |
41 | 40 | imbi2d 341 |
. . . 4
β’ (π = π β ((π β ((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅)) β (π β ((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅)))) |
42 | | ssidd 3972 |
. . . . . . 7
β’ (π β β β
β) |
43 | | mapsspm 8821 |
. . . . . . . 8
β’ (β
βm β) β (β βpm
β) |
44 | | dvntaylp.s |
. . . . . . . . . 10
β’ (π β π β {β, β}) |
45 | | dvntaylp.f |
. . . . . . . . . 10
β’ (π β πΉ:π΄βΆβ) |
46 | | dvntaylp.a |
. . . . . . . . . 10
β’ (π β π΄ β π) |
47 | | dvntaylp.n |
. . . . . . . . . . 11
β’ (π β π β
β0) |
48 | 47, 1 | nn0addcld 12484 |
. . . . . . . . . 10
β’ (π β (π + π) β
β0) |
49 | | dvntaylp.b |
. . . . . . . . . 10
β’ (π β π΅ β dom ((π Dπ πΉ)β(π + π))) |
50 | | eqid 2737 |
. . . . . . . . . 10
β’ ((π + π)(π Tayl πΉ)π΅) = ((π + π)(π Tayl πΉ)π΅) |
51 | 44, 45, 46, 48, 49, 50 | taylpf 25741 |
. . . . . . . . 9
β’ (π β ((π + π)(π Tayl πΉ)π΅):ββΆβ) |
52 | | cnex 11139 |
. . . . . . . . . 10
β’ β
β V |
53 | 52, 52 | elmap 8816 |
. . . . . . . . 9
β’ (((π + π)(π Tayl πΉ)π΅) β (β βm
β) β ((π + π)(π Tayl πΉ)π΅):ββΆβ) |
54 | 51, 53 | sylibr 233 |
. . . . . . . 8
β’ (π β ((π + π)(π Tayl πΉ)π΅) β (β βm
β)) |
55 | 43, 54 | sselid 3947 |
. . . . . . 7
β’ (π β ((π + π)(π Tayl πΉ)π΅) β (β βpm
β)) |
56 | | dvn0 25304 |
. . . . . . 7
β’ ((β
β β β§ ((π +
π)(π Tayl πΉ)π΅) β (β βpm
β)) β ((β Dπ ((π + π)(π Tayl πΉ)π΅))β0) = ((π + π)(π Tayl πΉ)π΅)) |
57 | 42, 55, 56 | syl2anc 585 |
. . . . . 6
β’ (π β ((β
Dπ ((π +
π)(π Tayl πΉ)π΅))β0) = ((π + π)(π Tayl πΉ)π΅)) |
58 | | recnprss 25284 |
. . . . . . . . . 10
β’ (π β {β, β}
β π β
β) |
59 | 44, 58 | syl 17 |
. . . . . . . . 9
β’ (π β π β β) |
60 | 52 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β
V) |
61 | | elpm2r 8790 |
. . . . . . . . . 10
β’
(((β β V β§ π β {β, β}) β§ (πΉ:π΄βΆβ β§ π΄ β π)) β πΉ β (β βpm π)) |
62 | 60, 44, 45, 46, 61 | syl22anc 838 |
. . . . . . . . 9
β’ (π β πΉ β (β βpm π)) |
63 | | dvn0 25304 |
. . . . . . . . 9
β’ ((π β β β§ πΉ β (β
βpm π))
β ((π
Dπ πΉ)β0) = πΉ) |
64 | 59, 62, 63 | syl2anc 585 |
. . . . . . . 8
β’ (π β ((π Dπ πΉ)β0) = πΉ) |
65 | 64 | oveq2d 7378 |
. . . . . . 7
β’ (π β (π Tayl ((π Dπ πΉ)β0)) = (π Tayl πΉ)) |
66 | 1 | nn0cnd 12482 |
. . . . . . . . 9
β’ (π β π β β) |
67 | 66 | subid1d 11508 |
. . . . . . . 8
β’ (π β (π β 0) = π) |
68 | 67 | oveq2d 7378 |
. . . . . . 7
β’ (π β (π + (π β 0)) = (π + π)) |
69 | | eqidd 2738 |
. . . . . . 7
β’ (π β π΅ = π΅) |
70 | 65, 68, 69 | oveq123d 7383 |
. . . . . 6
β’ (π β ((π + (π β 0))(π Tayl ((π Dπ πΉ)β0))π΅) = ((π + π)(π Tayl πΉ)π΅)) |
71 | 57, 70 | eqtr4d 2780 |
. . . . 5
β’ (π β ((β
Dπ ((π +
π)(π Tayl πΉ)π΅))β0) = ((π + (π β 0))(π Tayl ((π Dπ πΉ)β0))π΅)) |
72 | 71 | a1i 11 |
. . . 4
β’ (π β
(β€β₯β0) β (π β ((β Dπ
((π + π)(π Tayl πΉ)π΅))β0) = ((π + (π β 0))(π Tayl ((π Dπ πΉ)β0))π΅))) |
73 | | oveq2 7370 |
. . . . . . 7
β’
(((β Dπ ((π + π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅) β (β D ((β
Dπ ((π +
π)(π Tayl πΉ)π΅))βπ)) = (β D ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅))) |
74 | | ssidd 3972 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β β β
β) |
75 | 55 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β ((π + π)(π Tayl πΉ)π΅) β (β βpm
β)) |
76 | | elfzouz 13583 |
. . . . . . . . . . 11
β’ (π β (0..^π) β π β
(β€β₯β0)) |
77 | 76 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π β
(β€β₯β0)) |
78 | 77, 2 | eleqtrrdi 2849 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β π β β0) |
79 | | dvnp1 25305 |
. . . . . . . . 9
β’ ((β
β β β§ ((π +
π)(π Tayl πΉ)π΅) β (β βpm
β) β§ π β
β0) β ((β Dπ ((π + π)(π Tayl πΉ)π΅))β(π + 1)) = (β D ((β
Dπ ((π +
π)(π Tayl πΉ)π΅))βπ))) |
80 | 74, 75, 78, 79 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β ((β Dπ
((π + π)(π Tayl πΉ)π΅))β(π + 1)) = (β D ((β
Dπ ((π +
π)(π Tayl πΉ)π΅))βπ))) |
81 | 44 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π β {β, β}) |
82 | 62 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β πΉ β (β βpm π)) |
83 | | dvnf 25307 |
. . . . . . . . . . 11
β’ ((π β {β, β} β§
πΉ β (β
βpm π)
β§ π β
β0) β ((π Dπ πΉ)βπ):dom ((π Dπ πΉ)βπ)βΆβ) |
84 | 81, 82, 78, 83 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β ((π Dπ πΉ)βπ):dom ((π Dπ πΉ)βπ)βΆβ) |
85 | | dvnbss 25308 |
. . . . . . . . . . . . 13
β’ ((π β {β, β} β§
πΉ β (β
βpm π)
β§ π β
β0) β dom ((π Dπ πΉ)βπ) β dom πΉ) |
86 | 81, 82, 78, 85 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β dom ((π Dπ πΉ)βπ) β dom πΉ) |
87 | 45 | fdmd 6684 |
. . . . . . . . . . . . 13
β’ (π β dom πΉ = π΄) |
88 | 87 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β dom πΉ = π΄) |
89 | 86, 88 | sseqtrd 3989 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β dom ((π Dπ πΉ)βπ) β π΄) |
90 | 46 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β π΄ β π) |
91 | 89, 90 | sstrd 3959 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β dom ((π Dπ πΉ)βπ) β π) |
92 | 47 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β π β
β0) |
93 | | fzofzp1 13676 |
. . . . . . . . . . . . 13
β’ (π β (0..^π) β (π + 1) β (0...π)) |
94 | 93 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β (π + 1) β (0...π)) |
95 | | fznn0sub 13480 |
. . . . . . . . . . . 12
β’ ((π + 1) β (0...π) β (π β (π + 1)) β
β0) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β (π β (π + 1)) β
β0) |
97 | 92, 96 | nn0addcld 12484 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (π + (π β (π + 1))) β
β0) |
98 | 49 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β π΅ β dom ((π Dπ πΉ)β(π + π))) |
99 | | elfzofz 13595 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0..^π) β π β (0...π)) |
100 | 99 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β π β (0...π)) |
101 | | fznn0sub 13480 |
. . . . . . . . . . . . . . . 16
β’ (π β (0...π) β (π β π) β
β0) |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (π β π) β
β0) |
103 | 92, 102 | nn0addcld 12484 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (π + (π β π)) β
β0) |
104 | | dvnadd 25309 |
. . . . . . . . . . . . . 14
β’ (((π β {β, β} β§
πΉ β (β
βpm π))
β§ (π β
β0 β§ (π + (π β π)) β β0)) β
((π Dπ
((π Dπ
πΉ)βπ))β(π + (π β π))) = ((π Dπ πΉ)β(π + (π + (π β π))))) |
105 | 81, 82, 78, 103, 104 | syl22anc 838 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β ((π Dπ ((π Dπ πΉ)βπ))β(π + (π β π))) = ((π Dπ πΉ)β(π + (π + (π β π))))) |
106 | 47 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β) |
107 | 106 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β π β β) |
108 | 96 | nn0cnd 12482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (π β (π + 1)) β β) |
109 | | 1cnd 11157 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β 1 β β) |
110 | 107, 108,
109 | addassd 11184 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β ((π + (π β (π + 1))) + 1) = (π + ((π β (π + 1)) + 1))) |
111 | 66 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β π β β) |
112 | 78 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β π β β) |
113 | 111, 112,
109 | nppcan2d 11545 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β ((π β (π + 1)) + 1) = (π β π)) |
114 | 113 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (π + ((π β (π + 1)) + 1)) = (π + (π β π))) |
115 | 110, 114 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β ((π + (π β (π + 1))) + 1) = (π + (π β π))) |
116 | 115 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β ((π Dπ ((π Dπ πΉ)βπ))β((π + (π β (π + 1))) + 1)) = ((π Dπ ((π Dπ πΉ)βπ))β(π + (π β π)))) |
117 | 112, 111 | pncan3d 11522 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (π + (π β π)) = π) |
118 | 117 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (π + (π + (π β π))) = (π + π)) |
119 | 111, 112 | subcld 11519 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (π β π) β β) |
120 | 107, 112,
119 | add12d 11388 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β (π + (π + (π β π))) = (π + (π + (π β π)))) |
121 | 118, 120 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (π + π) = (π + (π + (π β π)))) |
122 | 121 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β ((π Dπ πΉ)β(π + π)) = ((π Dπ πΉ)β(π + (π + (π β π))))) |
123 | 105, 116,
122 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β ((π Dπ ((π Dπ πΉ)βπ))β((π + (π β (π + 1))) + 1)) = ((π Dπ πΉ)β(π + π))) |
124 | 123 | dmeqd 5866 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β dom ((π Dπ ((π Dπ πΉ)βπ))β((π + (π β (π + 1))) + 1)) = dom ((π Dπ πΉ)β(π + π))) |
125 | 98, 124 | eleqtrrd 2841 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π΅ β dom ((π Dπ ((π Dπ πΉ)βπ))β((π + (π β (π + 1))) + 1))) |
126 | 81, 84, 91, 97, 125 | dvtaylp 25745 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (β D (((π + (π β (π + 1))) + 1)(π Tayl ((π Dπ πΉ)βπ))π΅)) = ((π + (π β (π + 1)))(π Tayl (π D ((π Dπ πΉ)βπ)))π΅)) |
127 | 115 | oveq1d 7377 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (((π + (π β (π + 1))) + 1)(π Tayl ((π Dπ πΉ)βπ))π΅) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅)) |
128 | 127 | oveq2d 7378 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (β D (((π + (π β (π + 1))) + 1)(π Tayl ((π Dπ πΉ)βπ))π΅)) = (β D ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅))) |
129 | 59 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β π β β) |
130 | | dvnp1 25305 |
. . . . . . . . . . . . 13
β’ ((π β β β§ πΉ β (β
βpm π)
β§ π β
β0) β ((π Dπ πΉ)β(π + 1)) = (π D ((π Dπ πΉ)βπ))) |
131 | 129, 82, 78, 130 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0..^π)) β ((π Dπ πΉ)β(π + 1)) = (π D ((π Dπ πΉ)βπ))) |
132 | 131 | oveq2d 7378 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β (π Tayl ((π Dπ πΉ)β(π + 1))) = (π Tayl (π D ((π Dπ πΉ)βπ)))) |
133 | 132 | eqcomd 2743 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (π Tayl (π D ((π Dπ πΉ)βπ))) = (π Tayl ((π Dπ πΉ)β(π + 1)))) |
134 | 133 | oveqd 7379 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β ((π + (π β (π + 1)))(π Tayl (π D ((π Dπ πΉ)βπ)))π΅) = ((π + (π β (π + 1)))(π Tayl ((π Dπ πΉ)β(π + 1)))π΅)) |
135 | 126, 128,
134 | 3eqtr3rd 2786 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β ((π + (π β (π + 1)))(π Tayl ((π Dπ πΉ)β(π + 1)))π΅) = (β D ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅))) |
136 | 80, 135 | eqeq12d 2753 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (((β Dπ
((π + π)(π Tayl πΉ)π΅))β(π + 1)) = ((π + (π β (π + 1)))(π Tayl ((π Dπ πΉ)β(π + 1)))π΅) β (β D ((β
Dπ ((π +
π)(π Tayl πΉ)π΅))βπ)) = (β D ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅)))) |
137 | 73, 136 | syl5ibr 246 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅) β ((β Dπ
((π + π)(π Tayl πΉ)π΅))β(π + 1)) = ((π + (π β (π + 1)))(π Tayl ((π Dπ πΉ)β(π + 1)))π΅))) |
138 | 137 | expcom 415 |
. . . . 5
β’ (π β (0..^π) β (π β (((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅) β ((β Dπ
((π + π)(π Tayl πΉ)π΅))β(π + 1)) = ((π + (π β (π + 1)))(π Tayl ((π Dπ πΉ)β(π + 1)))π΅)))) |
139 | 138 | a2d 29 |
. . . 4
β’ (π β (0..^π) β ((π β ((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅)) β (π β ((β Dπ
((π + π)(π Tayl πΉ)π΅))β(π + 1)) = ((π + (π β (π + 1)))(π Tayl ((π Dπ πΉ)β(π + 1)))π΅)))) |
140 | 14, 23, 32, 41, 72, 139 | fzind2 13697 |
. . 3
β’ (π β (0...π) β (π β ((β Dπ
((π + π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅))) |
141 | 5, 140 | mpcom 38 |
. 2
β’ (π β ((β
Dπ ((π +
π)(π Tayl πΉ)π΅))βπ) = ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅)) |
142 | 66 | subidd 11507 |
. . . . 5
β’ (π β (π β π) = 0) |
143 | 142 | oveq2d 7378 |
. . . 4
β’ (π β (π + (π β π)) = (π + 0)) |
144 | 106 | addid1d 11362 |
. . . 4
β’ (π β (π + 0) = π) |
145 | 143, 144 | eqtrd 2777 |
. . 3
β’ (π β (π + (π β π)) = π) |
146 | 145 | oveq1d 7377 |
. 2
β’ (π β ((π + (π β π))(π Tayl ((π Dπ πΉ)βπ))π΅) = (π(π Tayl ((π Dπ πΉ)βπ))π΅)) |
147 | 141, 146 | eqtrd 2777 |
1
β’ (π β ((β
Dπ ((π +
π)(π Tayl πΉ)π΅))βπ) = (π(π Tayl ((π Dπ πΉ)βπ))π΅)) |