Metamath Proof Explorer

Theorem etransclem48

Description: _e is transcendental. Section *5 of Juillerat p. 11 can be used as a reference for this proof. In this lemma, a large enough prime p is chosen: it will be used by subsequent lemmas. (Contributed by Glauco Siliprandi, 5-Apr-2020) (Revised by AV, 28-Sep-2020)

Ref Expression
Hypotheses etransclem48.q 
|- ( ph -> Q e. ( ( Poly ` ZZ ) \ { 0p } ) )
etransclem48.qe0 
|- ( ph -> ( Q ` _e ) = 0 )
etransclem48.a 
|- A = ( coeff ` Q )
etransclem48.a0 
|- ( ph -> ( A ` 0 ) =/= 0 )
etransclem48.m 
|- M = ( deg ` Q )
etransclem48.c 
|- C = sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) )
etransclem48.s 
|- S = ( n e. NN0 |-> ( C x. ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) )
etransclem48.i 
|- I = inf ( { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 } , RR , < )
etransclem48.t 
|- T = sup ( { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } , RR* , < )
Assertion etransclem48 
|- ( ph -> E. k e. ZZ ( k =/= 0 /\ ( abs ` k ) < 1 ) )

Proof

Step Hyp Ref Expression
1 etransclem48.q 
 |-  ( ph -> Q e. ( ( Poly ` ZZ ) \ { 0p } ) )
2 etransclem48.qe0 
 |-  ( ph -> ( Q ` _e ) = 0 )
3 etransclem48.a 
 |-  A = ( coeff ` Q )
4 etransclem48.a0 
 |-  ( ph -> ( A ` 0 ) =/= 0 )
5 etransclem48.m 
 |-  M = ( deg ` Q )
6 etransclem48.c 
 |-  C = sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) )
7 etransclem48.s 
 |-  S = ( n e. NN0 |-> ( C x. ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) )
8 etransclem48.i 
 |-  I = inf ( { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 } , RR , < )
9 etransclem48.t 
 |-  T = sup ( { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } , RR* , < )
10 1 eldifad 
 |-  ( ph -> Q e. ( Poly ` ZZ ) )
11 0zd 
 |-  ( ph -> 0 e. ZZ )
12 3 coef2 
 |-  ( ( Q e. ( Poly ` ZZ ) /\ 0 e. ZZ ) -> A : NN0 --> ZZ )
13 10 11 12 syl2anc 
 |-  ( ph -> A : NN0 --> ZZ )
14 0nn0 
 |-  0 e. NN0
15 14 a1i 
 |-  ( ph -> 0 e. NN0 )
16 13 15 ffvelrnd 
 |-  ( ph -> ( A ` 0 ) e. ZZ )
17 zabscl 
 |-  ( ( A ` 0 ) e. ZZ -> ( abs ` ( A ` 0 ) ) e. ZZ )
18 16 17 syl 
 |-  ( ph -> ( abs ` ( A ` 0 ) ) e. ZZ )
19 dgrcl 
 |-  ( Q e. ( Poly ` ZZ ) -> ( deg ` Q ) e. NN0 )
20 10 19 syl 
 |-  ( ph -> ( deg ` Q ) e. NN0 )
21 5 20 eqeltrid 
 |-  ( ph -> M e. NN0 )
22 21 faccld 
 |-  ( ph -> ( ! ` M ) e. NN )
23 22 nnzd 
 |-  ( ph -> ( ! ` M ) e. ZZ )
24 ssrab2 
 |-  { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 } C_ NN0
25 nn0ssz 
 |-  NN0 C_ ZZ
26 24 25 sstri 
 |-  { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 } C_ ZZ
27 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
28 24 27 sseqtri 
 |-  { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 } C_ ( ZZ>= ` 0 )
29 1rp 
 |-  1 e. RR+
30 nfv 
 |-  F/ n ph
31 nfmpt1 
 |-  F/_ n ( n e. NN0 |-> C )
32 nfmpt1 
 |-  F/_ n ( n e. NN0 |-> ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) )
33 nfmpt1 
 |-  F/_ n ( n e. NN0 |-> ( C x. ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) )
34 7 33 nfcxfr 
 |-  F/_ n S
35 nn0ex 
 |-  NN0 e. _V
36 35 mptex 
 |-  ( n e. NN0 |-> C ) e. _V
37 36 a1i 
 |-  ( ph -> ( n e. NN0 |-> C ) e. _V )
38 fzfid 
 |-  ( ph -> ( 0 ... M ) e. Fin )
39 13 adantr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> A : NN0 --> ZZ )
40 elfznn0 
 |-  ( j e. ( 0 ... M ) -> j e. NN0 )
41 40 adantl 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> j e. NN0 )
42 39 41 ffvelrnd 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( A ` j ) e. ZZ )
43 42 zcnd 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( A ` j ) e. CC )
44 ere 
 |-  _e e. RR
45 44 recni 
 |-  _e e. CC
46 45 a1i 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> _e e. CC )
47 elfzelz 
 |-  ( j e. ( 0 ... M ) -> j e. ZZ )
48 47 zcnd 
 |-  ( j e. ( 0 ... M ) -> j e. CC )
49 48 adantl 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> j e. CC )
50 46 49 cxpcld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( _e ^c j ) e. CC )
51 43 50 mulcld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( A ` j ) x. ( _e ^c j ) ) e. CC )
52 51 abscld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) e. RR )
53 52 recnd 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) e. CC )
54 21 nn0cnd 
 |-  ( ph -> M e. CC )
