Theorem eluzelcn 12800

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 12799	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ)
2	1	recnd 11173	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6498  ℂcc 11036  ℤ_≥cuz 12788

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-cnex 11094  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-ov 7370  df-neg 11380  df-z 12525  df-uz 12789

This theorem is referenced by:  uzp1  12825  peano2uzr  12853  uzaddcl  12854  ge2halflem1  13059  eluzgtdifelfzo  13682  fzosplitpr  13732  fldiv4lem1div2uz2  13795  mulp1mod1  13873  seqm1  13981  bcval5  14280  swrdfv2  14624  relexpaddg  15015  shftuz  15031  seqshft  15047  climshftlem  15536  climshft  15538  isumshft  15804  dvdsexp  16297  pclem  16809  efgtlen  19701  dvradcnv  26386  logbgcd1irr  26758  clwwlkext2edg  30126  clwwlknonex2lem1  30177  clwwlknonex2lem2  30178  clwwlknonex2  30179  2clwwlk2clwwlk  30420  numclwwlk1lem2foalem  30421  numclwwlk1lem2fo  30428  numclwwlk2  30451  nn0prpwlem  36504  aks4d1p1p1  42502  fimgmcyc  42979  rmspecsqrtnq  43334  rmxm1  43362  rmym1  43363  rmxluc  43364  rmyluc  43365  rmyluc2  43366  jm2.17a  43388  relexpaddss  44145  trclfvdecomr  44155  binomcxplemnn0  44776  stoweidlem14  46442  2tceilhalfelfzo1  47784  2timesltsqm1  47827  fmtnorec3  48011  lighneallem4a  48071  lighneallem4b  48072  ppivalnnprm  48088  ppivalnnnprmge6  48089  evengpop3  48274  evengpoap3  48275  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  gpgedgvtx1  48538  expnegico01  48994  dignn0ldlem  49078  dignnld  49079  digexp  49083  dig1  49084  nn0sumshdiglemB  49096