Metamath Proof Explorer

Theorem etransclem23

Description: This is the claim proof in Juillerat p. 14 (but in our proof, Stirling's approximation is not used). (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem23.a 
|- ( ph -> A : NN0 --> ZZ )
etransclem23.l 
|- L = sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x )
etransclem23.k 
|- K = ( L / ( ! ` ( P - 1 ) ) )
etransclem23.p 
|- ( ph -> P e. NN )
etransclem23.m 
|- ( ph -> M e. NN )
etransclem23.f 
|- F = ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
etransclem23.lt1 
|- ( ph -> ( sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) x. ( ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) / ( ! ` ( P - 1 ) ) ) ) < 1 )
Assertion etransclem23 
|- ( ph -> ( abs ` K ) < 1 )

Proof

Step Hyp Ref Expression
1 etransclem23.a 
 |-  ( ph -> A : NN0 --> ZZ )
2 etransclem23.l 
 |-  L = sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x )
3 etransclem23.k 
 |-  K = ( L / ( ! ` ( P - 1 ) ) )
4 etransclem23.p 
 |-  ( ph -> P e. NN )
5 etransclem23.m 
 |-  ( ph -> M e. NN )
6 etransclem23.f 
 |-  F = ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
7 etransclem23.lt1 
 |-  ( ph -> ( sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) x. ( ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) / ( ! ` ( P - 1 ) ) ) ) < 1 )
8 2 oveq1i 
 |-  ( L / ( ! ` ( P - 1 ) ) ) = ( sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) / ( ! ` ( P - 1 ) ) )
9 3 8 eqtri 
 |-  K = ( sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) / ( ! ` ( P - 1 ) ) )
10 9 fveq2i 
 |-  ( abs ` K ) = ( abs ` ( sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) / ( ! ` ( P - 1 ) ) ) )
11 10 a1i 
 |-  ( ph -> ( abs ` K ) = ( abs ` ( sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) / ( ! ` ( P - 1 ) ) ) ) )
12 fzfid 
 |-  ( ph -> ( 0 ... M ) e. Fin )
13 1 adantr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> A : NN0 --> ZZ )
14 elfznn0 
 |-  ( j e. ( 0 ... M ) -> j e. NN0 )
15 14 adantl 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> j e. NN0 )
16 13 15 ffvelrnd 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( A ` j ) e. ZZ )
17 16 zcnd 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( A ` j ) e. CC )
18 ere 
 |-  _e e. RR
19 18 recni 
 |-  _e e. CC
20 19 a1i 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> _e e. CC )
21 elfzelz 
 |-  ( j e. ( 0 ... M ) -> j e. ZZ )
22 21 zcnd 
 |-  ( j e. ( 0 ... M ) -> j e. CC )
23 22 adantl 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> j e. CC )
24 20 23 cxpcld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( _e ^c j ) e. CC )
25 17 24 mulcld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( A ` j ) x. ( _e ^c j ) ) e. CC )
26 19 a1i 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> _e e. CC )
27 elioore 
 |-  ( x e. ( 0 (,) j ) -> x e. RR )
28 27 recnd 
 |-  ( x e. ( 0 (,) j ) -> x e. CC )
29 28 adantl 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> x e. CC )
30 29 negcld 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> -u x e. CC )
31 26 30 cxpcld 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( _e ^c -u x ) e. CC )
32 ax-resscn 
 |-  RR C_ CC
33 32 a1i 
 |-  ( ph -> RR C_ CC )
34 33 4 6 etransclem8 
 |-  ( ph -> F : RR --> CC )
35 34 adantr 
 |-  ( ( ph /\ x e. ( 0 (,) j ) ) -> F : RR --> CC )
36 27 adantl 
 |-  ( ( ph /\ x e. ( 0 (,) j ) ) -> x e. RR )
37 35 36 ffvelrnd 
 |-  ( ( ph /\ x e. ( 0 (,) j ) ) -> ( F ` x ) e. CC )
38 37 adantlr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( F ` x ) e. CC )
39 31 38 mulcld 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( ( _e ^c -u x ) x. ( F ` x ) ) e. CC )
40 reelprrecn 
 |-  RR e. { RR , CC }