55 peano2nn0 
 |-  ( M e. NN0 -> ( M + 1 ) e. NN0 )
56 21 55 syl 
 |-  ( ph -> ( M + 1 ) e. NN0 )
57 54 56 expcld 
 |-  ( ph -> ( M ^ ( M + 1 ) ) e. CC )
58 54 57 mulcld 
 |-  ( ph -> ( M x. ( M ^ ( M + 1 ) ) ) e. CC )
59 58 adantr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( M x. ( M ^ ( M + 1 ) ) ) e. CC )
60 53 59 mulcld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) e. CC )
61 38 60 fsumcl 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) e. CC )
62 6 61 eqeltrid 
 |-  ( ph -> C e. CC )
63 eqidd 
 |-  ( ( ph /\ i e. NN0 ) -> ( n e. NN0 |-> C ) = ( n e. NN0 |-> C ) )
64 eqidd 
 |-  ( ( ( ph /\ i e. NN0 ) /\ n = i ) -> C = C )
65 simpr 
 |-  ( ( ph /\ i e. NN0 ) -> i e. NN0 )
66 62 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> C e. CC )
67 63 64 65 66 fvmptd 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( n e. NN0 |-> C ) ` i ) = C )
68 27 11 37 62 67 climconst 
 |-  ( ph -> ( n e. NN0 |-> C ) ~~> C )
69 35 mptex 
 |-  ( n e. NN0 |-> ( C x. ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) ) e. _V
70 7 69 eqeltri 
 |-  S e. _V
71 70 a1i 
 |-  ( ph -> S e. _V )
72 eqid 
 |-  ( n e. NN0 |-> ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) )
73 72 expfac 
 |-  ( ( M ^ ( M + 1 ) ) e. CC -> ( n e. NN0 |-> ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) ~~> 0 )
74 57 73 syl 
 |-  ( ph -> ( n e. NN0 |-> ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) ~~> 0 )
75 simpr 
 |-  ( ( ph /\ n e. NN0 ) -> n e. NN0 )
76 62 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> C e. CC )
77 eqid 
 |-  ( n e. NN0 |-> C ) = ( n e. NN0 |-> C )
78 77 fvmpt2 
 |-  ( ( n e. NN0 /\ C e. CC ) -> ( ( n e. NN0 |-> C ) ` n ) = C )
79 75 76 78 syl2anc 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( n e. NN0 |-> C ) ` n ) = C )
80 79 76 eqeltrd 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( n e. NN0 |-> C ) ` n ) e. CC )
81 ovex 
 |-  ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) e. _V
82 72 fvmpt2 
 |-  ( ( n e. NN0 /\ ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) e. _V ) -> ( ( n e. NN0 |-> ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) ` n ) = ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) )
83 81 82 mpan2 
 |-  ( n e. NN0 -> ( ( n e. NN0 |-> ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) ` n ) = ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) )
