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