41 40 a1i 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> RR e. { RR , CC } )
42 reopn 
 |-  RR e. ( topGen ` ran (,) )
43 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
44 43 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
45 42 44 eleqtri 
 |-  RR e. ( ( TopOpen ` CCfld ) |`t RR )
46 45 a1i 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> RR e. ( ( TopOpen ` CCfld ) |`t RR ) )
47 4 adantr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> P e. NN )
48 5 nnnn0d 
 |-  ( ph -> M e. NN0 )
49 48 adantr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> M e. NN0 )
50 etransclem6 
 |-  ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) ) = ( y e. RR |-> ( ( y ^ ( P - 1 ) ) x. prod_ h e. ( 1 ... M ) ( ( y - h ) ^ P ) ) )
51 etransclem6 
 |-  ( y e. RR |-> ( ( y ^ ( P - 1 ) ) x. prod_ h e. ( 1 ... M ) ( ( y - h ) ^ P ) ) ) = ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ k e. ( 1 ... M ) ( ( x - k ) ^ P ) ) )
52 6 50 51 3eqtri 
 |-  F = ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ k e. ( 1 ... M ) ( ( x - k ) ^ P ) ) )
53 0red 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> 0 e. RR )
54 21 zred 
 |-  ( j e. ( 0 ... M ) -> j e. RR )
55 54 adantl 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> j e. RR )
56 41 46 47 49 52 53 55 etransclem18 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( x e. ( 0 (,) j ) |-> ( ( _e ^c -u x ) x. ( F ` x ) ) ) e. L^1 )
57 39 56 itgcl 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x e. CC )
58 25 57 mulcld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) e. CC )
59 12 58 fsumcl 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) e. CC )
60 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
61 4 60 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
62 61 faccld 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. NN )
63 62 nncnd 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. CC )
64 62 nnne0d 
 |-  ( ph -> ( ! ` ( P - 1 ) ) =/= 0 )
65 59 63 64 absdivd 
 |-  ( ph -> ( abs ` ( sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) / ( ! ` ( P - 1 ) ) ) ) = ( ( abs ` sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) / ( abs ` ( ! ` ( P - 1 ) ) ) ) )
66 62 nnred 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. RR )
67 62 nnnn0d 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. NN0 )
68 67 nn0ge0d 
 |-  ( ph -> 0 <_ ( ! ` ( P - 1 ) ) )
69 66 68 absidd 
 |-  ( ph -> ( abs ` ( ! ` ( P - 1 ) ) ) = ( ! ` ( P - 1 ) ) )
70 69 oveq2d 
 |-  ( ph -> ( ( abs ` sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) / ( abs ` ( ! ` ( P - 1 ) ) ) ) = ( ( abs ` sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) / ( ! ` ( P - 1 ) ) ) )
71 11 65 70 3eqtrd 
 |-  ( ph -> ( abs ` K ) = ( ( abs ` sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) / ( ! ` ( P - 1 ) ) ) )
72 2 59 eqeltrid 
 |-  ( ph -> L e. CC )
73 72 63 64 divcld 
 |-  ( ph -> ( L / ( ! ` ( P - 1 ) ) ) e. CC )
74 3 73 eqeltrid 
 |-  ( ph -> K e. CC )
75 74 abscld 
 |-  ( ph -> ( abs ` K ) e. RR )
76 71 75 eqeltrrd 
 |-  ( ph -> ( ( abs ` sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) / ( ! ` ( P - 1 ) ) ) e. RR )
77 5 nnred 
 |-  ( ph -> M e. RR )
78 4 nnnn0d 
 |-  ( ph -> P e. NN0 )
79 77 78 reexpcld 
 |-  ( ph -> ( M ^ P ) e. RR )
80 peano2nn0 
 |-  ( M e. NN0 -> ( M + 1 ) e. NN0 )
81 48 80 syl 
 |-  ( ph -> ( M + 1 ) e. NN0 )
82 79 81 reexpcld 
 |-  ( ph -> ( ( M ^ P ) ^ ( M + 1 ) ) e. RR )
83 82 recnd 
 |-  ( ph -> ( ( M ^ P ) ^ ( M + 1 ) ) e. CC )
84 5 nncnd 
 |-  ( ph -> M e. CC )
85 83 84 mulcomd 
 |-  ( ph -> ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) = ( M x. ( ( M ^ P ) ^ ( M + 1 ) ) ) )
86 4 nncnd 
 |-  ( ph -> P e. CC )
87 1cnd 
 |-  ( ph -> 1 e. CC )
88 86 87 npcand 
 |-  ( ph -> ( ( P - 1 ) + 1 ) = P )
89 88 eqcomd 
 |-  ( ph -> P = ( ( P - 1 ) + 1 ) )
90 89 oveq2d 
 |-  ( ph -> ( ( M ^ ( M + 1 ) ) ^ P ) = ( ( M ^ ( M + 1 ) ) ^ ( ( P - 1 ) + 1 ) ) )
91 81 nn0cnd 
 |-  ( ph -> ( M + 1 ) e. CC )
92 91 86 mulcomd 
 |-  ( ph -> ( ( M + 1 ) x. P ) = ( P x. ( M + 1 ) ) )
93 92 oveq2d 
 |-  ( ph -> ( M ^ ( ( M + 1 ) x. P ) ) = ( M ^ ( P x. ( M + 1 ) ) ) )
94 84 78 81 expmuld 
 |-  ( ph -> ( M ^ ( ( M + 1 ) x. P ) ) = ( ( M ^ ( M + 1 ) ) ^ P ) )
95 84 81 78 expmuld 
 |-  ( ph -> ( M ^ ( P x. ( M + 1 ) ) ) = ( ( M ^ P ) ^ ( M + 1 ) ) )
96 93 94 95 3eqtr3d 
 |-  ( ph -> ( ( M ^ ( M + 1 ) ) ^ P ) = ( ( M ^ P ) ^ ( M + 1 ) ) )
97 77 81 reexpcld 
 |-  ( ph -> ( M ^ ( M + 1 ) ) e. RR )
98 97 recnd 
 |-  ( ph -> ( M ^ ( M + 1 ) ) e. CC )
99 98 61 expp1d 
 |-  ( ph -> ( ( M ^ ( M + 1 ) ) ^ ( ( P - 1 ) + 1 ) ) = ( ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) x. ( M ^ ( M + 1 ) ) ) )
100 90 96 99 3eqtr3d 
 |-  ( ph -> ( ( M ^ P ) ^ ( M + 1 ) ) = ( ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) x. ( M ^ ( M + 1 ) ) ) )
101 100 oveq2d 
 |-  ( ph -> ( M x. ( ( M ^ P ) ^ ( M + 1 ) ) ) = ( M x. ( ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) x. ( M ^ ( M + 1 ) ) ) ) )
