Metamath Proof Explorer

Theorem etransc

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) (Proof shortened by AV, 28-Sep-2020)

Ref Expression
Assertion etransc 
|- _e e. ( CC \ AA )

Proof

Step Hyp Ref Expression
1 1red 
 |-  ( ( k e. ZZ /\ k =/= 0 ) -> 1 e. RR )
2 nn0abscl 
 |-  ( k e. ZZ -> ( abs ` k ) e. NN0 )
3 2 nn0red 
 |-  ( k e. ZZ -> ( abs ` k ) e. RR )
4 3 adantr 
 |-  ( ( k e. ZZ /\ k =/= 0 ) -> ( abs ` k ) e. RR )
5 nnabscl 
 |-  ( ( k e. ZZ /\ k =/= 0 ) -> ( abs ` k ) e. NN )
6 5 nnge1d 
 |-  ( ( k e. ZZ /\ k =/= 0 ) -> 1 <_ ( abs ` k ) )
7 1 4 6 lensymd 
 |-  ( ( k e. ZZ /\ k =/= 0 ) -> -. ( abs ` k ) < 1 )
8 nan 
 |-  ( ( k e. ZZ -> -. ( k =/= 0 /\ ( abs ` k ) < 1 ) ) <-> ( ( k e. ZZ /\ k =/= 0 ) -> -. ( abs ` k ) < 1 ) )
9 7 8 mpbir 
 |-  ( k e. ZZ -> -. ( k =/= 0 /\ ( abs ` k ) < 1 ) )
10 9 nrex 
 |-  -. E. k e. ZZ ( k =/= 0 /\ ( abs ` k ) < 1 )
11 ere 
 |-  _e e. RR
12 11 recni 
 |-  _e e. CC
13 neldif 
 |-  ( ( _e e. CC /\ -. _e e. ( CC \ AA ) ) -> _e e. AA )
14 12 13 mpan 
 |-  ( -. _e e. ( CC \ AA ) -> _e e. AA )
15 ene0 
 |-  _e =/= 0
16 elsng 
 |-  ( _e e. CC -> ( _e e. { 0 } <-> _e = 0 ) )
17 12 16 ax-mp 
 |-  ( _e e. { 0 } <-> _e = 0 )
18 15 17 nemtbir 
 |-  -. _e e. { 0 }
19 18 a1i 
 |-  ( -. _e e. ( CC \ AA ) -> -. _e e. { 0 } )
20 14 19 eldifd 
 |-  ( -. _e e. ( CC \ AA ) -> _e e. ( AA \ { 0 } ) )
21 elaa2 
 |-  ( _e e. ( AA \ { 0 } ) <-> ( _e e. CC /\ E. q e. ( Poly ` ZZ ) ( ( ( coeff ` q ) ` 0 ) =/= 0 /\ ( q ` _e ) = 0 ) ) )
22 20 21 sylib 
 |-  ( -. _e e. ( CC \ AA ) -> ( _e e. CC /\ E. q e. ( Poly ` ZZ ) ( ( ( coeff ` q ) ` 0 ) =/= 0 /\ ( q ` _e ) = 0 ) ) )
23 22 simprd 
 |-  ( -. _e e. ( CC \ AA ) -> E. q e. ( Poly ` ZZ ) ( ( ( coeff ` q ) ` 0 ) =/= 0 /\ ( q ` _e ) = 0 ) )
24 simpl 
 |-  ( ( q e. ( Poly ` ZZ ) /\ ( ( coeff ` q ) ` 0 ) =/= 0 ) -> q e. ( Poly ` ZZ ) )
25 0nn0 
 |-  0 e. NN0
26 n0p 
 |-  ( ( q e. ( Poly ` ZZ ) /\ 0 e. NN0 /\ ( ( coeff ` q ) ` 0 ) =/= 0 ) -> q =/= 0p )
27 25 26 mp3an2 
 |-  ( ( q e. ( Poly ` ZZ ) /\ ( ( coeff ` q ) ` 0 ) =/= 0 ) -> q =/= 0p )
28 nelsn 
 |-  ( q =/= 0p -> -. q e. { 0p } )
