Step |
Hyp |
Ref |
Expression |
1 |
|
dvnxpaek.s |
|- ( ph -> S e. { RR , CC } ) |
2 |
|
dvnxpaek.x |
|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) ) |
3 |
|
dvnxpaek.a |
|- ( ph -> A e. CC ) |
4 |
|
dvnxpaek.k |
|- ( ph -> K e. NN0 ) |
5 |
|
dvnxpaek.f |
|- F = ( x e. X |-> ( ( x + A ) ^ K ) ) |
6 |
|
fveq2 |
|- ( n = 0 -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` 0 ) ) |
7 |
|
breq2 |
|- ( n = 0 -> ( K < n <-> K < 0 ) ) |
8 |
|
eqidd |
|- ( n = 0 -> 0 = 0 ) |
9 |
|
oveq2 |
|- ( n = 0 -> ( K - n ) = ( K - 0 ) ) |
10 |
9
|
fveq2d |
|- ( n = 0 -> ( ! ` ( K - n ) ) = ( ! ` ( K - 0 ) ) ) |
11 |
10
|
oveq2d |
|- ( n = 0 -> ( ( ! ` K ) / ( ! ` ( K - n ) ) ) = ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) ) |
12 |
9
|
oveq2d |
|- ( n = 0 -> ( ( x + A ) ^ ( K - n ) ) = ( ( x + A ) ^ ( K - 0 ) ) ) |
13 |
11 12
|
oveq12d |
|- ( n = 0 -> ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) ) |
14 |
7 8 13
|
ifbieq12d |
|- ( n = 0 -> if ( K < n , 0 , ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) ) = if ( K < 0 , 0 , ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) ) ) |
15 |
14
|
mpteq2dv |
|- ( n = 0 -> ( x e. X |-> if ( K < n , 0 , ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) ) ) = ( x e. X |-> if ( K < 0 , 0 , ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) ) ) ) |
16 |
6 15
|
eqeq12d |
|- ( n = 0 -> ( ( ( S Dn F ) ` n ) = ( x e. X |-> if ( K < n , 0 , ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) ) ) <-> ( ( S Dn F ) ` 0 ) = ( x e. X |-> if ( K < 0 , 0 , ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) ) ) ) ) |
17 |
|
fveq2 |
|- ( n = m -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` m ) ) |
18 |
|
breq2 |
|- ( n = m -> ( K < n <-> K < m ) ) |
19 |
|
eqidd |
|- ( n = m -> 0 = 0 ) |
20 |
|
oveq2 |
|- ( n = m -> ( K - n ) = ( K - m ) ) |
21 |
20
|
fveq2d |
|- ( n = m -> ( ! ` ( K - n ) ) = ( ! ` ( K - m ) ) ) |
22 |
21
|
oveq2d |
|- ( n = m -> ( ( ! ` K ) / ( ! ` ( K - n ) ) ) = ( ( ! ` K ) / ( ! ` ( K - m ) ) ) ) |
23 |
20
|
oveq2d |
|- ( n = m -> ( ( x + A ) ^ ( K - n ) ) = ( ( x + A ) ^ ( K - m ) ) ) |
24 |
22 23
|
oveq12d |
|- ( n = m -> ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) |
25 |
18 19 24
|
ifbieq12d |
|- ( n = m -> if ( K < n , 0 , ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) ) = if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) |
26 |
25
|
mpteq2dv |
|- ( n = m -> ( x e. X |-> if ( K < n , 0 , ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) ) ) = ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) |
27 |
17 26
|
eqeq12d |
|- ( n = m -> ( ( ( S Dn F ) ` n ) = ( x e. X |-> if ( K < n , 0 , ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) ) ) <-> ( ( S Dn F ) ` m ) = ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) ) |
28 |
|
fveq2 |
|- ( n = ( m + 1 ) -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` ( m + 1 ) ) ) |
29 |
|
breq2 |
|- ( n = ( m + 1 ) -> ( K < n <-> K < ( m + 1 ) ) ) |
30 |
|
eqidd |
|- ( n = ( m + 1 ) -> 0 = 0 ) |
31 |
|
oveq2 |
|- ( n = ( m + 1 ) -> ( K - n ) = ( K - ( m + 1 ) ) ) |
32 |
31
|
fveq2d |
|- ( n = ( m + 1 ) -> ( ! ` ( K - n ) ) = ( ! ` ( K - ( m + 1 ) ) ) ) |
33 |
32
|
oveq2d |
|- ( n = ( m + 1 ) -> ( ( ! ` K ) / ( ! ` ( K - n ) ) ) = ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) ) |
34 |
31
|
oveq2d |
|- ( n = ( m + 1 ) -> ( ( x + A ) ^ ( K - n ) ) = ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) |
35 |
33 34
|
oveq12d |
|- ( n = ( m + 1 ) -> ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) |
36 |
29 30 35
|
ifbieq12d |
|- ( n = ( m + 1 ) -> if ( K < n , 0 , ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) ) = if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) |
37 |
36
|
mpteq2dv |
|- ( n = ( m + 1 ) -> ( x e. X |-> if ( K < n , 0 , ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) ) ) = ( x e. X |-> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) ) |
38 |
28 37
|
eqeq12d |
|- ( n = ( m + 1 ) -> ( ( ( S Dn F ) ` n ) = ( x e. X |-> if ( K < n , 0 , ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) ) ) <-> ( ( S Dn F ) ` ( m + 1 ) ) = ( x e. X |-> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) ) ) |
39 |
|
fveq2 |
|- ( n = N -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` N ) ) |
40 |
|
breq2 |
|- ( n = N -> ( K < n <-> K < N ) ) |
41 |
|
eqidd |
|- ( n = N -> 0 = 0 ) |
42 |
|
oveq2 |
|- ( n = N -> ( K - n ) = ( K - N ) ) |
43 |
42
|
fveq2d |
|- ( n = N -> ( ! ` ( K - n ) ) = ( ! ` ( K - N ) ) ) |
44 |
43
|
oveq2d |
|- ( n = N -> ( ( ! ` K ) / ( ! ` ( K - n ) ) ) = ( ( ! ` K ) / ( ! ` ( K - N ) ) ) ) |
45 |
42
|
oveq2d |
|- ( n = N -> ( ( x + A ) ^ ( K - n ) ) = ( ( x + A ) ^ ( K - N ) ) ) |
46 |
44 45
|
oveq12d |
|- ( n = N -> ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - N ) ) ) x. ( ( x + A ) ^ ( K - N ) ) ) ) |
47 |
40 41 46
|
ifbieq12d |
|- ( n = N -> if ( K < n , 0 , ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) ) = if ( K < N , 0 , ( ( ( ! ` K ) / ( ! ` ( K - N ) ) ) x. ( ( x + A ) ^ ( K - N ) ) ) ) ) |
48 |
47
|
mpteq2dv |
|- ( n = N -> ( x e. X |-> if ( K < n , 0 , ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) ) ) = ( x e. X |-> if ( K < N , 0 , ( ( ( ! ` K ) / ( ! ` ( K - N ) ) ) x. ( ( x + A ) ^ ( K - N ) ) ) ) ) ) |
49 |
39 48
|
eqeq12d |
|- ( n = N -> ( ( ( S Dn F ) ` n ) = ( x e. X |-> if ( K < n , 0 , ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) ) ) <-> ( ( S Dn F ) ` N ) = ( x e. X |-> if ( K < N , 0 , ( ( ( ! ` K ) / ( ! ` ( K - N ) ) ) x. ( ( x + A ) ^ ( K - N ) ) ) ) ) ) ) |
50 |
|
recnprss |
|- ( S e. { RR , CC } -> S C_ CC ) |
51 |
1 50
|
syl |
|- ( ph -> S C_ CC ) |
52 |
|
cnex |
|- CC e. _V |
53 |
52
|
a1i |
|- ( ph -> CC e. _V ) |
54 |
|
restsspw |
|- ( ( TopOpen ` CCfld ) |`t S ) C_ ~P S |
55 |
|
id |
|- ( X e. ( ( TopOpen ` CCfld ) |`t S ) -> X e. ( ( TopOpen ` CCfld ) |`t S ) ) |
56 |
54 55
|
sseldi |
|- ( X e. ( ( TopOpen ` CCfld ) |`t S ) -> X e. ~P S ) |
57 |
|
elpwi |
|- ( X e. ~P S -> X C_ S ) |
58 |
56 57
|
syl |
|- ( X e. ( ( TopOpen ` CCfld ) |`t S ) -> X C_ S ) |
59 |
2 58
|
syl |
|- ( ph -> X C_ S ) |
60 |
59 51
|
sstrd |
|- ( ph -> X C_ CC ) |
61 |
60
|
adantr |
|- ( ( ph /\ x e. X ) -> X C_ CC ) |
62 |
|
simpr |
|- ( ( ph /\ x e. X ) -> x e. X ) |
63 |
61 62
|
sseldd |
|- ( ( ph /\ x e. X ) -> x e. CC ) |
64 |
3
|
adantr |
|- ( ( ph /\ x e. X ) -> A e. CC ) |
65 |
63 64
|
addcld |
|- ( ( ph /\ x e. X ) -> ( x + A ) e. CC ) |
66 |
4
|
adantr |
|- ( ( ph /\ x e. X ) -> K e. NN0 ) |
67 |
65 66
|
expcld |
|- ( ( ph /\ x e. X ) -> ( ( x + A ) ^ K ) e. CC ) |
68 |
67 5
|
fmptd |
|- ( ph -> F : X --> CC ) |
69 |
|
elpm2r |
|- ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( F : X --> CC /\ X C_ S ) ) -> F e. ( CC ^pm S ) ) |
70 |
53 1 68 59 69
|
syl22anc |
|- ( ph -> F e. ( CC ^pm S ) ) |
71 |
|
dvn0 |
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F ) |
72 |
51 70 71
|
syl2anc |
|- ( ph -> ( ( S Dn F ) ` 0 ) = F ) |
73 |
5
|
a1i |
|- ( ph -> F = ( x e. X |-> ( ( x + A ) ^ K ) ) ) |
74 |
4
|
nn0ge0d |
|- ( ph -> 0 <_ K ) |
75 |
|
0red |
|- ( ph -> 0 e. RR ) |
76 |
4
|
nn0red |
|- ( ph -> K e. RR ) |
77 |
75 76
|
lenltd |
|- ( ph -> ( 0 <_ K <-> -. K < 0 ) ) |
78 |
74 77
|
mpbid |
|- ( ph -> -. K < 0 ) |
79 |
78
|
iffalsed |
|- ( ph -> if ( K < 0 , 0 , ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) ) |
80 |
79
|
adantr |
|- ( ( ph /\ x e. X ) -> if ( K < 0 , 0 , ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) ) |
81 |
4
|
nn0cnd |
|- ( ph -> K e. CC ) |
82 |
81
|
subid1d |
|- ( ph -> ( K - 0 ) = K ) |
83 |
82
|
fveq2d |
|- ( ph -> ( ! ` ( K - 0 ) ) = ( ! ` K ) ) |
84 |
83
|
oveq2d |
|- ( ph -> ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) = ( ( ! ` K ) / ( ! ` K ) ) ) |
85 |
|
faccl |
|- ( K e. NN0 -> ( ! ` K ) e. NN ) |
86 |
4 85
|
syl |
|- ( ph -> ( ! ` K ) e. NN ) |
87 |
86
|
nncnd |
|- ( ph -> ( ! ` K ) e. CC ) |
88 |
86
|
nnne0d |
|- ( ph -> ( ! ` K ) =/= 0 ) |
89 |
87 88
|
dividd |
|- ( ph -> ( ( ! ` K ) / ( ! ` K ) ) = 1 ) |
90 |
84 89
|
eqtrd |
|- ( ph -> ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) = 1 ) |
91 |
82
|
oveq2d |
|- ( ph -> ( ( x + A ) ^ ( K - 0 ) ) = ( ( x + A ) ^ K ) ) |
92 |
90 91
|
oveq12d |
|- ( ph -> ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) = ( 1 x. ( ( x + A ) ^ K ) ) ) |
93 |
92
|
adantr |
|- ( ( ph /\ x e. X ) -> ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) = ( 1 x. ( ( x + A ) ^ K ) ) ) |
94 |
67
|
mulid2d |
|- ( ( ph /\ x e. X ) -> ( 1 x. ( ( x + A ) ^ K ) ) = ( ( x + A ) ^ K ) ) |
95 |
80 93 94
|
3eqtrrd |
|- ( ( ph /\ x e. X ) -> ( ( x + A ) ^ K ) = if ( K < 0 , 0 , ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) ) ) |
96 |
95
|
mpteq2dva |
|- ( ph -> ( x e. X |-> ( ( x + A ) ^ K ) ) = ( x e. X |-> if ( K < 0 , 0 , ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) ) ) ) |
97 |
72 73 96
|
3eqtrd |
|- ( ph -> ( ( S Dn F ) ` 0 ) = ( x e. X |-> if ( K < 0 , 0 , ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) ) ) ) |
98 |
51
|
adantr |
|- ( ( ph /\ m e. NN0 ) -> S C_ CC ) |
99 |
70
|
adantr |
|- ( ( ph /\ m e. NN0 ) -> F e. ( CC ^pm S ) ) |
100 |
|
simpr |
|- ( ( ph /\ m e. NN0 ) -> m e. NN0 ) |
101 |
|
dvnp1 |
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ m e. NN0 ) -> ( ( S Dn F ) ` ( m + 1 ) ) = ( S _D ( ( S Dn F ) ` m ) ) ) |
102 |
98 99 100 101
|
syl3anc |
|- ( ( ph /\ m e. NN0 ) -> ( ( S Dn F ) ` ( m + 1 ) ) = ( S _D ( ( S Dn F ) ` m ) ) ) |
103 |
102
|
adantr |
|- ( ( ( ph /\ m e. NN0 ) /\ ( ( S Dn F ) ` m ) = ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) -> ( ( S Dn F ) ` ( m + 1 ) ) = ( S _D ( ( S Dn F ) ` m ) ) ) |
104 |
|
oveq2 |
|- ( ( ( S Dn F ) ` m ) = ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) -> ( S _D ( ( S Dn F ) ` m ) ) = ( S _D ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) ) |
105 |
104
|
adantl |
|- ( ( ( ph /\ m e. NN0 ) /\ ( ( S Dn F ) ` m ) = ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) -> ( S _D ( ( S Dn F ) ` m ) ) = ( S _D ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) ) |
106 |
|
iftrue |
|- ( K < m -> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) = 0 ) |
107 |
106
|
mpteq2dv |
|- ( K < m -> ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) = ( x e. X |-> 0 ) ) |
108 |
107
|
oveq2d |
|- ( K < m -> ( S _D ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) = ( S _D ( x e. X |-> 0 ) ) ) |
109 |
108
|
adantl |
|- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> ( S _D ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) = ( S _D ( x e. X |-> 0 ) ) ) |
110 |
|
0cnd |
|- ( ph -> 0 e. CC ) |
111 |
1 2 110
|
dvmptconst |
|- ( ph -> ( S _D ( x e. X |-> 0 ) ) = ( x e. X |-> 0 ) ) |
112 |
111
|
ad2antrr |
|- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> ( S _D ( x e. X |-> 0 ) ) = ( x e. X |-> 0 ) ) |
113 |
76
|
ad2antrr |
|- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> K e. RR ) |
114 |
|
nn0re |
|- ( m e. NN0 -> m e. RR ) |
115 |
114
|
ad2antlr |
|- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> m e. RR ) |
116 |
|
simpr |
|- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> K < m ) |
117 |
113 115 116
|
ltled |
|- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> K <_ m ) |
118 |
4
|
nn0zd |
|- ( ph -> K e. ZZ ) |
119 |
118
|
adantr |
|- ( ( ph /\ m e. NN0 ) -> K e. ZZ ) |
120 |
100
|
nn0zd |
|- ( ( ph /\ m e. NN0 ) -> m e. ZZ ) |
121 |
|
zleltp1 |
|- ( ( K e. ZZ /\ m e. ZZ ) -> ( K <_ m <-> K < ( m + 1 ) ) ) |
122 |
119 120 121
|
syl2anc |
|- ( ( ph /\ m e. NN0 ) -> ( K <_ m <-> K < ( m + 1 ) ) ) |
123 |
122
|
adantr |
|- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> ( K <_ m <-> K < ( m + 1 ) ) ) |
124 |
117 123
|
mpbid |
|- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> K < ( m + 1 ) ) |
125 |
124
|
iftrued |
|- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) = 0 ) |
126 |
125
|
mpteq2dv |
|- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> ( x e. X |-> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) = ( x e. X |-> 0 ) ) |
127 |
126
|
eqcomd |
|- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> ( x e. X |-> 0 ) = ( x e. X |-> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) ) |
128 |
109 112 127
|
3eqtrd |
|- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> ( S _D ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) = ( x e. X |-> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) ) |
129 |
|
simpl |
|- ( ( ( ph /\ m e. NN0 ) /\ -. K < m ) -> ( ph /\ m e. NN0 ) ) |
130 |
|
simpr |
|- ( ( ( ph /\ m e. NN0 ) /\ -. K < m ) -> -. K < m ) |
131 |
129 100 114
|
3syl |
|- ( ( ( ph /\ m e. NN0 ) /\ -. K < m ) -> m e. RR ) |
132 |
76
|
ad2antrr |
|- ( ( ( ph /\ m e. NN0 ) /\ -. K < m ) -> K e. RR ) |
133 |
131 132
|
lenltd |
|- ( ( ( ph /\ m e. NN0 ) /\ -. K < m ) -> ( m <_ K <-> -. K < m ) ) |
134 |
130 133
|
mpbird |
|- ( ( ( ph /\ m e. NN0 ) /\ -. K < m ) -> m <_ K ) |
135 |
|
simpr |
|- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> m = K ) |
136 |
114
|
ad2antlr |
|- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> m e. RR ) |
137 |
76
|
ad2antrr |
|- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> K e. RR ) |
138 |
136 137
|
lttri3d |
|- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> ( m = K <-> ( -. m < K /\ -. K < m ) ) ) |
139 |
135 138
|
mpbid |
|- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> ( -. m < K /\ -. K < m ) ) |
140 |
|
simpr |
|- ( ( -. m < K /\ -. K < m ) -> -. K < m ) |
141 |
139 140
|
syl |
|- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> -. K < m ) |
142 |
141
|
iffalsed |
|- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) |
143 |
142
|
mpteq2dv |
|- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) = ( x e. X |-> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) |
144 |
143
|
oveq2d |
|- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> ( S _D ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) = ( S _D ( x e. X |-> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) |
145 |
|
oveq2 |
|- ( m = K -> ( K - m ) = ( K - K ) ) |
146 |
145
|
fveq2d |
|- ( m = K -> ( ! ` ( K - m ) ) = ( ! ` ( K - K ) ) ) |
147 |
146
|
adantl |
|- ( ( ph /\ m = K ) -> ( ! ` ( K - m ) ) = ( ! ` ( K - K ) ) ) |
148 |
81
|
subidd |
|- ( ph -> ( K - K ) = 0 ) |
149 |
148
|
fveq2d |
|- ( ph -> ( ! ` ( K - K ) ) = ( ! ` 0 ) ) |
150 |
|
fac0 |
|- ( ! ` 0 ) = 1 |
151 |
150
|
a1i |
|- ( ph -> ( ! ` 0 ) = 1 ) |
152 |
149 151
|
eqtrd |
|- ( ph -> ( ! ` ( K - K ) ) = 1 ) |
153 |
152
|
adantr |
|- ( ( ph /\ m = K ) -> ( ! ` ( K - K ) ) = 1 ) |
154 |
147 153
|
eqtrd |
|- ( ( ph /\ m = K ) -> ( ! ` ( K - m ) ) = 1 ) |
155 |
154
|
oveq2d |
|- ( ( ph /\ m = K ) -> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) = ( ( ! ` K ) / 1 ) ) |
156 |
87
|
div1d |
|- ( ph -> ( ( ! ` K ) / 1 ) = ( ! ` K ) ) |
157 |
156
|
adantr |
|- ( ( ph /\ m = K ) -> ( ( ! ` K ) / 1 ) = ( ! ` K ) ) |
158 |
155 157
|
eqtrd |
|- ( ( ph /\ m = K ) -> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) = ( ! ` K ) ) |
159 |
158
|
adantr |
|- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) = ( ! ` K ) ) |
160 |
145
|
adantl |
|- ( ( ph /\ m = K ) -> ( K - m ) = ( K - K ) ) |
161 |
148
|
adantr |
|- ( ( ph /\ m = K ) -> ( K - K ) = 0 ) |
162 |
160 161
|
eqtrd |
|- ( ( ph /\ m = K ) -> ( K - m ) = 0 ) |
163 |
162
|
oveq2d |
|- ( ( ph /\ m = K ) -> ( ( x + A ) ^ ( K - m ) ) = ( ( x + A ) ^ 0 ) ) |
164 |
163
|
adantr |
|- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( x + A ) ^ ( K - m ) ) = ( ( x + A ) ^ 0 ) ) |
165 |
65
|
exp0d |
|- ( ( ph /\ x e. X ) -> ( ( x + A ) ^ 0 ) = 1 ) |
166 |
165
|
adantlr |
|- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( x + A ) ^ 0 ) = 1 ) |
167 |
164 166
|
eqtrd |
|- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( x + A ) ^ ( K - m ) ) = 1 ) |
168 |
159 167
|
oveq12d |
|- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) = ( ( ! ` K ) x. 1 ) ) |
169 |
87
|
mulid1d |
|- ( ph -> ( ( ! ` K ) x. 1 ) = ( ! ` K ) ) |
170 |
169
|
ad2antrr |
|- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( ! ` K ) x. 1 ) = ( ! ` K ) ) |
171 |
168 170
|
eqtrd |
|- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) = ( ! ` K ) ) |
172 |
171
|
mpteq2dva |
|- ( ( ph /\ m = K ) -> ( x e. X |-> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) = ( x e. X |-> ( ! ` K ) ) ) |
173 |
172
|
oveq2d |
|- ( ( ph /\ m = K ) -> ( S _D ( x e. X |-> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) = ( S _D ( x e. X |-> ( ! ` K ) ) ) ) |
174 |
1 2 87
|
dvmptconst |
|- ( ph -> ( S _D ( x e. X |-> ( ! ` K ) ) ) = ( x e. X |-> 0 ) ) |
175 |
174
|
adantr |
|- ( ( ph /\ m = K ) -> ( S _D ( x e. X |-> ( ! ` K ) ) ) = ( x e. X |-> 0 ) ) |
176 |
173 175
|
eqtrd |
|- ( ( ph /\ m = K ) -> ( S _D ( x e. X |-> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) = ( x e. X |-> 0 ) ) |
177 |
176
|
adantlr |
|- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> ( S _D ( x e. X |-> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) = ( x e. X |-> 0 ) ) |
178 |
137
|
ltp1d |
|- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> K < ( K + 1 ) ) |
179 |
|
oveq1 |
|- ( m = K -> ( m + 1 ) = ( K + 1 ) ) |
180 |
179
|
eqcomd |
|- ( m = K -> ( K + 1 ) = ( m + 1 ) ) |
181 |
180
|
adantl |
|- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> ( K + 1 ) = ( m + 1 ) ) |
182 |
178 181
|
breqtrd |
|- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> K < ( m + 1 ) ) |
183 |
182
|
iftrued |
|- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) = 0 ) |
184 |
183
|
eqcomd |
|- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> 0 = if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) |
185 |
184
|
mpteq2dv |
|- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> ( x e. X |-> 0 ) = ( x e. X |-> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) ) |
186 |
144 177 185
|
3eqtrd |
|- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> ( S _D ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) = ( x e. X |-> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) ) |
187 |
186
|
adantlr |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ m = K ) -> ( S _D ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) = ( x e. X |-> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) ) |
188 |
|
simpll |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ -. m = K ) -> ( ph /\ m e. NN0 ) ) |
189 |
188 100 114
|
3syl |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ -. m = K ) -> m e. RR ) |
190 |
76
|
ad3antrrr |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ -. m = K ) -> K e. RR ) |
191 |
|
simplr |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ -. m = K ) -> m <_ K ) |
192 |
|
neqne |
|- ( -. m = K -> m =/= K ) |
193 |
192
|
necomd |
|- ( -. m = K -> K =/= m ) |
194 |
193
|
adantl |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ -. m = K ) -> K =/= m ) |
195 |
189 190 191 194
|
leneltd |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ -. m = K ) -> m < K ) |
196 |
114
|
ad2antlr |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> m e. RR ) |
197 |
76
|
ad2antrr |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> K e. RR ) |
198 |
|
simpr |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> m < K ) |
199 |
196 197 198
|
ltled |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> m <_ K ) |
200 |
196 197
|
lenltd |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( m <_ K <-> -. K < m ) ) |
201 |
199 200
|
mpbid |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> -. K < m ) |
202 |
201
|
iffalsed |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) |
203 |
202
|
mpteq2dv |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) = ( x e. X |-> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) |
204 |
203
|
oveq2d |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( S _D ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) = ( S _D ( x e. X |-> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) |
205 |
1
|
adantr |
|- ( ( ph /\ m e. NN0 ) -> S e. { RR , CC } ) |
206 |
205
|
adantr |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> S e. { RR , CC } ) |
207 |
87
|
ad2antrr |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` K ) e. CC ) |
208 |
100
|
adantr |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> m e. NN0 ) |
209 |
4
|
ad2antrr |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> K e. NN0 ) |
210 |
|
nn0sub |
|- ( ( m e. NN0 /\ K e. NN0 ) -> ( m <_ K <-> ( K - m ) e. NN0 ) ) |
211 |
208 209 210
|
syl2anc |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( m <_ K <-> ( K - m ) e. NN0 ) ) |
212 |
199 211
|
mpbid |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( K - m ) e. NN0 ) |
213 |
|
faccl |
|- ( ( K - m ) e. NN0 -> ( ! ` ( K - m ) ) e. NN ) |
214 |
212 213
|
syl |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( K - m ) ) e. NN ) |
215 |
214
|
nncnd |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( K - m ) ) e. CC ) |
216 |
214
|
nnne0d |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( K - m ) ) =/= 0 ) |
217 |
207 215 216
|
divcld |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) e. CC ) |
218 |
217
|
adantr |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) e. CC ) |
219 |
75
|
ad3antrrr |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> 0 e. RR ) |
220 |
2
|
adantr |
|- ( ( ph /\ m e. NN0 ) -> X e. ( ( TopOpen ` CCfld ) |`t S ) ) |
221 |
220
|
adantr |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> X e. ( ( TopOpen ` CCfld ) |`t S ) ) |
222 |
206 221 217
|
dvmptconst |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( S _D ( x e. X |-> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) ) ) = ( x e. X |-> 0 ) ) |
223 |
65
|
adantlr |
|- ( ( ( ph /\ m e. NN0 ) /\ x e. X ) -> ( x + A ) e. CC ) |
224 |
223
|
adantlr |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( x + A ) e. CC ) |
225 |
212
|
adantr |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( K - m ) e. NN0 ) |
226 |
224 225
|
expcld |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( x + A ) ^ ( K - m ) ) e. CC ) |
227 |
225
|
nn0cnd |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( K - m ) e. CC ) |
228 |
212
|
nn0zd |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( K - m ) e. ZZ ) |
229 |
196 197
|
posdifd |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( m < K <-> 0 < ( K - m ) ) ) |
230 |
198 229
|
mpbid |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> 0 < ( K - m ) ) |
231 |
228 230
|
jca |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( K - m ) e. ZZ /\ 0 < ( K - m ) ) ) |
232 |
|
elnnz |
|- ( ( K - m ) e. NN <-> ( ( K - m ) e. ZZ /\ 0 < ( K - m ) ) ) |
233 |
231 232
|
sylibr |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( K - m ) e. NN ) |
234 |
|
nnm1nn0 |
|- ( ( K - m ) e. NN -> ( ( K - m ) - 1 ) e. NN0 ) |
235 |
233 234
|
syl |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( K - m ) - 1 ) e. NN0 ) |
236 |
235
|
adantr |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( K - m ) - 1 ) e. NN0 ) |
237 |
224 236
|
expcld |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( x + A ) ^ ( ( K - m ) - 1 ) ) e. CC ) |
238 |
227 237
|
mulcld |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) e. CC ) |
239 |
3
|
ad2antrr |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> A e. CC ) |
240 |
206 221 239 233
|
dvxpaek |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( S _D ( x e. X |-> ( ( x + A ) ^ ( K - m ) ) ) ) = ( x e. X |-> ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) ) ) |
241 |
206 218 219 222 226 238 240
|
dvmptmul |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( S _D ( x e. X |-> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) = ( x e. X |-> ( ( 0 x. ( ( x + A ) ^ ( K - m ) ) ) + ( ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) x. ( ( ! ` K ) / ( ! ` ( K - m ) ) ) ) ) ) ) |
242 |
226
|
mul02d |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( 0 x. ( ( x + A ) ^ ( K - m ) ) ) = 0 ) |
243 |
242
|
oveq1d |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( 0 x. ( ( x + A ) ^ ( K - m ) ) ) + ( ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) x. ( ( ! ` K ) / ( ! ` ( K - m ) ) ) ) ) = ( 0 + ( ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) x. ( ( ! ` K ) / ( ! ` ( K - m ) ) ) ) ) ) |
244 |
238 218
|
mulcld |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) x. ( ( ! ` K ) / ( ! ` ( K - m ) ) ) ) e. CC ) |
245 |
244
|
addid2d |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( 0 + ( ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) x. ( ( ! ` K ) / ( ! ` ( K - m ) ) ) ) ) = ( ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) x. ( ( ! ` K ) / ( ! ` ( K - m ) ) ) ) ) |
246 |
120
|
adantr |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> m e. ZZ ) |
247 |
119
|
adantr |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> K e. ZZ ) |
248 |
|
zltp1le |
|- ( ( m e. ZZ /\ K e. ZZ ) -> ( m < K <-> ( m + 1 ) <_ K ) ) |
249 |
246 247 248
|
syl2anc |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( m < K <-> ( m + 1 ) <_ K ) ) |
250 |
198 249
|
mpbid |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( m + 1 ) <_ K ) |
251 |
|
peano2re |
|- ( m e. RR -> ( m + 1 ) e. RR ) |
252 |
196 251
|
syl |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( m + 1 ) e. RR ) |
253 |
252 197
|
lenltd |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( m + 1 ) <_ K <-> -. K < ( m + 1 ) ) ) |
254 |
250 253
|
mpbid |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> -. K < ( m + 1 ) ) |
255 |
254
|
adantr |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> -. K < ( m + 1 ) ) |
256 |
255
|
iffalsed |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) |
257 |
218 227 237
|
mulassd |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( K - m ) ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) ) ) |
258 |
257
|
eqcomd |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) ) = ( ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( K - m ) ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) ) |
259 |
233
|
nncnd |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( K - m ) e. CC ) |
260 |
207 215 259 216
|
div32d |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( K - m ) ) = ( ( ! ` K ) x. ( ( K - m ) / ( ! ` ( K - m ) ) ) ) ) |
261 |
|
facnn2 |
|- ( ( K - m ) e. NN -> ( ! ` ( K - m ) ) = ( ( ! ` ( ( K - m ) - 1 ) ) x. ( K - m ) ) ) |
262 |
233 261
|
syl |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( K - m ) ) = ( ( ! ` ( ( K - m ) - 1 ) ) x. ( K - m ) ) ) |
263 |
262
|
oveq2d |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( K - m ) / ( ! ` ( K - m ) ) ) = ( ( K - m ) / ( ( ! ` ( ( K - m ) - 1 ) ) x. ( K - m ) ) ) ) |
264 |
|
faccl |
|- ( ( ( K - m ) - 1 ) e. NN0 -> ( ! ` ( ( K - m ) - 1 ) ) e. NN ) |
265 |
234 264
|
syl |
|- ( ( K - m ) e. NN -> ( ! ` ( ( K - m ) - 1 ) ) e. NN ) |
266 |
265
|
nncnd |
|- ( ( K - m ) e. NN -> ( ! ` ( ( K - m ) - 1 ) ) e. CC ) |
267 |
233 266
|
syl |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( ( K - m ) - 1 ) ) e. CC ) |
268 |
235 264
|
syl |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( ( K - m ) - 1 ) ) e. NN ) |
269 |
|
nnne0 |
|- ( ( ! ` ( ( K - m ) - 1 ) ) e. NN -> ( ! ` ( ( K - m ) - 1 ) ) =/= 0 ) |
270 |
268 269
|
syl |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( ( K - m ) - 1 ) ) =/= 0 ) |
271 |
|
nnne0 |
|- ( ( K - m ) e. NN -> ( K - m ) =/= 0 ) |
272 |
233 271
|
syl |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( K - m ) =/= 0 ) |
273 |
267 259 270 272
|
divcan8d |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( K - m ) / ( ( ! ` ( ( K - m ) - 1 ) ) x. ( K - m ) ) ) = ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) |
274 |
263 273
|
eqtrd |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( K - m ) / ( ! ` ( K - m ) ) ) = ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) |
275 |
274
|
oveq2d |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) x. ( ( K - m ) / ( ! ` ( K - m ) ) ) ) = ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) ) |
276 |
|
eqidd |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) = ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) ) |
277 |
260 275 276
|
3eqtrd |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( K - m ) ) = ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) ) |
278 |
277
|
adantr |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( K - m ) ) = ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) ) |
279 |
81
|
adantr |
|- ( ( ph /\ m e. NN0 ) -> K e. CC ) |
280 |
100
|
nn0cnd |
|- ( ( ph /\ m e. NN0 ) -> m e. CC ) |
281 |
|
1cnd |
|- ( ( ph /\ m e. NN0 ) -> 1 e. CC ) |
282 |
279 280 281
|
subsub4d |
|- ( ( ph /\ m e. NN0 ) -> ( ( K - m ) - 1 ) = ( K - ( m + 1 ) ) ) |
283 |
282
|
oveq2d |
|- ( ( ph /\ m e. NN0 ) -> ( ( x + A ) ^ ( ( K - m ) - 1 ) ) = ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) |
284 |
283
|
ad2antrr |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( x + A ) ^ ( ( K - m ) - 1 ) ) = ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) |
285 |
278 284
|
oveq12d |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( K - m ) ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) = ( ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) |
286 |
282
|
adantr |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( K - m ) - 1 ) = ( K - ( m + 1 ) ) ) |
287 |
286
|
eqcomd |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( K - ( m + 1 ) ) = ( ( K - m ) - 1 ) ) |
288 |
287
|
fveq2d |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( K - ( m + 1 ) ) ) = ( ! ` ( ( K - m ) - 1 ) ) ) |
289 |
288
|
oveq2d |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) = ( ( ! ` K ) / ( ! ` ( ( K - m ) - 1 ) ) ) ) |
290 |
207 267 270
|
divrecd |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) / ( ! ` ( ( K - m ) - 1 ) ) ) = ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) ) |
291 |
289 290
|
eqtr2d |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) = ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) ) |
292 |
291
|
adantr |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) = ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) ) |
293 |
292
|
oveq1d |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) |
294 |
258 285 293
|
3eqtrrd |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) ) ) |
295 |
218 238
|
mulcomd |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) ) = ( ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) x. ( ( ! ` K ) / ( ! ` ( K - m ) ) ) ) ) |
296 |
256 294 295
|
3eqtrrd |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) x. ( ( ! ` K ) / ( ! ` ( K - m ) ) ) ) = if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) |
297 |
243 245 296
|
3eqtrd |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( 0 x. ( ( x + A ) ^ ( K - m ) ) ) + ( ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) x. ( ( ! ` K ) / ( ! ` ( K - m ) ) ) ) ) = if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) |
298 |
297
|
mpteq2dva |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( x e. X |-> ( ( 0 x. ( ( x + A ) ^ ( K - m ) ) ) + ( ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) x. ( ( ! ` K ) / ( ! ` ( K - m ) ) ) ) ) ) = ( x e. X |-> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) ) |
299 |
204 241 298
|
3eqtrd |
|- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( S _D ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) = ( x e. X |-> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) ) |
300 |
188 195 299
|
syl2anc |
|- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ -. m = K ) -> ( S _D ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) = ( x e. X |-> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) ) |
301 |
187 300
|
pm2.61dan |
|- ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) -> ( S _D ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) = ( x e. X |-> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) ) |
302 |
129 134 301
|
syl2anc |
|- ( ( ( ph /\ m e. NN0 ) /\ -. K < m ) -> ( S _D ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) = ( x e. X |-> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) ) |
303 |
128 302
|
pm2.61dan |
|- ( ( ph /\ m e. NN0 ) -> ( S _D ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) = ( x e. X |-> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) ) |
304 |
303
|
adantr |
|- ( ( ( ph /\ m e. NN0 ) /\ ( ( S Dn F ) ` m ) = ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) -> ( S _D ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) = ( x e. X |-> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) ) |
305 |
103 105 304
|
3eqtrd |
|- ( ( ( ph /\ m e. NN0 ) /\ ( ( S Dn F ) ` m ) = ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) -> ( ( S Dn F ) ` ( m + 1 ) ) = ( x e. X |-> if ( K < ( m + 1 ) , 0 , ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) ) ) ) |
306 |
16 27 38 49 97 305
|
nn0indd |
|- ( ( ph /\ N e. NN0 ) -> ( ( S Dn F ) ` N ) = ( x e. X |-> if ( K < N , 0 , ( ( ( ! ` K ) / ( ! ` ( K - N ) ) ) x. ( ( x + A ) ^ ( K - N ) ) ) ) ) ) |