84 83 adantl 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( n e. NN0 |-> ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) ` n ) = ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) )
85 57 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> ( M ^ ( M + 1 ) ) e. CC )
86 85 75 expcld 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( M ^ ( M + 1 ) ) ^ n ) e. CC )
87 75 faccld 
 |-  ( ( ph /\ n e. NN0 ) -> ( ! ` n ) e. NN )
88 87 nncnd 
 |-  ( ( ph /\ n e. NN0 ) -> ( ! ` n ) e. CC )
89 87 nnne0d 
 |-  ( ( ph /\ n e. NN0 ) -> ( ! ` n ) =/= 0 )
90 86 88 89 divcld 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) e. CC )
91 84 90 eqeltrd 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( n e. NN0 |-> ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) ` n ) e. CC )
92 ovex 
 |-  ( C x. ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) e. _V
93 7 fvmpt2 
 |-  ( ( n e. NN0 /\ ( C x. ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) e. _V ) -> ( S ` n ) = ( C x. ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) )
94 92 93 mpan2 
 |-  ( n e. NN0 -> ( S ` n ) = ( C x. ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) )
95 94 adantl 
 |-  ( ( ph /\ n e. NN0 ) -> ( S ` n ) = ( C x. ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) )
96 79 84 oveq12d 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( ( n e. NN0 |-> C ) ` n ) x. ( ( n e. NN0 |-> ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) ` n ) ) = ( C x. ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) )
97 95 96 eqtr4d 
 |-  ( ( ph /\ n e. NN0 ) -> ( S ` n ) = ( ( ( n e. NN0 |-> C ) ` n ) x. ( ( n e. NN0 |-> ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) ` n ) ) )
98 30 31 32 34 27 11 68 71 74 80 91 97 climmulf 
 |-  ( ph -> S ~~> ( C x. 0 ) )
99 62 mul01d 
 |-  ( ph -> ( C x. 0 ) = 0 )
100 98 99 breqtrd 
 |-  ( ph -> S ~~> 0 )
101 eqidd 
 |-  ( ( ph /\ n e. NN0 ) -> ( S ` n ) = ( S ` n ) )
102 80 91 mulcld 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( ( n e. NN0 |-> C ) ` n ) x. ( ( n e. NN0 |-> ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) ` n ) ) e. CC )
103 97 102 eqeltrd 
 |-  ( ( ph /\ n e. NN0 ) -> ( S ` n ) e. CC )
104 34 27 11 71 101 103 clim0cf 
 |-  ( ph -> ( S ~~> 0 <-> A. e e. RR+ E. i e. NN0 A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < e ) )
105 100 104 mpbid 
 |-  ( ph -> A. e e. RR+ E. i e. NN0 A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < e )
106 breq2 
 |-  ( e = 1 -> ( ( abs ` ( S ` n ) ) < e <-> ( abs ` ( S ` n ) ) < 1 ) )
107 106 rexralbidv 
 |-  ( e = 1 -> ( E. i e. NN0 A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < e <-> E. i e. NN0 A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 ) )
108 107 rspcva 
 |-  ( ( 1 e. RR+ /\ A. e e. RR+ E. i e. NN0 A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < e ) -> E. i e. NN0 A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 )
109 29 105 108 sylancr 
 |-  ( ph -> E. i e. NN0 A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 )
110 rabn0 
 |-  ( { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 } =/= (/) <-> E. i e. NN0 A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 )
111 109 110 sylibr 
 |-  ( ph -> { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 } =/= (/) )
