Theorem dvnxpaek 37811

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

Hypotheses

Ref	Expression
dvnxpaek.s	|- ( ph -> S e. { RR , CC } )
dvnxpaek.x	|- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )
dvnxpaek.a	|- ( ph -> A e. CC )
dvnxpaek.k	|- ( ph -> K e. NN0 )
dvnxpaek.f	|- F = ( x e. X |-> ( ( x + A ) ^ K ) )

Assertion

Ref	Expression
dvnxpaek	|- ( ( ph /\ N e. NN0 ) -> ( ( S Dn F ) ` N ) = ( x e. X |-> if ( K < N , 0 , ( ( ( ! ` K ) / ( ! ` ( K - N ) ) ) x. ( ( x + A ) ^ ( K - N ) ) ) ) ) )

Distinct variable groups:   x, A   x, K   x, N   x, S   x, X   ph, x

Allowed substitution hint:   F( x)

Proof of Theorem dvnxpaek

Dummy variables m n are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5863	. . 3 |- ( n = 0 -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` 0 ) )
2		breq2 4405	. . . . 5 |- ( n = 0 -> ( K < n <-> K < 0 ) )
3		eqidd 2451	. . . . 5 |- ( n = 0 -> 0 = 0 )
4		oveq2 6296	. . . . . . . 8 |- ( n = 0 -> ( K - n ) = ( K - 0 ) )
5	4	fveq2d 5867	. . . . . . 7 |- ( n = 0 -> ( ! ` ( K - n ) ) = ( ! ` ( K - 0 ) ) )
6	5	oveq2d 6304	. . . . . 6 |- ( n = 0 -> ( ( ! ` K ) / ( ! ` ( K - n ) ) ) = ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) )
7	4	oveq2d 6304	. . . . . 6 |- ( n = 0 -> ( ( x + A ) ^ ( K - n ) ) = ( ( x + A ) ^ ( K - 0 ) ) )
8	6, 7	oveq12d 6306	. . . . 5 |- ( n = 0 -> ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) )
9	2, 3, 8	ifbieq12d 3907	. . . 4 |- ( 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 ) ) ) ) )
10	9	mpteq2dv 4489	. . 3 |- ( 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 ) ) ) ) ) )
11	1, 10	eqeq12d 2465	. 2 |- ( 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 ) ) ) ) ) ) )
12		fveq2 5863	. . 3 |- ( n = m -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` m ) )
13		breq2 4405	. . . . 5 |- ( n = m -> ( K < n <-> K < m ) )
14		eqidd 2451	. . . . 5 |- ( n = m -> 0 = 0 )
15		oveq2 6296	. . . . . . . 8 |- ( n = m -> ( K - n ) = ( K - m ) )
16	15	fveq2d 5867	. . . . . . 7 |- ( n = m -> ( ! ` ( K - n ) ) = ( ! ` ( K - m ) ) )
17	16	oveq2d 6304	. . . . . 6 |- ( n = m -> ( ( ! ` K ) / ( ! ` ( K - n ) ) ) = ( ( ! ` K ) / ( ! ` ( K - m ) ) ) )
18	15	oveq2d 6304	. . . . . 6 |- ( n = m -> ( ( x + A ) ^ ( K - n ) ) = ( ( x + A ) ^ ( K - m ) ) )
19	17, 18	oveq12d 6306	. . . . 5 |- ( n = m -> ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) )
20	13, 14, 19	ifbieq12d 3907	. . . 4 |- ( 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 ) ) ) ) )
21	20	mpteq2dv 4489	. . 3 |- ( 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 ) ) ) ) ) )
22	12, 21	eqeq12d 2465	. 2 |- ( 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 ) ) ) ) ) ) )
23		fveq2 5863	. . 3 |- ( n = ( m + 1 ) -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` ( m + 1 ) ) )
24		breq2 4405	. . . . 5 |- ( n = ( m + 1 ) -> ( K < n <-> K < ( m + 1 ) ) )
25		eqidd 2451	. . . . 5 |- ( n = ( m + 1 ) -> 0 = 0 )
26		oveq2 6296	. . . . . . . 8 |- ( n = ( m + 1 ) -> ( K - n ) = ( K - ( m + 1 ) ) )
27	26	fveq2d 5867	. . . . . . 7 |- ( n = ( m + 1 ) -> ( ! ` ( K - n ) ) = ( ! ` ( K - ( m + 1 ) ) ) )
28	27	oveq2d 6304	. . . . . 6 |- ( n = ( m + 1 ) -> ( ( ! ` K ) / ( ! ` ( K - n ) ) ) = ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) )
29	26	oveq2d 6304	. . . . . 6 |- ( n = ( m + 1 ) -> ( ( x + A ) ^ ( K - n ) ) = ( ( x + A ) ^ ( K - ( m + 1 ) ) ) )
30	28, 29	oveq12d 6306	. . . . 5 |- ( n = ( m + 1 ) -> ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) x. ( ( x + A ) ^ ( K - ( m + 1 ) ) ) ) )
31	24, 25, 30	ifbieq12d 3907	. . . 4 |- ( 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 ) ) ) ) ) )
32	31	mpteq2dv 4489	. . 3 |- ( 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 ) ) ) ) ) ) )
33	23, 32	eqeq12d 2465	. 2 |- ( 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 ) ) ) ) ) ) ) )
34		fveq2 5863	. . 3 |- ( n = N -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` N ) )
35		breq2 4405	. . . . 5 |- ( n = N -> ( K < n <-> K < N ) )
36		eqidd 2451	. . . . 5 |- ( n = N -> 0 = 0 )
37		oveq2 6296	. . . . . . . 8 |- ( n = N -> ( K - n ) = ( K - N ) )
38	37	fveq2d 5867	. . . . . . 7 |- ( n = N -> ( ! ` ( K - n ) ) = ( ! ` ( K - N ) ) )
39	38	oveq2d 6304	. . . . . 6 |- ( n = N -> ( ( ! ` K ) / ( ! ` ( K - n ) ) ) = ( ( ! ` K ) / ( ! ` ( K - N ) ) ) )
40	37	oveq2d 6304	. . . . . 6 |- ( n = N -> ( ( x + A ) ^ ( K - n ) ) = ( ( x + A ) ^ ( K - N ) ) )
41	39, 40	oveq12d 6306	. . . . 5 |- ( n = N -> ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - N ) ) ) x. ( ( x + A ) ^ ( K - N ) ) ) )
42	35, 36, 41	ifbieq12d 3907	. . . 4 |- ( 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 ) ) ) ) )
43	42	mpteq2dv 4489	. . 3 |- ( 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 ) ) ) ) ) )
44	34, 43	eqeq12d 2465	. 2 |- ( 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 ) ) ) ) ) ) )
45		dvnxpaek.s	. . . . 5 |- ( ph -> S e. { RR , CC } )
46		recnprss 22852	. . . . 5 |- ( S e. { RR , CC } -> S C_ CC )
47	45, 46	syl 17	. . . 4 |- ( ph -> S C_ CC )
48		cnex 9617	. . . . . 6 |- CC e. _V
49	48	a1i 11	. . . . 5 |- ( ph -> CC e. _V )
50		dvnxpaek.x	. . . . . . . . . . . 12 |- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )
51		restsspw 15323	. . . . . . . . . . . . . 14 |- ( ( TopOpen ` ℂfld ) ↾t S ) C_ ~P S
52		id 22	. . . . . . . . . . . . . 14 |- ( X e. ( ( TopOpen ` ℂfld ) ↾t S ) -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )
53	51, 52	sseldi 3429	. . . . . . . . . . . . 13 |- ( X e. ( ( TopOpen ` ℂfld ) ↾t S ) -> X e. ~P S )
54		elpwi 3959	. . . . . . . . . . . . 13 |- ( X e. ~P S -> X C_ S )
55	53, 54	syl 17	. . . . . . . . . . . 12 |- ( X e. ( ( TopOpen ` ℂfld ) ↾t S ) -> X C_ S )
56	50, 55	syl 17	. . . . . . . . . . 11 |- ( ph -> X C_ S )
57	56, 47	sstrd 3441	. . . . . . . . . 10 |- ( ph -> X C_ CC )
58	57	adantr 467	. . . . . . . . 9 |- ( ( ph /\ x e. X ) -> X C_ CC )
59		simpr 463	. . . . . . . . 9 |- ( ( ph /\ x e. X ) -> x e. X )
60	58, 59	sseldd 3432	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> x e. CC )
61		dvnxpaek.a	. . . . . . . . 9 |- ( ph -> A e. CC )
62	61	adantr 467	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> A e. CC )
63	60, 62	addcld 9659	. . . . . . 7 |- ( ( ph /\ x e. X ) -> ( x + A ) e. CC )
64		dvnxpaek.k	. . . . . . . 8 |- ( ph -> K e. NN0 )
65	64	adantr 467	. . . . . . 7 |- ( ( ph /\ x e. X ) -> K e. NN0 )
66	63, 65	expcld 12413	. . . . . 6 |- ( ( ph /\ x e. X ) -> ( ( x + A ) ^ K ) e. CC )
67		dvnxpaek.f	. . . . . 6 |- F = ( x e. X |-> ( ( x + A ) ^ K ) )
68	66, 67	fmptd 6044	. . . . 5 |- ( ph -> F : X --> CC )
69		elpm2r 7486	. . . . 5 |- ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( F : X --> CC /\ X C_ S ) ) -> F e. ( CC ^pm S ) )
70	49, 45, 68, 56, 69	syl22anc 1268	. . . 4 |- ( ph -> F e. ( CC ^pm S ) )
71		dvn0 22871	. . . 4 |- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )
72	47, 70, 71	syl2anc 666	. . 3 |- ( ph -> ( ( S Dn F ) ` 0 ) = F )
73	67	a1i 11	. . 3 |- ( ph -> F = ( x e. X |-> ( ( x + A ) ^ K ) ) )
74	64	nn0ge0d 10925	. . . . . . . 8 |- ( ph -> 0 <_ K )
75		0red 9641	. . . . . . . . 9 |- ( ph -> 0 e. RR )
76	64	nn0red 10923	. . . . . . . . 9 |- ( ph -> K e. RR )
77	75, 76	lenltd 9778	. . . . . . . 8 |- ( ph -> ( 0 <_ K <-> -. K < 0 ) )
78	74, 77	mpbid 214	. . . . . . 7 |- ( ph -> -. K < 0 )
79	78	iffalsed 3891	. . . . . 6 |- ( ph -> if ( K < 0 , 0 , ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) )
80	79	adantr 467	. . . . 5 |- ( ( 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	64	nn0cnd 10924	. . . . . . . . . . 11 |- ( ph -> K e. CC )
82	81	subid1d 9972	. . . . . . . . . 10 |- ( ph -> ( K - 0 ) = K )
83	82	fveq2d 5867	. . . . . . . . 9 |- ( ph -> ( ! ` ( K - 0 ) ) = ( ! ` K ) )
84	83	oveq2d 6304	. . . . . . . 8 |- ( ph -> ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) = ( ( ! ` K ) / ( ! ` K ) ) )
85		faccl 12466	. . . . . . . . . . 11 |- ( K e. NN0 -> ( ! ` K ) e. NN )
86	64, 85	syl 17	. . . . . . . . . 10 |- ( ph -> ( ! ` K ) e. NN )
87	86	nncnd 10622	. . . . . . . . 9 |- ( ph -> ( ! ` K ) e. CC )
88	86	nnne0d 10651	. . . . . . . . 9 |- ( ph -> ( ! ` K ) =/= 0 )
89	87, 88	dividd 10378	. . . . . . . 8 |- ( ph -> ( ( ! ` K ) / ( ! ` K ) ) = 1 )
90	84, 89	eqtrd 2484	. . . . . . 7 |- ( ph -> ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) = 1 )
91	82	oveq2d 6304	. . . . . . 7 |- ( ph -> ( ( x + A ) ^ ( K - 0 ) ) = ( ( x + A ) ^ K ) )
92	90, 91	oveq12d 6306	. . . . . 6 |- ( ph -> ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) = ( 1 x. ( ( x + A ) ^ K ) ) )
93	92	adantr 467	. . . . 5 |- ( ( ph /\ x e. X ) -> ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) = ( 1 x. ( ( x + A ) ^ K ) ) )
94	66	mulid2d 9658	. . . . 5 |- ( ( ph /\ x e. X ) -> ( 1 x. ( ( x + A ) ^ K ) ) = ( ( x + A ) ^ K ) )
95	80, 93, 94	3eqtrrd 2489	. . . 4 |- ( ( ph /\ x e. X ) -> ( ( x + A ) ^ K ) = if ( K < 0 , 0 , ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) ) )
96	95	mpteq2dva 4488	. . 3 |- ( 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 2488	. 2 |- ( ph -> ( ( S Dn F ) ` 0 ) = ( x e. X |-> if ( K < 0 , 0 , ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) ) ) )
98	47	adantr 467	. . . . 5 |- ( ( ph /\ m e. NN0 ) -> S C_ CC )
99	70	adantr 467	. . . . 5 |- ( ( ph /\ m e. NN0 ) -> F e. ( CC ^pm S ) )
100		simpr 463	. . . . 5 |- ( ( ph /\ m e. NN0 ) -> m e. NN0 )
101		dvnp1 22872	. . . . 5 |- ( ( 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 1267	. . . 4 |- ( ( ph /\ m e. NN0 ) -> ( ( S Dn F ) ` ( m + 1 ) ) = ( S _D ( ( S Dn F ) ` m ) ) )
103	102	adantr 467	. . 3 |- ( ( ( 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 6296	. . . 4 |- ( ( ( 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 468	. . 3 |- ( ( ( 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 3886	. . . . . . . . 9 |- ( K < m -> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) = 0 )
107	106	mpteq2dv 4489	. . . . . . . 8 |- ( K < m -> ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) = ( x e. X |-> 0 ) )
108	107	oveq2d 6304	. . . . . . 7 |- ( 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 468	. . . . . 6 |- ( ( ( 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 9633	. . . . . . . 8 |- ( ph -> 0 e. CC )
111	45, 50, 110	dvmptconst 37779	. . . . . . 7 |- ( ph -> ( S _D ( x e. X |-> 0 ) ) = ( x e. X |-> 0 ) )
112	111	ad2antrr 731	. . . . . 6 |- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> ( S _D ( x e. X |-> 0 ) ) = ( x e. X |-> 0 ) )
113	76	ad2antrr 731	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> K e. RR )
114		nn0re 10875	. . . . . . . . . . . 12 |- ( m e. NN0 -> m e. RR )
115	114	ad2antlr 732	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> m e. RR )
116		simpr 463	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> K < m )
117	113, 115, 116	ltled 9780	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> K <_ m )
118	64	nn0zd 11035	. . . . . . . . . . . . 13 |- ( ph -> K e. ZZ )
119	118	adantr 467	. . . . . . . . . . . 12 |- ( ( ph /\ m e. NN0 ) -> K e. ZZ )
120	100	nn0zd 11035	. . . . . . . . . . . 12 |- ( ( ph /\ m e. NN0 ) -> m e. ZZ )
121		zleltp1 10984	. . . . . . . . . . . 12 |- ( ( K e. ZZ /\ m e. ZZ ) -> ( K <_ m <-> K < ( m + 1 ) ) )
122	119, 120, 121	syl2anc 666	. . . . . . . . . . 11 |- ( ( ph /\ m e. NN0 ) -> ( K <_ m <-> K < ( m + 1 ) ) )
123	122	adantr 467	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> ( K <_ m <-> K < ( m + 1 ) ) )
124	117, 123	mpbid 214	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> K < ( m + 1 ) )
125	124	iftrued 3888	. . . . . . . 8 |- ( ( ( 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 4489	. . . . . . 7 |- ( ( ( 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 2456	. . . . . 6 |- ( ( ( 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 2488	. . . . 5 |- ( ( ( 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 459	. . . . . 6 |- ( ( ( ph /\ m e. NN0 ) /\ -. K < m ) -> ( ph /\ m e. NN0 ) )
130		simpr 463	. . . . . . 7 |- ( ( ( ph /\ m e. NN0 ) /\ -. K < m ) -> -. K < m )
131	129, 100, 114	3syl 18	. . . . . . . 8 |- ( ( ( ph /\ m e. NN0 ) /\ -. K < m ) -> m e. RR )
132	76	ad2antrr 731	. . . . . . . 8 |- ( ( ( ph /\ m e. NN0 ) /\ -. K < m ) -> K e. RR )
133	131, 132	lenltd 9778	. . . . . . 7 |- ( ( ( ph /\ m e. NN0 ) /\ -. K < m ) -> ( m <_ K <-> -. K < m ) )
134	130, 133	mpbird 236	. . . . . 6 |- ( ( ( ph /\ m e. NN0 ) /\ -. K < m ) -> m <_ K )
135		simpr 463	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> m = K )
136	114	ad2antlr 732	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> m e. RR )
137	76	ad2antrr 731	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> K e. RR )
138	136, 137	lttri3d 9772	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> ( m = K <-> ( -. m < K /\ -. K < m ) ) )
139	135, 138	mpbid 214	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> ( -. m < K /\ -. K < m ) )
140		simpr 463	. . . . . . . . . . . . 13 |- ( ( -. m < K /\ -. K < m ) -> -. K < m )
141	139, 140	syl 17	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> -. K < m )
142	141	iffalsed 3891	. . . . . . . . . . 11 |- ( ( ( 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 4489	. . . . . . . . . 10 |- ( ( ( 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 6304	. . . . . . . . 9 |- ( ( ( 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 6296	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = K -> ( K - m ) = ( K - K ) )
146	145	fveq2d 5867	. . . . . . . . . . . . . . . . . . . 20 |- ( m = K -> ( ! ` ( K - m ) ) = ( ! ` ( K - K ) ) )
147	146	adantl 468	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ m = K ) -> ( ! ` ( K - m ) ) = ( ! ` ( K - K ) ) )
148	81	subidd 9971	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( K - K ) = 0 )
149	148	fveq2d 5867	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ! ` ( K - K ) ) = ( ! ` 0 ) )
150		fac0 12459	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ! ` 0 ) = 1
151	150	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ! ` 0 ) = 1 )
152	149, 151	eqtrd 2484	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ! ` ( K - K ) ) = 1 )
153	152	adantr 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ m = K ) -> ( ! ` ( K - K ) ) = 1 )
154	147, 153	eqtrd 2484	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ m = K ) -> ( ! ` ( K - m ) ) = 1 )
155	154	oveq2d 6304	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m = K ) -> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) = ( ( ! ` K ) / 1 ) )
156	87	div1d 10372	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( ! ` K ) / 1 ) = ( ! ` K ) )
157	156	adantr 467	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m = K ) -> ( ( ! ` K ) / 1 ) = ( ! ` K ) )
158	155, 157	eqtrd 2484	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ m = K ) -> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) = ( ! ` K ) )
159	158	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) = ( ! ` K ) )
160	145	adantl 468	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ m = K ) -> ( K - m ) = ( K - K ) )
161	148	adantr 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ m = K ) -> ( K - K ) = 0 )
162	160, 161	eqtrd 2484	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ m = K ) -> ( K - m ) = 0 )
163	162	oveq2d 6304	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m = K ) -> ( ( x + A ) ^ ( K - m ) ) = ( ( x + A ) ^ 0 ) )
164	163	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( x + A ) ^ ( K - m ) ) = ( ( x + A ) ^ 0 ) )
165	63	exp0d 12407	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. X ) -> ( ( x + A ) ^ 0 ) = 1 )
166	165	adantlr 720	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( x + A ) ^ 0 ) = 1 )
167	164, 166	eqtrd 2484	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( x + A ) ^ ( K - m ) ) = 1 )
168	159, 167	oveq12d 6306	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) = ( ( ! ` K ) x. 1 ) )
169	87	mulid1d 9657	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ! ` K ) x. 1 ) = ( ! ` K ) )
170	169	ad2antrr 731	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( ! ` K ) x. 1 ) = ( ! ` K ) )
171	168, 170	eqtrd 2484	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) = ( ! ` K ) )
172	171	mpteq2dva 4488	. . . . . . . . . . . 12 |- ( ( ph /\ m = K ) -> ( x e. X |-> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) = ( x e. X |-> ( ! ` K ) ) )
173	172	oveq2d 6304	. . . . . . . . . . 11 |- ( ( ph /\ m = K ) -> ( S _D ( x e. X |-> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) = ( S _D ( x e. X |-> ( ! ` K ) ) ) )
174	45, 50, 87	dvmptconst 37779	. . . . . . . . . . . 12 |- ( ph -> ( S _D ( x e. X |-> ( ! ` K ) ) ) = ( x e. X |-> 0 ) )
175	174	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ m = K ) -> ( S _D ( x e. X |-> ( ! ` K ) ) ) = ( x e. X |-> 0 ) )
176	173, 175	eqtrd 2484	. . . . . . . . . 10 |- ( ( ph /\ m = K ) -> ( S _D ( x e. X |-> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) = ( x e. X |-> 0 ) )
177	176	adantlr 720	. . . . . . . . 9 |- ( ( ( 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 10534	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> K < ( K + 1 ) )
179		oveq1 6295	. . . . . . . . . . . . . . 15 |- ( m = K -> ( m + 1 ) = ( K + 1 ) )
180	179	eqcomd 2456	. . . . . . . . . . . . . 14 |- ( m = K -> ( K + 1 ) = ( m + 1 ) )
181	180	adantl 468	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> ( K + 1 ) = ( m + 1 ) )
182	178, 181	breqtrd 4426	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> K < ( m + 1 ) )
183	182	iftrued 3888	. . . . . . . . . . 11 |- ( ( ( 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 2456	. . . . . . . . . 10 |- ( ( ( 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 4489	. . . . . . . . 9 |- ( ( ( 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 2488	. . . . . . . 8 |- ( ( ( 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 720	. . . . . . 7 |- ( ( ( ( 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 759	. . . . . . . 8 |- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ -. m = K ) -> ( ph /\ m e. NN0 ) )
189	188, 100, 114	3syl 18	. . . . . . . . 9 |- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ -. m = K ) -> m e. RR )
190	76	ad3antrrr 735	. . . . . . . . 9 |- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ -. m = K ) -> K e. RR )
191		simplr 761	. . . . . . . . 9 |- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ -. m = K ) -> m <_ K )
192		neqne 37368	. . . . . . . . . . 11 |- ( -. m = K -> m =/= K )
193	192	necomd 2678	. . . . . . . . . 10 |- ( -. m = K -> K =/= m )
194	193	adantl 468	. . . . . . . . 9 |- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ -. m = K ) -> K =/= m )
195	189, 190, 191, 194	leneltd 9786	. . . . . . . 8 |- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ -. m = K ) -> m < K )
196	114	ad2antlr 732	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> m e. RR )
197	76	ad2antrr 731	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> K e. RR )
198		simpr 463	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> m < K )
199	196, 197, 198	ltled 9780	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> m <_ K )
200	196, 197	lenltd 9778	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( m <_ K <-> -. K < m ) )
201	199, 200	mpbid 214	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> -. K < m )
202	201	iffalsed 3891	. . . . . . . . . . 11 |- ( ( ( 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 4489	. . . . . . . . . 10 |- ( ( ( 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 6304	. . . . . . . . 9 |- ( ( ( 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	45	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ m e. NN0 ) -> S e. { RR , CC } )
206	205	adantr 467	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> S e. { RR , CC } )
207	87	ad2antrr 731	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` K ) e. CC )
208	100	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> m e. NN0 )
209	64	ad2antrr 731	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> K e. NN0 )
210		nn0sub 10917	. . . . . . . . . . . . . . . 16 |- ( ( m e. NN0 /\ K e. NN0 ) -> ( m <_ K <-> ( K - m ) e. NN0 ) )
211	208, 209, 210	syl2anc 666	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( m <_ K <-> ( K - m ) e. NN0 ) )
212	199, 211	mpbid 214	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( K - m ) e. NN0 )
213		faccl 12466	. . . . . . . . . . . . . 14 |- ( ( K - m ) e. NN0 -> ( ! ` ( K - m ) ) e. NN )
214	212, 213	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( K - m ) ) e. NN )
215	214	nncnd 10622	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( K - m ) ) e. CC )
216	214	nnne0d 10651	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( K - m ) ) =/= 0 )
217	207, 215, 216	divcld 10380	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) e. CC )
218	217	adantr 467	. . . . . . . . . 10 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) e. CC )
219	75	ad3antrrr 735	. . . . . . . . . 10 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> 0 e. RR )
220	50	adantr 467	. . . . . . . . . . . 12 |- ( ( ph /\ m e. NN0 ) -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )
221	220	adantr 467	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )
222	206, 221, 217	dvmptconst 37779	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( S _D ( x e. X |-> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) ) ) = ( x e. X |-> 0 ) )
223	63	adantlr 720	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN0 ) /\ x e. X ) -> ( x + A ) e. CC )
224	223	adantlr 720	. . . . . . . . . . 11 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( x + A ) e. CC )
225	212	adantr 467	. . . . . . . . . . 11 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( K - m ) e. NN0 )
226	224, 225	expcld 12413	. . . . . . . . . 10 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( x + A ) ^ ( K - m ) ) e. CC )
227	225	nn0cnd 10924	. . . . . . . . . . 11 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( K - m ) e. CC )
228	212	nn0zd 11035	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( K - m ) e. ZZ )
229	196, 197	posdifd 10197	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( m < K <-> 0 < ( K - m ) ) )
230	198, 229	mpbid 214	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> 0 < ( K - m ) )
231	228, 230	jca 535	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( K - m ) e. ZZ /\ 0 < ( K - m ) ) )
232		elnnz 10944	. . . . . . . . . . . . . . 15 |- ( ( K - m ) e. NN <-> ( ( K - m ) e. ZZ /\ 0 < ( K - m ) ) )
233	231, 232	sylibr 216	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( K - m ) e. NN )
234		nnm1nn0 10908	. . . . . . . . . . . . . 14 |- ( ( K - m ) e. NN -> ( ( K - m ) - 1 ) e. NN0 )
235	233, 234	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( K - m ) - 1 ) e. NN0 )
236	235	adantr 467	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( K - m ) - 1 ) e. NN0 )
237	224, 236	expcld 12413	. . . . . . . . . . 11 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( x + A ) ^ ( ( K - m ) - 1 ) ) e. CC )
238	227, 237	mulcld 9660	. . . . . . . . . 10 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) e. CC )
239	61	ad2antrr 731	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> A e. CC )
240	206, 221, 239, 233	dvxpaek 37809	. . . . . . . . . 10 |- ( ( ( 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 22908	. . . . . . . . 9 |- ( ( ( 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 9828	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( 0 x. ( ( x + A ) ^ ( K - m ) ) ) = 0 )
243	242	oveq1d 6303	. . . . . . . . . . 11 |- ( ( ( ( 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 9660	. . . . . . . . . . . 12 |- ( ( ( ( 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 9831	. . . . . . . . . . 11 |- ( ( ( ( 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 467	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> m e. ZZ )
247	119	adantr 467	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> K e. ZZ )
248		zltp1le 10983	. . . . . . . . . . . . . . . . 17 |- ( ( m e. ZZ /\ K e. ZZ ) -> ( m < K <-> ( m + 1 ) <_ K ) )
249	246, 247, 248	syl2anc 666	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( m < K <-> ( m + 1 ) <_ K ) )
250	198, 249	mpbid 214	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( m + 1 ) <_ K )
251		peano2re 9803	. . . . . . . . . . . . . . . . 17 |- ( m e. RR -> ( m + 1 ) e. RR )
252	196, 251	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( m + 1 ) e. RR )
253	252, 197	lenltd 9778	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( m + 1 ) <_ K <-> -. K < ( m + 1 ) ) )
254	250, 253	mpbid 214	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> -. K < ( m + 1 ) )
255	254	adantr 467	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> -. K < ( m + 1 ) )
256	255	iffalsed 3891	. . . . . . . . . . . 12 |- ( ( ( ( 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 9663	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 2456	. . . . . . . . . . . . 13 |- ( ( ( ( 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 10622	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( K - m ) e. CC )
260	207, 215, 259, 216	div32d 10403	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( K - m ) ) = ( ( ! ` K ) x. ( ( K - m ) / ( ! ` ( K - m ) ) ) ) )
261		facnn2 12465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( K - m ) e. NN -> ( ! ` ( K - m ) ) = ( ( ! ` ( ( K - m ) - 1 ) ) x. ( K - m ) ) )
262	233, 261	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( K - m ) ) = ( ( ! ` ( ( K - m ) - 1 ) ) x. ( K - m ) ) )
263	262	oveq2d 6304	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( K - m ) / ( ! ` ( K - m ) ) ) = ( ( K - m ) / ( ( ! ` ( ( K - m ) - 1 ) ) x. ( K - m ) ) ) )
264		faccl 12466	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( K - m ) - 1 ) e. NN0 -> ( ! ` ( ( K - m ) - 1 ) ) e. NN )
265	234, 264	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( K - m ) e. NN -> ( ! ` ( ( K - m ) - 1 ) ) e. NN )
266	265	nncnd 10622	. . . . . . . . . . . . . . . . . . . 20 |- ( ( K - m ) e. NN -> ( ! ` ( ( K - m ) - 1 ) ) e. CC )
267	233, 266	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( ( K - m ) - 1 ) ) e. CC )
268	235, 264	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( ( K - m ) - 1 ) ) e. NN )
269		nnne0 10639	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ! ` ( ( K - m ) - 1 ) ) e. NN -> ( ! ` ( ( K - m ) - 1 ) ) =/= 0 )
270	268, 269	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( ( K - m ) - 1 ) ) =/= 0 )
271		nnne0 10639	. . . . . . . . . . . . . . . . . . . 20 |- ( ( K - m ) e. NN -> ( K - m ) =/= 0 )
272	233, 271	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( K - m ) =/= 0 )
273	267, 259, 270, 272	divcan8d 37526	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( K - m ) / ( ( ! ` ( ( K - m ) - 1 ) ) x. ( K - m ) ) ) = ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) )
274	263, 273	eqtrd 2484	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( K - m ) / ( ! ` ( K - m ) ) ) = ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) )
275	274	oveq2d 6304	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) x. ( ( K - m ) / ( ! ` ( K - m ) ) ) ) = ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) )
276		eqidd 2451	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) = ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) )
277	260, 275, 276	3eqtrd 2488	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( K - m ) ) = ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) )
278	277	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( K - m ) ) = ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) )
279	81	adantr 467	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m e. NN0 ) -> K e. CC )
280	100	nn0cnd 10924	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m e. NN0 ) -> m e. CC )
281		1cnd 9656	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m e. NN0 ) -> 1 e. CC )
282	279, 280, 281	subsub4d 10014	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ m e. NN0 ) -> ( ( K - m ) - 1 ) = ( K - ( m + 1 ) ) )
283	282	oveq2d 6304	. . . . . . . . . . . . . . 15 |- ( ( ph /\ m e. NN0 ) -> ( ( x + A ) ^ ( ( K - m ) - 1 ) ) = ( ( x + A ) ^ ( K - ( m + 1 ) ) ) )
284	283	ad2antrr 731	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( x + A ) ^ ( ( K - m ) - 1 ) ) = ( ( x + A ) ^ ( K - ( m + 1 ) ) ) )
285	278, 284	oveq12d 6306	. . . . . . . . . . . . 13 |- ( ( ( ( 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 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( K - m ) - 1 ) = ( K - ( m + 1 ) ) )
287	286	eqcomd 2456	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( K - ( m + 1 ) ) = ( ( K - m ) - 1 ) )
288	287	fveq2d 5867	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( K - ( m + 1 ) ) ) = ( ! ` ( ( K - m ) - 1 ) ) )
289	288	oveq2d 6304	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) = ( ( ! ` K ) / ( ! ` ( ( K - m ) - 1 ) ) ) )
290	207, 267, 270	divrecd 10383	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) / ( ! ` ( ( K - m ) - 1 ) ) ) = ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) )
291	289, 290	eqtr2d 2485	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) = ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) )
292	291	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) = ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) )
293	292	oveq1d 6303	. . . . . . . . . . . . 13 |- ( ( ( ( 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 2489	. . . . . . . . . . . 12 |- ( ( ( ( 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 9661	. . . . . . . . . . . 12 |- ( ( ( ( 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 2489	. . . . . . . . . . 11 |- ( ( ( ( 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 2488	. . . . . . . . . 10 |- ( ( ( ( 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 4488	. . . . . . . . 9 |- ( ( ( 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 2488	. . . . . . . 8 |- ( ( ( 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 666	. . . . . . 7 |- ( ( ( ( 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 799	. . . . . 6 |- ( ( ( 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 666	. . . . 5 |- ( ( ( 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 799	. . . 4 |- ( ( 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 467	. . 3 |- ( ( ( 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 2488	. 2 |- ( ( ( 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	11, 22, 33, 44, 97, 305	nn0indd 11029	1 |- ( ( ph /\ N e. NN0 ) -> ( ( S Dn F ) ` N ) = ( x e. X |-> if ( K < N , 0 , ( ( ( ! ` K ) / ( ! ` ( K - N ) ) ) x. ( ( x + A ) ^ ( K - N ) ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1443   e. wcel 1886   =/= wne 2621   _Vcvv 3044   C_ wss 3403   ifcif 3880   ~Pcpw 3950   {cpr 3969   class class class wbr 4401   |-> cmpt 4460   -->wf 5577   ` cfv 5581  (class class class)co 6288   ^pm cpm 7470   CCcc 9534   RRcr 9535   0cc0 9536   1c1 9537   + caddc 9539   x. cmul 9541   < clt 9672   <_ cle 9673   - cmin 9857   / cdiv 10266   NNcn 10606   NN0cn0 10866   ZZcz 10934   ^cexp 12269   !cfa 12456   ↾_t crest 15312   TopOpenctopn 15313  ℂ_fldccnfld 18963   _D cdv 22811   Dncdvn 22812

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-inf2 8143  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613  ax-pre-sup 9614  ax-addf 9615  ax-mulf 9616

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-iin 4280  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-se 4793  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-isom 5590  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-of 6528  df-om 6690  df-1st 6790  df-2nd 6791  df-supp 6912  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-1o 7179  df-2o 7180  df-oadd 7183  df-er 7360  df-map 7471  df-pm 7472  df-ixp 7520  df-en 7567  df-dom 7568  df-sdom 7569  df-fin 7570  df-fsupp 7881  df-fi 7922  df-sup 7953  df-inf 7954  df-oi 8022  df-card 8370  df-cda 8595  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-nn 10607  df-2 10665  df-3 10666  df-4 10667  df-5 10668  df-6 10669  df-7 10670  df-8 10671  df-9 10672  df-10 10673  df-n0 10867  df-z 10935  df-dec 11049  df-uz 11157  df-q 11262  df-rp 11300  df-xneg 11406  df-xadd 11407  df-xmul 11408  df-icc 11639  df-fz 11782  df-fzo 11913  df-seq 12211  df-exp 12270  df-fac 12457  df-hash 12513  df-cj 13155  df-re 13156  df-im 13157  df-sqrt 13291  df-abs 13292  df-struct 15116  df-ndx 15117  df-slot 15118  df-base 15119  df-sets 15120  df-ress 15121  df-plusg 15196  df-mulr 15197  df-starv 15198  df-sca 15199  df-vsca 15200  df-ip 15201  df-tset 15202  df-ple 15203  df-ds 15205  df-unif 15206  df-hom 15207  df-cco 15208  df-rest 15314  df-topn 15315  df-0g 15333  df-gsum 15334  df-topgen 15335  df-pt 15336  df-prds 15339  df-xrs 15393  df-qtop 15399  df-imas 15400  df-xps 15403  df-mre 15485  df-mrc 15486  df-acs 15488  df-mgm 16481  df-sgrp 16520  df-mnd 16530  df-submnd 16576  df-mulg 16669  df-cntz 16964  df-cmn 17425  df-psmet 18955  df-xmet 18956  df-met 18957  df-bl 18958  df-mopn 18959  df-fbas 18960  df-fg 18961  df-cnfld 18964  df-top 19914  df-bases 19915  df-topon 19916  df-topsp 19917  df-cld 20027  df-ntr 20028  df-cls 20029  df-nei 20107  df-lp 20145  df-perf 20146  df-cn 20236  df-cnp 20237  df-haus 20324  df-tx 20570  df-hmeo 20763  df-fil 20854  df-fm 20946  df-flim 20947  df-flf 20948  df-xms 21328  df-ms 21329  df-tms 21330  df-cncf 21903  df-limc 22814  df-dv 22815  df-dvn 22816

This theorem is referenced by:  etransclem17  38110