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