112 infssuzcl 
 |-  ( ( { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 } C_ ( ZZ>= ` 0 ) /\ { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 } =/= (/) ) -> inf ( { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 } , RR , < ) e. { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 } )
113 28 111 112 sylancr 
 |-  ( ph -> inf ( { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 } , RR , < ) e. { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 } )
114 8 113 eqeltrid 
 |-  ( ph -> I e. { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 } )
115 26 114 sselid 
 |-  ( ph -> I e. ZZ )
116 tpssi 
 |-  ( ( ( abs ` ( A ` 0 ) ) e. ZZ /\ ( ! ` M ) e. ZZ /\ I e. ZZ ) -> { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } C_ ZZ )
117 18 23 115 116 syl3anc 
 |-  ( ph -> { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } C_ ZZ )
118 xrltso 
 |-  < Or RR*
119 118 a1i 
 |-  ( ph -> < Or RR* )
120 tpfi 
 |-  { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } e. Fin
121 120 a1i 
 |-  ( ph -> { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } e. Fin )
122 18 tpnzd 
 |-  ( ph -> { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } =/= (/) )
123 zssre 
 |-  ZZ C_ RR
124 ressxr 
 |-  RR C_ RR*
125 123 124 sstri 
 |-  ZZ C_ RR*
126 117 125 sstrdi 
 |-  ( ph -> { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } C_ RR* )
127 fisupcl 
 |-  ( ( < Or RR* /\ ( { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } e. Fin /\ { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } =/= (/) /\ { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } C_ RR* ) ) -> sup ( { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } , RR* , < ) e. { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } )
128 119 121 122 126 127 syl13anc 
 |-  ( ph -> sup ( { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } , RR* , < ) e. { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } )
129 9 128 eqeltrid 
 |-  ( ph -> T e. { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } )
130 117 129 sseldd 
 |-  ( ph -> T e. ZZ )
131 0red 
 |-  ( ph -> 0 e. RR )
132 22 nnred 
 |-  ( ph -> ( ! ` M ) e. RR )
133 130 zred 
 |-  ( ph -> T e. RR )
134 22 nngt0d 
 |-  ( ph -> 0 < ( ! ` M ) )
135 fvex 
 |-  ( ! ` M ) e. _V
136 135 tpid2 
 |-  ( ! ` M ) e. { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I }
137 supxrub 
 |-  ( ( { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } C_ RR* /\ ( ! ` M ) e. { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } ) -> ( ! ` M ) <_ sup ( { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } , RR* , < ) )
138 126 136 137 sylancl 
 |-  ( ph -> ( ! ` M ) <_ sup ( { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } , RR* , < ) )
139 138 9 breqtrrdi 
 |-  ( ph -> ( ! ` M ) <_ T )
140 131 132 133 134 139 ltletrd 
 |-  ( ph -> 0 < T )
141 elnnz 
 |-  ( T e. NN <-> ( T e. ZZ /\ 0 < T ) )
142 130 140 141 sylanbrc 
 |-  ( ph -> T e. NN )
143 prmunb 
 |-  ( T e. NN -> E. p e. Prime T < p )
144 142 143 syl 
 |-  ( ph -> E. p e. Prime T < p )
145 1 3ad2ant1 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> Q e. ( ( Poly ` ZZ ) \ { 0p } ) )
146 2 3ad2ant1 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( Q ` _e ) = 0 )
147 4 3ad2ant1 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( A ` 0 ) =/= 0 )
148 simp2 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> p e. Prime )
149 16 zcnd 
 |-  ( ph -> ( A ` 0 ) e. CC )
150 149 3ad2ant1 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( A ` 0 ) e. CC )
151 150 abscld 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( abs ` ( A ` 0 ) ) e. RR )
152 133 3ad2ant1 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> T e. RR )
153 prmz 
 |-  ( p e. Prime -> p e. ZZ )
154 153 zred 
 |-  ( p e. Prime -> p e. RR )
155 154 3ad2ant2 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> p e. RR )
156 126 adantr 
 |-  ( ( ph /\ p e. Prime ) -> { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } C_ RR* )
157 fvex 
 |-  ( abs ` ( A ` 0 ) ) e. _V
158 157 tpid1 
 |-  ( abs ` ( A ` 0 ) ) e. { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I }
159 supxrub 
 |-  ( ( { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } C_ RR* /\ ( abs ` ( A ` 0 ) ) e. { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } ) -> ( abs ` ( A ` 0 ) ) <_ sup ( { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } , RR* , < ) )
160 156 158 159 sylancl 
 |-  ( ( ph /\ p e. Prime ) -> ( abs ` ( A ` 0 ) ) <_ sup ( { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } , RR* , < ) )
161 160 9 breqtrrdi 
 |-  ( ( ph /\ p e. Prime ) -> ( abs ` ( A ` 0 ) ) <_ T )
162 161 3adant3 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( abs ` ( A ` 0 ) ) <_ T )
163 simp3 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> T < p )
164 151 152 155 162 163 lelttrd 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( abs ` ( A ` 0 ) ) < p )
165 132 3ad2ant1 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( ! ` M ) e. RR )
166 139 3ad2ant1 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( ! ` M ) <_ T )
167 165 152 155 166 163 lelttrd 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( ! ` M ) < p )
168 6 a1i 
 |-  ( n = ( p - 1 ) -> C = sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) )
169 oveq2 
 |-  ( n = ( p - 1 ) -> ( ( M ^ ( M + 1 ) ) ^ n ) = ( ( M ^ ( M + 1 ) ) ^ ( p - 1 ) ) )
170 fveq2 
 |-  ( n = ( p - 1 ) -> ( ! ` n ) = ( ! ` ( p - 1 ) ) )
171 169 170 oveq12d 
 |-  ( n = ( p - 1 ) -> ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) = ( ( ( M ^ ( M + 1 ) ) ^ ( p - 1 ) ) / ( ! ` ( p - 1 ) ) ) )
172 168 171 oveq12d 
 |-  ( n = ( p - 1 ) -> ( C x. ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) = ( 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 ) ) ) ) )
173 prmnn 
 |-  ( p e. Prime -> p e. NN )
174 nnm1nn0 
 |-  ( p e. NN -> ( p - 1 ) e. NN0 )
175 173 174 syl 
 |-  ( p e. Prime -> ( p - 1 ) e. NN0 )
176 175 adantl 
 |-  ( ( ph /\ p e. Prime ) -> ( p - 1 ) e. NN0 )
177 61 adantr 
 |-  ( ( ph /\ p e. Prime ) -> sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) e. CC )
178 57 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( M ^ ( M + 1 ) ) e. CC )
179 178 176 expcld 
 |-  ( ( ph /\ p e. Prime ) -> ( ( M ^ ( M + 1 ) ) ^ ( p - 1 ) ) e. CC )
180 175 faccld 
 |-  ( p e. Prime -> ( ! ` ( p - 1 ) ) e. NN )
181 180 nncnd 
 |-  ( p e. Prime -> ( ! ` ( p - 1 ) ) e. CC )
182 181 adantl 
 |-  ( ( ph /\ p e. Prime ) -> ( ! ` ( p - 1 ) ) e. CC )
183 180 nnne0d 
 |-  ( p e. Prime -> ( ! ` ( p - 1 ) ) =/= 0 )
184 183 adantl 
 |-  ( ( ph /\ p e. Prime ) -> ( ! ` ( p - 1 ) ) =/= 0 )
185 179 182 184 divcld 
 |-  ( ( ph /\ p e. Prime ) -> ( ( ( M ^ ( M + 1 ) ) ^ ( p - 1 ) ) / ( ! ` ( p - 1 ) ) ) e. CC )
186 177 185 mulcld 
 |-  ( ( ph /\ p e. Prime ) -> ( 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. CC )
187 7 172 176 186 fvmptd3 
 |-  ( ( ph /\ p e. Prime ) -> ( S ` ( 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 ) ) ) ) )
188 187 eqcomd 
 |-  ( ( ph /\ p e. Prime ) -> ( 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 ) ) ) ) = ( S ` ( p - 1 ) ) )
189 188 3adant3 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( 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 ) ) ) ) = ( S ` ( p - 1 ) ) )
190 115 3ad2ant1 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> I e. ZZ )
191 1zzd 
 |-  ( p e. Prime -> 1 e. ZZ )
192 153 191 zsubcld 
 |-  ( p e. Prime -> ( p - 1 ) e. ZZ )
193 192 3ad2ant2 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( p - 1 ) e. ZZ )
194 190 zred 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> I e. RR )
195 tpid3g 
 |-  ( I e. ZZ -> I e. { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } )
