Metamath Proof Explorer

Theorem etransclem47

Description: _e is transcendental. Section *5 of Juillerat p. 11 can be used as a reference for this proof. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem47.q 
|- ( ph -> Q e. ( ( Poly ` ZZ ) \ { 0p } ) )
etransclem47.qe0 
|- ( ph -> ( Q ` _e ) = 0 )
etransclem47.a 
|- A = ( coeff ` Q )
etransclem47.a0 
|- ( ph -> ( A ` 0 ) =/= 0 )
etransclem47.m 
|- M = ( deg ` Q )
etransclem47.p 
|- ( ph -> P e. Prime )
etransclem47.ap 
|- ( ph -> ( abs ` ( A ` 0 ) ) < P )
etransclem47.mp 
|- ( ph -> ( ! ` M ) < P )
etransclem47.9 
|- ( 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 )
etransclem47.f 
|- F = ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
etransclem47.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 )
etransclem47.k 
|- K = ( L / ( ! ` ( P - 1 ) ) )
Assertion etransclem47 
|- ( ph -> E. k e. ZZ ( k =/= 0 /\ ( abs ` k ) < 1 ) )

Proof

Step Hyp Ref Expression
1 etransclem47.q 
 |-  ( ph -> Q e. ( ( Poly ` ZZ ) \ { 0p } ) )
2 etransclem47.qe0 
 |-  ( ph -> ( Q ` _e ) = 0 )
3 etransclem47.a 
 |-  A = ( coeff ` Q )
4 etransclem47.a0 
 |-  ( ph -> ( A ` 0 ) =/= 0 )
5 etransclem47.m 
 |-  M = ( deg ` Q )
6 etransclem47.p 
 |-  ( ph -> P e. Prime )
7 etransclem47.ap 
 |-  ( ph -> ( abs ` ( A ` 0 ) ) < P )
8 etransclem47.mp 
 |-  ( ph -> ( ! ` M ) < P )
9 etransclem47.9 
 |-  ( 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 )
10 etransclem47.f 
 |-  F = ( x e. RR |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
11 etransclem47.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 )
12 etransclem47.k 
 |-  K = ( L / ( ! ` ( P - 1 ) ) )
13 12 a1i 
 |-  ( ph -> K = ( L / ( ! ` ( P - 1 ) ) ) )
14 ssid 
 |-  RR C_ RR
15 14 a1i 
 |-  ( ph -> RR C_ RR )
16 reelprrecn 
 |-  RR e. { RR , CC }
17 16 a1i 
 |-  ( ph -> RR e. { RR , CC } )
