Metamath Proof Explorer

Theorem dvnxpaek

Description: The n -th derivative of the polynomial ( x + A ) ^ K . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvnxpaek.s 
|- ( ph -> S e. { RR , CC } )
dvnxpaek.x 
|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
dvnxpaek.a 
|- ( ph -> A e. CC )
dvnxpaek.k 
|- ( ph -> K e. NN0 )
dvnxpaek.f 
|- F = ( x e. X |-> ( ( x + A ) ^ K ) )
Assertion dvnxpaek 
|- ( ( ph /\ N e. NN0 ) -> ( ( S Dn F ) ` N ) = ( x e. X |-> if ( K < N , 0 , ( ( ( ! ` K ) / ( ! ` ( K - N ) ) ) x. ( ( x + A ) ^ ( K - N ) ) ) ) ) )

Proof

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 sselid 
 |-  ( 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 ) ) ) ) ) )