Step |
Hyp |
Ref |
Expression |
1 |
|
taylth.f |
|- ( ph -> F : A --> RR ) |
2 |
|
taylth.a |
|- ( ph -> A C_ RR ) |
3 |
|
taylth.d |
|- ( ph -> dom ( ( RR Dn F ) ` N ) = A ) |
4 |
|
taylth.n |
|- ( ph -> N e. NN ) |
5 |
|
taylth.b |
|- ( ph -> B e. A ) |
6 |
|
taylth.t |
|- T = ( N ( RR Tayl F ) B ) |
7 |
|
taylthlem2.m |
|- ( ph -> M e. ( 1 ..^ N ) ) |
8 |
|
taylthlem2.i |
|- ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ) limCC B ) ) |
9 |
|
fz1ssfz0 |
|- ( 1 ... N ) C_ ( 0 ... N ) |
10 |
|
fzofzp1 |
|- ( M e. ( 1 ..^ N ) -> ( M + 1 ) e. ( 1 ... N ) ) |
11 |
7 10
|
syl |
|- ( ph -> ( M + 1 ) e. ( 1 ... N ) ) |
12 |
9 11
|
sselid |
|- ( ph -> ( M + 1 ) e. ( 0 ... N ) ) |
13 |
|
fznn0sub2 |
|- ( ( M + 1 ) e. ( 0 ... N ) -> ( N - ( M + 1 ) ) e. ( 0 ... N ) ) |
14 |
12 13
|
syl |
|- ( ph -> ( N - ( M + 1 ) ) e. ( 0 ... N ) ) |
15 |
|
elfznn0 |
|- ( ( N - ( M + 1 ) ) e. ( 0 ... N ) -> ( N - ( M + 1 ) ) e. NN0 ) |
16 |
14 15
|
syl |
|- ( ph -> ( N - ( M + 1 ) ) e. NN0 ) |
17 |
|
dvnfre |
|- ( ( F : A --> RR /\ A C_ RR /\ ( N - ( M + 1 ) ) e. NN0 ) -> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) --> RR ) |
18 |
1 2 16 17
|
syl3anc |
|- ( ph -> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) --> RR ) |
19 |
|
reelprrecn |
|- RR e. { RR , CC } |
20 |
19
|
a1i |
|- ( ph -> RR e. { RR , CC } ) |
21 |
|
cnex |
|- CC e. _V |
22 |
21
|
a1i |
|- ( ph -> CC e. _V ) |
23 |
|
reex |
|- RR e. _V |
24 |
23
|
a1i |
|- ( ph -> RR e. _V ) |
25 |
|
ax-resscn |
|- RR C_ CC |
26 |
|
fss |
|- ( ( F : A --> RR /\ RR C_ CC ) -> F : A --> CC ) |
27 |
1 25 26
|
sylancl |
|- ( ph -> F : A --> CC ) |
28 |
|
elpm2r |
|- ( ( ( CC e. _V /\ RR e. _V ) /\ ( F : A --> CC /\ A C_ RR ) ) -> F e. ( CC ^pm RR ) ) |
29 |
22 24 27 2 28
|
syl22anc |
|- ( ph -> F e. ( CC ^pm RR ) ) |
30 |
|
dvnbss |
|- ( ( RR e. { RR , CC } /\ F e. ( CC ^pm RR ) /\ ( N - ( M + 1 ) ) e. NN0 ) -> dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) C_ dom F ) |
31 |
20 29 16 30
|
syl3anc |
|- ( ph -> dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) C_ dom F ) |
32 |
1 31
|
fssdmd |
|- ( ph -> dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) C_ A ) |
33 |
|
dvn2bss |
|- ( ( RR e. { RR , CC } /\ F e. ( CC ^pm RR ) /\ ( N - ( M + 1 ) ) e. ( 0 ... N ) ) -> dom ( ( RR Dn F ) ` N ) C_ dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) |
34 |
20 29 14 33
|
syl3anc |
|- ( ph -> dom ( ( RR Dn F ) ` N ) C_ dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) |
35 |
3 34
|
eqsstrrd |
|- ( ph -> A C_ dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) |
36 |
32 35
|
eqssd |
|- ( ph -> dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) = A ) |
37 |
36
|
feq2d |
|- ( ph -> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) --> RR <-> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : A --> RR ) ) |
38 |
18 37
|
mpbid |
|- ( ph -> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : A --> RR ) |
39 |
38
|
ffvelrnda |
|- ( ( ph /\ y e. A ) -> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) e. RR ) |
40 |
2
|
sselda |
|- ( ( ph /\ y e. A ) -> y e. RR ) |
41 |
|
fvres |
|- ( y e. RR -> ( ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) |` RR ) ` y ) = ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) |
42 |
41
|
adantl |
|- ( ( ph /\ y e. RR ) -> ( ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) |` RR ) ` y ) = ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) |
43 |
|
resubdrg |
|- ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing ) |
44 |
43
|
simpli |
|- RR e. ( SubRing ` CCfld ) |
45 |
44
|
a1i |
|- ( ph -> RR e. ( SubRing ` CCfld ) ) |
46 |
4
|
nnnn0d |
|- ( ph -> N e. NN0 ) |
47 |
5 3
|
eleqtrrd |
|- ( ph -> B e. dom ( ( RR Dn F ) ` N ) ) |
48 |
2 5
|
sseldd |
|- ( ph -> B e. RR ) |
49 |
|
elfznn0 |
|- ( k e. ( 0 ... N ) -> k e. NN0 ) |
50 |
|
dvnfre |
|- ( ( F : A --> RR /\ A C_ RR /\ k e. NN0 ) -> ( ( RR Dn F ) ` k ) : dom ( ( RR Dn F ) ` k ) --> RR ) |
51 |
1 2 49 50
|
syl2an3an |
|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( RR Dn F ) ` k ) : dom ( ( RR Dn F ) ` k ) --> RR ) |
52 |
|
simpr |
|- ( ( ph /\ k e. ( 0 ... N ) ) -> k e. ( 0 ... N ) ) |
53 |
|
dvn2bss |
|- ( ( RR e. { RR , CC } /\ F e. ( CC ^pm RR ) /\ k e. ( 0 ... N ) ) -> dom ( ( RR Dn F ) ` N ) C_ dom ( ( RR Dn F ) ` k ) ) |
54 |
19 29 52 53
|
mp3an2ani |
|- ( ( ph /\ k e. ( 0 ... N ) ) -> dom ( ( RR Dn F ) ` N ) C_ dom ( ( RR Dn F ) ` k ) ) |
55 |
47
|
adantr |
|- ( ( ph /\ k e. ( 0 ... N ) ) -> B e. dom ( ( RR Dn F ) ` N ) ) |
56 |
54 55
|
sseldd |
|- ( ( ph /\ k e. ( 0 ... N ) ) -> B e. dom ( ( RR Dn F ) ` k ) ) |
57 |
51 56
|
ffvelrnd |
|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( RR Dn F ) ` k ) ` B ) e. RR ) |
58 |
49
|
adantl |
|- ( ( ph /\ k e. ( 0 ... N ) ) -> k e. NN0 ) |
59 |
58
|
faccld |
|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ! ` k ) e. NN ) |
60 |
57 59
|
nndivred |
|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( ( RR Dn F ) ` k ) ` B ) / ( ! ` k ) ) e. RR ) |
61 |
20 27 2 46 47 6 45 48 60
|
taylply2 |
|- ( ph -> ( T e. ( Poly ` RR ) /\ ( deg ` T ) <_ N ) ) |
62 |
61
|
simpld |
|- ( ph -> T e. ( Poly ` RR ) ) |
63 |
|
dvnply2 |
|- ( ( RR e. ( SubRing ` CCfld ) /\ T e. ( Poly ` RR ) /\ ( N - ( M + 1 ) ) e. NN0 ) -> ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) e. ( Poly ` RR ) ) |
64 |
45 62 16 63
|
syl3anc |
|- ( ph -> ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) e. ( Poly ` RR ) ) |
65 |
|
plyreres |
|- ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) e. ( Poly ` RR ) -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) |` RR ) : RR --> RR ) |
66 |
64 65
|
syl |
|- ( ph -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) |` RR ) : RR --> RR ) |
67 |
66
|
ffvelrnda |
|- ( ( ph /\ y e. RR ) -> ( ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) |` RR ) ` y ) e. RR ) |
68 |
42 67
|
eqeltrrd |
|- ( ( ph /\ y e. RR ) -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) e. RR ) |
69 |
40 68
|
syldan |
|- ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) e. RR ) |
70 |
39 69
|
resubcld |
|- ( ( ph /\ y e. A ) -> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) e. RR ) |
71 |
70
|
fmpttd |
|- ( ph -> ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) : A --> RR ) |
72 |
48
|
adantr |
|- ( ( ph /\ y e. A ) -> B e. RR ) |
73 |
40 72
|
resubcld |
|- ( ( ph /\ y e. A ) -> ( y - B ) e. RR ) |
74 |
|
elfzouz |
|- ( M e. ( 1 ..^ N ) -> M e. ( ZZ>= ` 1 ) ) |
75 |
7 74
|
syl |
|- ( ph -> M e. ( ZZ>= ` 1 ) ) |
76 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
77 |
75 76
|
eleqtrrdi |
|- ( ph -> M e. NN ) |
78 |
77
|
nnnn0d |
|- ( ph -> M e. NN0 ) |
79 |
78
|
adantr |
|- ( ( ph /\ y e. A ) -> M e. NN0 ) |
80 |
|
1nn0 |
|- 1 e. NN0 |
81 |
80
|
a1i |
|- ( ( ph /\ y e. A ) -> 1 e. NN0 ) |
82 |
79 81
|
nn0addcld |
|- ( ( ph /\ y e. A ) -> ( M + 1 ) e. NN0 ) |
83 |
73 82
|
reexpcld |
|- ( ( ph /\ y e. A ) -> ( ( y - B ) ^ ( M + 1 ) ) e. RR ) |
84 |
83
|
fmpttd |
|- ( ph -> ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) : A --> RR ) |
85 |
|
retop |
|- ( topGen ` ran (,) ) e. Top |
86 |
|
uniretop |
|- RR = U. ( topGen ` ran (,) ) |
87 |
86
|
ntrss2 |
|- ( ( ( topGen ` ran (,) ) e. Top /\ A C_ RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) C_ A ) |
88 |
85 2 87
|
sylancr |
|- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) C_ A ) |
89 |
4
|
nncnd |
|- ( ph -> N e. CC ) |
90 |
77
|
nncnd |
|- ( ph -> M e. CC ) |
91 |
|
1cnd |
|- ( ph -> 1 e. CC ) |
92 |
89 90 91
|
nppcan2d |
|- ( ph -> ( ( N - ( M + 1 ) ) + 1 ) = ( N - M ) ) |
93 |
92
|
fveq2d |
|- ( ph -> ( ( RR Dn F ) ` ( ( N - ( M + 1 ) ) + 1 ) ) = ( ( RR Dn F ) ` ( N - M ) ) ) |
94 |
25
|
a1i |
|- ( ph -> RR C_ CC ) |
95 |
|
dvnp1 |
|- ( ( RR C_ CC /\ F e. ( CC ^pm RR ) /\ ( N - ( M + 1 ) ) e. NN0 ) -> ( ( RR Dn F ) ` ( ( N - ( M + 1 ) ) + 1 ) ) = ( RR _D ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) ) |
96 |
94 29 16 95
|
syl3anc |
|- ( ph -> ( ( RR Dn F ) ` ( ( N - ( M + 1 ) ) + 1 ) ) = ( RR _D ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) ) |
97 |
93 96
|
eqtr3d |
|- ( ph -> ( ( RR Dn F ) ` ( N - M ) ) = ( RR _D ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) ) |
98 |
97
|
dmeqd |
|- ( ph -> dom ( ( RR Dn F ) ` ( N - M ) ) = dom ( RR _D ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) ) |
99 |
|
fzonnsub |
|- ( M e. ( 1 ..^ N ) -> ( N - M ) e. NN ) |
100 |
7 99
|
syl |
|- ( ph -> ( N - M ) e. NN ) |
101 |
100
|
nnnn0d |
|- ( ph -> ( N - M ) e. NN0 ) |
102 |
|
dvnbss |
|- ( ( RR e. { RR , CC } /\ F e. ( CC ^pm RR ) /\ ( N - M ) e. NN0 ) -> dom ( ( RR Dn F ) ` ( N - M ) ) C_ dom F ) |
103 |
20 29 101 102
|
syl3anc |
|- ( ph -> dom ( ( RR Dn F ) ` ( N - M ) ) C_ dom F ) |
104 |
1 103
|
fssdmd |
|- ( ph -> dom ( ( RR Dn F ) ` ( N - M ) ) C_ A ) |
105 |
|
elfzofz |
|- ( M e. ( 1 ..^ N ) -> M e. ( 1 ... N ) ) |
106 |
7 105
|
syl |
|- ( ph -> M e. ( 1 ... N ) ) |
107 |
9 106
|
sselid |
|- ( ph -> M e. ( 0 ... N ) ) |
108 |
|
fznn0sub2 |
|- ( M e. ( 0 ... N ) -> ( N - M ) e. ( 0 ... N ) ) |
109 |
107 108
|
syl |
|- ( ph -> ( N - M ) e. ( 0 ... N ) ) |
110 |
|
dvn2bss |
|- ( ( RR e. { RR , CC } /\ F e. ( CC ^pm RR ) /\ ( N - M ) e. ( 0 ... N ) ) -> dom ( ( RR Dn F ) ` N ) C_ dom ( ( RR Dn F ) ` ( N - M ) ) ) |
111 |
20 29 109 110
|
syl3anc |
|- ( ph -> dom ( ( RR Dn F ) ` N ) C_ dom ( ( RR Dn F ) ` ( N - M ) ) ) |
112 |
3 111
|
eqsstrrd |
|- ( ph -> A C_ dom ( ( RR Dn F ) ` ( N - M ) ) ) |
113 |
104 112
|
eqssd |
|- ( ph -> dom ( ( RR Dn F ) ` ( N - M ) ) = A ) |
114 |
98 113
|
eqtr3d |
|- ( ph -> dom ( RR _D ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) = A ) |
115 |
|
fss |
|- ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : A --> RR /\ RR C_ CC ) -> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : A --> CC ) |
116 |
38 25 115
|
sylancl |
|- ( ph -> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : A --> CC ) |
117 |
|
eqid |
|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
118 |
117
|
tgioo2 |
|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR ) |
119 |
94 116 2 118 117
|
dvbssntr |
|- ( ph -> dom ( RR _D ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` A ) ) |
120 |
114 119
|
eqsstrrd |
|- ( ph -> A C_ ( ( int ` ( topGen ` ran (,) ) ) ` A ) ) |
121 |
88 120
|
eqssd |
|- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) = A ) |
122 |
86
|
isopn3 |
|- ( ( ( topGen ` ran (,) ) e. Top /\ A C_ RR ) -> ( A e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` A ) = A ) ) |
123 |
85 2 122
|
sylancr |
|- ( ph -> ( A e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` A ) = A ) ) |
124 |
121 123
|
mpbird |
|- ( ph -> A e. ( topGen ` ran (,) ) ) |
125 |
|
eqid |
|- ( A \ { B } ) = ( A \ { B } ) |
126 |
|
difss |
|- ( A \ { B } ) C_ A |
127 |
39
|
recnd |
|- ( ( ph /\ y e. A ) -> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) e. CC ) |
128 |
|
dvnf |
|- ( ( RR e. { RR , CC } /\ F e. ( CC ^pm RR ) /\ ( N - M ) e. NN0 ) -> ( ( RR Dn F ) ` ( N - M ) ) : dom ( ( RR Dn F ) ` ( N - M ) ) --> CC ) |
129 |
20 29 101 128
|
syl3anc |
|- ( ph -> ( ( RR Dn F ) ` ( N - M ) ) : dom ( ( RR Dn F ) ` ( N - M ) ) --> CC ) |
130 |
113
|
feq2d |
|- ( ph -> ( ( ( RR Dn F ) ` ( N - M ) ) : dom ( ( RR Dn F ) ` ( N - M ) ) --> CC <-> ( ( RR Dn F ) ` ( N - M ) ) : A --> CC ) ) |
131 |
129 130
|
mpbid |
|- ( ph -> ( ( RR Dn F ) ` ( N - M ) ) : A --> CC ) |
132 |
131
|
ffvelrnda |
|- ( ( ph /\ y e. A ) -> ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) e. CC ) |
133 |
|
dvnfre |
|- ( ( F : A --> RR /\ A C_ RR /\ ( N - M ) e. NN0 ) -> ( ( RR Dn F ) ` ( N - M ) ) : dom ( ( RR Dn F ) ` ( N - M ) ) --> RR ) |
134 |
1 2 101 133
|
syl3anc |
|- ( ph -> ( ( RR Dn F ) ` ( N - M ) ) : dom ( ( RR Dn F ) ` ( N - M ) ) --> RR ) |
135 |
113
|
feq2d |
|- ( ph -> ( ( ( RR Dn F ) ` ( N - M ) ) : dom ( ( RR Dn F ) ` ( N - M ) ) --> RR <-> ( ( RR Dn F ) ` ( N - M ) ) : A --> RR ) ) |
136 |
134 135
|
mpbid |
|- ( ph -> ( ( RR Dn F ) ` ( N - M ) ) : A --> RR ) |
137 |
136
|
feqmptd |
|- ( ph -> ( ( RR Dn F ) ` ( N - M ) ) = ( y e. A |-> ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) ) ) |
138 |
38
|
feqmptd |
|- ( ph -> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) = ( y e. A |-> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) |
139 |
138
|
oveq2d |
|- ( ph -> ( RR _D ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) = ( RR _D ( y e. A |-> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) |
140 |
97 137 139
|
3eqtr3rd |
|- ( ph -> ( RR _D ( y e. A |-> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) = ( y e. A |-> ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) ) ) |
141 |
69
|
recnd |
|- ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) e. CC ) |
142 |
|
fvexd |
|- ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) e. _V ) |
143 |
68
|
recnd |
|- ( ( ph /\ y e. RR ) -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) e. CC ) |
144 |
|
recn |
|- ( y e. RR -> y e. CC ) |
145 |
|
dvnply2 |
|- ( ( RR e. ( SubRing ` CCfld ) /\ T e. ( Poly ` RR ) /\ ( N - M ) e. NN0 ) -> ( ( CC Dn T ) ` ( N - M ) ) e. ( Poly ` RR ) ) |
146 |
45 62 101 145
|
syl3anc |
|- ( ph -> ( ( CC Dn T ) ` ( N - M ) ) e. ( Poly ` RR ) ) |
147 |
|
plyf |
|- ( ( ( CC Dn T ) ` ( N - M ) ) e. ( Poly ` RR ) -> ( ( CC Dn T ) ` ( N - M ) ) : CC --> CC ) |
148 |
146 147
|
syl |
|- ( ph -> ( ( CC Dn T ) ` ( N - M ) ) : CC --> CC ) |
149 |
148
|
ffvelrnda |
|- ( ( ph /\ y e. CC ) -> ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) e. CC ) |
150 |
144 149
|
sylan2 |
|- ( ( ph /\ y e. RR ) -> ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) e. CC ) |
151 |
117
|
cnfldtopon |
|- ( TopOpen ` CCfld ) e. ( TopOn ` CC ) |
152 |
|
toponmax |
|- ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) -> CC e. ( TopOpen ` CCfld ) ) |
153 |
151 152
|
mp1i |
|- ( ph -> CC e. ( TopOpen ` CCfld ) ) |
154 |
|
df-ss |
|- ( RR C_ CC <-> ( RR i^i CC ) = RR ) |
155 |
94 154
|
sylib |
|- ( ph -> ( RR i^i CC ) = RR ) |
156 |
|
plyf |
|- ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) e. ( Poly ` RR ) -> ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) : CC --> CC ) |
157 |
64 156
|
syl |
|- ( ph -> ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) : CC --> CC ) |
158 |
157
|
ffvelrnda |
|- ( ( ph /\ y e. CC ) -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) e. CC ) |
159 |
92
|
fveq2d |
|- ( ph -> ( ( CC Dn T ) ` ( ( N - ( M + 1 ) ) + 1 ) ) = ( ( CC Dn T ) ` ( N - M ) ) ) |
160 |
|
ssid |
|- CC C_ CC |
161 |
160
|
a1i |
|- ( ph -> CC C_ CC ) |
162 |
|
mapsspm |
|- ( CC ^m CC ) C_ ( CC ^pm CC ) |
163 |
|
plyf |
|- ( T e. ( Poly ` RR ) -> T : CC --> CC ) |
164 |
62 163
|
syl |
|- ( ph -> T : CC --> CC ) |
165 |
21 21
|
elmap |
|- ( T e. ( CC ^m CC ) <-> T : CC --> CC ) |
166 |
164 165
|
sylibr |
|- ( ph -> T e. ( CC ^m CC ) ) |
167 |
162 166
|
sselid |
|- ( ph -> T e. ( CC ^pm CC ) ) |
168 |
|
dvnp1 |
|- ( ( CC C_ CC /\ T e. ( CC ^pm CC ) /\ ( N - ( M + 1 ) ) e. NN0 ) -> ( ( CC Dn T ) ` ( ( N - ( M + 1 ) ) + 1 ) ) = ( CC _D ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ) ) |
169 |
161 167 16 168
|
syl3anc |
|- ( ph -> ( ( CC Dn T ) ` ( ( N - ( M + 1 ) ) + 1 ) ) = ( CC _D ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ) ) |
170 |
159 169
|
eqtr3d |
|- ( ph -> ( ( CC Dn T ) ` ( N - M ) ) = ( CC _D ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ) ) |
171 |
148
|
feqmptd |
|- ( ph -> ( ( CC Dn T ) ` ( N - M ) ) = ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) |
172 |
157
|
feqmptd |
|- ( ph -> ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) = ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) |
173 |
172
|
oveq2d |
|- ( ph -> ( CC _D ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ) = ( CC _D ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) |
174 |
170 171 173
|
3eqtr3rd |
|- ( ph -> ( CC _D ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) = ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) |
175 |
117 20 153 155 158 149 174
|
dvmptres3 |
|- ( ph -> ( RR _D ( y e. RR |-> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) = ( y e. RR |-> ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) |
176 |
20 143 150 175 2 118 117 124
|
dvmptres |
|- ( ph -> ( RR _D ( y e. A |-> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) = ( y e. A |-> ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) |
177 |
20 127 132 140 141 142 176
|
dvmptsub |
|- ( ph -> ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) = ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) ) |
178 |
177
|
dmeqd |
|- ( ph -> dom ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) = dom ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) ) |
179 |
|
ovex |
|- ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) e. _V |
180 |
|
eqid |
|- ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) = ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) |
181 |
179 180
|
dmmpti |
|- dom ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) = A |
182 |
178 181
|
eqtrdi |
|- ( ph -> dom ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) = A ) |
183 |
126 182
|
sseqtrrid |
|- ( ph -> ( A \ { B } ) C_ dom ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) ) |
184 |
|
simpr |
|- ( ( ph /\ y e. CC ) -> y e. CC ) |
185 |
48
|
adantr |
|- ( ( ph /\ y e. CC ) -> B e. RR ) |
186 |
185
|
recnd |
|- ( ( ph /\ y e. CC ) -> B e. CC ) |
187 |
184 186
|
subcld |
|- ( ( ph /\ y e. CC ) -> ( y - B ) e. CC ) |
188 |
78
|
adantr |
|- ( ( ph /\ y e. CC ) -> M e. NN0 ) |
189 |
80
|
a1i |
|- ( ( ph /\ y e. CC ) -> 1 e. NN0 ) |
190 |
188 189
|
nn0addcld |
|- ( ( ph /\ y e. CC ) -> ( M + 1 ) e. NN0 ) |
191 |
187 190
|
expcld |
|- ( ( ph /\ y e. CC ) -> ( ( y - B ) ^ ( M + 1 ) ) e. CC ) |
192 |
144 191
|
sylan2 |
|- ( ( ph /\ y e. RR ) -> ( ( y - B ) ^ ( M + 1 ) ) e. CC ) |
193 |
90
|
adantr |
|- ( ( ph /\ y e. CC ) -> M e. CC ) |
194 |
|
1cnd |
|- ( ( ph /\ y e. CC ) -> 1 e. CC ) |
195 |
193 194
|
addcld |
|- ( ( ph /\ y e. CC ) -> ( M + 1 ) e. CC ) |
196 |
187 188
|
expcld |
|- ( ( ph /\ y e. CC ) -> ( ( y - B ) ^ M ) e. CC ) |
197 |
195 196
|
mulcld |
|- ( ( ph /\ y e. CC ) -> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) e. CC ) |
198 |
144 197
|
sylan2 |
|- ( ( ph /\ y e. RR ) -> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) e. CC ) |
199 |
21
|
prid2 |
|- CC e. { RR , CC } |
200 |
199
|
a1i |
|- ( ph -> CC e. { RR , CC } ) |
201 |
|
simpr |
|- ( ( ph /\ x e. CC ) -> x e. CC ) |
202 |
|
elfznn |
|- ( ( M + 1 ) e. ( 1 ... N ) -> ( M + 1 ) e. NN ) |
203 |
11 202
|
syl |
|- ( ph -> ( M + 1 ) e. NN ) |
204 |
203
|
nnnn0d |
|- ( ph -> ( M + 1 ) e. NN0 ) |
205 |
204
|
adantr |
|- ( ( ph /\ x e. CC ) -> ( M + 1 ) e. NN0 ) |
206 |
201 205
|
expcld |
|- ( ( ph /\ x e. CC ) -> ( x ^ ( M + 1 ) ) e. CC ) |
207 |
|
ovexd |
|- ( ( ph /\ x e. CC ) -> ( ( M + 1 ) x. ( x ^ M ) ) e. _V ) |
208 |
200
|
dvmptid |
|- ( ph -> ( CC _D ( y e. CC |-> y ) ) = ( y e. CC |-> 1 ) ) |
209 |
|
0cnd |
|- ( ( ph /\ y e. CC ) -> 0 e. CC ) |
210 |
48
|
recnd |
|- ( ph -> B e. CC ) |
211 |
200 210
|
dvmptc |
|- ( ph -> ( CC _D ( y e. CC |-> B ) ) = ( y e. CC |-> 0 ) ) |
212 |
200 184 194 208 186 209 211
|
dvmptsub |
|- ( ph -> ( CC _D ( y e. CC |-> ( y - B ) ) ) = ( y e. CC |-> ( 1 - 0 ) ) ) |
213 |
|
1m0e1 |
|- ( 1 - 0 ) = 1 |
214 |
213
|
mpteq2i |
|- ( y e. CC |-> ( 1 - 0 ) ) = ( y e. CC |-> 1 ) |
215 |
212 214
|
eqtrdi |
|- ( ph -> ( CC _D ( y e. CC |-> ( y - B ) ) ) = ( y e. CC |-> 1 ) ) |
216 |
|
dvexp |
|- ( ( M + 1 ) e. NN -> ( CC _D ( x e. CC |-> ( x ^ ( M + 1 ) ) ) ) = ( x e. CC |-> ( ( M + 1 ) x. ( x ^ ( ( M + 1 ) - 1 ) ) ) ) ) |
217 |
203 216
|
syl |
|- ( ph -> ( CC _D ( x e. CC |-> ( x ^ ( M + 1 ) ) ) ) = ( x e. CC |-> ( ( M + 1 ) x. ( x ^ ( ( M + 1 ) - 1 ) ) ) ) ) |
218 |
90 91
|
pncand |
|- ( ph -> ( ( M + 1 ) - 1 ) = M ) |
219 |
218
|
oveq2d |
|- ( ph -> ( x ^ ( ( M + 1 ) - 1 ) ) = ( x ^ M ) ) |
220 |
219
|
oveq2d |
|- ( ph -> ( ( M + 1 ) x. ( x ^ ( ( M + 1 ) - 1 ) ) ) = ( ( M + 1 ) x. ( x ^ M ) ) ) |
221 |
220
|
mpteq2dv |
|- ( ph -> ( x e. CC |-> ( ( M + 1 ) x. ( x ^ ( ( M + 1 ) - 1 ) ) ) ) = ( x e. CC |-> ( ( M + 1 ) x. ( x ^ M ) ) ) ) |
222 |
217 221
|
eqtrd |
|- ( ph -> ( CC _D ( x e. CC |-> ( x ^ ( M + 1 ) ) ) ) = ( x e. CC |-> ( ( M + 1 ) x. ( x ^ M ) ) ) ) |
223 |
|
oveq1 |
|- ( x = ( y - B ) -> ( x ^ ( M + 1 ) ) = ( ( y - B ) ^ ( M + 1 ) ) ) |
224 |
|
oveq1 |
|- ( x = ( y - B ) -> ( x ^ M ) = ( ( y - B ) ^ M ) ) |
225 |
224
|
oveq2d |
|- ( x = ( y - B ) -> ( ( M + 1 ) x. ( x ^ M ) ) = ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) |
226 |
200 200 187 194 206 207 215 222 223 225
|
dvmptco |
|- ( ph -> ( CC _D ( y e. CC |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) = ( y e. CC |-> ( ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) x. 1 ) ) ) |
227 |
197
|
mulid1d |
|- ( ( ph /\ y e. CC ) -> ( ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) x. 1 ) = ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) |
228 |
227
|
mpteq2dva |
|- ( ph -> ( y e. CC |-> ( ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) x. 1 ) ) = ( y e. CC |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) ) |
229 |
226 228
|
eqtrd |
|- ( ph -> ( CC _D ( y e. CC |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) = ( y e. CC |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) ) |
230 |
117 20 153 155 191 197 229
|
dvmptres3 |
|- ( ph -> ( RR _D ( y e. RR |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) = ( y e. RR |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) ) |
231 |
20 192 198 230 2 118 117 124
|
dvmptres |
|- ( ph -> ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) = ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) ) |
232 |
231
|
dmeqd |
|- ( ph -> dom ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) = dom ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) ) |
233 |
|
ovex |
|- ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) e. _V |
234 |
|
eqid |
|- ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) = ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) |
235 |
233 234
|
dmmpti |
|- dom ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) = A |
236 |
232 235
|
eqtrdi |
|- ( ph -> dom ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) = A ) |
237 |
126 236
|
sseqtrrid |
|- ( ph -> ( A \ { B } ) C_ dom ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ) |
238 |
20 27 2 14 47 6
|
dvntaylp0 |
|- ( ph -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` B ) = ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) ) |
239 |
238
|
oveq2d |
|- ( ph -> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` B ) ) = ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) - ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) ) ) |
240 |
116 5
|
ffvelrnd |
|- ( ph -> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) e. CC ) |
241 |
240
|
subidd |
|- ( ph -> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) - ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) ) = 0 ) |
242 |
239 241
|
eqtrd |
|- ( ph -> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` B ) ) = 0 ) |
243 |
117
|
subcn |
|- - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) |
244 |
243
|
a1i |
|- ( ph -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) ) |
245 |
|
dvcn |
|- ( ( ( RR C_ CC /\ ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : A --> CC /\ A C_ RR ) /\ dom ( RR _D ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) = A ) -> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) e. ( A -cn-> CC ) ) |
246 |
94 116 2 114 245
|
syl31anc |
|- ( ph -> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) e. ( A -cn-> CC ) ) |
247 |
138 246
|
eqeltrrd |
|- ( ph -> ( y e. A |-> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) ) e. ( A -cn-> CC ) ) |
248 |
|
plycn |
|- ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) e. ( Poly ` RR ) -> ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) e. ( CC -cn-> CC ) ) |
249 |
64 248
|
syl |
|- ( ph -> ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) e. ( CC -cn-> CC ) ) |
250 |
2 25
|
sstrdi |
|- ( ph -> A C_ CC ) |
251 |
|
cncfmptid |
|- ( ( A C_ CC /\ CC C_ CC ) -> ( y e. A |-> y ) e. ( A -cn-> CC ) ) |
252 |
250 160 251
|
sylancl |
|- ( ph -> ( y e. A |-> y ) e. ( A -cn-> CC ) ) |
253 |
249 252
|
cncfmpt1f |
|- ( ph -> ( y e. A |-> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) e. ( A -cn-> CC ) ) |
254 |
117 244 247 253
|
cncfmpt2f |
|- ( ph -> ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) e. ( A -cn-> CC ) ) |
255 |
|
fveq2 |
|- ( y = B -> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) = ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) ) |
256 |
|
fveq2 |
|- ( y = B -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` B ) ) |
257 |
255 256
|
oveq12d |
|- ( y = B -> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) = ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` B ) ) ) |
258 |
254 5 257
|
cnmptlimc |
|- ( ph -> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` B ) ) e. ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) limCC B ) ) |
259 |
242 258
|
eqeltrrd |
|- ( ph -> 0 e. ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) limCC B ) ) |
260 |
210
|
subidd |
|- ( ph -> ( B - B ) = 0 ) |
261 |
260
|
oveq1d |
|- ( ph -> ( ( B - B ) ^ ( M + 1 ) ) = ( 0 ^ ( M + 1 ) ) ) |
262 |
203
|
0expd |
|- ( ph -> ( 0 ^ ( M + 1 ) ) = 0 ) |
263 |
261 262
|
eqtrd |
|- ( ph -> ( ( B - B ) ^ ( M + 1 ) ) = 0 ) |
264 |
250
|
sselda |
|- ( ( ph /\ y e. A ) -> y e. CC ) |
265 |
264 191
|
syldan |
|- ( ( ph /\ y e. A ) -> ( ( y - B ) ^ ( M + 1 ) ) e. CC ) |
266 |
265
|
fmpttd |
|- ( ph -> ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) : A --> CC ) |
267 |
|
dvcn |
|- ( ( ( RR C_ CC /\ ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) : A --> CC /\ A C_ RR ) /\ dom ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) = A ) -> ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) e. ( A -cn-> CC ) ) |
268 |
94 266 2 236 267
|
syl31anc |
|- ( ph -> ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) e. ( A -cn-> CC ) ) |
269 |
|
oveq1 |
|- ( y = B -> ( y - B ) = ( B - B ) ) |
270 |
269
|
oveq1d |
|- ( y = B -> ( ( y - B ) ^ ( M + 1 ) ) = ( ( B - B ) ^ ( M + 1 ) ) ) |
271 |
268 5 270
|
cnmptlimc |
|- ( ph -> ( ( B - B ) ^ ( M + 1 ) ) e. ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) limCC B ) ) |
272 |
263 271
|
eqeltrrd |
|- ( ph -> 0 e. ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) limCC B ) ) |
273 |
250
|
ssdifssd |
|- ( ph -> ( A \ { B } ) C_ CC ) |
274 |
273
|
sselda |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> y e. CC ) |
275 |
210
|
adantr |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> B e. CC ) |
276 |
274 275
|
subcld |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> ( y - B ) e. CC ) |
277 |
|
eldifsni |
|- ( y e. ( A \ { B } ) -> y =/= B ) |
278 |
277
|
adantl |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> y =/= B ) |
279 |
274 275 278
|
subne0d |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> ( y - B ) =/= 0 ) |
280 |
203
|
adantr |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> ( M + 1 ) e. NN ) |
281 |
280
|
nnzd |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> ( M + 1 ) e. ZZ ) |
282 |
276 279 281
|
expne0d |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> ( ( y - B ) ^ ( M + 1 ) ) =/= 0 ) |
283 |
282
|
necomd |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> 0 =/= ( ( y - B ) ^ ( M + 1 ) ) ) |
284 |
283
|
neneqd |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> -. 0 = ( ( y - B ) ^ ( M + 1 ) ) ) |
285 |
284
|
nrexdv |
|- ( ph -> -. E. y e. ( A \ { B } ) 0 = ( ( y - B ) ^ ( M + 1 ) ) ) |
286 |
|
df-ima |
|- ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) " ( A \ { B } ) ) = ran ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) |` ( A \ { B } ) ) |
287 |
286
|
eleq2i |
|- ( 0 e. ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) " ( A \ { B } ) ) <-> 0 e. ran ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) |` ( A \ { B } ) ) ) |
288 |
|
resmpt |
|- ( ( A \ { B } ) C_ A -> ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) |` ( A \ { B } ) ) = ( y e. ( A \ { B } ) |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) |
289 |
126 288
|
ax-mp |
|- ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) |` ( A \ { B } ) ) = ( y e. ( A \ { B } ) |-> ( ( y - B ) ^ ( M + 1 ) ) ) |
290 |
|
ovex |
|- ( ( y - B ) ^ ( M + 1 ) ) e. _V |
291 |
289 290
|
elrnmpti |
|- ( 0 e. ran ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) |` ( A \ { B } ) ) <-> E. y e. ( A \ { B } ) 0 = ( ( y - B ) ^ ( M + 1 ) ) ) |
292 |
287 291
|
bitri |
|- ( 0 e. ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) " ( A \ { B } ) ) <-> E. y e. ( A \ { B } ) 0 = ( ( y - B ) ^ ( M + 1 ) ) ) |
293 |
285 292
|
sylnibr |
|- ( ph -> -. 0 e. ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) " ( A \ { B } ) ) ) |
294 |
90
|
adantr |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> M e. CC ) |
295 |
|
1cnd |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> 1 e. CC ) |
296 |
294 295
|
addcld |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> ( M + 1 ) e. CC ) |
297 |
274 196
|
syldan |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> ( ( y - B ) ^ M ) e. CC ) |
298 |
280
|
nnne0d |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> ( M + 1 ) =/= 0 ) |
299 |
77
|
adantr |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> M e. NN ) |
300 |
299
|
nnzd |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> M e. ZZ ) |
301 |
276 279 300
|
expne0d |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> ( ( y - B ) ^ M ) =/= 0 ) |
302 |
296 297 298 301
|
mulne0d |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) =/= 0 ) |
303 |
302
|
necomd |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> 0 =/= ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) |
304 |
303
|
neneqd |
|- ( ( ph /\ y e. ( A \ { B } ) ) -> -. 0 = ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) |
305 |
304
|
nrexdv |
|- ( ph -> -. E. y e. ( A \ { B } ) 0 = ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) |
306 |
231
|
imaeq1d |
|- ( ph -> ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) " ( A \ { B } ) ) = ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) " ( A \ { B } ) ) ) |
307 |
|
df-ima |
|- ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) " ( A \ { B } ) ) = ran ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) |` ( A \ { B } ) ) |
308 |
306 307
|
eqtrdi |
|- ( ph -> ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) " ( A \ { B } ) ) = ran ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) |` ( A \ { B } ) ) ) |
309 |
308
|
eleq2d |
|- ( ph -> ( 0 e. ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) " ( A \ { B } ) ) <-> 0 e. ran ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) |` ( A \ { B } ) ) ) ) |
310 |
|
resmpt |
|- ( ( A \ { B } ) C_ A -> ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) |` ( A \ { B } ) ) = ( y e. ( A \ { B } ) |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) ) |
311 |
126 310
|
ax-mp |
|- ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) |` ( A \ { B } ) ) = ( y e. ( A \ { B } ) |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) |
312 |
311 233
|
elrnmpti |
|- ( 0 e. ran ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) |` ( A \ { B } ) ) <-> E. y e. ( A \ { B } ) 0 = ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) |
313 |
309 312
|
bitrdi |
|- ( ph -> ( 0 e. ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) " ( A \ { B } ) ) <-> E. y e. ( A \ { B } ) 0 = ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) ) |
314 |
305 313
|
mtbird |
|- ( ph -> -. 0 e. ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) " ( A \ { B } ) ) ) |
315 |
|
eldifi |
|- ( x e. ( A \ { B } ) -> x e. A ) |
316 |
131
|
ffvelrnda |
|- ( ( ph /\ x e. A ) -> ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) e. CC ) |
317 |
315 316
|
sylan2 |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) e. CC ) |
318 |
2
|
ssdifssd |
|- ( ph -> ( A \ { B } ) C_ RR ) |
319 |
318
|
sselda |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> x e. RR ) |
320 |
319
|
recnd |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> x e. CC ) |
321 |
148
|
ffvelrnda |
|- ( ( ph /\ x e. CC ) -> ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) e. CC ) |
322 |
320 321
|
syldan |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) e. CC ) |
323 |
317 322
|
subcld |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) e. CC ) |
324 |
48
|
adantr |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> B e. RR ) |
325 |
319 324
|
resubcld |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( x - B ) e. RR ) |
326 |
78
|
adantr |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> M e. NN0 ) |
327 |
325 326
|
reexpcld |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( x - B ) ^ M ) e. RR ) |
328 |
327
|
recnd |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( x - B ) ^ M ) e. CC ) |
329 |
324
|
recnd |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> B e. CC ) |
330 |
320 329
|
subcld |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( x - B ) e. CC ) |
331 |
|
eldifsni |
|- ( x e. ( A \ { B } ) -> x =/= B ) |
332 |
331
|
adantl |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> x =/= B ) |
333 |
320 329 332
|
subne0d |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( x - B ) =/= 0 ) |
334 |
326
|
nn0zd |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> M e. ZZ ) |
335 |
330 333 334
|
expne0d |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( x - B ) ^ M ) =/= 0 ) |
336 |
323 328 335
|
divcld |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) e. CC ) |
337 |
203
|
nnrecred |
|- ( ph -> ( 1 / ( M + 1 ) ) e. RR ) |
338 |
337
|
recnd |
|- ( ph -> ( 1 / ( M + 1 ) ) e. CC ) |
339 |
338
|
adantr |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( 1 / ( M + 1 ) ) e. CC ) |
340 |
|
txtopon |
|- ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) e. ( TopOn ` ( CC X. CC ) ) ) |
341 |
151 151 340
|
mp2an |
|- ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) e. ( TopOn ` ( CC X. CC ) ) |
342 |
341
|
toponrestid |
|- ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) = ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) |`t ( CC X. CC ) ) |
343 |
|
limcresi |
|- ( ( x e. A |-> ( 1 / ( M + 1 ) ) ) limCC B ) C_ ( ( ( x e. A |-> ( 1 / ( M + 1 ) ) ) |` ( A \ { B } ) ) limCC B ) |
344 |
|
resmpt |
|- ( ( A \ { B } ) C_ A -> ( ( x e. A |-> ( 1 / ( M + 1 ) ) ) |` ( A \ { B } ) ) = ( x e. ( A \ { B } ) |-> ( 1 / ( M + 1 ) ) ) ) |
345 |
126 344
|
ax-mp |
|- ( ( x e. A |-> ( 1 / ( M + 1 ) ) ) |` ( A \ { B } ) ) = ( x e. ( A \ { B } ) |-> ( 1 / ( M + 1 ) ) ) |
346 |
345
|
oveq1i |
|- ( ( ( x e. A |-> ( 1 / ( M + 1 ) ) ) |` ( A \ { B } ) ) limCC B ) = ( ( x e. ( A \ { B } ) |-> ( 1 / ( M + 1 ) ) ) limCC B ) |
347 |
343 346
|
sseqtri |
|- ( ( x e. A |-> ( 1 / ( M + 1 ) ) ) limCC B ) C_ ( ( x e. ( A \ { B } ) |-> ( 1 / ( M + 1 ) ) ) limCC B ) |
348 |
|
cncfmptc |
|- ( ( ( 1 / ( M + 1 ) ) e. RR /\ A C_ CC /\ RR C_ CC ) -> ( x e. A |-> ( 1 / ( M + 1 ) ) ) e. ( A -cn-> RR ) ) |
349 |
337 250 94 348
|
syl3anc |
|- ( ph -> ( x e. A |-> ( 1 / ( M + 1 ) ) ) e. ( A -cn-> RR ) ) |
350 |
|
eqidd |
|- ( x = B -> ( 1 / ( M + 1 ) ) = ( 1 / ( M + 1 ) ) ) |
351 |
349 5 350
|
cnmptlimc |
|- ( ph -> ( 1 / ( M + 1 ) ) e. ( ( x e. A |-> ( 1 / ( M + 1 ) ) ) limCC B ) ) |
352 |
347 351
|
sselid |
|- ( ph -> ( 1 / ( M + 1 ) ) e. ( ( x e. ( A \ { B } ) |-> ( 1 / ( M + 1 ) ) ) limCC B ) ) |
353 |
117
|
mulcn |
|- x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) |
354 |
|
0cn |
|- 0 e. CC |
355 |
|
opelxpi |
|- ( ( 0 e. CC /\ ( 1 / ( M + 1 ) ) e. CC ) -> <. 0 , ( 1 / ( M + 1 ) ) >. e. ( CC X. CC ) ) |
356 |
354 338 355
|
sylancr |
|- ( ph -> <. 0 , ( 1 / ( M + 1 ) ) >. e. ( CC X. CC ) ) |
357 |
341
|
toponunii |
|- ( CC X. CC ) = U. ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) |
358 |
357
|
cncnpi |
|- ( ( x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) /\ <. 0 , ( 1 / ( M + 1 ) ) >. e. ( CC X. CC ) ) -> x. e. ( ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) CnP ( TopOpen ` CCfld ) ) ` <. 0 , ( 1 / ( M + 1 ) ) >. ) ) |
359 |
353 356 358
|
sylancr |
|- ( ph -> x. e. ( ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) CnP ( TopOpen ` CCfld ) ) ` <. 0 , ( 1 / ( M + 1 ) ) >. ) ) |
360 |
336 339 161 161 117 342 8 352 359
|
limccnp2 |
|- ( ph -> ( 0 x. ( 1 / ( M + 1 ) ) ) e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) limCC B ) ) |
361 |
338
|
mul02d |
|- ( ph -> ( 0 x. ( 1 / ( M + 1 ) ) ) = 0 ) |
362 |
177
|
fveq1d |
|- ( ph -> ( ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) ` x ) = ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) ` x ) ) |
363 |
|
fveq2 |
|- ( y = x -> ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) = ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) ) |
364 |
|
fveq2 |
|- ( y = x -> ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) |
365 |
363 364
|
oveq12d |
|- ( y = x -> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) = ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) ) |
366 |
|
ovex |
|- ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) e. _V |
367 |
365 180 366
|
fvmpt |
|- ( x e. A -> ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) ` x ) = ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) ) |
368 |
315 367
|
syl |
|- ( x e. ( A \ { B } ) -> ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) ` x ) = ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) ) |
369 |
362 368
|
sylan9eq |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) ` x ) = ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) ) |
370 |
231
|
fveq1d |
|- ( ph -> ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) = ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) ` x ) ) |
371 |
|
oveq1 |
|- ( y = x -> ( y - B ) = ( x - B ) ) |
372 |
371
|
oveq1d |
|- ( y = x -> ( ( y - B ) ^ M ) = ( ( x - B ) ^ M ) ) |
373 |
372
|
oveq2d |
|- ( y = x -> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) = ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) ) |
374 |
|
ovex |
|- ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) e. _V |
375 |
373 234 374
|
fvmpt |
|- ( x e. A -> ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) ` x ) = ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) ) |
376 |
315 375
|
syl |
|- ( x e. ( A \ { B } ) -> ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) ` x ) = ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) ) |
377 |
370 376
|
sylan9eq |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) = ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) ) |
378 |
203
|
adantr |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( M + 1 ) e. NN ) |
379 |
378
|
nncnd |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( M + 1 ) e. CC ) |
380 |
379 328
|
mulcomd |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) = ( ( ( x - B ) ^ M ) x. ( M + 1 ) ) ) |
381 |
377 380
|
eqtrd |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) = ( ( ( x - B ) ^ M ) x. ( M + 1 ) ) ) |
382 |
369 381
|
oveq12d |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) ` x ) / ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) ) = ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( ( x - B ) ^ M ) x. ( M + 1 ) ) ) ) |
383 |
378
|
nnne0d |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( M + 1 ) =/= 0 ) |
384 |
323 328 379 335 383
|
divdiv1d |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) / ( M + 1 ) ) = ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( ( x - B ) ^ M ) x. ( M + 1 ) ) ) ) |
385 |
336 379 383
|
divrecd |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) / ( M + 1 ) ) = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) |
386 |
382 384 385
|
3eqtr2rd |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) = ( ( ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) ` x ) / ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) ) ) |
387 |
386
|
mpteq2dva |
|- ( ph -> ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) = ( x e. ( A \ { B } ) |-> ( ( ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) ` x ) / ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) ) ) ) |
388 |
387
|
oveq1d |
|- ( ph -> ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) limCC B ) = ( ( x e. ( A \ { B } ) |-> ( ( ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) ` x ) / ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) ) ) limCC B ) ) |
389 |
360 361 388
|
3eltr3d |
|- ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) ` x ) / ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) ) ) limCC B ) ) |
390 |
2 71 84 124 5 125 183 237 259 272 293 314 389
|
lhop |
|- ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ` x ) / ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ` x ) ) ) limCC B ) ) |
391 |
315
|
adantl |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> x e. A ) |
392 |
|
fveq2 |
|- ( y = x -> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) = ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) ) |
393 |
|
fveq2 |
|- ( y = x -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) |
394 |
392 393
|
oveq12d |
|- ( y = x -> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) = ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) ) |
395 |
|
eqid |
|- ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) = ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) |
396 |
|
ovex |
|- ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) e. _V |
397 |
394 395 396
|
fvmpt |
|- ( x e. A -> ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ` x ) = ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) ) |
398 |
391 397
|
syl |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ` x ) = ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) ) |
399 |
371
|
oveq1d |
|- ( y = x -> ( ( y - B ) ^ ( M + 1 ) ) = ( ( x - B ) ^ ( M + 1 ) ) ) |
400 |
|
eqid |
|- ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) = ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) |
401 |
|
ovex |
|- ( ( x - B ) ^ ( M + 1 ) ) e. _V |
402 |
399 400 401
|
fvmpt |
|- ( x e. A -> ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ` x ) = ( ( x - B ) ^ ( M + 1 ) ) ) |
403 |
391 402
|
syl |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ` x ) = ( ( x - B ) ^ ( M + 1 ) ) ) |
404 |
398 403
|
oveq12d |
|- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ` x ) / ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ` x ) ) = ( ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( M + 1 ) ) ) ) |
405 |
404
|
mpteq2dva |
|- ( ph -> ( x e. ( A \ { B } ) |-> ( ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ` x ) / ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ` x ) ) ) = ( x e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( M + 1 ) ) ) ) ) |
406 |
405
|
oveq1d |
|- ( ph -> ( ( x e. ( A \ { B } ) |-> ( ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ` x ) / ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ` x ) ) ) limCC B ) = ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( M + 1 ) ) ) ) limCC B ) ) |
407 |
390 406
|
eleqtrd |
|- ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( M + 1 ) ) ) ) limCC B ) ) |