196 115 195 syl 
 |-  ( ph -> I e. { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } )
197 supxrub 
 |-  ( ( { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } C_ RR* /\ I e. { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } ) -> I <_ sup ( { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } , RR* , < ) )
198 126 196 197 syl2anc 
 |-  ( ph -> I <_ sup ( { ( abs ` ( A ` 0 ) ) , ( ! ` M ) , I } , RR* , < ) )
199 198 9 breqtrrdi 
 |-  ( ph -> I <_ T )
200 199 3ad2ant1 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> I <_ T )
201 194 152 155 200 163 lelttrd 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> I < p )
202 153 3ad2ant2 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> p e. ZZ )
203 zltlem1 
 |-  ( ( I e. ZZ /\ p e. ZZ ) -> ( I < p <-> I <_ ( p - 1 ) ) )
204 190 202 203 syl2anc 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( I < p <-> I <_ ( p - 1 ) ) )
205 201 204 mpbid 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> I <_ ( p - 1 ) )
206 eluz2 
 |-  ( ( p - 1 ) e. ( ZZ>= ` I ) <-> ( I e. ZZ /\ ( p - 1 ) e. ZZ /\ I <_ ( p - 1 ) ) )
207 190 193 205 206 syl3anbrc 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( p - 1 ) e. ( ZZ>= ` I ) )
208 114 3ad2ant1 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> I e. { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 } )
209 fveq2 
 |-  ( i = I -> ( ZZ>= ` i ) = ( ZZ>= ` I ) )
210 209 raleqdv 
 |-  ( i = I -> ( A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 <-> A. n e. ( ZZ>= ` I ) ( abs ` ( S ` n ) ) < 1 ) )
