Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  etransclem24 Structured version   Visualization version   Unicode version
Theorem etransclem24 40475
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 k A are mutually distinct and distinct from all other variables.
StepHypRef 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 )
42, 3etransclem12 40463 . . . . . . . 8 |- ( ph -> ( C ` I ) = { c e. ( ( 0 ... I ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = I } )
51, 4eleqtrd 2703 . . . . . . 7 |- ( ph -> D e. { c e. ( ( 0 ... I ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = I } )
6 fveq1 6190 . . . . . . . . . 10 |- ( c = D -> ( c ` j ) = ( D ` j ) )
76sumeq2ad 14434 . . . . . . . . 9 |- ( c = D -> sum_ j e. ( 0 ... M ) ( c ` j ) = sum_ j e. ( 0 ... M ) ( D ` j ) )
87eqeq1d 2624 . . . . . . . 8 |- ( c = D -> ( sum_ j e. ( 0 ... M ) ( c ` j ) = I <-> sum_ j e. ( 0 ... M ) ( D ` j ) = I ) )
98elrab 3363 . . . . . . 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 ) )
105, 9sylib 208 . . . . . 6 |- ( ph -> ( D e. ( ( 0 ... I ) ^m ( 0 ... M ) ) /\ sum_ j e. ( 0 ... M ) ( D ` j ) = I ) )
1110simprd 479 . . . . 5 |- ( ph -> sum_ j e. ( 0 ... M ) ( D ` j ) = I )
1211ad2antrr 762 . . . 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 2992 . . . . 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 11722 . . . . . . . . . . 11 |- NN0 = ( ZZ>= ` 0 )
1614, 15syl6eleq 2711 . . . . . . . . . 10 |- ( ph -> M e. ( ZZ>= ` 0 ) )
1716ad2antrr 762 . . . . . . . . 9 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> M e. ( ZZ>= ` 0 ) )
18 fzsscn 39526 . . . . . . . . . . 11 |- ( 0 ... I ) C_ CC
19 ssrab2 3687 . . . . . . . . . . . . . . 15 |- { c e. ( ( 0 ... I ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = I } C_ ( ( 0 ... I ) ^m ( 0 ... M ) )
204, 19syl6eqss 3655 . . . . . . . . . . . . . 14 |- ( ph -> ( C ` I ) C_ ( ( 0 ... I ) ^m ( 0 ... M ) ) )
2120, 1sseldd 3604 . . . . . . . . . . . . 13 |- ( ph -> D e. ( ( 0 ... I ) ^m ( 0 ... M ) ) )
22 elmapi 7879 . . . . . . . . . . . . 13 |- ( D e. ( ( 0 ... I ) ^m ( 0 ... M ) ) -> D : ( 0 ... M ) --> ( 0 ... I ) )
2321, 22syl 17 . . . . . . . . . . . 12 |- ( ph -> D : ( 0 ... M ) --> ( 0 ... I ) )
2423ffvelrnda 6359 . . . . . . . . . . 11 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. ( 0 ... I ) )
2518, 24sseldi 3601 . . . . . . . . . 10 |- ( ( ph /\ j e. ( 0 ... M ) ) -> ( D ` j ) e. CC )
2625ad4ant14 1293 . . . . . . . . 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 6191 . . . . . . . . 9 |- ( j = 0 -> ( D ` j ) = ( D ` 0 ) )
2817, 26, 27fsum1p 14482 . . . . . . . 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 792 . . . . . . . . 9 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> ( D ` 0 ) = ( P - 1 ) )
30 0p1e1 11132 . . . . . . . . . . . . . 14 |- ( 0 + 1 ) = 1
3130oveq1i 6660 . . . . . . . . . . . . 13 |- ( ( 0 + 1 ) ... M ) = ( 1 ... M )
3231sumeq1i 14428 . . . . . . . . . . . 12 |- sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = sum_ j e. ( 1 ... M ) ( D ` j )
3332a1i 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 6191 . . . . . . . . . . . . . . . . 17 |- ( k = j -> ( D ` k ) = ( D ` j ) )
3534eleq1d 2686 . . . . . . . . . . . . . . . 16 |- ( k = j -> ( ( D ` k ) e. NN <-> ( D ` j ) e. NN ) )
3635notbid 308 . . . . . . . . . . . . . . 15 |- ( k = j -> ( -. ( D ` k ) e. NN <-> -. ( D ` j ) e. NN ) )
3736rspccva 3308 . . . . . . . . . . . . . 14 |- ( ( A. k e. ( 1 ... M ) -. ( D ` k ) e. NN /\ j e. ( 1 ... M ) ) -> -. ( D ` j ) e. NN )
3837adantll 750 . . . . . . . . . . . . 13 |- ( ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) /\ j e. ( 1 ... M ) ) -> -. ( D ` j ) e. NN )
39 fzssnn0 39533 . . . . . . . . . . . . . . . 16 |- ( 0 ... I ) C_ NN0
40 fz1ssfz0 39524 . . . . . . . . . . . . . . . . . 18 |- ( 1 ... M ) C_ ( 0 ... M )
4140sseli 3599 . . . . . . . . . . . . . . . . 17 |- ( j e. ( 1 ... M ) -> j e. ( 0 ... M ) )
4241, 24sylan2 491 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) e. ( 0 ... I ) )
4339, 42sseldi 3601 . . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( D ` j ) e. NN0 )
44 elnn0 11294 . . . . . . . . . . . . . . 15 |- ( ( D ` j ) e. NN0 <-> ( ( D ` j ) e. NN \/ ( D ` j ) = 0 ) )
4543, 44sylib 208 . . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( D ` j ) e. NN \/ ( D ` j ) = 0 ) )
4645adantlr 751 . . . . . . . . . . . . 13 |- ( ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) /\ j e. ( 1 ... M ) ) -> ( ( D ` j ) e. NN \/ ( D ` j ) = 0 ) )
47 orel1 397 . . . . . . . . . . . . 13 |- ( -. ( D ` j ) e. NN -> ( ( ( D ` j ) e. NN \/ ( D ` j ) = 0 ) -> ( D ` j ) = 0 ) )
4838, 46, 47sylc 65 . . . . . . . . . . . 12 |- ( ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) /\ j e. ( 1 ... M ) ) -> ( D ` j ) = 0 )
4948sumeq2dv 14433 . . . . . . . . . . 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 12771 . . . . . . . . . . . . 13 |- ( 1 ... M ) e. Fin
5150olci 406 . . . . . . . . . . . 12 |- ( ( 1 ... M ) C_ ( ZZ>= ` A ) \/ ( 1 ... M ) e. Fin )
52 sumz 14453 . . . . . . . . . . . 12 |- ( ( ( 1 ... M ) C_ ( ZZ>= ` A ) \/ ( 1 ... M ) e. Fin ) -> sum_ j e. ( 1 ... M ) 0 = 0 )
5351, 52mp1i 13 . . . . . . . . . . 11 |- ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( 1 ... M ) 0 = 0 )
5433, 49, 533eqtrd 2660 . . . . . . . . . 10 |- ( ( ph /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = 0 )
5554adantlr 751 . . . . . . . . 9 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( ( 0 + 1 ) ... M ) ( D ` j ) = 0 )
5629, 55oveq12d 6668 . . . . . . . 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 11334 . . . . . . . . . . . . 13 |- ( P e. NN -> ( P - 1 ) e. NN0 )
5957, 58syl 17 . . . . . . . . . . . 12 |- ( ph -> ( P - 1 ) e. NN0 )
6059nn0red 11352 . . . . . . . . . . 11 |- ( ph -> ( P - 1 ) e. RR )
6160recnd 10068 . . . . . . . . . 10 |- ( ph -> ( P - 1 ) e. CC )
6261addid1d 10236 . . . . . . . . 9 |- ( ph -> ( ( P - 1 ) + 0 ) = ( P - 1 ) )
6362ad2antrr 762 . . . . . . . 8 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> ( ( P - 1 ) + 0 ) = ( P - 1 ) )
6428, 56, 633eqtrd 2660 . . . . . . 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 ) )
6665necomd 2849 . . . . . . . 8 |- ( ph -> ( P - 1 ) =/= I )
6766ad2antrr 762 . . . . . . 7 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> ( P - 1 ) =/= I )
6864, 67eqnetrd 2861 . . . . . 6 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> sum_ j e. ( 0 ... M ) ( D ` j ) =/= I )
6968neneqd 2799 . . . . 5 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ A. k e. ( 1 ... M ) -. ( D ` k ) e. NN ) -> -. sum_ j e. ( 0 ... M ) ( D ` j ) = I )
7013, 69sylan2br 493 . . . 4 |- ( ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) /\ -. E. k e. ( 1 ... M ) ( D ` k ) e. NN ) -> -. sum_ j e. ( 0 ... M ) ( D ` j ) = I )
7112, 70condan 835 . . 3 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> E. k e. ( 1 ... M ) ( D ` k ) e. NN )
7257nnzd 11481 . . . . . . . . 9 |- ( ph -> P e. ZZ )
7311eqcomd 2628 . . . . . . . . . . . . 13 |- ( ph -> I = sum_ j e. ( 0 ... M ) ( D ` j ) )
7473fveq2d 6195 . . . . . . . . . . . 12 |- ( ph -> ( ! ` I ) = ( ! ` sum_ j e. ( 0 ... M ) ( D ` j ) ) )
7574oveq1d 6665 . . . . . . . . . . 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 2764 . . . . . . . . . . . 12 |- F/_ j D
77 fzfid 12772 . . . . . . . . . . . 12 |- ( ph -> ( 0 ... M ) e. Fin )
78 nn0ex 11298 . . . . . . . . . . . . . 14 |- NN0 e. _V
79 mapss 7900 . . . . . . . . . . . . . 14 |- ( ( NN0 e. _V /\ ( 0 ... I ) C_ NN0 ) -> ( ( 0 ... I ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) ) )
8078, 39, 79mp2an 708 . . . . . . . . . . . . 13 |- ( ( 0 ... I ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) )
8180, 21sseldi 3601 . . . . . . . . . . . 12 |- ( ph -> D e. ( NN0 ^m ( 0 ... M ) ) )
8276, 77, 81mccl 39830 . . . . . . . . . . 11 |- ( ph -> ( ( ! ` sum_ j e. ( 0 ... M ) ( D ` j ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. NN )
8375, 82eqeltrd 2701 . . . . . . . . . 10 |- ( ph -> ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. NN )
8483nnzd 11481 . . . . . . . . 9 |- ( ph -> ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. ZZ )
85 fzfid 12772 . . . . . . . . . 10 |- ( ph -> ( 1 ... M ) e. Fin )
8657adantr 481 . . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> P e. NN )
8723adantr 481 . . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> D : ( 0 ... M ) --> ( 0 ... I ) )
8841adantl 482 . . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> j e. ( 0 ... M ) )
89 etransclem24.j . . . . . . . . . . . . 13 |- ( ph -> J = 0 )
90 0zd 11389 . . . . . . . . . . . . 13 |- ( ph -> 0 e. ZZ )
9189, 90eqeltrd 2701 . . . . . . . . . . . 12 |- ( ph -> J e. ZZ )
9291adantr 481 . . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> J e. ZZ )
9386, 87, 88, 92etransclem3 40454 . . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
9485, 93fprodzcl 14684 . . . . . . . . 9 |- ( ph -> prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
9572, 84, 943jca 1242 . . . . . . . 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 ) )
96953ad2ant1 1082 . . . . . . 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 ) )
9772adantr 481 . . . . . . . . . . 11 |- ( ( ph /\ k e. ( 1 ... M ) ) -> P e. ZZ )
9857adantr 481 . . . . . . . . . . . 12 |- ( ( ph /\ k e. ( 1 ... M ) ) -> P e. NN )
9923adantr 481 . . . . . . . . . . . 12 |- ( ( ph /\ k e. ( 1 ... M ) ) -> D : ( 0 ... M ) --> ( 0 ... I ) )
10040sseli 3599 . . . . . . . . . . . . 13 |- ( k e. ( 1 ... M ) -> k e. ( 0 ... M ) )
101100adantl 482 . . . . . . . . . . . 12 |- ( ( ph /\ k e. ( 1 ... M ) ) -> k e. ( 0 ... M ) )
10291adantr 481 . . . . . . . . . . . 12 |- ( ( ph /\ k e. ( 1 ... M ) ) -> J e. ZZ )
10398, 99, 101, 102etransclem3 40454 . . . . . . . . . . 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 3737 . . . . . . . . . . . . . . 15 |- ( ( 1 ... M ) \ { k } ) C_ ( 1 ... M )
105 ssfi 8180 . . . . . . . . . . . . . . 15 |- ( ( ( 1 ... M ) e. Fin /\ ( ( 1 ... M ) \ { k } ) C_ ( 1 ... M ) ) -> ( ( 1 ... M ) \ { k } ) e. Fin )
10650, 104, 105mp2an 708 . . . . . . . . . . . . . 14 |- ( ( 1 ... M ) \ { k } ) e. Fin
107106a1i 11 . . . . . . . . . . . . 13 |- ( ph -> ( ( 1 ... M ) \ { k } ) e. Fin )
10857adantr 481 . . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( ( 1 ... M ) \ { k } ) ) -> P e. NN )
10923adantr 481 . . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( ( 1 ... M ) \ { k } ) ) -> D : ( 0 ... M ) --> ( 0 ... I ) )
110104, 40sstri 3612 . . . . . . . . . . . . . . . 16 |- ( ( 1 ... M ) \ { k } ) C_ ( 0 ... M )
111110sseli 3599 . . . . . . . . . . . . . . 15 |- ( j e. ( ( 1 ... M ) \ { k } ) -> j e. ( 0 ... M ) )
112111adantl 482 . . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( ( 1 ... M ) \ { k } ) ) -> j e. ( 0 ... M ) )
11391adantr 481 . . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( ( 1 ... M ) \ { k } ) ) -> J e. ZZ )
114108, 109, 112, 113etransclem3 40454 . . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( ( 1 ... M ) \ { k } ) ) -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
115107, 114fprodzcl 14684 . . . . . . . . . . . 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 )
116115adantr 481 . . . . . . . . . . 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 )
11797, 103, 1163jca 1242 . . . . . . . . . 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 ) )
1181173adant3 1081 . . . . . . . . 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 14997 . . . . . . . . . . . . . 14 |- ( P e. ZZ -> P || 0 )
12072, 119syl 17 . . . . . . . . . . . . 13 |- ( ph -> P || 0 )
121120adantr 481 . . . . . . . . . . . 12 |- ( ( ph /\ P < ( D ` k ) ) -> P || 0 )
1221213ad2antl1 1223 . . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ P < ( D ` k ) ) -> P || 0 )
123 iftrue 4092 . . . . . . . . . . . . 13 |- ( P < ( D ` k ) -> if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) = 0 )
124123eqcomd 2628 . . . . . . . . . . . 12 |- ( P < ( D ` k ) -> 0 = if ( P < ( D ` k ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) ) )
125124adantl 482 . . . . . . . . . . 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 ) ) ) ) ) )
126122, 125breqtrd 4679 . . . . . . . . . 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 ) ) ) ) ) )
12797adantr 481 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> P e. ZZ )
128 0zd 11389 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. ( 1 ... M ) ) -> 0 e. ZZ )
12999, 101ffvelrnd 6360 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ k e. ( 1 ... M ) ) -> ( D ` k ) e. ( 0 ... I ) )
130129elfzelzd 39530 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. ( 1 ... M ) ) -> ( D ` k ) e. ZZ )
13197, 130zsubcld 11487 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. ( 1 ... M ) ) -> ( P - ( D ` k ) ) e. ZZ )
132128, 97, 1313jca 1242 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( 1 ... M ) ) -> ( 0 e. ZZ /\ P e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) )
133132adantr 481 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( 0 e. ZZ /\ P e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) )
134 fzssre 39529 . . . . . . . . . . . . . . . . . . . . . 22 |- ( 0 ... I ) C_ RR
135134, 129sseldi 3601 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. ( 1 ... M ) ) -> ( D ` k ) e. RR )
136135adantr 481 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( D ` k ) e. RR )
137127zred 11482 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> P e. RR )
138 simpr 477 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> -. P < ( D ` k ) )
139136, 137, 138nltled 10187 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( D ` k ) <_ P )
140137, 136subge0d 10617 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( 0 <_ ( P - ( D ` k ) ) <-> ( D ` k ) <_ P ) )
141139, 140mpbird 247 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> 0 <_ ( P - ( D ` k ) ) )
142 elfzle1 12344 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( D ` k ) e. ( 0 ... I ) -> 0 <_ ( D ` k ) )
143129, 142syl 17 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. ( 1 ... M ) ) -> 0 <_ ( D ` k ) )
144143adantr 481 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> 0 <_ ( D ` k ) )
145137, 136subge02d 10619 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( 0 <_ ( D ` k ) <-> ( P - ( D ` k ) ) <_ P ) )
146144, 145mpbid 222 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) <_ P )
147133, 141, 146jca32 558 . . . . . . . . . . . . . . . . 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 12333 . . . . . . . . . . . . . . . . 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 ) ) )
149147, 148sylibr 224 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) e. ( 0 ... P ) )
150 permnn 13113 . . . . . . . . . . . . . . . 16 |- ( ( P - ( D ` k ) ) e. ( 0 ... P ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) e. NN )
151149, 150syl 17 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) e. NN )
152151nnzd 11481 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) e. ZZ )
153101elfzelzd 39530 . . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. ( 1 ... M ) ) -> k e. ZZ )
154102, 153zsubcld 11487 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( 1 ... M ) ) -> ( J - k ) e. ZZ )
155154adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( J - k ) e. ZZ )
156131adantr 481 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) e. ZZ )
157 elnn0z 11390 . . . . . . . . . . . . . . . 16 |- ( ( P - ( D ` k ) ) e. NN0 <-> ( ( P - ( D ` k ) ) e. ZZ /\ 0 <_ ( P - ( D ` k ) ) ) )
158156, 141, 157sylanbrc 698 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) e. NN0 )
159 zexpcl 12875 . . . . . . . . . . . . . . 15 |- ( ( ( J - k ) e. ZZ /\ ( P - ( D ` k ) ) e. NN0 ) -> ( ( J - k ) ^ ( P - ( D ` k ) ) ) e. ZZ )
160155, 158, 159syl2anc 693 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ( J - k ) ^ ( P - ( D ` k ) ) ) e. ZZ )
161127, 152, 1603jca 1242 . . . . . . . . . . . . 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 ) )
1621613adantl3 1219 . . . . . . . . . . . 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 ) )
1631273adantl3 1219 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> P e. ZZ )
16459nn0zd 11480 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( P - 1 ) e. ZZ )
165164adantr 481 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ k e. ( 1 ... M ) ) -> ( P - 1 ) e. ZZ )
166128, 165, 1313jca 1242 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. ( 1 ... M ) ) -> ( 0 e. ZZ /\ ( P - 1 ) e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) )
1671663adant3 1081 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> ( 0 e. ZZ /\ ( P - 1 ) e. ZZ /\ ( P - ( D ` k ) ) e. ZZ ) )
168167adantr 481 . . . . . . . . . . . . . . . . . 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 ) )
1691413adantl3 1219 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> 0 <_ ( P - ( D ` k ) ) )
170 1red 10055 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( D ` k ) e. NN ) -> 1 e. RR )
171 nnre 11027 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( D ` k ) e. NN -> ( D ` k ) e. RR )
172171adantl 482 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( D ` k ) e. NN ) -> ( D ` k ) e. RR )
17357nnred 11035 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> P e. RR )
174173adantr 481 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( D ` k ) e. NN ) -> P e. RR )
175 nnge1 11046 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( D ` k ) e. NN -> 1 <_ ( D ` k ) )
176175adantl 482 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( D ` k ) e. NN ) -> 1 <_ ( D ` k ) )
177170, 172, 174, 176lesub2dd 10644 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( D ` k ) e. NN ) -> ( P - ( D ` k ) ) <_ ( P - 1 ) )
1781773adant2 1080 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> ( P - ( D ` k ) ) <_ ( P - 1 ) )
179178adantr 481 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) <_ ( P - 1 ) )
180168, 169, 179jca32 558 . . . . . . . . . . . . . . . . 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 12333 . . . . . . . . . . . . . . . . 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 ) ) ) )
182180, 181sylibr 224 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( P - ( D ` k ) ) e. ( 0 ... ( P - 1 ) ) )
183 permnn 13113 . . . . . . . . . . . . . . . 16 |- ( ( P - ( D ` k ) ) e. ( 0 ... ( P - 1 ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) e. NN )
184182, 183syl 17 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) e. NN )
185184nnzd 11481 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) e. ZZ )
186 dvdsmul1 15003 . . . . . . . . . . . . . 14 |- ( ( P e. ZZ /\ ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) e. ZZ ) -> P || ( P x. ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) ) )
187163, 185, 186syl2anc 693 . . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> P || ( P x. ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) ) )
18857nncnd 11036 . . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> P e. CC )
189 1cnd 10056 . . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> 1 e. CC )
190188, 189npcand 10396 . . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( P - 1 ) + 1 ) = P )
191190eqcomd 2628 . . . . . . . . . . . . . . . . . . 19 |- ( ph -> P = ( ( P - 1 ) + 1 ) )
192191fveq2d 6195 . . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ! ` P ) = ( ! ` ( ( P - 1 ) + 1 ) ) )
193 facp1 13065 . . . . . . . . . . . . . . . . . . 19 |- ( ( P - 1 ) e. NN0 -> ( ! ` ( ( P - 1 ) + 1 ) ) = ( ( ! ` ( P - 1 ) ) x. ( ( P - 1 ) + 1 ) ) )
19459, 193syl 17 . . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ! ` ( ( P - 1 ) + 1 ) ) = ( ( ! ` ( P - 1 ) ) x. ( ( P - 1 ) + 1 ) ) )
195190oveq2d 6666 . . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( ! ` ( P - 1 ) ) x. ( ( P - 1 ) + 1 ) ) = ( ( ! ` ( P - 1 ) ) x. P ) )
19659faccld 13071 . . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ! ` ( P - 1 ) ) e. NN )
197196nncnd 11036 . . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ! ` ( P - 1 ) ) e. CC )
198197, 188mulcomd 10061 . . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( ! ` ( P - 1 ) ) x. P ) = ( P x. ( ! ` ( P - 1 ) ) ) )
199195, 198eqtrd 2656 . . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( ! ` ( P - 1 ) ) x. ( ( P - 1 ) + 1 ) ) = ( P x. ( ! ` ( P - 1 ) ) ) )
200192, 194, 1993eqtrd 2660 . . . . . . . . . . . . . . . . 17 |- ( ph -> ( ! ` P ) = ( P x. ( ! ` ( P - 1 ) ) ) )
201200oveq1d 6665 . . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) = ( ( P x. ( ! ` ( P - 1 ) ) ) / ( ! ` ( P - ( D ` k ) ) ) ) )
202201adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ph /\ -. P < ( D ` k ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) = ( ( P x. ( ! ` ( P - 1 ) ) ) / ( ! ` ( P - ( D ` k ) ) ) ) )
2032023ad2antl1 1223 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) = ( ( P x. ( ! ` ( P - 1 ) ) ) / ( ! ` ( P - ( D ` k ) ) ) ) )
204188ad2antrr 762 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> P e. CC )
205197ad2antrr 762 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ! ` ( P - 1 ) ) e. CC )
206158faccld 13071 . . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ! ` ( P - ( D ` k ) ) ) e. NN )
207206nncnd 11036 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ! ` ( P - ( D ` k ) ) ) e. CC )
208206nnne0d 11065 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ! ` ( P - ( D ` k ) ) ) =/= 0 )
209204, 205, 207, 208divassd 10836 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( 1 ... M ) ) /\ -. P < ( D ` k ) ) -> ( ( P x. ( ! ` ( P - 1 ) ) ) / ( ! ` ( P - ( D ` k ) ) ) ) = ( P x. ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) ) )
2102093adantl3 1219 . . . . . . . . . . . . . 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 ) ) ) ) ) )
211203, 210eqtr2d 2657 . . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> ( P x. ( ( ! ` ( P - 1 ) ) / ( ! ` ( P - ( D ` k ) ) ) ) ) = ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) )
212187, 211breqtrd 4679 . . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) /\ -. P < ( D ` k ) ) -> P || ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) )
213 dvdsmultr1 15019 . . . . . . . . . . . 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 ) ) ) ) ) )
214162, 212, 213sylc 65 . . . . . . . . . . 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 4095 . . . . . . . . . . . 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 ) ) ) ) )
216215adantl 482 . . . . . . . . . . 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 ) ) ) ) )
217214, 216breqtrrd 4681 . . . . . . . . . 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 ) ) ) ) ) )
218126, 217pm2.61dan 832 . . . . . . . . 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 15019 . . . . . . . . 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 ) ) ) ) ) ) ) )
220118, 218, 219sylc 65 . . . . . . . 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 12772 . . . . . . . . 9 |- ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> ( 1 ... M ) e. Fin )
22293zcnd 11483 . . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. CC )
2232223ad2antl1 1223 . . . . . . . . 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 1062 . . . . . . . . 9 |- ( ( ph /\ k e. ( 1 ... M ) /\ ( D ` k ) e. NN ) -> k e. ( 1 ... M ) )
225 fveq2 6191 . . . . . . . . . . . 12 |- ( j = k -> ( D ` j ) = ( D ` k ) )
226225breq2d 4665 . . . . . . . . . . 11 |- ( j = k -> ( P < ( D ` j ) <-> P < ( D ` k ) ) )
227225oveq2d 6666 . . . . . . . . . . . . . 14 |- ( j = k -> ( P - ( D ` j ) ) = ( P - ( D ` k ) ) )
228227fveq2d 6195 . . . . . . . . . . . . 13 |- ( j = k -> ( ! ` ( P - ( D ` j ) ) ) = ( ! ` ( P - ( D ` k ) ) ) )
229228oveq2d 6666 . . . . . . . . . . . 12 |- ( j = k -> ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) = ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) )
230 oveq2 6658 . . . . . . . . . . . . 13 |- ( j = k -> ( J - j ) = ( J - k ) )
231230, 227oveq12d 6668 . . . . . . . . . . . 12 |- ( j = k -> ( ( J - j ) ^ ( P - ( D ` j ) ) ) = ( ( J - k ) ^ ( P - ( D ` k ) ) ) )
232229, 231oveq12d 6668 . . . . . . . . . . 11 |- ( j = k -> ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( D ` k ) ) ) ) x. ( ( J - k ) ^ ( P - ( D ` k ) ) ) ) )
233226, 232ifbieq2d 4111 . . . . . . . . . 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 ) ) ) ) ) )
234233adantl 482 . . . . . . . . 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 ) ) ) ) ) )
235221, 223, 224, 234fprodsplit1 39825 . . . . . . . 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 ) ) ) ) ) ) )
236220, 235breqtrrd 4681 . . . . . . 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 15021 . . . . . . 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 ) ) ) ) ) ) ) )
23896, 236, 237sylc 65 . . . . . 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 ) ) ) ) ) ) )
2392383adant1r 1319 . . . . 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 477 . . . . . . . . . . . . . 14 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( D ` 0 ) = ( P - 1 ) )
241 eluzfz1 12348 . . . . . . . . . . . . . . . . . . 19 |- ( M e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... M ) )
24216, 241syl 17 . . . . . . . . . . . . . . . . . 18 |- ( ph -> 0 e. ( 0 ... M ) )
24323, 242ffvelrnd 6360 . . . . . . . . . . . . . . . . 17 |- ( ph -> ( D ` 0 ) e. ( 0 ... I ) )
244134, 243sseldi 3601 . . . . . . . . . . . . . . . 16 |- ( ph -> ( D ` 0 ) e. RR )
245244adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( D ` 0 ) e. RR )
24660adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( P - 1 ) e. RR )
247245, 246lttri3d 10177 . . . . . . . . . . . . . 14 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( D ` 0 ) = ( P - 1 ) <-> ( -. ( D ` 0 ) < ( P - 1 ) /\ -. ( P - 1 ) < ( D ` 0 ) ) ) )
248240, 247mpbid 222 . . . . . . . . . . . . 13 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( -. ( D ` 0 ) < ( P - 1 ) /\ -. ( P - 1 ) < ( D ` 0 ) ) )
249248simprd 479 . . . . . . . . . . . 12 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> -. ( P - 1 ) < ( D ` 0 ) )
250249iffalsed 4097 . . . . . . . . . . 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 6658 . . . . . . . . . . . . . . . . 17 |- ( ( D ` 0 ) = ( P - 1 ) -> ( ( P - 1 ) - ( D ` 0 ) ) = ( ( P - 1 ) - ( P - 1 ) ) )
25261subidd 10380 . . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( P - 1 ) - ( P - 1 ) ) = 0 )
253251, 252sylan9eqr 2678 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( P - 1 ) - ( D ` 0 ) ) = 0 )
254253fveq2d 6195 . . . . . . . . . . . . . . 15 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) = ( ! ` 0 ) )
255 fac0 13063 . . . . . . . . . . . . . . 15 |- ( ! ` 0 ) = 1
256254, 255syl6eq 2672 . . . . . . . . . . . . . 14 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) = 1 )
257256oveq2d 6666 . . . . . . . . . . . . 13 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) / 1 ) )
258197div1d 10793 . . . . . . . . . . . . . 14 |- ( ph -> ( ( ! ` ( P - 1 ) ) / 1 ) = ( ! ` ( P - 1 ) ) )
259258adantr 481 . . . . . . . . . . . . 13 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ! ` ( P - 1 ) ) / 1 ) = ( ! ` ( P - 1 ) ) )
260257, 259eqtrd 2656 . . . . . . . . . . . 12 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ! ` ( P - 1 ) ) )
261253oveq2d 6666 . . . . . . . . . . . . 13 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = ( J ^ 0 ) )
26291zcnd 11483 . . . . . . . . . . . . . . 15 |- ( ph -> J e. CC )
263262exp0d 13002 . . . . . . . . . . . . . 14 |- ( ph -> ( J ^ 0 ) = 1 )
264263adantr 481 . . . . . . . . . . . . 13 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( J ^ 0 ) = 1 )
265261, 264eqtrd 2656 . . . . . . . . . . . 12 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = 1 )
266260, 265oveq12d 6668 . . . . . . . . . . 11 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ( ! ` ( P - 1 ) ) x. 1 ) )
267197mulid1d 10057 . . . . . . . . . . . 12 |- ( ph -> ( ( ! ` ( P - 1 ) ) x. 1 ) = ( ! ` ( P - 1 ) ) )
268267adantr 481 . . . . . . . . . . 11 |- ( ( ph /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ! ` ( P - 1 ) ) x. 1 ) = ( ! ` ( P - 1 ) ) )
269250, 266, 2683eqtrd 2660 . . . . . . . . . 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 ) ) )
270269oveq1d 6665 . . . . . . . . 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 ) ) ) ) ) ) )
271270oveq2d 6666 . . . . . . . 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 ) ) ) ) ) ) ) )
272271oveq1d 6665 . . . . . . 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 ) ) ) )
27383nncnd 11036 . . . . . . . . 9 |- ( ph -> ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. CC )
27494zcnd 11483 . . . . . . . . . 10 |- ( ph -> prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. CC )
275197, 274mulcld 10060 . . . . . . . . 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 )
276196nnne0d 11065 . . . . . . . . 9 |- ( ph -> ( ! ` ( P - 1 ) ) =/= 0 )
277273, 275, 197, 276divassd 10836 . . . . . . . 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 ) ) ) ) )
278277adantr 481 . . . . . . 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 ) ) ) ) )
279274, 197, 276divcan3d 10806 . . . . . . . . 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 ) ) ) ) ) )
280279oveq2d 6666 . . . . . . . 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 ) ) ) ) ) ) )
281280adantr 481 . . . . . . 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 ) ) ) ) ) ) )
282272, 278, 2813eqtrd 2660 . . . . . 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 ) ) ) ) ) ) )
2832823ad2ant1 1082 . . . . 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 ) ) ) ) ) ) )
284239, 283breqtrrd 4681 . . . 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 ) ) ) )
285284rexlimdv3a 3033 . . 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 ) ) ) ) )
28671, 285mpd 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 ) ) ) )
287120adantr 481 . . 3 |- ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> P || 0 )
288 simpr 477 . . . . . . . . . . 11 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ ( P - 1 ) < ( D ` 0 ) ) -> ( P - 1 ) < ( D ` 0 ) )
289288iftrued 4094 . . . . . . . . . 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 477 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> -. ( P - 1 ) < ( D ` 0 ) )
291290iffalsed 4097 . . . . . . . . . . 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 790 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ph )
293244ad2antrr 762 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ( D ` 0 ) e. RR )
29460ad2antrr 762 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ( P - 1 ) e. RR )
295293, 294, 290nltled 10187 . . . . . . . . . . . . 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 ) )
297296necomd 2849 . . . . . . . . . . . . . 14 |- ( ( D ` 0 ) =/= ( P - 1 ) -> ( P - 1 ) =/= ( D ` 0 ) )
298297ad2antlr 763 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ( P - 1 ) =/= ( D ` 0 ) )
299293, 294, 295, 298leneltd 10191 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ( D ` 0 ) < ( P - 1 ) )
30089oveq1d 6665 . . . . . . . . . . . . . . . 16 |- ( ph -> ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) )
301300adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) )
302243elfzelzd 39530 . . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( D ` 0 ) e. ZZ )
303164, 302zsubcld 11487 . . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( P - 1 ) - ( D ` 0 ) ) e. ZZ )
304303adantr 481 . . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( P - 1 ) - ( D ` 0 ) ) e. ZZ )
305 simpr 477 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( D ` 0 ) < ( P - 1 ) )
306244adantr 481 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( D ` 0 ) e. RR )
30760adantr 481 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( P - 1 ) e. RR )
308306, 307posdifd 10614 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( D ` 0 ) < ( P - 1 ) <-> 0 < ( ( P - 1 ) - ( D ` 0 ) ) ) )
309305, 308mpbid 222 . . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> 0 < ( ( P - 1 ) - ( D ` 0 ) ) )
310 elnnz 11387 . . . . . . . . . . . . . . . . 17 |- ( ( ( P - 1 ) - ( D ` 0 ) ) e. NN <-> ( ( ( P - 1 ) - ( D ` 0 ) ) e. ZZ /\ 0 < ( ( P - 1 ) - ( D ` 0 ) ) ) )
311304, 309, 310sylanbrc 698 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( P - 1 ) - ( D ` 0 ) ) e. NN )
3123110expd 13024 . . . . . . . . . . . . . . 15 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( 0 ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = 0 )
313301, 312eqtrd 2656 . . . . . . . . . . . . . 14 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) = 0 )
314313oveq2d 6666 . . . . . . . . . . . . 13 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) = ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. 0 ) )
315197adantr 481 . . . . . . . . . . . . . . 15 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ! ` ( P - 1 ) ) e. CC )
316311nnnn0d 11351 . . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( P - 1 ) - ( D ` 0 ) ) e. NN0 )
317316faccld 13071 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) e. NN )
318317nncnd 11036 . . . . . . . . . . . . . . 15 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) e. CC )
319317nnne0d 11065 . . . . . . . . . . . . . . 15 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) =/= 0 )
320315, 318, 319divcld 10801 . . . . . . . . . . . . . 14 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) e. CC )
321320mul01d 10235 . . . . . . . . . . . . 13 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. 0 ) = 0 )
322314, 321eqtrd 2656 . . . . . . . . . . . 12 |- ( ( ph /\ ( D ` 0 ) < ( P - 1 ) ) -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) = 0 )
323292, 299, 322syl2anc 693 . . . . . . . . . . 11 |- ( ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) /\ -. ( P - 1 ) < ( D ` 0 ) ) -> ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) = 0 )
324291, 323eqtrd 2656 . . . . . . . . . 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 )
325289, 324pm2.61dan 832 . . . . . . . . 9 |- ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> if ( ( P - 1 ) < ( D ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( D ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( D ` 0 ) ) ) ) ) = 0 )
326325oveq1d 6665 . . . . . . . 8 |- ( ( 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 ) ) ) ) ) ) = ( 0 x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) )
327274mul02d 10234 . . . . . . . . 9 |- ( ph -> ( 0 x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) = 0 )
328327adantr 481 . . . . . . . 8 |- ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> ( 0 x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) ) = 0 )
329326, 328eqtrd 2656 . . . . . . 7 |- ( ( 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 ) ) ) ) ) ) = 0 )
330329oveq2d 6666 . . . . . 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 ) ) ) ) ) ) ) = ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. 0 ) )
331273mul01d 10235 . . . . . . 7 |- ( ph -> ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. 0 ) = 0 )
332331adantr 481 . . . . . 6 |- ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> ( ( ( ! ` I ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) x. 0 ) = 0 )
333330, 332eqtrd 2656 . . . . 5 |- ( ( 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 ) ) ) ) ) ) ) = 0 )
334333oveq1d 6665 . . . 4 |- ( ( 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 ) ) ) = ( 0 / ( ! ` ( P - 1 ) ) ) )
335197, 276div0d 10800 . . . . 5 |- ( ph -> ( 0 / ( ! ` ( P - 1 ) ) ) = 0 )
336335adantr 481 . . . 4 |- ( ( ph /\ ( D ` 0 ) =/= ( P - 1 ) ) -> ( 0 / ( ! ` ( P - 1 ) ) ) = 0 )
337334, 336eqtrd 2656 . . 3 |- ( ( 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 ) ) ) = 0 )
338287, 337breqtrrd 4681 . 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 ) ) ) )
339286, 338pm2.61dane 2881 1 |- ( 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 ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   \ cdif 3571   C_ wss 3574   ifcif 4086   {csn 4177   class class class wbr 4653   |-> cmpt 4729   -->wf 5884   ` cfv 5888  (class class class)co 6650   ^m cmap 7857   Fincfn 7955   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   < clt 10074   <_ cle 10075   - cmin 10266   / cdiv 10684   NNcn 11020   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   ...cfz 12326   ^cexp 12860   !cfa 13060   sum_csu 14416   prod_cprod 14635   || cdvds 14983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-rp 11833  df-fz 12327  df-fzo 12466  df-seq 12802  df-exp 12861  df-fac 13061  df-bc 13090  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-sum 14417  df-prod 14636  df-dvds 14984
This theorem is referenced by:  etransclem38  40489
  Copyright terms: Public domain W3C validator