102 98 61 expcld 
 |-  ( ph -> ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) e. CC )
103 84 102 98 mul12d 
 |-  ( ph -> ( M x. ( ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) x. ( M ^ ( M + 1 ) ) ) ) = ( ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) )
104 84 98 mulcld 
 |-  ( ph -> ( M x. ( M ^ ( M + 1 ) ) ) e. CC )
105 102 104 mulcomd 
 |-  ( ph -> ( ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) = ( ( M x. ( M ^ ( M + 1 ) ) ) x. ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) ) )
106 103 105 eqtrd 
 |-  ( ph -> ( M x. ( ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) x. ( M ^ ( M + 1 ) ) ) ) = ( ( M x. ( M ^ ( M + 1 ) ) ) x. ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) ) )
107 85 101 106 3eqtrd 
 |-  ( ph -> ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) = ( ( M x. ( M ^ ( M + 1 ) ) ) x. ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) ) )
108 107 adantr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) = ( ( M x. ( M ^ ( M + 1 ) ) ) x. ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) ) )
109 108 oveq2d 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) ) = ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( ( M x. ( M ^ ( M + 1 ) ) ) x. ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) ) ) )
110 25 abscld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) e. RR )
111 110 recnd 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) e. CC )
112 104 adantr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( M x. ( M ^ ( M + 1 ) ) ) e. CC )
113 102 adantr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) e. CC )
114 111 112 113 mulassd 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) x. ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) ) = ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( ( M x. ( M ^ ( M + 1 ) ) ) x. ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) ) ) )
115 109 114 eqtr4d 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) ) = ( ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) x. ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) ) )
116 115 sumeq2dv 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) ) = sum_ j e. ( 0 ... M ) ( ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) x. ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) ) )
117 111 112 mulcld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) e. CC )
118 12 102 117 fsummulc1 
 |-  ( ph -> ( sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) x. ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) ) = sum_ j e. ( 0 ... M ) ( ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) x. ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) ) )
119 116 118 eqtr4d 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) ) = ( sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) x. ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) ) )
120 119 oveq1d 
 |-  ( ph -> ( sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) ) / ( ! ` ( P - 1 ) ) ) = ( ( sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) x. ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) ) / ( ! ` ( P - 1 ) ) ) )
121 12 117 fsumcl 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) e. CC )
122 121 102 63 64 divassd 
 |-  ( ph -> ( ( sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) x. ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) ) / ( ! ` ( P - 1 ) ) ) = ( sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) x. ( ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) / ( ! ` ( P - 1 ) ) ) ) )
123 120 122 eqtrd 
 |-  ( ph -> ( sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) ) / ( ! ` ( P - 1 ) ) ) = ( sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) x. ( ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) / ( ! ` ( P - 1 ) ) ) ) )
124 82 adantr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( M ^ P ) ^ ( M + 1 ) ) e. RR )
125 77 adantr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> M e. RR )
126 124 125 remulcld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) e. RR )
127 110 126 remulcld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) ) e. RR )
128 12 127 fsumrecl 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) ) e. RR )
129 128 62 nndivred 
 |-  ( ph -> ( sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) ) / ( ! ` ( P - 1 ) ) ) e. RR )
130 123 129 eqeltrrd 
 |-  ( ph -> ( sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) x. ( ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) / ( ! ` ( P - 1 ) ) ) ) e. RR )
131 1red 
 |-  ( ph -> 1 e. RR )
132 59 abscld 
 |-  ( ph -> ( abs ` sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) e. RR )
133 62 nnrpd 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. RR+ )
134 58 abscld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( abs ` ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) e. RR )
135 12 134 fsumrecl 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( abs ` ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) e. RR )
136 12 58 fsumabs 
 |-  ( ph -> ( abs ` sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) <_ sum_ j e. ( 0 ... M ) ( abs ` ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) )
137 82 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( ( M ^ P ) ^ ( M + 1 ) ) e. RR )
138 ioombl 
 |-  ( 0 (,) j ) e. dom vol
139 138 a1i 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( 0 (,) j ) e. dom vol )
140 0red 
 |-  ( j e. ( 0 ... M ) -> 0 e. RR )
141 elfzle1 
 |-  ( j e. ( 0 ... M ) -> 0 <_ j )
142 volioo 
 |-  ( ( 0 e. RR /\ j e. RR /\ 0 <_ j ) -> ( vol ` ( 0 (,) j ) ) = ( j - 0 ) )