211 210 elrab 
 |-  ( I e. { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( S ` n ) ) < 1 } <-> ( I e. NN0 /\ A. n e. ( ZZ>= ` I ) ( abs ` ( S ` n ) ) < 1 ) )
212 208 211 sylib 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( I e. NN0 /\ A. n e. ( ZZ>= ` I ) ( abs ` ( S ` n ) ) < 1 ) )
213 212 simprd 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> A. n e. ( ZZ>= ` I ) ( abs ` ( S ` n ) ) < 1 )
214 nfcv 
 |-  F/_ n abs
215 nfcv 
 |-  F/_ n ( p - 1 )
216 34 215 nffv 
 |-  F/_ n ( S ` ( p - 1 ) )
217 214 216 nffv 
 |-  F/_ n ( abs ` ( S ` ( p - 1 ) ) )
218 nfcv 
 |-  F/_ n <
219 nfcv 
 |-  F/_ n 1
220 217 218 219 nfbr 
 |-  F/ n ( abs ` ( S ` ( p - 1 ) ) ) < 1
221 2fveq3 
 |-  ( n = ( p - 1 ) -> ( abs ` ( S ` n ) ) = ( abs ` ( S ` ( p - 1 ) ) ) )
222 221 breq1d 
 |-  ( n = ( p - 1 ) -> ( ( abs ` ( S ` n ) ) < 1 <-> ( abs ` ( S ` ( p - 1 ) ) ) < 1 ) )
223 220 222 rspc 
 |-  ( ( p - 1 ) e. ( ZZ>= ` I ) -> ( A. n e. ( ZZ>= ` I ) ( abs ` ( S ` n ) ) < 1 -> ( abs ` ( S ` ( p - 1 ) ) ) < 1 ) )
224 207 213 223 sylc 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( abs ` ( S ` ( p - 1 ) ) ) < 1 )
225 171 oveq2d 
 |-  ( n = ( p - 1 ) -> ( C x. ( ( ( M ^ ( M + 1 ) ) ^ n ) / ( ! ` n ) ) ) = ( C x. ( ( ( M ^ ( M + 1 ) ) ^ ( p - 1 ) ) / ( ! ` ( p - 1 ) ) ) ) )
226 ovexd 
 |-  ( ( ph /\ p e. Prime ) -> ( C x. ( ( ( M ^ ( M + 1 ) ) ^ ( p - 1 ) ) / ( ! ` ( p - 1 ) ) ) ) e. _V )
227 7 225 176 226 fvmptd3 
 |-  ( ( ph /\ p e. Prime ) -> ( S ` ( p - 1 ) ) = ( C x. ( ( ( M ^ ( M + 1 ) ) ^ ( p - 1 ) ) / ( ! ` ( p - 1 ) ) ) ) )
228 21 nn0red 
 |-  ( ph -> M e. RR )
229 228 56 reexpcld 
 |-  ( ph -> ( M ^ ( M + 1 ) ) e. RR )
230 228 229 remulcld 
 |-  ( ph -> ( M x. ( M ^ ( M + 1 ) ) ) e. RR )
231 230 adantr 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( M x. ( M ^ ( M + 1 ) ) ) e. RR )
232 52 231 remulcld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) e. RR )
233 38 232 fsumrecl 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( ( abs ` ( ( A ` j ) x. ( _e ^c j ) ) ) x. ( M x. ( M ^ ( M + 1 ) ) ) ) e. RR )
234 6 233 eqeltrid 
 |-  ( ph -> C e. RR )
