Theorem etransclem24 38235

Description: P divides the I -th derivative of F applied to J. when J = 0 and I is not equal to P - 1. This is the second part of case 2 proven in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.)

Hypotheses

Ref	Expression
etransclem24.p	|- ( ph -> P e. NN )
etransclem24.m	|- ( ph -> M e. NN0 )
etransclem24.i	|- ( ph -> I e. NN0 )
etransclem24.ip	|- ( ph -> I =/= ( P - 1 ) )
etransclem24.j	|- ( ph -> J = 0 )
etransclem24.c	|- C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
etransclem24.d	|- ( ph -> D e. ( C ` I ) )

Assertion

Ref	Expression
etransclem24	|- ( ph -> P || ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) )

Distinct variable groups:   D, c, j   I, c, n   j, J   M, c, j, n   P, j   ph, j, n

Allowed substitution hints:   ph( c)   C( j, n, c)   D( n)   P( n, c)   I( j)   J( n, c)

Proof of Theorem etransclem24

Dummy variables A k are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		etransclem24.d	. . . . . . . 8 |- ( ph -> D e. ( C ` I ) )
2		etransclem24.c	. . . . . . . . 9 |- C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
3		etransclem24.i	. . . . . . . . 9 |- ( ph -> I e. NN0 )
4	2, 3	etransclem12 38223	. . . . . . . 8 |- ( ph -> ( C ` I ) = { c e. ( ( 0 ... I ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = I } )
5	1, 4	eleqtrd 2551	. . . . . . 7 |- ( ph -> D e. { c e. ( ( 0 ... I ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = I } )
6		fveq1 5878	. . . . . . . . . 10 |- ( c = D -> ( c ` j ) = ( D ` j ) )
7	6	sumeq2ad 37740	. . . . . . . . 9 |- ( c = D -> sum_ j e. ( 0 ... M ) ( c ` j ) = sum_ j e. ( 0 ... M ) ( D ` j ) )
8	7	eqeq1d 2473	. . . . . . . 8 |- ( c = D -> ( sum_ j e. ( 0 ... M ) ( c ` j ) = I <-> sum_ j e. ( 0 ... M ) ( D ` j ) = I ) )
9	8	elrab 3184	. . . . . . 7 |- ( D e. { c e. ( ( 0 ... I ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = I } <-> ( D e. ( ( 0 ... I ) ^m ( 0 ... M ) ) /\ sum_ j e. ( 0 ... M ) ( D ` j ) = I ) )
10	5, 9	sylib 201	. . . . . 6 |- ( ph -> ( D e. ( ( 0 ... I ) ^m ( 0 ... M ) ) /\ sum_ j e. ( 0 ... M ) ( D ` j ) = I ) )
11	10	simprd 470	. . . . 5 |- ( ph -> sum_ j e. ( 0 ... M ) ( D ` j ) = I )
12	11	ad2antrr 740	. . . 4 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ -. E. k e. ( 1 ... M ) ( D ` k ) e. NN ) -> sum_ j e. ( 0 ... M ) ( D ` j ) = I )
13		ralnex 2834	. . . . 5 |- ( A. k e. ( 1 ... M ) -. ( D ` k ) e. NN <-> -. E. k e. ( 1 ... M ) ( D ` k ) e. NN )
14		etransclem24.m	. . . . . . . . . . 11 |- ( ph -> M e. NN0 )
15		nn0uz 11217	. . . . . . . . . . 11 |- NN0 = ( ZZ>= ` 0 )
16	14, 15	syl6eleq 2559	. . . . . . . . . 10 |- ( ph -> M e. ( ZZ>= ` 0 ) )
17	16	ad2antrr 740	. . . . . . . . 9 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> M e. ( ZZ>= ` 0 ) )
18		fzsscn 37619	. . . . . . . . . . 11 |- ( 0 ... I ) C_ CC
19		ssrab2 3500	. . . . . . . . . . . . . . 15 |- { c e. ( ( 0 ... I ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = I } C_ ( ( 0 ... I ) ^m ( 0 ... M ) )
20	4, 19	syl6eqss 3468	. . . . . . . . . . . . . 14 |- ( ph -> ( C ` I ) C_ ( ( 0 ... I ) ^m ( 0 ... M ) ) )
21	20, 1	sseldd 3419	. . . . . . . . . . . . 13 |- ( ph -> D e. ( ( 0 ... I ) ^m ( 0 ... M ) ) )
22		elmapi 7511	. . . . . . . . . . . . 13 |- ( D e. ( ( 0 ... I ) ^m ( 0 ... M ) ) -> D : ( 0 ... M ) --> ( 0 ... I ) )
23	21, 22	syl 17	. . . . . . . . . . . 12 |- ( ph -> D : ( 0 ... M ) --> ( 0 ... I ) )
24	23	ffvelrnda 6037	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. ( 0 ... I ) )
25	18, 24	sseldi 3416	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. CC )
26	25	adant423 37430	. . . . . . . . 9 |- ( ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. CC )
27		fveq2 5879	. . . . . . . . 9 |- ( j = 0 -> ( D ` j ) = ( D ` 0 ) )
28	17, 26, 27	fsum1p 13891	. . . . . . . 8 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( 0 ... M ) ( D ` j ) = ( ( D ` 0 ) + sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) ) )
29		simplr 770	. . . . . . . . 9 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> ( D ` 0 ) = ( P - 1 ) )
30		0p1e1 10743	. . . . . . . . . . . . . 14 |- ( 0 + 1 ) = 1
31	30	oveq1i 6318	. . . . . . . . . . . . 13 |- ( ( 0 + 1 ) ... M ) = ( 1 ... M )
32	31	sumeq1i 13841	. . . . . . . . . . . 12 |- sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = sum_ j e. ( 1 ... M ) ( D ` j )
33	32	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = sum_ j e. ( 1 ... M ) ( D ` j ) )
34		fveq2 5879	. . . . . . . . . . . . . . . . 17 |- ( k = j -> ( D ` k ) = ( D ` j ) )
35	34	eleq1d 2533	. . . . . . . . . . . . . . . 16 |- ( k = j -> ( ( D ` k ) e. NN <-> ( D ` j ) e. NN ) )
36	35	notbid 301	. . . . . . . . . . . . . . 15 |- ( k = j -> ( -. ( D ` k ) e. NN <-> -. ( D ` j ) e. NN ) )
37	36	rspccva 3135	. . . . . . . . . . . . . 14 |- ( ( A. k e. ( 1 ... M ) -. ( D ` k ) e. NN /\ j e. ( 1 ... M ) ) -> -. ( D ` j ) e. NN )
38	37	adantll 728	. . . . . . . . . . . . 13 |- ( ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) /\ j e. ( 1 ... M ) ) -> -. ( D ` j ) e. NN )
39		fzssnn0 37627	. . . . . . . . . . . . . . . 16 |- ( 0 ... I ) C_ NN0
40		fz1ssfz0 37616	. . . . . . . . . . . . . . . . . 18 |- ( 1 ... M ) C_ ( 0 ... M )
41	40	sseli 3414	. . . . . . . . . . . . . . . . 17 |- ( j e. ( 1 ... M ) -> j e. ( 0 ... M ) )
42	41, 24	sylan2 482	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) e. ( 0 ... I ) )
43	39, 42	sseldi 3416	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) e. NN0 )
44		elnn0 10895	. . . . . . . . . . . . . . 15 |- ( ( D ` j ) e. NN0 <-> ( ( D ` j ) e. NN \/ ( D ` j ) = 0 ) )
45	43, 44	sylib 201	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( D ` j ) e. NN \/ ( D ` j ) = 0 ) )
46	45	adantlr 729	. . . . . . . . . . . . 13 |- ( ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) /\ j e. ( 1 ... M ) ) -> ( ( D ` j ) e. NN \/ ( D ` j ) = 0 ) )
47		orel1 389	. . . . . . . . . . . . 13 |- ( -. ( D ` j ) e. NN -> ( ( ( D ` j ) e. NN \/ ( D ` j ) = 0 ) -> ( D ` j ) = 0 ) )
48	38, 46, 47	sylc 61	. . . . . . . . . . . 12 |- ( ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) /\ j e. ( 1 ... M ) ) -> ( D ` j ) = 0 )
49	48	sumeq2dv 13846	. . . . . . . . . . 11 |- ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( 1 ... M ) ( D ` j ) = sum_ j e. ( 1 ... M ) 0 )
50		fzfi 12223	. . . . . . . . . . . . 13 |- ( 1 ... M ) e. Fin
51	50	olci 398	. . . . . . . . . . . 12 |- ( ( 1 ... M ) C_ ( ZZ>= ` A ) \/ ( 1 ... M ) e. Fin )
52		sumz 13865	. . . . . . . . . . . 12 |- ( ( ( 1 ... M ) C_ ( ZZ>= ` A ) \/ ( 1 ... M ) e. Fin ) -> sum_ j e. ( 1 ... M ) 0 = 0 )
53	51, 52	mp1i 13	. . . . . . . . . . 11 |- ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( 1 ... M ) 0 = 0 )
54	33, 49, 53	3eqtrd 2509	. . . . . . . . . 10 |- ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = 0 )
55	54	adantlr 729	. . . . . . . . 9 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = 0 )
56	29, 55	oveq12d 6326	. . . . . . . 8 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> ( ( D ` 0 ) + sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) ) = ( ( P - 1 ) + 0 ) )
57		etransclem24.p	. . . . . . . . . . . . 13 |- ( ph -> P e. NN )
58		nnm1nn0 10935	. . . . . . . . . . . . 13 |- ( P e. NN -> ( P - 1 ) e. NN0 )
59	57, 58	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( P - 1 ) e. NN0 )
60	59	nn0red 10950	. . . . . . . . . . 11 |- ( ph -> ( P - 1 ) e. RR )
61	60	recnd 9687	. . . . . . . . . 10 |- ( ph -> ( P - 1 ) e. CC )
62	61	addid1d 9851	. . . . . . . . 9 |- ( ph -> ( ( P - 1 ) + 0 ) = ( P - 1 ) )
63	62	ad2antrr 740	. . . . . . . 8 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> ( ( P - 1 ) + 0 ) = ( P - 1 ) )
64	28, 56, 63	3eqtrd 2509	. . . . . . 7 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( 0 ... M ) ( D ` j ) = ( P - 1 ) )
65		etransclem24.ip	. . . . . . . . 9 |- ( ph -> I =/= ( P - 1 ) )
66	65	necomd 2698	. . . . . . . 8 |- ( ph -> ( P - 1 ) =/= I )
67	66	ad2antrr 740	. . . . . . 7 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> ( P - 1 ) =/= I )
68	64, 67	eqnetrd 2710	. . . . . 6 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( 0 ... M ) ( D ` j ) =/= I )
69	68	neneqd 2648	. . . . 5 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> -. sum_ j e. ( 0 ... M ) ( D ` j ) = I )
70	13, 69	sylan2br 484	. . . 4 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ -. E. k e. ( 1 ... M ) ( D ` k ) e. NN ) -> -. sum_ j e. ( 0 ... M ) ( D ` j ) = I )
71	12, 70	condan 811	. . 3 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> E. k e. ( 1 ... M ) ( D ` k ) e. NN )
72	57	nnzd 11062	. . . . . . . . 9 |- ( ph -> P e. ZZ )
73	11	eqcomd 2477	. . . . . . . . . . . . 13 |- ( ph -> I = sum_ j e. ( 0 ... M ) ( D ` j ) )
74	73	fveq2d 5883	. . . . . . . . . . . 12 |- ( ph -> ( ! ` I ) = ( ! ` sum_ j e. ( 0 ... M ) ( D ` j ) ) )
75	74	oveq1d 6323	. . . . . . . . . . 11 |- ( ph -> ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) = ( ( ! ` sum_ j e. ( 0 ... M ) ( D ` j ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) )
76		nfcv 2612	. . . . . . . . . . . 12 |- F/_ j D
77		fzfid 12224	. . . . . . . . . . . 12 |- ( ph -> ( 0 ... M ) e. Fin )
78		nn0ex 10899	. . . . . . . . . . . . . 14 |- NN0 e. _V
79		mapss 7532	. . . . . . . . . . . . . 14 |- ( ( NN0 e. _V /\ ( 0 ... I ) C_ NN0 ) -> ( ( 0 ... I ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) ) )
80	78, 39, 79	mp2an 686	. . . . . . . . . . . . 13 |- ( ( 0 ... I ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) )
81	80, 21	sseldi 3416	. . . . . . . . . . . 12 |- ( ph -> D e. ( NN0 ^m ( 0 ... M ) ) )
82	76, 77, 81	mccl 37775	. . . . . . . . . . 11 |- ( ph -> ( ( ! ` sum_ j e. ( 0 ... M ) ( D ` j ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. NN )
83	75, 82	eqeltrd 2549	. . . . . . . . . 10 |- ( ph -> ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. NN )
84	83	nnzd 11062	. . . . . . . . 9 |- ( ph -> ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. ZZ )
85		fzfid 12224	. . . . . . . . . 10 |- ( ph -> ( 1 ... M ) e. Fin )
86	57	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> P e. NN )
87	23	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> D : ( 0 ... M ) --> ( 0 ... I ) )
88	41	adantl 473	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> j e. ( 0 ... M ) )
89		etransclem24.j	. . . . . . . . . . . . 13 |- ( ph -> J = 0 )
90		0zd 10973	. . . . . . . . . . . . 13 |- ( ph -> 0 e. ZZ )
91	89, 90	eqeltrd 2549	. . . . . . . . . . . 12 |- ( ph -> J e. ZZ )
92	91	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> J e. ZZ )
93	86, 87, 88, 92	etransclem3 38214	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
94	85, 93	fprodzcl 14085	. . . . . . . . 9 |- ( ph -> prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
95	72, 84, 94	3jca 1210	. . . . . . . 8 |- ( ph -> ( P e. ZZ /\ ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. ZZ /\ prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ ) )
96	95	3ad2ant1 1051	. . . . . . 7 |- ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> ( P e. ZZ /\ ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. ZZ /\ prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ ) )
97	72	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( 1 ... M ) ) -> P e. ZZ )
98	57	adantr 472	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( 1 ... M ) ) -> P e. NN )
99	23	adantr 472	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( 1 ... M ) ) -> D : ( 0 ... M ) --> ( 0 ... I ) )
100	40	sseli 3414	. . . . . . . . . . . . 13 |- ( k e. ( 1 ... M ) -> k e. ( 0 ... M ) )
101	100	adantl 473	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( 1 ... M ) ) -> k e. ( 0 ... M ) )
102	91	adantr 472	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( 1 ... M ) ) -> J e. ZZ )
103	98, 99, 101, 102	etransclem3 38214	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( 1 ... M ) ) -> if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) e. ZZ )
104		difss 3549	. . . . . . . . . . . . . . 15 |- ( ( 1 ... M ) \ { k } ) C_ ( 1 ... M )
105		ssfi 7810	. . . . . . . . . . . . . . 15 |- ( ( ( 1 ... M ) e. Fin /\ ( ( 1 ... M ) \ { k } ) C_ ( 1 ... M ) ) -> ( ( 1 ... M ) \ { k } ) e. Fin )
106	50, 104, 105	mp2an 686	. . . . . . . . . . . . . 14 |- ( ( 1 ... M ) \ { k } ) e. Fin
107	106	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( ( 1 ... M ) \ { k } ) e. Fin )
108	57	adantr 472	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( ( 1 ... M ) \ { k } ) ) -> P e. NN )
109	23	adantr 472	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( ( 1 ... M ) \ { k } ) ) -> D : ( 0 ... M ) --> ( 0 ... I ) )
110	104, 40	sstri 3427	. . . . . . . . . . . . . . . 16 |- ( ( 1 ... M ) \ { k } ) C_ ( 0 ... M )
111	110	sseli 3414	. . . . . . . . . . . . . . 15 |- ( j e. ( ( 1 ... M ) \ { k } ) -> j e. ( 0 ... M ) )
112	111	adantl 473	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( ( 1 ... M ) \ { k } ) ) -> j e. ( 0 ... M ) )
113	91	adantr 472	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( ( 1 ... M ) \ { k } ) ) -> J e. ZZ )
114	108, 109, 112, 113	etransclem3 38214	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( ( 1 ... M ) \ { k } ) ) -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
115	107, 114	fprodzcl 14085	. . . . . . . . . . . 12 |- ( ph -> prod_ j e. ( ( 1 ... M ) \ { k } ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
116	115	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( 1 ... M ) ) -> prod_ j e. ( ( 1 ... M ) \ { k } ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
117	97, 103, 116	3jca 1210	. . . . . . . . . 10 |- ( ( ph /\ k e. ( 1 ... M ) ) -> ( P e. ZZ /\ if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) e. ZZ /\ prod_ j e. ( ( 1 ... M ) \ { k } ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ ) )
118	117	3adant3 1050	. . . . . . . . 9 |- ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> ( P e. ZZ /\ if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) e. ZZ /\ prod_ j e. ( ( 1 ... M ) \ { k } ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ ) )
119		dvds0 14395	. . . . . . . . . . . . . 14 |- ( P e. ZZ -> P || 0 )
120	72, 119	syl 17	. . . . . . . . . . . . 13 |- ( ph -> P || 0 )
121	120	adantr 472	. . . . . . . . . . . 12 |- ( ( ph /\ P < ( D ` k ) ) -> P || 0 )
122	121	3ad2antl1 1192	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ P < ( D ` k ) ) -> P || 0 )
123		iftrue 3878	. . . . . . . . . . . . 13 |- ( P < ( D ` k ) -> if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) = 0 )
124	123	eqcomd 2477	. . . . . . . . . . . 12 |- ( P < ( D ` k ) -> 0 = if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) )
125	124	adantl 473	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ P < ( D ` k ) ) -> 0 = if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) )
126	122, 125	breqtrd 4420	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ P < ( D ` k ) ) -> P || if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) )
127	97	adantr 472	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> P e. ZZ )
128		0zd 10973	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. ( 1 ... M ) ) -> 0 e. ZZ )
129	99, 101	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ k e. ( 1 ... M ) ) -> ( D ` k ) e. ( 0 ... I ) )
130	129	elfzelzd 37624	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. ( 1 ... M ) ) -> ( D ` k ) e. ZZ )
131	97, 130	zsubcld 11068	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. ( 1 ... M ) ) -> ( P - ( D ` k ) ) e. ZZ )
132	128, 97, 131	3jca 1210	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( 1 ... M ) ) -> ( 0 e. ZZ /\ P e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) )
133	132	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( 0 e. ZZ /\ P e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) )
134		fzssre 37623	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 0 ... I ) C_ RR
135	134, 129	sseldi 3416	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. ( 1 ... M ) ) -> ( D ` k ) e. RR )
136	135	adantr 472	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( D ` k ) e. RR )
137	127	zred 11063	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> P e. RR )
138		simpr 468	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> -. P < ( D ` k ) )
139	136, 137, 138	nltled 9802	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( D ` k ) <_ P )
140	137, 136	subge0d 10224	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( 0 <_ ( P - ( D ` k ) ) <-> ( D ` k ) <_ P ) )
141	139, 140	mpbird 240	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> 0 <_ ( P - ( D ` k ) ) )
142		elfzle1 11828	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( D ` k ) e. ( 0 ... I ) -> 0 <_ ( D ` k ) )
143	129, 142	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. ( 1 ... M ) ) -> 0 <_ ( D ` k ) )
144	143	adantr 472	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> 0 <_ ( D ` k ) )
145	137, 136	subge02d 10226	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( 0 <_ ( D ` k ) <-> ( P - ( D ` k ) ) <_ P ) )
146	144, 145	mpbid 215	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) <_ P )
147	133, 141, 146	jca32 544	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ( 0 e. ZZ /\ P e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) /\ ( 0 <_ ( P - ( D ` k ) ) /\ ( P - ( D ` k ) ) <_ P ) ) )
148		elfz2 11817	. . . . . . . . . . . . . . . . 17 |- ( ( P - ( D ` k ) ) e. ( 0 ... P ) <-> ( ( 0 e. ZZ /\ P e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) /\ ( 0 <_ ( P - ( D ` k ) ) /\ ( P - ( D ` k ) ) <_ P ) ) )
149	147, 148	sylibr 217	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) e. ( 0 ... P ) )
150		permnn 12549	. . . . . . . . . . . . . . . 16 |- ( ( P - ( D ` k ) ) e. ( 0 ... P ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) e. NN )
151	149, 150	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) e. NN )
152	151	nnzd 11062	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) e. ZZ )
153	101	elfzelzd 37624	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. ( 1 ... M ) ) -> k e. ZZ )
154	102, 153	zsubcld 11068	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( 1 ... M ) ) -> ( J - k ) e. ZZ )
155	154	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( J - k ) e. ZZ )
156	131	adantr 472	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) e. ZZ )
157		elnn0z 10974	. . . . . . . . . . . . . . . 16 |- ( ( P - ( D ` k ) ) e. NN0 <-> ( ( P - ( D ` k ) ) e. ZZ /\ 0 <_ ( P - ( D ` k ) ) ) )
158	156, 141, 157	sylanbrc 677	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) e. NN0 )
159		zexpcl 12325	. . . . . . . . . . . . . . 15 |- ( ( ( J - k ) e. ZZ /\ ( P - ( D ` k ) ) e. NN0 ) -> ( ( J - k ) ^ ( P - ( D ` k ) ) ) e. ZZ )
160	155, 158, 159	syl2anc 673	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ( J - k ) ^ ( P - ( D ` k ) ) ) e. ZZ )
161	127, 152, 160	3jca 1210	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( P e. ZZ /\ ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) e. ZZ /\ ( ( J - k ) ^ ( P - ( D ` k ) ) ) e. ZZ ) )
162	161	3adantl3 1188	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( P e. ZZ /\ ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) e. ZZ /\ ( ( J - k ) ^ ( P - ( D ` k ) ) ) e. ZZ ) )
163	127	3adantl3 1188	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> P e. ZZ )
164	59	nn0zd 11061	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( P - 1 ) e. ZZ )
165	164	adantr 472	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. ( 1 ... M ) ) -> ( P - 1 ) e. ZZ )
166	128, 165, 131	3jca 1210	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. ( 1 ... M ) ) -> ( 0 e. ZZ /\ ( P - 1 ) e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) )
167	166	3adant3 1050	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> ( 0 e. ZZ /\ ( P - 1 ) e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) )
168	167	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( 0 e. ZZ /\ ( P - 1 ) e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) )
169	141	3adantl3 1188	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> 0 <_ ( P - ( D ` k ) ) )
170		1red 9676	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( D ` k ) e. NN ) -> 1 e. RR )
171		nnre 10638	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( D ` k ) e. NN -> ( D ` k ) e. RR )
172	171	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( D ` k ) e. NN ) -> ( D ` k ) e. RR )
173	57	nnred 10646	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> P e. RR )
174	173	adantr 472	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( D ` k ) e. NN ) -> P e. RR )
175		nnge1 10657	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( D ` k ) e. NN -> 1 <_ ( D ` k ) )
176	175	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( D ` k ) e. NN ) -> 1 <_ ( D ` k ) )
177	170, 172, 174, 176	lesub2dd 10251	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( D ` k ) e. NN ) -> ( P - ( D ` k ) ) <_ ( P - 1 ) )
178	177	3adant2 1049	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> ( P - ( D ` k ) ) <_ ( P - 1 ) )
179	178	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) <_ ( P - 1 ) )
180	168, 169, 179	jca32 544	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( ( 0 e. ZZ /\ ( P - 1 ) e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) /\ ( 0 <_ ( P - ( D ` k ) ) /\ ( P - ( D ` k ) ) <_ ( P - 1 ) ) ) )
181		elfz2 11817	. . . . . . . . . . . . . . . . 17 |- ( ( P - ( D ` k ) ) e. ( 0 ... ( P - 1 ) ) <-> ( ( 0 e. ZZ /\ ( P - 1 ) e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) /\ ( 0 <_ ( P - ( D ` k ) ) /\ ( P - ( D ` k ) ) <_ ( P - 1 ) ) ) )
182	180, 181	sylibr 217	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) e. ( 0 ... ( P - 1 ) ) )
183		permnn 12549	. . . . . . . . . . . . . . . 16 |- ( ( P - ( D ` k ) ) e. ( 0 ... ( P - 1 ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) e. NN )
184	182, 183	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) e. NN )
185	184	nnzd 11062	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) e. ZZ )
186		dvdsmul1 14401	. . . . . . . . . . . . . 14 |- ( ( P e. ZZ /\ ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) e. ZZ ) -> P || ( P x. ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) ) )
187	163, 185, 186	syl2anc 673	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> P || ( P x. ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) ) )
188	57	nncnd 10647	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> P e. CC )
189		1cnd 9677	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> 1 e. CC )
190	188, 189	npcand 10009	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( P - 1 ) + 1 ) = P )
191	190	eqcomd 2477	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> P = ( ( P - 1 ) + 1 ) )
192	191	fveq2d 5883	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ! ` P ) = ( ! ` ( ( P - 1 ) + 1 ) ) )
193		facp1 12502	. . . . . . . . . . . . . . . . . . 19 |- ( ( P - 1 ) e. NN0 -> ( ! ` ( ( P - 1 ) + 1 ) ) = ( ( ! ` ( P - 1 ) ) x. ( ( P - 1 ) + 1 ) ) )
194	59, 193	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ! ` ( ( P - 1 ) + 1 ) ) = ( ( ! ` ( P - 1 ) ) x. ( ( P - 1 ) + 1 ) ) )
195	190	oveq2d 6324	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( ! ` ( P - 1 ) ) x. ( ( P - 1 ) + 1 ) ) = ( ( ! ` ( P - 1 ) ) x. P ) )
196	59	faccld 37621	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ! ` ( P - 1 ) ) e. NN )
197	196	nncnd 10647	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ! ` ( P - 1 ) ) e. CC )
198	197, 188	mulcomd 9682	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( ! ` ( P - 1 ) ) x. P ) = ( P x. ( ! ` ( P - 1 ) ) ) )
199	195, 198	eqtrd 2505	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( ! ` ( P - 1 ) ) x. ( ( P - 1 ) + 1 ) ) = ( P x. ( ! ` ( P - 1 ) ) ) )
200	192, 194, 199	3eqtrd 2509	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ! ` P ) = ( P x. ( ! ` ( P - 1 ) ) ) )
201	200	oveq1d 6323	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) = ( ( P x. ( ! ` ( P - 1 ) ) ) / ( ! ` ( P - ( D ` k ) ) ) ) )
202	201	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. P < ( D ` k ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) = ( ( P x. ( ! ` ( P - 1 ) ) ) / ( ! ` ( P - ( D ` k ) ) ) ) )
203	202	3ad2antl1 1192	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) = ( ( P x. ( ! ` ( P - 1 ) ) ) / ( ! ` ( P - ( D ` k ) ) ) ) )
204	188	ad2antrr 740	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> P e. CC )
205	197	ad2antrr 740	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ! ` ( P - 1 ) ) e. CC )
206	158	faccld 37621	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ! ` ( P - ( D ` k ) ) ) e. NN )
207	206	nncnd 10647	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ! ` ( P - ( D ` k ) ) ) e. CC )
208	206	nnne0d 10676	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ! ` ( P - ( D ` k ) ) ) =/= 0 )
209	204, 205, 207, 208	divassd 10440	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ( P x. ( ! ` ( P - 1 ) ) ) / ( ! ` ( P - ( D ` k ) ) ) ) = ( P x. ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) ) )
210	209	3adantl3 1188	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( ( P x. ( ! ` ( P - 1 ) ) ) / ( ! ` ( P - ( D ` k ) ) ) ) = ( P x. ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) ) )
211	203, 210	eqtr2d 2506	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( P x. ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) ) = ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) )
212	187, 211	breqtrd 4420	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> P || ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) )
213		dvdsmultr1 14415	. . . . . . . . . . . 12 |- ( ( P e. ZZ /\ ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) e. ZZ /\ ( ( J - k ) ^ ( P - ( D ` k ) ) ) e. ZZ ) -> ( P || ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) -> P || ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) )
214	162, 212, 213	sylc 61	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> P || ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) )
215		iffalse 3881	. . . . . . . . . . . 12 |- ( -. P < ( D ` k ) -> if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) )
216	215	adantl 473	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) )
217	214, 216	breqtrrd 4422	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> P || if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) )
218	126, 217	pm2.61dan 808	. . . . . . . . 9 |- ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> P || if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) )
219		dvdsmultr1 14415	. . . . . . . . 9 |- ( ( P e. ZZ /\ if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) e. ZZ /\ prod_ j e. ( ( 1 ... M ) \ { k } ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ ) -> ( P || if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) -> P || ( if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) x. prod_ j e. ( ( 1 ... M ) \ { k } ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) )
220	118, 218, 219	sylc 61	. . . . . . . 8 |- ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> P || ( if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) x. prod_ j e. ( ( 1 ... M ) \ { k } ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
221		fzfid 12224	. . . . . . . . 9 |- ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> ( 1 ... M ) e. Fin )
222	93	zcnd 11064	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. CC )
223	222	3ad2antl1 1192	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ j e. ( 1 ... M ) ) -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. CC )
224		simp2 1031	. . . . . . . . 9 |- ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> k e. ( 1 ... M ) )
225		fveq2 5879	. . . . . . . . . . . 12 |- ( j = k -> ( D ` j ) = ( D ` k ) )
226	225	breq2d 4407	. . . . . . . . . . 11 |- ( j = k -> ( P < ( D ` j ) <-> P < ( D ` k ) ) )
227	225	oveq2d 6324	. . . . . . . . . . . . . 14 |- ( j = k -> ( P - ( D ` j ) ) = ( P - ( D ` k ) ) )
228	227	fveq2d 5883	. . . . . . . . . . . . 13 |- ( j = k -> ( ! ` ( P - ( D ` j ) ) ) = ( ! ` ( P - ( D ` k ) ) ) )
229	228	oveq2d 6324	. . . . . . . . . . . 12 |- ( j = k -> ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) = ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) )
230		oveq2 6316	. . . . . . . . . . . . 13 |- ( j = k -> ( J - j ) = ( J - k ) )
231	230, 227	oveq12d 6326	. . . . . . . . . . . 12 |- ( j = k -> ( ( J - j ) ^ ( P - ( D ` j ) ) ) = ( ( J - k ) ^ ( P - ( D ` k ) ) ) )
232	229, 231	oveq12d 6326	. . . . . . . . . . 11 |- ( j = k -> ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) )
233	226, 232	ifbieq2d 3897	. . . . . . . . . 10 |- ( j = k -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) = if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) )
234	233	adantl 473	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ j = k ) -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) = if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) )
235	221, 223, 224, 234	fprodsplit1 37770	. . . . . . . 8 |- ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) = ( if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) x. prod_ j e. ( ( 1 ... M ) \ { k } ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
236	220, 235	breqtrrd 4422	. . . . . . 7 |- ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> P || prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) )
237		dvdsmultr2 14417	. . . . . . 7 |- ( ( P e. ZZ /\ ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. ZZ /\ prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ ) -> ( P || prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) -> P || ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) )
238	96, 236, 237	sylc 61	. . . . . 6 |- ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> P || ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
239	238	3adant1r 1285	. . . . 5 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> P || ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
240		simpr 468	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( D ` 0 ) = ( P - 1 ) )
241		eluzfz1 11832	. . . . . . . . . . . . . . . . . . 19 |- ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
242	16, 241	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> 0 e. ( 0 ... M ) )
243	23, 242	ffvelrnd 6038	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( D ` 0 ) e. ( 0 ... I ) )
244	134, 243	sseldi 3416	. . . . . . . . . . . . . . . 16 |- ( ph -> ( D ` 0 ) e. RR )
245	244	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( D ` 0 ) e. RR )
246	60	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( P - 1 ) e. RR )
247	245, 246	lttri3d 9792	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( D ` 0 ) = ( P - 1 ) <-> ( -. ( D ` 0 ) < ( P - 1 ) /\ -. ( P - 1 ) < ( D ` 0 ) ) ) )
248	240, 247	mpbid 215	. . . . . . . . . . . . 13 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( -. ( D ` 0 ) < ( P - 1 ) /\ -. ( P - 1 ) < ( D ` 0 ) ) )
249	248	simprd 470	. . . . . . . . . . . 12 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> -. ( P - 1 ) < ( D ` 0 ) )
250	249	iffalsed 3883	. . . . . . . . . . 11 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) = ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) )
251		oveq2 6316	. . . . . . . . . . . . . . . . 17 |- ( ( D ` 0 ) = ( P - 1 ) -> ( ( P - 1 ) - ( D ` 0 ) ) = ( ( P - 1 ) - ( P - 1 ) ) )
252	61	subidd 9993	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( P - 1 ) - ( P - 1 ) ) = 0 )
253	251, 252	sylan9eqr 2527	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( P - 1 ) - ( D ` 0 ) ) = 0 )
254	253	fveq2d 5883	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) = ( ! ` 0 ) )
255		fac0 12500	. . . . . . . . . . . . . . 15 |- ( ! ` 0 ) = 1
256	254, 255	syl6eq 2521	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) = 1 )
257	256	oveq2d 6324	. . . . . . . . . . . . 13 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) / 1 ) )
258	197	div1d 10397	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ! ` ( P - 1 ) ) / 1 ) = ( ! ` ( P - 1 ) ) )
259	258	adantr 472	. . . . . . . . . . . . 13 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ! ` ( P - 1 ) ) / 1 ) = ( ! ` ( P - 1 ) ) )
260	257, 259	eqtrd 2505	. . . . . . . . . . . 12 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ! ` ( P - 1 ) ) )
261	253	oveq2d 6324	. . . . . . . . . . . . 13 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = ( J ^ 0 ) )
262	91	zcnd 11064	. . . . . . . . . . . . . . 15 |- ( ph -> J e. CC )
263	262	exp0d 12448	. . . . . . . . . . . . . 14 |- ( ph -> ( J ^ 0 ) = 1 )
264	263	adantr 472	. . . . . . . . . . . . 13 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( J ^ 0 ) = 1 )
265	261, 264	eqtrd 2505	. . . . . . . . . . . 12 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = 1 )
266	260, 265	oveq12d 6326	. . . . . . . . . . 11 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) x. 1 ) )
267	197	mulid1d 9678	. . . . . . . . . . . 12 |- ( ph -> ( ( ! ` ( P - 1 ) ) x. 1 ) = ( ! ` ( P - 1 ) ) )
268	267	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ! ` ( P - 1 ) ) x. 1 ) = ( ! ` ( P - 1 ) ) )
269	250, 266, 268	3eqtrd 2509	. . . . . . . . . 10 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) = ( ! ` ( P - 1 ) ) )
270	269	oveq1d 6323	. . . . . . . . 9 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) = ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
271	270	oveq2d 6324	. . . . . . . 8 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) = ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) )
272	271	oveq1d 6323	. . . . . . 7 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) = ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) )
273	83	nncnd 10647	. . . . . . . . 9 |- ( ph -> ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. CC )
274	94	zcnd 11064	. . . . . . . . . 10 |- ( ph -> prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. CC )
275	197, 274	mulcld 9681	. . . . . . . . 9 |- ( ph -> ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) e. CC )
276	196	nnne0d 10676	. . . . . . . . 9 |- ( ph -> ( ! ` ( P - 1 ) ) =/= 0 )
277	273, 275, 197, 276	divassd 10440	. . . . . . . 8 |- ( ph -> ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) = ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) ) )
278	277	adantr 472	. . . . . . 7 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) = ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) ) )
279	274, 197, 276	divcan3d 10410	. . . . . . . . 9 |- ( ph -> ( ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) = prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) )
280	279	oveq2d 6324	. . . . . . . 8 |- ( ph -> ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) ) = ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
281	280	adantr 472	. . . . . . 7 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) ) = ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
282	272, 278, 281	3eqtrd 2509	. . . . . 6 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) = ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
283	282	3ad2ant1 1051	. . . . 5 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) = ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
284	239, 283	breqtrrd 4422	. . . 4 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> P || ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) )
285	284	rexlimdv3a 2873	. . 3 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( E. k e. ( 1 ... M ) ( D ` k ) e. NN -> P || ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) ) )
286	71, 285	mpd 15	. 2 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> P || ( ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. ( if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) ) / ( ! ` ( P - 1 ) ) ) )
287	120	adantr 472	. . 3 |- ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> P || 0 )
288		simpr 468	. . . . . . . . . . 11 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ ( P - 1 ) < ( D ` 0 ) ) -> ( P - 1 ) < ( D ` 0 ) )
289	288	iftrued 3880	. . . . . . . . . 10 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ ( P - 1 ) < ( D ` 0 ) ) -> if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) = 0 )
290		simpr 468	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> -. ( P - 1 ) < ( D ` 0 ) )
291	290	iffalsed 3883	. . . . . . . . . . 11 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) = ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) )
292		simpll 768	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ph )
293	244	ad2antrr 740	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ( D ` 0 ) e. RR )
294	60	ad2antrr 740	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ( P - 1 ) e. RR )
295	293, 294, 290	nltled 9802	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ( D ` 0 ) <_ ( P - 1 ) )
296		id 22	. . . . . . . . . . . . . . 15 |- ( ( D ` 0 ) =/= ( P - 1 ) -> ( D ` 0 ) =/= ( P - 1 ) )
297	296	necomd 2698	. . . . . . . . . . . . . 14 |- ( ( D ` 0 ) =/= ( P - 1 ) -> ( P - 1 ) =/= ( D ` 0 ) )
298	297	ad2antlr 741	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ( P - 1 ) =/= ( D ` 0 ) )
299	293, 294, 295, 298	leneltd 9806	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ( D ` 0 ) < ( P - 1 ) )
300	89	oveq1d 6323	. . . . . . . . . . . . . . . 16 |- ( ph -> ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) )
301	300	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) )
302	243	elfzelzd 37624	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( D ` 0 ) e. ZZ )
303	164, 302	zsubcld 11068	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( P - 1 ) - ( D ` 0 ) ) e. ZZ )
304	303	adantr 472	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( P - 1 ) - ( D ` 0 ) ) e. ZZ )
305		simpr 468	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( D ` 0 ) < ( P - 1 ) )
306	244	adantr 472	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( D ` 0 ) e. RR )
307	60	adantr 472	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( P - 1 ) e. RR )
308	306, 307	posdifd 10221	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( D ` 0 ) < ( P - 1 ) <-> 0 < ( ( P - 1 ) - ( D ` 0 ) ) ) )
309	305, 308	mpbid 215	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> 0 < ( ( P - 1 ) - ( D ` 0 ) ) )
310		elnnz 10971	. . . . . . . . . . . . . . . . 17 |- ( ( ( P - 1 ) - ( D ` 0 ) ) e. NN <-> ( ( ( P - 1 ) - ( D ` 0 ) ) e. ZZ /\ 0 < ( ( P - 1 ) - ( D ` 0 ) ) ) )
311	304, 309, 310	sylanbrc 677	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( P - 1 ) - ( D ` 0 ) ) e. NN )
312	311	0expd 12470	. . . . . . . . . . . . . . 15 |- ( ( ph /\