Theorem dvnxpaek 37419

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 5872	. . 3 |- ( n = 0 -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` 0 ) )
2		breq2 4421	. . . . 5 |- ( n = 0 -> ( K < n <-> K < 0 ) )
3		eqidd 2421	. . . . 5 |- ( n = 0 -> 0 = 0 )
4		oveq2 6304	. . . . . . . 8 |- ( n = 0 -> ( K - n ) = ( K - 0 ) )
5	4	fveq2d 5876	. . . . . . 7 |- ( n = 0 -> ( ! ` ( K - n ) ) = ( ! ` ( K - 0 ) ) )
6	5	oveq2d 6312	. . . . . 6 |- ( n = 0 -> ( ( ! ` K ) / ( ! ` ( K - n ) ) ) = ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) )
7	4	oveq2d 6312	. . . . . 6 |- ( n = 0 -> ( ( x + A ) ^ ( K - n ) ) = ( ( x + A ) ^ ( K - 0 ) ) )
8	6, 7	oveq12d 6314	. . . . 5 |- ( n = 0 -> ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) )
9	2, 3, 8	ifbieq12d 3933	. . . 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 4504	. . 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 2442	. 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 5872	. . 3 |- ( n = m -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` m ) )
13		breq2 4421	. . . . 5 |- ( n = m -> ( K < n <-> K < m ) )
14		eqidd 2421	. . . . 5 |- ( n = m -> 0 = 0 )
15		oveq2 6304	. . . . . . . 8 |- ( n = m -> ( K - n ) = ( K - m ) )
16	15	fveq2d 5876	. . . . . . 7 |- ( n = m -> ( ! ` ( K - n ) ) = ( ! ` ( K - m ) ) )
17	16	oveq2d 6312	. . . . . 6 |- ( n = m -> ( ( ! ` K ) / ( ! ` ( K - n ) ) ) = ( ( ! ` K ) / ( ! ` ( K - m ) ) ) )
18	15	oveq2d 6312	. . . . . 6 |- ( n = m -> ( ( x + A ) ^ ( K - n ) ) = ( ( x + A ) ^ ( K - m ) ) )
19	17, 18	oveq12d 6314	. . . . 5 |- ( n = m -> ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) )
20	13, 14, 19	ifbieq12d 3933	. . . 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 4504	. . 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 2442	. 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 5872	. . 3 |- ( n = ( m + 1 ) -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` ( m + 1 ) ) )
24		breq2 4421	. . . . 5 |- ( n = ( m + 1 ) -> ( K < n <-> K < ( m + 1 ) ) )
25		eqidd 2421	. . . . 5 |- ( n = ( m + 1 ) -> 0 = 0 )
26		oveq2 6304	. . . . . . . 8 |- ( n = ( m + 1 ) -> ( K - n ) = ( K - ( m + 1 ) ) )
27	26	fveq2d 5876	. . . . . . 7 |- ( n = ( m + 1 ) -> ( ! ` ( K - n ) ) = ( ! ` ( K - ( m + 1 ) ) ) )
28	27	oveq2d 6312	. . . . . 6 |- ( n = ( m + 1 ) -> ( ( ! ` K ) / ( ! ` ( K - n ) ) ) = ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) )
29	26	oveq2d 6312	. . . . . 6 |- ( n = ( m + 1 ) -> ( ( x + A ) ^ ( K - n ) ) = ( ( x + A ) ^ ( K - ( m + 1 ) ) ) )
30	28, 29	oveq12d 6314	. . . . 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 3933	. . . 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 4504	. . 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 2442	. 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 5872	. . 3 |- ( n = N -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` N ) )
35		breq2 4421	. . . . 5 |- ( n = N -> ( K < n <-> K < N ) )
36		eqidd 2421	. . . . 5 |- ( n = N -> 0 = 0 )
37		oveq2 6304	. . . . . . . 8 |- ( n = N -> ( K - n ) = ( K - N ) )
38	37	fveq2d 5876	. . . . . . 7 |- ( n = N -> ( ! ` ( K - n ) ) = ( ! ` ( K - N ) ) )
39	38	oveq2d 6312	. . . . . 6 |- ( n = N -> ( ( ! ` K ) / ( ! ` ( K - n ) ) ) = ( ( ! ` K ) / ( ! ` ( K - N ) ) ) )
40	37	oveq2d 6312	. . . . . 6 |- ( n = N -> ( ( x + A ) ^ ( K - n ) ) = ( ( x + A ) ^ ( K - N ) ) )
41	39, 40	oveq12d 6314	. . . . 5 |- ( n = N -> ( ( ( ! ` K ) / ( ! ` ( K - n ) ) ) x. ( ( x + A ) ^ ( K - n ) ) ) = ( ( ( ! ` K ) / ( ! ` ( K - N ) ) ) x. ( ( x + A ) ^ ( K - N ) ) ) )
42	35, 36, 41	ifbieq12d 3933	. . . 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 4504	. . 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 2442	. 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 22753	. . . . 5 |- ( S e. { RR , CC } -> S C_ CC )
47	45, 46	syl 17	. . . 4 |- ( ph -> S C_ CC )
48		cnex 9609	. . . . . 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 15282	. . . . . . . . . . . . . 14 |- ( ( TopOpen ` ℂfld ) ↾t S ) C_ ~P S
52		id 23	. . . . . . . . . . . . . 14 |- ( X e. ( ( TopOpen ` ℂfld ) ↾t S ) -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )
53	51, 52	sseldi 3459	. . . . . . . . . . . . 13 |- ( X e. ( ( TopOpen ` ℂfld ) ↾t S ) -> X e. ~P S )
54		elpwi 3985	. . . . . . . . . . . . 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 3471	. . . . . . . . . 10 |- ( ph -> X C_ CC )
58	57	adantr 466	. . . . . . . . 9 |- ( ( ph /\ x e. X ) -> X C_ CC )
59		simpr 462	. . . . . . . . 9 |- ( ( ph /\ x e. X ) -> x e. X )
60	58, 59	sseldd 3462	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> x e. CC )
61		dvnxpaek.a	. . . . . . . . 9 |- ( ph -> A e. CC )
62	61	adantr 466	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> A e. CC )
63	60, 62	addcld 9651	. . . . . . 7 |- ( ( ph /\ x e. X ) -> ( x + A ) e. CC )
64		dvnxpaek.k	. . . . . . . 8 |- ( ph -> K e. NN0 )
65	64	adantr 466	. . . . . . 7 |- ( ( ph /\ x e. X ) -> K e. NN0 )
66	63, 65	expcld 12402	. . . . . 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 6052	. . . . 5 |- ( ph -> F : X --> CC )
69		elpm2r 7488	. . . . 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 1265	. . . 4 |- ( ph -> F e. ( CC ^pm S ) )
71		dvn0 22772	. . . 4 |- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )
72	47, 70, 71	syl2anc 665	. . 3 |- ( ph -> ( ( S Dn F ) ` 0 ) = F )
73	67	a1i 11	. . 3 |- ( ph -> F = ( x e. X |-> ( ( x + A ) ^ K ) ) )
74	64	nn0ge0d 10917	. . . . . . . 8 |- ( ph -> 0 <_ K )
75		0red 9633	. . . . . . . . 9 |- ( ph -> 0 e. RR )
76	64	nn0red 10915	. . . . . . . . 9 |- ( ph -> K e. RR )
77	75, 76	lenltd 9770	. . . . . . . 8 |- ( ph -> ( 0 <_ K <-> -. K < 0 ) )
78	74, 77	mpbid 213	. . . . . . 7 |- ( ph -> -. K < 0 )
79	78	iffalsed 3917	. . . . . 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 466	. . . . 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 10916	. . . . . . . . . . 11 |- ( ph -> K e. CC )
82	81	subid1d 9964	. . . . . . . . . 10 |- ( ph -> ( K - 0 ) = K )
83	82	fveq2d 5876	. . . . . . . . 9 |- ( ph -> ( ! ` ( K - 0 ) ) = ( ! ` K ) )
84	83	oveq2d 6312	. . . . . . . 8 |- ( ph -> ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) = ( ( ! ` K ) / ( ! ` K ) ) )
85		faccl 12455	. . . . . . . . . . 11 |- ( K e. NN0 -> ( ! ` K ) e. NN )
86	64, 85	syl 17	. . . . . . . . . 10 |- ( ph -> ( ! ` K ) e. NN )
87	86	nncnd 10614	. . . . . . . . 9 |- ( ph -> ( ! ` K ) e. CC )
88	86	nnne0d 10643	. . . . . . . . 9 |- ( ph -> ( ! ` K ) =/= 0 )
89	87, 88	dividd 10370	. . . . . . . 8 |- ( ph -> ( ( ! ` K ) / ( ! ` K ) ) = 1 )
90	84, 89	eqtrd 2461	. . . . . . 7 |- ( ph -> ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) = 1 )
91	82	oveq2d 6312	. . . . . . 7 |- ( ph -> ( ( x + A ) ^ ( K - 0 ) ) = ( ( x + A ) ^ K ) )
92	90, 91	oveq12d 6314	. . . . . 6 |- ( ph -> ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) = ( 1 x. ( ( x + A ) ^ K ) ) )
93	92	adantr 466	. . . . 5 |- ( ( ph /\ x e. X ) -> ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) = ( 1 x. ( ( x + A ) ^ K ) ) )
94	66	mulid2d 9650	. . . . 5 |- ( ( ph /\ x e. X ) -> ( 1 x. ( ( x + A ) ^ K ) ) = ( ( x + A ) ^ K ) )
95	80, 93, 94	3eqtrrd 2466	. . . 4 |- ( ( ph /\ x e. X ) -> ( ( x + A ) ^ K ) = if ( K < 0 , 0 , ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) ) )
96	95	mpteq2dva 4503	. . 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 2465	. 2 |- ( ph -> ( ( S Dn F ) ` 0 ) = ( x e. X |-> if ( K < 0 , 0 , ( ( ( ! ` K ) / ( ! ` ( K - 0 ) ) ) x. ( ( x + A ) ^ ( K - 0 ) ) ) ) ) )
98	47	adantr 466	. . . . 5 |- ( ( ph /\ m e. NN0 ) -> S C_ CC )
99	70	adantr 466	. . . . 5 |- ( ( ph /\ m e. NN0 ) -> F e. ( CC ^pm S ) )
100		simpr 462	. . . . 5 |- ( ( ph /\ m e. NN0 ) -> m e. NN0 )
101		dvnp1 22773	. . . . 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 1264	. . . 4 |- ( ( ph /\ m e. NN0 ) -> ( ( S Dn F ) ` ( m + 1 ) ) = ( S _D ( ( S Dn F ) ` m ) ) )
103	102	adantr 466	. . 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 6304	. . . 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 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 ( ( S Dn F ) ` m ) ) = ( S _D ( x e. X |-> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) ) )
106		iftrue 3912	. . . . . . . . 9 |- ( K < m -> if ( K < m , 0 , ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) = 0 )
107	106	mpteq2dv 4504	. . . . . . . 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 6312	. . . . . . 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 467	. . . . . 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 9625	. . . . . . . 8 |- ( ph -> 0 e. CC )
111	45, 50, 110	dvmptconst 37390	. . . . . . 7 |- ( ph -> ( S _D ( x e. X |-> 0 ) ) = ( x e. X |-> 0 ) )
112	111	ad2antrr 730	. . . . . 6 |- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> ( S _D ( x e. X |-> 0 ) ) = ( x e. X |-> 0 ) )
113	76	ad2antrr 730	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> K e. RR )
114		nn0re 10867	. . . . . . . . . . . 12 |- ( m e. NN0 -> m e. RR )
115	114	ad2antlr 731	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> m e. RR )
116		simpr 462	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> K < m )
117	113, 115, 116	ltled 9772	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> K <_ m )
118	64	nn0zd 11027	. . . . . . . . . . . . 13 |- ( ph -> K e. ZZ )
119	118	adantr 466	. . . . . . . . . . . 12 |- ( ( ph /\ m e. NN0 ) -> K e. ZZ )
120	100	nn0zd 11027	. . . . . . . . . . . 12 |- ( ( ph /\ m e. NN0 ) -> m e. ZZ )
121		zleltp1 10976	. . . . . . . . . . . 12 |- ( ( K e. ZZ /\ m e. ZZ ) -> ( K <_ m <-> K < ( m + 1 ) ) )
122	119, 120, 121	syl2anc 665	. . . . . . . . . . 11 |- ( ( ph /\ m e. NN0 ) -> ( K <_ m <-> K < ( m + 1 ) ) )
123	122	adantr 466	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> ( K <_ m <-> K < ( m + 1 ) ) )
124	117, 123	mpbid 213	. . . . . . . . 9 |- ( ( ( ph /\ m e. NN0 ) /\ K < m ) -> K < ( m + 1 ) )
125	124	iftrued 3914	. . . . . . . 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 4504	. . . . . . 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 2428	. . . . . 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 2465	. . . . 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 458	. . . . . 6 |- ( ( ( ph /\ m e. NN0 ) /\ -. K < m ) -> ( ph /\ m e. NN0 ) )
130		simpr 462	. . . . . . 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 730	. . . . . . . 8 |- ( ( ( ph /\ m e. NN0 ) /\ -. K < m ) -> K e. RR )
133	131, 132	lenltd 9770	. . . . . . 7 |- ( ( ( ph /\ m e. NN0 ) /\ -. K < m ) -> ( m <_ K <-> -. K < m ) )
134	130, 133	mpbird 235	. . . . . 6 |- ( ( ( ph /\ m e. NN0 ) /\ -. K < m ) -> m <_ K )
135		simpr 462	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> m = K )
136	114	ad2antlr 731	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> m e. RR )
137	76	ad2antrr 730	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> K e. RR )
138	136, 137	lttri3d 9764	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> ( m = K <-> ( -. m < K /\ -. K < m ) ) )
139	135, 138	mpbid 213	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> ( -. m < K /\ -. K < m ) )
140		simpr 462	. . . . . . . . . . . . 13 |- ( ( -. m < K /\ -. K < m ) -> -. K < m )
141	139, 140	syl 17	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> -. K < m )
142	141	iffalsed 3917	. . . . . . . . . . 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 4504	. . . . . . . . . 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 6312	. . . . . . . . 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 6304	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = K -> ( K - m ) = ( K - K ) )
146	145	fveq2d 5876	. . . . . . . . . . . . . . . . . . . 20 |- ( m = K -> ( ! ` ( K - m ) ) = ( ! ` ( K - K ) ) )
147	146	adantl 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ m = K ) -> ( ! ` ( K - m ) ) = ( ! ` ( K - K ) ) )
148	81	subidd 9963	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( K - K ) = 0 )
149	148	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ! ` ( K - K ) ) = ( ! ` 0 ) )
150		fac0 12448	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ! ` 0 ) = 1
151	150	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ! ` 0 ) = 1 )
152	149, 151	eqtrd 2461	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ! ` ( K - K ) ) = 1 )
153	152	adantr 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ m = K ) -> ( ! ` ( K - K ) ) = 1 )
154	147, 153	eqtrd 2461	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ m = K ) -> ( ! ` ( K - m ) ) = 1 )
155	154	oveq2d 6312	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m = K ) -> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) = ( ( ! ` K ) / 1 ) )
156	87	div1d 10364	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( ! ` K ) / 1 ) = ( ! ` K ) )
157	156	adantr 466	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m = K ) -> ( ( ! ` K ) / 1 ) = ( ! ` K ) )
158	155, 157	eqtrd 2461	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ m = K ) -> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) = ( ! ` K ) )
159	158	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) = ( ! ` K ) )
160	145	adantl 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ m = K ) -> ( K - m ) = ( K - K ) )
161	148	adantr 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ m = K ) -> ( K - K ) = 0 )
162	160, 161	eqtrd 2461	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ m = K ) -> ( K - m ) = 0 )
163	162	oveq2d 6312	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m = K ) -> ( ( x + A ) ^ ( K - m ) ) = ( ( x + A ) ^ 0 ) )
164	163	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( x + A ) ^ ( K - m ) ) = ( ( x + A ) ^ 0 ) )
165	63	exp0d 12396	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. X ) -> ( ( x + A ) ^ 0 ) = 1 )
166	165	adantlr 719	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( x + A ) ^ 0 ) = 1 )
167	164, 166	eqtrd 2461	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( x + A ) ^ ( K - m ) ) = 1 )
168	159, 167	oveq12d 6314	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) = ( ( ! ` K ) x. 1 ) )
169	87	mulid1d 9649	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ! ` K ) x. 1 ) = ( ! ` K ) )
170	169	ad2antrr 730	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( ! ` K ) x. 1 ) = ( ! ` K ) )
171	168, 170	eqtrd 2461	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m = K ) /\ x e. X ) -> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) = ( ! ` K ) )
172	171	mpteq2dva 4503	. . . . . . . . . . . 12 |- ( ( ph /\ m = K ) -> ( x e. X |-> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) = ( x e. X |-> ( ! ` K ) ) )
173	172	oveq2d 6312	. . . . . . . . . . 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 37390	. . . . . . . . . . . 12 |- ( ph -> ( S _D ( x e. X |-> ( ! ` K ) ) ) = ( x e. X |-> 0 ) )
175	174	adantr 466	. . . . . . . . . . 11 |- ( ( ph /\ m = K ) -> ( S _D ( x e. X |-> ( ! ` K ) ) ) = ( x e. X |-> 0 ) )
176	173, 175	eqtrd 2461	. . . . . . . . . 10 |- ( ( ph /\ m = K ) -> ( S _D ( x e. X |-> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( ( x + A ) ^ ( K - m ) ) ) ) ) = ( x e. X |-> 0 ) )
177	176	adantlr 719	. . . . . . . . 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 10526	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> K < ( K + 1 ) )
179		oveq1 6303	. . . . . . . . . . . . . . 15 |- ( m = K -> ( m + 1 ) = ( K + 1 ) )
180	179	eqcomd 2428	. . . . . . . . . . . . . 14 |- ( m = K -> ( K + 1 ) = ( m + 1 ) )
181	180	adantl 467	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> ( K + 1 ) = ( m + 1 ) )
182	178, 181	breqtrd 4441	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN0 ) /\ m = K ) -> K < ( m + 1 ) )
183	182	iftrued 3914	. . . . . . . . . . 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 2428	. . . . . . . . . 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 4504	. . . . . . . . 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 2465	. . . . . . . 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 719	. . . . . . 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 758	. . . . . . . 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 734	. . . . . . . . 9 |- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ -. m = K ) -> K e. RR )
191		simplr 760	. . . . . . . . 9 |- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ -. m = K ) -> m <_ K )
192		neqne 37047	. . . . . . . . . . 11 |- ( -. m = K -> m =/= K )
193	192	necomd 2693	. . . . . . . . . 10 |- ( -. m = K -> K =/= m )
194	193	adantl 467	. . . . . . . . 9 |- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ -. m = K ) -> K =/= m )
195	189, 190, 191, 194	leneltd 9778	. . . . . . . 8 |- ( ( ( ( ph /\ m e. NN0 ) /\ m <_ K ) /\ -. m = K ) -> m < K )
196	114	ad2antlr 731	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> m e. RR )
197	76	ad2antrr 730	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> K e. RR )
198		simpr 462	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> m < K )
199	196, 197, 198	ltled 9772	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> m <_ K )
200	196, 197	lenltd 9770	. . . . . . . . . . . . 13 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( m <_ K <-> -. K < m ) )
201	199, 200	mpbid 213	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> -. K < m )
202	201	iffalsed 3917	. . . . . . . . . . 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 4504	. . . . . . . . . 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 6312	. . . . . . . . 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 466	. . . . . . . . . . 11 |- ( ( ph /\ m e. NN0 ) -> S e. { RR , CC } )
206	205	adantr 466	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> S e. { RR , CC } )
207	87	ad2antrr 730	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` K ) e. CC )
208	100	adantr 466	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> m e. NN0 )
209	64	ad2antrr 730	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> K e. NN0 )
210		nn0sub 10909	. . . . . . . . . . . . . . . 16 |- ( ( m e. NN0 /\ K e. NN0 ) -> ( m <_ K <-> ( K - m ) e. NN0 ) )
211	208, 209, 210	syl2anc 665	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( m <_ K <-> ( K - m ) e. NN0 ) )
212	199, 211	mpbid 213	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( K - m ) e. NN0 )
213		faccl 12455	. . . . . . . . . . . . . 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 10614	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( K - m ) ) e. CC )
216	214	nnne0d 10643	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( K - m ) ) =/= 0 )
217	207, 215, 216	divcld 10372	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) e. CC )
218	217	adantr 466	. . . . . . . . . 10 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) e. CC )
219	75	ad3antrrr 734	. . . . . . . . . 10 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> 0 e. RR )
220	50	adantr 466	. . . . . . . . . . . 12 |- ( ( ph /\ m e. NN0 ) -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )
221	220	adantr 466	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )
222	206, 221, 217	dvmptconst 37390	. . . . . . . . . 10 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( S _D ( x e. X |-> ( ( ! ` K ) / ( ! ` ( K - m ) ) ) ) ) = ( x e. X |-> 0 ) )
223	63	adantlr 719	. . . . . . . . . . . 12 |- ( ( ( ph /\ m e. NN0 ) /\ x e. X ) -> ( x + A ) e. CC )
224	223	adantlr 719	. . . . . . . . . . 11 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( x + A ) e. CC )
225	212	adantr 466	. . . . . . . . . . 11 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( K - m ) e. NN0 )
226	224, 225	expcld 12402	. . . . . . . . . 10 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( x + A ) ^ ( K - m ) ) e. CC )
227	225	nn0cnd 10916	. . . . . . . . . . 11 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( K - m ) e. CC )
228	212	nn0zd 11027	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( K - m ) e. ZZ )
229	196, 197	posdifd 10189	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( m < K <-> 0 < ( K - m ) ) )
230	198, 229	mpbid 213	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> 0 < ( K - m ) )
231	228, 230	jca 534	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( K - m ) e. ZZ /\ 0 < ( K - m ) ) )
232		elnnz 10936	. . . . . . . . . . . . . . 15 |- ( ( K - m ) e. NN <-> ( ( K - m ) e. ZZ /\ 0 < ( K - m ) ) )
233	231, 232	sylibr 215	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( K - m ) e. NN )
234		nnm1nn0 10900	. . . . . . . . . . . . . 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 466	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( K - m ) - 1 ) e. NN0 )
237	224, 236	expcld 12402	. . . . . . . . . . 11 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( x + A ) ^ ( ( K - m ) - 1 ) ) e. CC )
238	227, 237	mulcld 9652	. . . . . . . . . 10 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( K - m ) x. ( ( x + A ) ^ ( ( K - m ) - 1 ) ) ) e. CC )
239	61	ad2antrr 730	. . . . . . . . . . 11 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> A e. CC )
240	206, 221, 239, 233	dvxpaek 37417	. . . . . . . . . 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 22809	. . . . . . . . 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 9820	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( 0 x. ( ( x + A ) ^ ( K - m ) ) ) = 0 )
243	242	oveq1d 6311	. . . . . . . . . . 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 9652	. . . . . . . . . . . 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 9823	. . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> m e. ZZ )
247	119	adantr 466	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> K e. ZZ )
248		zltp1le 10975	. . . . . . . . . . . . . . . . 17 |- ( ( m e. ZZ /\ K e. ZZ ) -> ( m < K <-> ( m + 1 ) <_ K ) )
249	246, 247, 248	syl2anc 665	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( m < K <-> ( m + 1 ) <_ K ) )
250	198, 249	mpbid 213	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( m + 1 ) <_ K )
251		peano2re 9795	. . . . . . . . . . . . . . . . 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 9770	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( m + 1 ) <_ K <-> -. K < ( m + 1 ) ) )
254	250, 253	mpbid 213	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> -. K < ( m + 1 ) )
255	254	adantr 466	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> -. K < ( m + 1 ) )
256	255	iffalsed 3917	. . . . . . . . . . . 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 9655	. . . . . . . . . . . . . 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 2428	. . . . . . . . . . . . 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 10614	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( K - m ) e. CC )
260	207, 215, 259, 216	div32d 10395	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( K - m ) ) = ( ( ! ` K ) x. ( ( K - m ) / ( ! ` ( K - m ) ) ) ) )
261		facnn2 12454	. . . . . . . . . . . . . . . . . . . 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 6312	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( K - m ) / ( ! ` ( K - m ) ) ) = ( ( K - m ) / ( ( ! ` ( ( K - m ) - 1 ) ) x. ( K - m ) ) ) )
264		faccl 12455	. . . . . . . . . . . . . . . . . . . . . 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 10614	. . . . . . . . . . . . . . . . . . . 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 10631	. . . . . . . . . . . . . . . . . . . 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 10631	. . . . . . . . . . . . . . . . . . . 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 37174	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( K - m ) / ( ( ! ` ( ( K - m ) - 1 ) ) x. ( K - m ) ) ) = ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) )
274	263, 273	eqtrd 2461	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( K - m ) / ( ! ` ( K - m ) ) ) = ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) )
275	274	oveq2d 6312	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) x. ( ( K - m ) / ( ! ` ( K - m ) ) ) ) = ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) )
276		eqidd 2421	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) = ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) )
277	260, 275, 276	3eqtrd 2465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ( ! ` K ) / ( ! ` ( K - m ) ) ) x. ( K - m ) ) = ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) )
278	277	adantr 466	. . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m e. NN0 ) -> K e. CC )
280	100	nn0cnd 10916	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m e. NN0 ) -> m e. CC )
281		1cnd 9648	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m e. NN0 ) -> 1 e. CC )
282	279, 280, 281	subsub4d 10006	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ m e. NN0 ) -> ( ( K - m ) - 1 ) = ( K - ( m + 1 ) ) )
283	282	oveq2d 6312	. . . . . . . . . . . . . . 15 |- ( ( ph /\ m e. NN0 ) -> ( ( x + A ) ^ ( ( K - m ) - 1 ) ) = ( ( x + A ) ^ ( K - ( m + 1 ) ) ) )
284	283	ad2antrr 730	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( x + A ) ^ ( ( K - m ) - 1 ) ) = ( ( x + A ) ^ ( K - ( m + 1 ) ) ) )
285	278, 284	oveq12d 6314	. . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( K - m ) - 1 ) = ( K - ( m + 1 ) ) )
287	286	eqcomd 2428	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( K - ( m + 1 ) ) = ( ( K - m ) - 1 ) )
288	287	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ! ` ( K - ( m + 1 ) ) ) = ( ! ` ( ( K - m ) - 1 ) ) )
289	288	oveq2d 6312	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) = ( ( ! ` K ) / ( ! ` ( ( K - m ) - 1 ) ) ) )
290	207, 267, 270	divrecd 10375	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) / ( ! ` ( ( K - m ) - 1 ) ) ) = ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) )
291	289, 290	eqtr2d 2462	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. NN0 ) /\ m < K ) -> ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) = ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) )
292	291	adantr 466	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ m e. NN0 ) /\ m < K ) /\ x e. X ) -> ( ( ! ` K ) x. ( 1 / ( ! ` ( ( K - m ) - 1 ) ) ) ) = ( ( ! ` K ) / ( ! ` ( K - ( m + 1 ) ) ) ) )
293	292	oveq1d 6311	. . . . . . . . . . . . 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 2466	. . . . . . . . . . . 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 9653	. . . . . . . . . . . 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 2466	. . . . . . . . . . 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 2465	. . . . . . . . . 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 4503	. . . . . . . . 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 2465	. . . . . . . 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 665	. . . . . . 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 798	. . . . . 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 665	. . . . 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 798	. . . 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 466	. . 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 2465	. 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 11021	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 187   /\ wa 370   = wceq 1437   e. wcel 1867   =/= wne 2616   _Vcvv 3078   C_ wss 3433   ifcif 3906   ~Pcpw 3976   {cpr 3995   class class class wbr 4417   |-> cmpt 4475   -->wf 5588   ` cfv 5592  (class class class)co 6296   ^pm cpm 7472   CCcc 9526   RRcr 9527   0cc0 9528   1c1 9529   + caddc 9531   x. cmul 9533   < clt 9664   <_ cle 9665   - cmin 9849   / cdiv 10258   NNcn 10598   NN0cn0 10858   ZZcz 10926   ^cexp 12258   !cfa 12445   ↾_t crest 15271   TopOpenctopn 15272  ℂ_fldccnfld 18898   _D cdv 22712   Dncdvn 22713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4529  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-inf2 8137  ax-cnex 9584  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-mulcom 9592  ax-addass 9593  ax-mulass 9594  ax-distr 9595  ax-i2m1 9596  ax-1ne0 9597  ax-1rid 9598  ax-rnegex 9599  ax-rrecex 9600  ax-cnre 9601  ax-pre-lttri 9602  ax-pre-lttrn 9603  ax-pre-ltadd 9604  ax-pre-mulgt0 9605  ax-pre-sup 9606  ax-addf 9607  ax-mulf 9608

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rmo 2781  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-int 4250  df-iun 4295  df-iin 4296  df-br 4418  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4756  df-id 4760  df-po 4766  df-so 4767  df-fr 4804  df-se 4805  df-we 4806  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-pred 5390  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-isom 5601  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-of 6536  df-om 6698  df-1st 6798  df-2nd 6799  df-supp 6917  df-wrecs 7027  df-recs 7089  df-rdg 7127  df-1o 7181  df-2o 7182  df-oadd 7185  df-er 7362  df-map 7473  df-pm 7474  df-ixp 7522  df-en 7569  df-dom 7570  df-sdom 7571  df-fin 7572  df-fsupp 7881  df-fi 7922  df-sup 7953  df-oi 8016  df-card 8363  df-cda 8587  df-pnf 9666  df-mnf 9667  df-xr 9668  df-ltxr 9669  df-le 9670  df-sub 9851  df-neg 9852  df-div 10259  df-nn 10599  df-2 10657  df-3 10658  df-4 10659  df-5 10660  df-6 10661  df-7 10662  df-8 10663  df-9 10664  df-10 10665  df-n0 10859  df-z 10927  df-dec 11041  df-uz 11149  df-q 11254  df-rp 11292  df-xneg 11398  df-xadd 11399  df-xmul 11400  df-icc 11631  df-fz 11772  df-fzo 11903  df-seq 12200  df-exp 12259  df-fac 12446  df-hash 12502  df-cj 13130  df-re 13131  df-im 13132  df-sqrt 13266  df-abs 13267  df-struct 15075  df-ndx 15076  df-slot 15077  df-base 15078  df-sets 15079  df-ress 15080  df-plusg 15155  df-mulr 15156  df-starv 15157  df-sca 15158  df-vsca 15159  df-ip 15160  df-tset 15161  df-ple 15162  df-ds 15164  df-unif 15165  df-hom 15166  df-cco 15167  df-rest 15273  df-topn 15274  df-0g 15292  df-gsum 15293  df-topgen 15294  df-pt 15295  df-prds 15298  df-xrs 15352  df-qtop 15357  df-imas 15358  df-xps 15360  df-mre 15436  df-mrc 15437  df-acs 15439  df-mgm 16432  df-sgrp 16471  df-mnd 16481  df-submnd 16527  df-mulg 16620  df-cntz 16915  df-cmn 17360  df-psmet 18890  df-xmet 18891  df-met 18892  df-bl 18893  df-mopn 18894  df-fbas 18895  df-fg 18896  df-cnfld 18899  df-top 19845  df-bases 19846  df-topon 19847  df-topsp 19848  df-cld 19958  df-ntr 19959  df-cls 19960  df-nei 20038  df-lp 20076  df-perf 20077  df-cn 20167  df-cnp 20168  df-haus 20255  df-tx 20501  df-hmeo 20694  df-fil 20785  df-fm 20877  df-flim 20878  df-flf 20879  df-xms 21259  df-ms 21260  df-tms 21261  df-cncf 21819  df-limc 22715  df-dv 22716  df-dvn 22717

This theorem is referenced by:  etransclem17  37716