235 234 adantr 
 |-  ( ( ph /\ p e. Prime ) -> C e. RR )
236 229 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( M ^ ( M + 1 ) ) e. RR )
237 236 176 reexpcld 
 |-  ( ( ph /\ p e. Prime ) -> ( ( M ^ ( M + 1 ) ) ^ ( p - 1 ) ) e. RR )
238 180 nnred 
 |-  ( p e. Prime -> ( ! ` ( p - 1 ) ) e. RR )
239 238 adantl 
 |-  ( ( ph /\ p e. Prime ) -> ( ! ` ( p - 1 ) ) e. RR )
240 237 239 184 redivcld 
 |-  ( ( ph /\ p e. Prime ) -> ( ( ( M ^ ( M + 1 ) ) ^ ( p - 1 ) ) / ( ! ` ( p - 1 ) ) ) e. RR )
241 235 240 remulcld 
 |-  ( ( ph /\ p e. Prime ) -> ( C x. ( ( ( M ^ ( M + 1 ) ) ^ ( p - 1 ) ) / ( ! ` ( p - 1 ) ) ) ) e. RR )
242 227 241 eqeltrd 
 |-  ( ( ph /\ p e. Prime ) -> ( S ` ( p - 1 ) ) e. RR )
243 242 3adant3 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( S ` ( p - 1 ) ) e. RR )
244 1red 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> 1 e. RR )
245 243 244 absltd 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( ( abs ` ( S ` ( p - 1 ) ) ) < 1 <-> ( -u 1 < ( S ` ( p - 1 ) ) /\ ( S ` ( p - 1 ) ) < 1 ) ) )
246 224 245 mpbid 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( -u 1 < ( S ` ( p - 1 ) ) /\ ( S ` ( p - 1 ) ) < 1 ) )
247 246 simprd 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( S ` ( p - 1 ) ) < 1 )
248 189 247 eqbrtrd 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> ( 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 )
249 etransclem6 
 |-  ( y e. RR |-> ( ( y ^ ( p - 1 ) ) x. prod_ z e. ( 1 ... M ) ( ( y - z ) ^ p ) ) ) = ( x e. RR |-> ( ( x ^ ( p - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ p ) ) )
250 eqid 
 |-  sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( ( y e. RR |-> ( ( y ^ ( p - 1 ) ) x. prod_ z e. ( 1 ... M ) ( ( y - z ) ^ p ) ) ) ` x ) ) _d x ) = sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( ( y e. RR |-> ( ( y ^ ( p - 1 ) ) x. prod_ z e. ( 1 ... M ) ( ( y - z ) ^ p ) ) ) ` x ) ) _d x )
251 eqid 
 |-  ( sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( ( y e. RR |-> ( ( y ^ ( p - 1 ) ) x. prod_ z e. ( 1 ... M ) ( ( y - z ) ^ p ) ) ) ` x ) ) _d x ) / ( ! ` ( p - 1 ) ) ) = ( sum_ j e. ( 0 ... M ) ( ( ( A ` j ) x. ( _e ^c j ) ) x. S. ( 0 (,) j ) ( ( _e ^c -u x ) x. ( ( y e. RR |-> ( ( y ^ ( p - 1 ) ) x. prod_ z e. ( 1 ... M ) ( ( y - z ) ^ p ) ) ) ` x ) ) _d x ) / ( ! ` ( p - 1 ) ) )
252 145 146 3 147 5 148 164 167 248 249 250 251 etransclem47 
 |-  ( ( ph /\ p e. Prime /\ T < p ) -> E. k e. ZZ ( k =/= 0 /\ ( abs ` k ) < 1 ) )
253 252 rexlimdv3a 
 |-  ( ph -> ( E. p e. Prime T < p -> E. k e. ZZ ( k =/= 0 /\ ( abs ` k ) < 1 ) ) )
254 144 253 mpd 
 |-  ( ph -> E. k e. ZZ ( k =/= 0 /\ ( abs ` k ) < 1 ) )