143 140 54 141 142 syl3anc 
 |-  ( j e. ( 0 ... M ) -> ( vol ` ( 0 (,) j ) ) = ( j - 0 ) )
144 54 140 resubcld 
 |-  ( j e. ( 0 ... M ) -> ( j - 0 ) e. RR )
145 143 144 eqeltrd 
 |-  ( j e. ( 0 ... M ) -> ( vol ` ( 0 (,) j ) ) e. RR )
146 145 adantl 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( vol ` ( 0 (,) j ) ) e. RR )
147 83 adantr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( M ^ P ) ^ ( M + 1 ) ) e. CC )
148 iblconstmpt 
 |-  ( ( ( 0 (,) j ) e. dom vol /\ ( vol ` ( 0 (,) j ) ) e. RR /\ ( ( M ^ P ) ^ ( M + 1 ) ) e. CC ) -> ( x e. ( 0 (,) j ) |-> ( ( M ^ P ) ^ ( M + 1 ) ) ) e. L^1 )
149 139 146 147 148 syl3anc 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( x e. ( 0 (,) j ) |-> ( ( M ^ P ) ^ ( M + 1 ) ) ) e. L^1 )
150 137 149 itgrecl 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> S. ( 0 (,) j ) ( ( M ^ P ) ^ ( M + 1 ) ) _d x e. RR )
151 110 150 remulcld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. S. ( 0 (,) j ) ( ( M ^ P ) ^ ( M + 1 ) ) _d x ) e. RR )
152 12 151 fsumrecl 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. S. ( 0 (,) j ) ( ( M ^ P ) ^ ( M + 1 ) ) _d x ) e. RR )
153 25 57 absmuld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( abs ` ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) = ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( abs ` S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) )
154 57 abscld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( abs ` S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) e. RR )
155 25 absge0d 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> 0 <_ ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) )
156 39 abscld 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( abs ` ( ( _e ^c -u x ) x. ( F ` x ) ) ) e. RR )
157 39 56 iblabs 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( x e. ( 0 (,) j ) |-> ( abs ` ( ( _e ^c -u x ) x. ( F ` x ) ) ) ) e. L^1 )
158 156 157 itgrecl 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> S. ( 0 (,) j ) ( abs ` ( ( _e ^c -u x ) x. ( F ` x ) ) ) _d x e. RR )
159 39 56 itgabs 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( abs ` S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) <_ S. ( 0 (,) j ) ( abs ` ( ( _e ^c -u x ) x. ( F ` x ) ) ) _d x )
160 31 38 absmuld 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( abs ` ( ( _e ^c -u x ) x. ( F ` x ) ) ) = ( ( abs ` ( _e ^c -u x ) ) x. ( abs ` ( F ` x ) ) ) )
161 31 abscld 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( abs ` ( _e ^c -u x ) ) e. RR )
162 1red 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> 1 e. RR )
163 38 abscld 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( abs ` ( F ` x ) ) e. RR )
164 31 absge0d 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> 0 <_ ( abs ` ( _e ^c -u x ) ) )
165 38 absge0d 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> 0 <_ ( abs ` ( F ` x ) ) )
166 18 a1i 
 |-  ( x e. ( 0 (,) j ) -> _e e. RR )
167 0re 
 |-  0 e. RR
168 epos 
 |-  0 < _e
169 167 18 168 ltleii 
 |-  0 <_ _e
170 169 a1i 
 |-  ( x e. ( 0 (,) j ) -> 0 <_ _e )
171 27 renegcld 
 |-  ( x e. ( 0 (,) j ) -> -u x e. RR )
172 166 170 171 recxpcld 
 |-  ( x e. ( 0 (,) j ) -> ( _e ^c -u x ) e. RR )
173 166 170 171 cxpge0d 
 |-  ( x e. ( 0 (,) j ) -> 0 <_ ( _e ^c -u x ) )
174 172 173 absidd 
 |-  ( x e. ( 0 (,) j ) -> ( abs ` ( _e ^c -u x ) ) = ( _e ^c -u x ) )
