Theorem eluzelcn 12069

Description: A member of an upper set of integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017.)

Assertion

Ref	Expression
eluzelcn	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ)

Proof of Theorem eluzelcn

Step	Hyp	Ref	Expression
1		eluzelre 12068	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ)
2	1	recnd 10467	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2051  ‘cfv 6186  ℂcc 10332  ℤ_≥cuz 12057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-cnex 10390  ax-resscn 10391

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-ral 3088  df-rex 3089  df-rab 3092  df-v 3412  df-sbc 3677  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-br 4927  df-opab 4989  df-mpt 5006  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-fv 6194  df-ov 6978  df-neg 10672  df-z 11793  df-uz 12058

This theorem is referenced by:  uzp1  12092  peano2uzr  12116  uzaddcl  12117  eluzgtdifelfzo  12913  fzosplitpr  12960  fldiv4lem1div2uz2  13020  mulp1mod1  13094  seqm1  13201  bcval5  13492  swrdfv2  13837  relexpaddg  14272  shftuz  14288  seqshft  14304  climshftlem  14791  climshft  14793  isumshft  15053  dvdsexp  15536  pclem  16030  efgtlen  18623  dvradcnv  24728  logbgcd1irr  25089  clwwlkext2edg  27595  clwwlknonex2lem1  27651  clwwlknonex2lem2  27652  clwwlknonex2  27653  2clwwlk2clwwlk  27903  2clwwlk2clwwlkOLD  27904  numclwwlk1lem2foalem  27905  numclwwlk1lem2foalemOLD  27906  numclwwlk1lem2fo  27916  numclwwlk1lem2foOLD  27921  numclwwlk2  27954  nn0prpwlem  33224  rmspecsqrtnq  38933  rmxm1  38961  rmym1  38962  rmxluc  38963  rmyluc  38964  rmyluc2  38965  jm2.17a  38987  relexpaddss  39460  trclfvdecomr  39470  binomcxplemnn0  40131  stoweidlem14  41760  fmtnorec3  43108  lighneallem4a  43171  lighneallem4b  43172  evengpop3  43361  evengpoap3  43362  nnsum4primeseven  43363  nnsum4primesevenALTV  43364  expnegico01  43971  dignn0ldlem  44060  dignnld  44061  digexp  44065  dig1  44066  nn0sumshdiglemB  44078