18 reopn 
 |-  RR e. ( topGen ` ran (,) )
19 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
20 18 19 eleqtri 
 |-  RR e. ( ( TopOpen ` CCfld ) |`t RR )
21 20 a1i 
 |-  ( ph -> RR e. ( ( TopOpen ` CCfld ) |`t RR ) )
22 prmnn 
 |-  ( P e. Prime -> P e. NN )
23 6 22 syl 
 |-  ( ph -> P e. NN )
24 eqid 
 |-  ( ( M x. P ) + ( P - 1 ) ) = ( ( M x. P ) + ( P - 1 ) )
25 fveq2 
 |-  ( y = x -> ( ( ( RR Dn F ) ` i ) ` y ) = ( ( ( RR Dn F ) ` i ) ` x ) )
26 25 sumeq2sdv 
 |-  ( y = x -> sum_ i e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ( ( ( RR Dn F ) ` i ) ` y ) = sum_ i e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ( ( ( RR Dn F ) ` i ) ` x ) )
27 26 cbvmptv 
 |-  ( y e. RR |-> sum_ i e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ( ( ( RR Dn F ) ` i ) ` y ) ) = ( x e. RR |-> sum_ i e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ( ( ( RR Dn F ) ` i ) ` x ) )
28 negeq 
 |-  ( z = x -> -u z = -u x )
29 28 oveq2d 
 |-  ( z = x -> ( _e ^c -u z ) = ( _e ^c -u x ) )
30 fveq2 
 |-  ( z = x -> ( ( y e. RR |-> sum_ i e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ( ( ( RR Dn F ) ` i ) ` y ) ) ` z ) = ( ( y e. RR |-> sum_ i e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ( ( ( RR Dn F ) ` i ) ` y ) ) ` x ) )
31 29 30 oveq12d 
 |-  ( z = x -> ( ( _e ^c -u z ) x. ( ( y e. RR |-> sum_ i e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ( ( ( RR Dn F ) ` i ) ` y ) ) ` z ) ) = ( ( _e ^c -u x ) x. ( ( y e. RR |-> sum_ i e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ( ( ( RR Dn F ) ` i ) ` y ) ) ` x ) ) )
32 31 negeqd 
 |-  ( z = x -> -u ( ( _e ^c -u z ) x. ( ( y e. RR |-> sum_ i e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ( ( ( RR Dn F ) ` i ) ` y ) ) ` z ) ) = -u ( ( _e ^c -u x ) x. ( ( y e. RR |-> sum_ i e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ( ( ( RR Dn F ) ` i ) ` y ) ) ` x ) ) )
33 32 cbvmptv 
 |-  ( z e. ( 0 [,] j ) |-> -u ( ( _e ^c -u z ) x. ( ( y e. RR |-> sum_ i e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ( ( ( RR Dn F ) ` i ) ` y ) ) ` z ) ) ) = ( x e. ( 0 [,] j ) |-> -u ( ( _e ^c -u x ) x. ( ( y e. RR |-> sum_ i e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ( ( ( RR Dn F ) ` i ) ` y ) ) ` x ) ) )
34 1 2 3 5 15 17 21 23 10 11 24 27 33 etransclem46 
 |-  ( ph -> ( L / ( ! ` ( P - 1 ) ) ) = ( -u sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) )
35 fzfid 
 |-  ( ph -> ( 0 ... M ) e. Fin )
36 fzfid 
 |-  ( ph -> ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) e. Fin )
37 xpfi 
 |-  ( ( ( 0 ... M ) e. Fin /\ ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) e. Fin ) -> ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) e. Fin )
38 35 36 37 syl2anc 
 |-  ( ph -> ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) e. Fin )
39 1 eldifad 
 |-  ( ph -> Q e. ( Poly ` ZZ ) )
40 0zd 
 |-  ( ph -> 0 e. ZZ )
41 3 coef2 
 |-  ( ( Q e. ( Poly ` ZZ ) /\ 0 e. ZZ ) -> A : NN0 --> ZZ )
42 39 40 41 syl2anc 
 |-  ( ph -> A : NN0 --> ZZ )
43 42 adantr 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> A : NN0 --> ZZ )
44 xp1st 
 |-  ( k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) -> ( 1st ` k ) e. ( 0 ... M ) )
45 elfznn0 
 |-  ( ( 1st ` k ) e. ( 0 ... M ) -> ( 1st ` k ) e. NN0 )
46 44 45 syl 
 |-  ( k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) -> ( 1st ` k ) e. NN0 )
47 46 adantl 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( 1st ` k ) e. NN0 )
48 43 47 ffvelcdmd 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( A ` ( 1st ` k ) ) e. ZZ )
49 48 zcnd 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( A ` ( 1st ` k ) ) e. CC )
50 16 a1i 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> RR e. { RR , CC } )
51 20 a1i 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> RR e. ( ( TopOpen ` CCfld ) |`t RR ) )
52 23 adantr 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> P e. NN )
53 dgrcl 
 |-  ( Q e. ( Poly ` ZZ ) -> ( deg ` Q ) e. NN0 )
54 39 53 syl 
 |-  ( ph -> ( deg ` Q ) e. NN0 )
55 5 54 eqeltrid 
 |-  ( ph -> M e. NN0 )
56 55 adantr 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> M e. NN0 )
57 xp2nd 
 |-  ( k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) -> ( 2nd ` k ) e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) )
58 elfznn0 
 |-  ( ( 2nd ` k ) e. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) -> ( 2nd ` k ) e. NN0 )
59 57 58 syl 
 |-  ( k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) -> ( 2nd ` k ) e. NN0 )