175 174 adantl 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> ( abs ` ( _e ^c -u x ) ) = ( _e ^c -u x ) )
176 172 adantl 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> ( _e ^c -u x ) e. RR )
177 1red 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> 1 e. RR )
178 0xr 
 |-  0 e. RR*
179 178 a1i 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> 0 e. RR* )
180 54 rexrd 
 |-  ( j e. ( 0 ... M ) -> j e. RR* )
181 180 adantr 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> j e. RR* )
182 simpr 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> x e. ( 0 (,) j ) )
183 ioogtlb 
 |-  ( ( 0 e. RR* /\ j e. RR* /\ x e. ( 0 (,) j ) ) -> 0 < x )
184 179 181 182 183 syl3anc 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> 0 < x )
185 27 adantl 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> x e. RR )
186 185 lt0neg2d 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> ( 0 < x <-> -u x < 0 ) )
187 184 186 mpbid 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> -u x < 0 )
188 18 a1i 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> _e e. RR )
189 1lt2 
 |-  1 < 2
190 egt2lt3 
 |-  ( 2 < _e /\ _e < 3 )
191 190 simpli 
 |-  2 < _e
192 1re 
 |-  1 e. RR
193 2re 
 |-  2 e. RR
194 192 193 18 lttri 
 |-  ( ( 1 < 2 /\ 2 < _e ) -> 1 < _e )
195 189 191 194 mp2an 
 |-  1 < _e
196 195 a1i 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> 1 < _e )
197 171 adantl 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> -u x e. RR )
198 0red 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> 0 e. RR )
199 188 196 197 198 cxpltd 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> ( -u x < 0 <-> ( _e ^c -u x ) < ( _e ^c 0 ) ) )
200 187 199 mpbid 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> ( _e ^c -u x ) < ( _e ^c 0 ) )
201 cxp0 
 |-  ( _e e. CC -> ( _e ^c 0 ) = 1 )
202 19 201 mp1i 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> ( _e ^c 0 ) = 1 )
203 200 202 breqtrd 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> ( _e ^c -u x ) < 1 )
204 176 177 203 ltled 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> ( _e ^c -u x ) <_ 1 )
205 175 204 eqbrtrd 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> ( abs ` ( _e ^c -u x ) ) <_ 1 )
206 205 adantll 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( abs ` ( _e ^c -u x ) ) <_ 1 )
207 32 a1i 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> RR C_ CC )
208 4 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> P e. NN )
209 48 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> M e. NN0 )
210 6 50 eqtri 
 |-  F = ( y e. RR |-> ( ( y ^ ( P - 1 ) ) x. prod_ h e. ( 1 ... M ) ( ( y - h ) ^ P ) ) )
211 27 adantl 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> x e. RR )
212 207 208 209 210 211 etransclem13 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( F ` x ) = prod_ h e. ( 0 ... M ) ( ( x - h ) ^ if ( h = 0 , ( P - 1 ) , P ) ) )
213 212 fveq2d 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( abs ` ( F ` x ) ) = ( abs ` prod_ h e. ( 0 ... M ) ( ( x - h ) ^ if ( h = 0 , ( P - 1 ) , P ) ) ) )
214 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
215 27 adantr 
 |-  ( ( x e. ( 0 (,) j ) /\ h e. NN0 ) -> x e. RR )
216 nn0re 
 |-  ( h e. NN0 -> h e. RR )
217 216 adantl 
 |-  ( ( x e. ( 0 (,) j ) /\ h e. NN0 ) -> h e. RR )
218 215 217 resubcld 
 |-  ( ( x e. ( 0 (,) j ) /\ h e. NN0 ) -> ( x - h ) e. RR )
219 218 adantll 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. NN0 ) -> ( x - h ) e. RR )
220 61 78 ifcld 
 |-  ( ph -> if ( h = 0 , ( P - 1 ) , P ) e. NN0 )
221 220 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. NN0 ) -> if ( h = 0 , ( P - 1 ) , P ) e. NN0 )
222 219 221 reexpcld 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. NN0 ) -> ( ( x - h ) ^ if ( h = 0 , ( P - 1 ) , P ) ) e. RR )
223 222 recnd 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. NN0 ) -> ( ( x - h ) ^ if ( h = 0 , ( P - 1 ) , P ) ) e. CC )
224 214 209 223 fprodabs 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( abs ` prod_ h e. ( 0 ... M ) ( ( x - h ) ^ if ( h = 0 , ( P - 1 ) , P ) ) ) = prod_ h e. ( 0 ... M ) ( abs ` ( ( x - h ) ^ if ( h = 0 , ( P - 1 ) , P ) ) ) )
225 elfznn0 
 |-  ( h e. ( 0 ... M ) -> h e. NN0 )
226 28 adantr 
 |-  ( ( x e. ( 0 (,) j ) /\ h e. NN0 ) -> x e. CC )
227 nn0cn 
 |-  ( h e. NN0 -> h e. CC )
228 227 adantl 
 |-  ( ( x e. ( 0 (,) j ) /\ h e. NN0 ) -> h e. CC )
229 226 228 subcld 
 |-  ( ( x e. ( 0 (,) j ) /\ h e. NN0 ) -> ( x - h ) e. CC )
230 229 adantll 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. NN0 ) -> ( x - h ) e. CC )
231 225 230 sylan2 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> ( x - h ) e. CC )
232 220 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> if ( h = 0 , ( P - 1 ) , P ) e. NN0 )
233 231 232 absexpd 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> ( abs ` ( ( x - h ) ^ if ( h = 0 , ( P - 1 ) , P ) ) ) = ( ( abs ` ( x - h ) ) ^ if ( h = 0 , ( P - 1 ) , P ) ) )
234 233 prodeq2dv 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> prod_ h e. ( 0 ... M ) ( abs ` ( ( x - h ) ^ if ( h = 0 , ( P - 1 ) , P ) ) ) = prod_ h e. ( 0 ... M ) ( ( abs ` ( x - h ) ) ^ if ( h = 0 , ( P - 1 ) , P ) ) )
235 213 224 234 3eqtrd 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( abs ` ( F ` x ) ) = prod_ h e. ( 0 ... M ) ( ( abs ` ( x - h ) ) ^ if ( h = 0 , ( P - 1 ) , P ) ) )
236 nfv 
 |-  F/ h ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) )
237 fzfid 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( 0 ... M ) e. Fin )
238 225 229 sylan2 
 |-  ( ( x e. ( 0 (,) j ) /\ h e. ( 0 ... M ) ) -> ( x - h ) e. CC )
