Metamath Proof Explorer

Theorem lgamgulmlem1

Description: Lemma for lgamgulm . (Contributed by Mario Carneiro, 3-Jul-2017)

Ref Expression
Hypotheses lgamgulm.r 
|- ( ph -> R e. NN )
lgamgulm.u 
|- U = { x e. CC | ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) }
Assertion lgamgulmlem1 
|- ( ph -> U C_ ( CC \ ( ZZ \ NN ) ) )

Proof

Step Hyp Ref Expression
1 lgamgulm.r 
 |-  ( ph -> R e. NN )
2 lgamgulm.u 
 |-  U = { x e. CC | ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) }
3 simp2 
 |-  ( ( ph /\ x e. CC /\ ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) ) -> x e. CC )
4 1 3ad2ant1 
 |-  ( ( ph /\ x e. CC /\ ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) ) -> R e. NN )
5 4 nnred 
 |-  ( ( ph /\ x e. CC /\ ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) ) -> R e. RR )
6 4 nngt0d 
 |-  ( ( ph /\ x e. CC /\ ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) ) -> 0 < R )
7 5 6 recgt0d 
 |-  ( ( ph /\ x e. CC /\ ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) ) -> 0 < ( 1 / R ) )
8 0red 
 |-  ( ( ph /\ x e. CC /\ ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) ) -> 0 e. RR )
9 4 nnrecred 
 |-  ( ( ph /\ x e. CC /\ ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) ) -> ( 1 / R ) e. RR )
10 8 9 ltnled 
 |-  ( ( ph /\ x e. CC /\ ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) ) -> ( 0 < ( 1 / R ) <-> -. ( 1 / R ) <_ 0 ) )
11 7 10 mpbid 
 |-  ( ( ph /\ x e. CC /\ ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) ) -> -. ( 1 / R ) <_ 0 )
12 oveq2 
 |-  ( k = -u x -> ( x + k ) = ( x + -u x ) )
13 12 fveq2d 
 |-  ( k = -u x -> ( abs ` ( x + k ) ) = ( abs ` ( x + -u x ) ) )
14 13 breq2d 
 |-  ( k = -u x -> ( ( 1 / R ) <_ ( abs ` ( x + k ) ) <-> ( 1 / R ) <_ ( abs ` ( x + -u x ) ) ) )
15 14 rspccv 
 |-  ( A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) -> ( -u x e. NN0 -> ( 1 / R ) <_ ( abs ` ( x + -u x ) ) ) )
16 15 adantl 
 |-  ( ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) -> ( -u x e. NN0 -> ( 1 / R ) <_ ( abs ` ( x + -u x ) ) ) )
17 16 3ad2ant3 
 |-  ( ( ph /\ x e. CC /\ ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) ) -> ( -u x e. NN0 -> ( 1 / R ) <_ ( abs ` ( x + -u x ) ) ) )
18 3 negidd 
 |-  ( ( ph /\ x e. CC /\ ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) ) -> ( x + -u x ) = 0 )
19 18 fveq2d 
 |-  ( ( ph /\ x e. CC /\ ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) ) -> ( abs ` ( x + -u x ) ) = ( abs ` 0 ) )
20 abs0 
 |-  ( abs ` 0 ) = 0
21 19 20 eqtrdi 
 |-  ( ( ph /\ x e. CC /\ ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) ) -> ( abs ` ( x + -u x ) ) = 0 )
22 21 breq2d 
 |-  ( ( ph /\ x e. CC /\ ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) ) -> ( ( 1 / R ) <_ ( abs ` ( x + -u x ) ) <-> ( 1 / R ) <_ 0 ) )
23 17 22 sylibd 
 |-  ( ( ph /\ x e. CC /\ ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) ) -> ( -u x e. NN0 -> ( 1 / R ) <_ 0 ) )
24 11 23 mtod 
 |-  ( ( ph /\ x e. CC /\ ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) ) -> -. -u x e. NN0 )
25 eldmgm 
 |-  ( x e. ( CC \ ( ZZ \ NN ) ) <-> ( x e. CC /\ -. -u x e. NN0 ) )
26 3 24 25 sylanbrc 
 |-  ( ( ph /\ x e. CC /\ ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) ) -> x e. ( CC \ ( ZZ \ NN ) ) )
27 26 rabssdv 
 |-  ( ph -> { x e. CC | ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) } C_ ( CC \ ( ZZ \ NN ) ) )
28 2 27 eqsstrid 
 |-  ( ph -> U C_ ( CC \ ( ZZ \ NN ) ) )