60 59 adantl 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( 2nd ` k ) e. NN0 )
61 50 51 52 56 10 60 etransclem33 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( ( RR Dn F ) ` ( 2nd ` k ) ) : RR --> CC )
62 47 nn0red 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( 1st ` k ) e. RR )
63 61 62 ffvelcdmd 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) e. CC )
64 49 63 mulcld 
 |-  ( ( ph /\ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ) -> ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) e. CC )
65 38 64 fsumcl 
 |-  ( ph -> sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) e. CC )
66 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
67 23 66 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
68 67 faccld 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. NN )
69 68 nncnd 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. CC )
70 68 nnne0d 
 |-  ( ph -> ( ! ` ( P - 1 ) ) =/= 0 )
71 65 69 70 divnegd 
 |-  ( ph -> -u ( sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) = ( -u sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) )
72 71 eqcomd 
 |-  ( ph -> ( -u sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) = -u ( sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) )
73 13 34 72 3eqtrd 
 |-  ( ph -> K = -u ( sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) )
74 eqid 
 |-  ( sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) = ( sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) )
75 23 55 10 42 74 etransclem45 
 |-  ( ph -> ( sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) e. ZZ )
76 75 znegcld 
 |-  ( ph -> -u ( sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) e. ZZ )
77 73 76 eqeltrd 
 |-  ( ph -> K e. ZZ )
78 12 34 eqtrid 
 |-  ( ph -> K = ( -u sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) )
79 65 69 70 divcld 
 |-  ( ph -> ( sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) e. CC )
80 42 4 55 6 7 8 10 74 etransclem44 
 |-  ( ph -> ( sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) =/= 0 )
81 79 80 negne0d 
 |-  ( ph -> -u ( sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) =/= 0 )
82 72 81 eqnetrd 
 |-  ( ph -> ( -u sum_ k e. ( ( 0 ... M ) X. ( 0 ... ( ( M x. P ) + ( P - 1 ) ) ) ) ( ( A ` ( 1st ` k ) ) x. ( ( ( RR Dn F ) ` ( 2nd ` k ) ) ` ( 1st ` k ) ) ) / ( ! ` ( P - 1 ) ) ) =/= 0 )
83 78 82 eqnetrd 
 |-  ( ph -> K =/= 0 )
84 eldifsni 
 |-  ( Q e. ( ( Poly ` ZZ ) \ { 0p } ) -> Q =/= 0p )
85 1 84 syl 
 |-  ( ph -> Q =/= 0p )
86 ere 
 |-  _e e. RR
87 86 recni 
 |-  _e e. CC
88 87 a1i 
 |-  ( ph -> _e e. CC )
89 dgrnznn 
 |-  ( ( ( Q e. ( Poly ` ZZ ) /\ Q =/= 0p ) /\ ( _e e. CC /\ ( Q ` _e ) = 0 ) ) -> ( deg ` Q ) e. NN )
90 39 85 88 2 89 syl22anc 
 |-  ( ph -> ( deg ` Q ) e. NN )
91 5 90 eqeltrid 
 |-  ( ph -> M e. NN )
92 42 11 12 23 91 10 9 etransclem23 
 |-  ( ph -> ( abs ` K ) < 1 )
93 neeq1 
 |-  ( k = K -> ( k =/= 0 <-> K =/= 0 ) )
94 fveq2 
 |-  ( k = K -> ( abs ` k ) = ( abs ` K ) )
95 94 breq1d 
 |-  ( k = K -> ( ( abs ` k ) < 1 <-> ( abs ` K ) < 1 ) )
96 93 95 anbi12d 
 |-  ( k = K -> ( ( k =/= 0 /\ ( abs ` k ) < 1 ) <-> ( K =/= 0 /\ ( abs ` K ) < 1 ) ) )
97 96 rspcev 
 |-  ( ( K e. ZZ /\ ( K =/= 0 /\ ( abs ` K ) < 1 ) ) -> E. k e. ZZ ( k =/= 0 /\ ( abs ` k ) < 1 ) )
98 77 83 92 97 syl12anc 
 |-  ( ph -> E. k e. ZZ ( k =/= 0 /\ ( abs ` k ) < 1 ) )