239 238 abscld 
 |-  ( ( x e. ( 0 (,) j ) /\ h e. ( 0 ... M ) ) -> ( abs ` ( x - h ) ) e. RR )
240 239 adantll 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> ( abs ` ( x - h ) ) e. RR )
241 240 232 reexpcld 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> ( ( abs ` ( x - h ) ) ^ if ( h = 0 , ( P - 1 ) , P ) ) e. RR )
242 238 absge0d 
 |-  ( ( x e. ( 0 (,) j ) /\ h e. ( 0 ... M ) ) -> 0 <_ ( abs ` ( x - h ) ) )
243 242 adantll 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> 0 <_ ( abs ` ( x - h ) ) )
244 240 232 243 expge0d 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> 0 <_ ( ( abs ` ( x - h ) ) ^ if ( h = 0 , ( P - 1 ) , P ) ) )
245 79 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> ( M ^ P ) e. RR )
246 77 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> M e. RR )
247 246 232 reexpcld 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> ( M ^ if ( h = 0 , ( P - 1 ) , P ) ) e. RR )
248 225 219 sylan2 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> ( x - h ) e. RR )
249 28 adantr 
 |-  ( ( x e. ( 0 (,) j ) /\ h e. ( 0 ... M ) ) -> x e. CC )
250 225 228 sylan2 
 |-  ( ( x e. ( 0 (,) j ) /\ h e. ( 0 ... M ) ) -> h e. CC )
251 249 250 negsubdi2d 
 |-  ( ( x e. ( 0 (,) j ) /\ h e. ( 0 ... M ) ) -> -u ( x - h ) = ( h - x ) )
252 251 adantll 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> -u ( x - h ) = ( h - x ) )
253 225 adantl 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> h e. NN0 )
254 253 nn0red 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> h e. RR )
255 0red 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> 0 e. RR )
256 211 adantr 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> x e. RR )
257 elfzle2 
 |-  ( h e. ( 0 ... M ) -> h <_ M )
258 257 adantl 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> h <_ M )
259 198 185 184 ltled 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> 0 <_ x )
260 259 adantll 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> 0 <_ x )
261 260 adantr 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> 0 <_ x )
262 254 255 246 256 258 261 le2subd 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> ( h - x ) <_ ( M - 0 ) )
263 84 subid1d 
 |-  ( ph -> ( M - 0 ) = M )
264 263 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> ( M - 0 ) = M )
265 262 264 breqtrd 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> ( h - x ) <_ M )
266 252 265 eqbrtrd 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> -u ( x - h ) <_ M )
267 248 246 266 lenegcon1d 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> -u M <_ ( x - h ) )
268 elfzel2 
 |-  ( j e. ( 0 ... M ) -> M e. ZZ )
269 268 zred 
 |-  ( j e. ( 0 ... M ) -> M e. RR )
270 269 adantr 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> M e. RR )
271 54 adantr 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> j e. RR )
272 iooltub 
 |-  ( ( 0 e. RR* /\ j e. RR* /\ x e. ( 0 (,) j ) ) -> x < j )
273 179 181 182 272 syl3anc 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> x < j )
274 elfzle2 
 |-  ( j e. ( 0 ... M ) -> j <_ M )
275 274 adantr 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> j <_ M )
276 185 271 270 273 275 ltletrd 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> x < M )
277 185 270 276 ltled 
 |-  ( ( j e. ( 0 ... M ) /\ x e. ( 0 (,) j ) ) -> x <_ M )
