# 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 )`
` |-  ( ( 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 } ) )`
` |-  ( ( 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 )`