MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eluzelcn Structured version   Unicode version

Theorem eluzelcn 11054
Description: A member of an upper set of integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
Assertion
Ref Expression
eluzelcn  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  CC )

Proof of Theorem eluzelcn
StepHypRef Expression
1 eluzelre 11053 . 2  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  RR )
21recnd 9570 1  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1840   ` cfv 5523   CCcc 9438   ZZ>=cuz 11043
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-8 1842  ax-9 1844  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378  ax-sep 4514  ax-nul 4522  ax-pow 4569  ax-pr 4627  ax-cnex 9496  ax-resscn 9497
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 973  df-3an 974  df-tru 1406  df-ex 1632  df-nf 1636  df-sb 1762  df-eu 2240  df-mo 2241  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-ne 2598  df-ral 2756  df-rex 2757  df-rab 2760  df-v 3058  df-sbc 3275  df-dif 3414  df-un 3416  df-in 3418  df-ss 3425  df-nul 3736  df-if 3883  df-pw 3954  df-sn 3970  df-pr 3972  df-op 3976  df-uni 4189  df-br 4393  df-opab 4451  df-mpt 4452  df-id 4735  df-xp 4946  df-rel 4947  df-cnv 4948  df-co 4949  df-dm 4950  df-rn 4951  df-res 4952  df-ima 4953  df-iota 5487  df-fun 5525  df-fn 5526  df-f 5527  df-fv 5531  df-ov 6235  df-neg 9762  df-z 10824  df-uz 11044
This theorem is referenced by:  uzp1  11076  peano2uzr  11098  uzaddcl  11099  eluzgtdifelfzo  11825  seqm1  12076  bcval5  12348  swrdfv2  12632  relexpaddg  12940  shftuz  12956  seqshft  12972  climshftlem  13451  climshft  13453  isumshft  13707  dvdsexp  14141  pclem  14461  efgtlen  16958  dvradcnv  22998  clwwlkext2edg  25101  extwwlkfablem1  25373  extwwlkfablem2  25377  numclwwlkovf2ex  25385  numclwlk1lem2foa  25390  numclwlk1lem2fo  25394  numclwwlk2  25406  nn0prpwlem  30533  rmspecsqrtnq  35167  rmxm1  35195  rmym1  35196  rmxluc  35197  rmyluc  35198  rmyluc2  35199  jm2.17a  35223  relexpaddss  35661  trclfvdecomr  35671  binomcxplemnn0  36066  stoweidlem14  37131  evengpop3  37787  nnsum4primeseven  37788  fzosplitpr  37906  expnegico01  38567  dignn0ldlem  38667  dignnld  38668  digexp  38672  dig1  38673  nn0sumshdiglemB  38685
  Copyright terms: Public domain W3C validator