278 277 adantll 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> x <_ M )
279 278 adantr 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> x <_ M )
280 253 nn0ge0d 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> 0 <_ h )
281 256 255 246 254 279 280 le2subd 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> ( x - h ) <_ ( M - 0 ) )
282 281 264 breqtrd 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> ( x - h ) <_ M )
283 248 246 absled 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> ( ( abs ` ( x - h ) ) <_ M <-> ( -u M <_ ( x - h ) /\ ( x - h ) <_ M ) ) )
284 267 282 283 mpbir2and 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> ( abs ` ( x - h ) ) <_ M )
285 leexp1a 
 |-  ( ( ( ( abs ` ( x - h ) ) e. RR /\ M e. RR /\ if ( h = 0 , ( P - 1 ) , P ) e. NN0 ) /\ ( 0 <_ ( abs ` ( x - h ) ) /\ ( abs ` ( x - h ) ) <_ M ) ) -> ( ( abs ` ( x - h ) ) ^ if ( h = 0 , ( P - 1 ) , P ) ) <_ ( M ^ if ( h = 0 , ( P - 1 ) , P ) ) )
286 240 246 232 243 284 285 syl32anc 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> ( ( abs ` ( x - h ) ) ^ if ( h = 0 , ( P - 1 ) , P ) ) <_ ( M ^ if ( h = 0 , ( P - 1 ) , P ) ) )
287 5 nnge1d 
 |-  ( ph -> 1 <_ M )
288 287 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> 1 <_ M )
289 220 nn0zd 
 |-  ( ph -> if ( h = 0 , ( P - 1 ) , P ) e. ZZ )
290 78 nn0zd 
 |-  ( ph -> P e. ZZ )
291 iftrue 
 |-  ( h = 0 -> if ( h = 0 , ( P - 1 ) , P ) = ( P - 1 ) )
292 291 adantl 
 |-  ( ( ph /\ h = 0 ) -> if ( h = 0 , ( P - 1 ) , P ) = ( P - 1 ) )
293 4 nnred 
 |-  ( ph -> P e. RR )
294 293 lem1d 
 |-  ( ph -> ( P - 1 ) <_ P )
295 294 adantr 
 |-  ( ( ph /\ h = 0 ) -> ( P - 1 ) <_ P )
296 292 295 eqbrtrd 
 |-  ( ( ph /\ h = 0 ) -> if ( h = 0 , ( P - 1 ) , P ) <_ P )
297 iffalse 
 |-  ( -. h = 0 -> if ( h = 0 , ( P - 1 ) , P ) = P )
298 297 adantl 
 |-  ( ( ph /\ -. h = 0 ) -> if ( h = 0 , ( P - 1 ) , P ) = P )
299 293 leidd 
 |-  ( ph -> P <_ P )
300 299 adantr 
 |-  ( ( ph /\ -. h = 0 ) -> P <_ P )
301 298 300 eqbrtrd 
 |-  ( ( ph /\ -. h = 0 ) -> if ( h = 0 , ( P - 1 ) , P ) <_ P )
302 296 301 pm2.61dan 
 |-  ( ph -> if ( h = 0 , ( P - 1 ) , P ) <_ P )
303 eluz2 
 |-  ( P e. ( ZZ>= ` if ( h = 0 , ( P - 1 ) , P ) ) <-> ( if ( h = 0 , ( P - 1 ) , P ) e. ZZ /\ P e. ZZ /\ if ( h = 0 , ( P - 1 ) , P ) <_ P ) )
304 289 290 302 303 syl3anbrc 
 |-  ( ph -> P e. ( ZZ>= ` if ( h = 0 , ( P - 1 ) , P ) ) )
305 304 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> P e. ( ZZ>= ` if ( h = 0 , ( P - 1 ) , P ) ) )
306 246 288 305 leexp2ad 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> ( M ^ if ( h = 0 , ( P - 1 ) , P ) ) <_ ( M ^ P ) )
307 241 247 245 286 306 letrd 
 |-  ( ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) /\ h e. ( 0 ... M ) ) -> ( ( abs ` ( x - h ) ) ^ if ( h = 0 , ( P - 1 ) , P ) ) <_ ( M ^ P ) )
308 236 237 241 244 245 307 fprodle 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> prod_ h e. ( 0 ... M ) ( ( abs ` ( x - h ) ) ^ if ( h = 0 , ( P - 1 ) , P ) ) <_ prod_ h e. ( 0 ... M ) ( M ^ P ) )
309 79 recnd 
 |-  ( ph -> ( M ^ P ) e. CC )