29 27 28 syl 
 |-  ( ( q e. ( Poly ` ZZ ) /\ ( ( coeff ` q ) ` 0 ) =/= 0 ) -> -. q e. { 0p } )
30 24 29 eldifd 
 |-  ( ( q e. ( Poly ` ZZ ) /\ ( ( coeff ` q ) ` 0 ) =/= 0 ) -> q e. ( ( Poly ` ZZ ) \ { 0p } ) )
31 30 adantrr 
 |-  ( ( q e. ( Poly ` ZZ ) /\ ( ( ( coeff ` q ) ` 0 ) =/= 0 /\ ( q ` _e ) = 0 ) ) -> q e. ( ( Poly ` ZZ ) \ { 0p } ) )
32 simprr 
 |-  ( ( q e. ( Poly ` ZZ ) /\ ( ( ( coeff ` q ) ` 0 ) =/= 0 /\ ( q ` _e ) = 0 ) ) -> ( q ` _e ) = 0 )
33 eqid 
 |-  ( coeff ` q ) = ( coeff ` q )
34 simprl 
 |-  ( ( q e. ( Poly ` ZZ ) /\ ( ( ( coeff ` q ) ` 0 ) =/= 0 /\ ( q ` _e ) = 0 ) ) -> ( ( coeff ` q ) ` 0 ) =/= 0 )
35 eqid 
 |-  ( deg ` q ) = ( deg ` q )
36 eqid 
 |-  sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) = sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) )
37 eqid 
 |-  ( n e. NN0 |-> ( sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ n ) / ( ! ` n ) ) ) ) = ( n e. NN0 |-> ( sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ n ) / ( ! ` n ) ) ) )
38 fveq2 
 |-  ( h = l -> ( ( coeff ` q ) ` h ) = ( ( coeff ` q ) ` l ) )
39 oveq2 
 |-  ( h = l -> ( _e ^c h ) = ( _e ^c l ) )
40 38 39 oveq12d 
 |-  ( h = l -> ( ( ( coeff ` q ) ` h ) x. ( _e ^c h ) ) = ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) )
41 40 fveq2d 
 |-  ( h = l -> ( abs ` ( ( ( coeff ` q ) ` h ) x. ( _e ^c h ) ) ) = ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) )
42 41 oveq1d 
 |-  ( h = l -> ( ( abs ` ( ( ( coeff ` q ) ` h ) x. ( _e ^c h ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) = ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) )
43 42 cbvsumv 
 |-  sum_ h e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` h ) x. ( _e ^c h ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) = sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) )
44 43 a1i 
 |-  ( m = n -> sum_ h e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` h ) x. ( _e ^c h ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) = sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) )
45 oveq2 
 |-  ( m = n -> ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ m ) = ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ n ) )
46 fveq2 
 |-  ( m = n -> ( ! ` m ) = ( ! ` n ) )
47 45 46 oveq12d 
 |-  ( m = n -> ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ m ) / ( ! ` m ) ) = ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ n ) / ( ! ` n ) ) )
48 44 47 oveq12d 
 |-  ( m = n -> ( sum_ h e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` h ) x. ( _e ^c h ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ m ) / ( ! ` m ) ) ) = ( sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ n ) / ( ! ` n ) ) ) )
49 48 cbvmptv 
 |-  ( m e. NN0 |-> ( sum_ h e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` h ) x. ( _e ^c h ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ m ) / ( ! ` m ) ) ) ) = ( n e. NN0 |-> ( sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ n ) / ( ! ` n ) ) ) )
50 49 a1i 
 |-  ( m = n -> ( m e. NN0 |-> ( sum_ h e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` h ) x. ( _e ^c h ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ m ) / ( ! ` m ) ) ) ) = ( n e. NN0 |-> ( sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ n ) / ( ! ` n ) ) ) ) )
51 id 
 |-  ( m = n -> m = n )
52 50 51 fveq12d 
 |-  ( m = n -> ( ( m e. NN0 |-> ( sum_ h e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` h ) x. ( _e ^c h ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ m ) / ( ! ` m ) ) ) ) ` m ) = ( ( n e. NN0 |-> ( sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ n ) / ( ! ` n ) ) ) ) ` n ) )
53 52 fveq2d 
 |-  ( m = n -> ( abs ` ( ( m e. NN0 |-> ( sum_ h e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` h ) x. ( _e ^c h ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ m ) / ( ! ` m ) ) ) ) ` m ) ) = ( abs ` ( ( n e. NN0 |-> ( sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ n ) / ( ! ` n ) ) ) ) ` n ) ) )