310 fprodconst 
 |-  ( ( ( 0 ... M ) e. Fin /\ ( M ^ P ) e. CC ) -> prod_ h e. ( 0 ... M ) ( M ^ P ) = ( ( M ^ P ) ^ ( # ` ( 0 ... M ) ) ) )
311 12 309 310 syl2anc 
 |-  ( ph -> prod_ h e. ( 0 ... M ) ( M ^ P ) = ( ( M ^ P ) ^ ( # ` ( 0 ... M ) ) ) )
312 hashfz0 
 |-  ( M e. NN0 -> ( # ` ( 0 ... M ) ) = ( M + 1 ) )
313 48 312 syl 
 |-  ( ph -> ( # ` ( 0 ... M ) ) = ( M + 1 ) )
314 313 oveq2d 
 |-  ( ph -> ( ( M ^ P ) ^ ( # ` ( 0 ... M ) ) ) = ( ( M ^ P ) ^ ( M + 1 ) ) )
315 311 314 eqtrd 
 |-  ( ph -> prod_ h e. ( 0 ... M ) ( M ^ P ) = ( ( M ^ P ) ^ ( M + 1 ) ) )
316 315 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> prod_ h e. ( 0 ... M ) ( M ^ P ) = ( ( M ^ P ) ^ ( M + 1 ) ) )
317 308 316 breqtrd 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> prod_ h e. ( 0 ... M ) ( ( abs ` ( x - h ) ) ^ if ( h = 0 , ( P - 1 ) , P ) ) <_ ( ( M ^ P ) ^ ( M + 1 ) ) )
318 235 317 eqbrtrd 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( abs ` ( F ` x ) ) <_ ( ( M ^ P ) ^ ( M + 1 ) ) )
319 161 162 163 137 164 165 206 318 lemul12ad 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( ( abs ` ( _e ^c -u x ) ) x. ( abs ` ( F ` x ) ) ) <_ ( 1 x. ( ( M ^ P ) ^ ( M + 1 ) ) ) )
320 83 mulid2d 
 |-  ( ph -> ( 1 x. ( ( M ^ P ) ^ ( M + 1 ) ) ) = ( ( M ^ P ) ^ ( M + 1 ) ) )
321 320 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( 1 x. ( ( M ^ P ) ^ ( M + 1 ) ) ) = ( ( M ^ P ) ^ ( M + 1 ) ) )
322 319 321 breqtrd 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( ( abs ` ( _e ^c -u x ) ) x. ( abs ` ( F ` x ) ) ) <_ ( ( M ^ P ) ^ ( M + 1 ) ) )
323 160 322 eqbrtrd 
 |-  ( ( ( ph /\ j e. ( 0 ... M ) ) /\ x e. ( 0 (,) j ) ) -> ( abs ` ( ( _e ^c -u x ) x. ( F ` x ) ) ) <_ ( ( M ^ P ) ^ ( M + 1 ) ) )
324 157 149 156 137 323 itgle 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> S. ( 0 (,) j ) ( abs ` ( ( _e ^c -u x ) x. ( F ` x ) ) ) _d x <_ S. ( 0 (,) j ) ( ( M ^ P ) ^ ( M + 1 ) ) _d x )
325 154 158 150 159 324 letrd 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( abs ` S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) <_ S. ( 0 (,) j ) ( ( M ^ P ) ^ ( M + 1 ) ) _d x )
326 154 150 110 155 325 lemul2ad 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( abs ` S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) <_ ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. S. ( 0 (,) j ) ( ( M ^ P ) ^ ( M + 1 ) ) _d x ) )
327 153 326 eqbrtrd 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( abs ` ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) <_ ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. S. ( 0 (,) j ) ( ( M ^ P ) ^ ( M + 1 ) ) _d x ) )
328 12 134 151 327 fsumle 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( abs ` ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) <_ sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. S. ( 0 (,) j ) ( ( M ^ P ) ^ ( M + 1 ) ) _d x ) )
329 itgconst 
 |-  ( ( ( 0 (,) j ) e. dom vol /\ ( vol ` ( 0 (,) j ) ) e. RR /\ ( ( M ^ P ) ^ ( M + 1 ) ) e. CC ) -> S. ( 0 (,) j ) ( ( M ^ P ) ^ ( M + 1 ) ) _d x = ( ( ( M ^ P ) ^ ( M + 1 ) ) x. ( vol ` ( 0 (,) j ) ) ) )
330 139 146 147 329 syl3anc 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> S. ( 0 (,) j ) ( ( M ^ P ) ^ ( M + 1 ) ) _d x = ( ( ( M ^ P ) ^ ( M + 1 ) ) x. ( vol ` ( 0 (,) j ) ) ) )
331 48 nn0ge0d 
 |-  ( ph -> 0 <_ M )
332 77 78 331 expge0d 
 |-  ( ph -> 0 <_ ( M ^ P ) )
333 79 81 332 expge0d 
 |-  ( ph -> 0 <_ ( ( M ^ P ) ^ ( M + 1 ) ) )
334 333 adantr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> 0 <_ ( ( M ^ P ) ^ ( M + 1 ) ) )
335 22 subid1d 
 |-  ( j e. ( 0 ... M ) -> ( j - 0 ) = j )
336 143 335 eqtrd 
 |-  ( j e. ( 0 ... M ) -> ( vol ` ( 0 (,) j ) ) = j )
337 336 274 eqbrtrd 
 |-  ( j e. ( 0 ... M ) -> ( vol ` ( 0 (,) j ) ) <_ M )
338 337 adantl 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( vol ` ( 0 (,) j ) ) <_ M )
339 146 125 124 334 338 lemul2ad 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( ( M ^ P ) ^ ( M + 1 ) ) x. ( vol ` ( 0 (,) j ) ) ) <_ ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) )
340 330 339 eqbrtrd 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> S. ( 0 (,) j ) ( ( M ^ P ) ^ ( M + 1 ) ) _d x <_ ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) )
341 150 126 110 155 340 lemul2ad 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. S. ( 0 (,) j ) ( ( M ^ P ) ^ ( M + 1 ) ) _d x ) <_ ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) ) )
342 12 151 127 341 fsumle 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. S. ( 0 (,) j ) ( ( M ^ P ) ^ ( M + 1 ) ) _d x ) <_ sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) ) )
343 135 152 128 328 342 letrd 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( abs ` ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) <_ sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) ) )
344 132 135 128 136 343 letrd 
 |-  ( ph -> ( abs ` sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) <_ sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) ) )
345 132 128 133 344 lediv1dd 
 |-  ( ph -> ( ( abs ` sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) / ( ! ` ( P - 1 ) ) ) <_ ( sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( ( ( M ^ P ) ^ ( M + 1 ) ) x. M ) ) / ( ! ` ( P - 1 ) ) ) )
346 345 123 breqtrd 
 |-  ( ph -> ( ( abs ` sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) / ( ! ` ( P - 1 ) ) ) <_ ( sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) x. ( ( ( M ^ ( M + 1 ) ) ^ ( P - 1 ) ) / ( ! ` ( P - 1 ) ) ) ) )
347 76 130 131 346 7 lelttrd 
 |-  ( ph -> ( ( abs ` sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( F ` x ) ) _d x ) ) / ( ! ` ( P - 1 ) ) ) < 1 )
348 71 347 eqbrtrd 
 |-  ( ph -> ( abs ` K ) < 1 )