54 53 breq1d 
 |-  ( m = n -> ( ( abs ` ( ( m e. NN0 |-> ( sum_ h e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` h ) x. ( _e ^c h ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ m ) / ( ! ` m ) ) ) ) ` m ) ) < 1 <-> ( abs ` ( ( n e. NN0 |-> ( sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ n ) / ( ! ` n ) ) ) ) ` n ) ) < 1 ) )
55 54 cbvralvw 
 |-  ( A. m e. ( ZZ>= ` j ) ( abs ` ( ( m e. NN0 |-> ( sum_ h e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` h ) x. ( _e ^c h ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ m ) / ( ! ` m ) ) ) ) ` m ) ) < 1 <-> A. n e. ( ZZ>= ` j ) ( abs ` ( ( n e. NN0 |-> ( sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ n ) / ( ! ` n ) ) ) ) ` n ) ) < 1 )
56 fveq2 
 |-  ( j = i -> ( ZZ>= ` j ) = ( ZZ>= ` i ) )
57 56 raleqdv 
 |-  ( j = i -> ( A. n e. ( ZZ>= ` j ) ( abs ` ( ( n e. NN0 |-> ( sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ n ) / ( ! ` n ) ) ) ) ` n ) ) < 1 <-> A. n e. ( ZZ>= ` i ) ( abs ` ( ( n e. NN0 |-> ( sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ n ) / ( ! ` n ) ) ) ) ` n ) ) < 1 ) )
58 55 57 syl5bb 
 |-  ( j = i -> ( A. m e. ( ZZ>= ` j ) ( abs ` ( ( m e. NN0 |-> ( sum_ h e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` h ) x. ( _e ^c h ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ m ) / ( ! ` m ) ) ) ) ` m ) ) < 1 <-> A. n e. ( ZZ>= ` i ) ( abs ` ( ( n e. NN0 |-> ( sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ n ) / ( ! ` n ) ) ) ) ` n ) ) < 1 ) )
59 58 cbvrabv 
 |-  { j e. NN0 | A. m e. ( ZZ>= ` j ) ( abs ` ( ( m e. NN0 |-> ( sum_ h e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` h ) x. ( _e ^c h ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ m ) / ( ! ` m ) ) ) ) ` m ) ) < 1 } = { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( ( n e. NN0 |-> ( sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ n ) / ( ! ` n ) ) ) ) ` n ) ) < 1 }
60 59 infeq1i 
 |-  inf ( { j e. NN0 | A. m e. ( ZZ>= ` j ) ( abs ` ( ( m e. NN0 |-> ( sum_ h e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` h ) x. ( _e ^c h ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ m ) / ( ! ` m ) ) ) ) ` m ) ) < 1 } , RR , < ) = inf ( { i e. NN0 | A. n e. ( ZZ>= ` i ) ( abs ` ( ( n e. NN0 |-> ( sum_ l e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` l ) x. ( _e ^c l ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ n ) / ( ! ` n ) ) ) ) ` n ) ) < 1 } , RR , < )
61 eqid 
 |-  sup ( { ( abs ` ( ( coeff ` q ) ` 0 ) ) , ( ! ` ( deg ` q ) ) , inf ( { j e. NN0 | A. m e. ( ZZ>= ` j ) ( abs ` ( ( m e. NN0 |-> ( sum_ h e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` h ) x. ( _e ^c h ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ m ) / ( ! ` m ) ) ) ) ` m ) ) < 1 } , RR , < ) } , RR* , < ) = sup ( { ( abs ` ( ( coeff ` q ) ` 0 ) ) , ( ! ` ( deg ` q ) ) , inf ( { j e. NN0 | A. m e. ( ZZ>= ` j ) ( abs ` ( ( m e. NN0 |-> ( sum_ h e. ( 0 ... ( deg ` q ) ) ( ( abs ` ( ( ( coeff ` q ) ` h ) x. ( _e ^c h ) ) ) x. ( ( deg ` q ) x. ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ) ) x. ( ( ( ( deg ` q ) ^ ( ( deg ` q ) + 1 ) ) ^ m ) / ( ! ` m ) ) ) ) ` m ) ) < 1 } , RR , < ) } , RR* , < )
62 31 32 33 34 35 36 37 60 61 etransclem48 
 |-  ( ( q e. ( Poly ` ZZ ) /\ ( ( ( coeff ` q ) ` 0 ) =/= 0 /\ ( q ` _e ) = 0 ) ) -> E. k e. ZZ ( k =/= 0 /\ ( abs ` k ) < 1 ) )
63 62 rexlimiva 
 |-  ( E. q e. ( Poly ` ZZ ) ( ( ( coeff ` q ) ` 0 ) =/= 0 /\ ( q ` _e ) = 0 ) -> E. k e. ZZ ( k =/= 0 /\ ( abs ` k ) < 1 ) )
64 23 63 syl 
 |-  ( -. _e e. ( CC \ AA ) -> E. k e. ZZ ( k =/= 0 /\ ( abs ` k ) < 1 ) )
65 10 64 mt3 
 |-  _e e. ( CC \ AA )