Theorem eluzelcn 12872

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

Syntax hints:   → wi 4   ∈ wcel 2098  ‘cfv 6549  ℂcc 11143  ℤ_≥cuz 12860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429  ax-cnex 11201  ax-resscn 11202

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-fv 6557  df-ov 7422  df-neg 11484  df-z 12597  df-uz 12861

This theorem is referenced by:  uzp1  12901  peano2uzr  12925  uzaddcl  12926  eluzgtdifelfzo  13734  fzosplitpr  13782  fldiv4lem1div2uz2  13842  mulp1mod1  13918  seqm1  14025  bcval5  14321  swrdfv2  14655  relexpaddg  15044  shftuz  15060  seqshft  15076  climshftlem  15562  climshft  15564  isumshft  15829  dvdsexp  16316  pclem  16826  efgtlen  19710  dvradcnv  26419  logbgcd1irr  26791  clwwlkext2edg  29958  clwwlknonex2lem1  30009  clwwlknonex2lem2  30010  clwwlknonex2  30011  2clwwlk2clwwlk  30252  numclwwlk1lem2foalem  30253  numclwwlk1lem2fo  30260  numclwwlk2  30283  nn0prpwlem  35957  aks4d1p1p1  41686  rmspecsqrtnq  42473  rmxm1  42502  rmym1  42503  rmxluc  42504  rmyluc  42505  rmyluc2  42506  jm2.17a  42528  relexpaddss  43295  trclfvdecomr  43305  binomcxplemnn0  43933  stoweidlem14  45545  fmtnorec3  47030  lighneallem4a  47090  lighneallem4b  47091  evengpop3  47280  evengpoap3  47281  nnsum4primeseven  47282  nnsum4primesevenALTV  47283  expnegico01  47777  dignn0ldlem  47866  dignnld  47867  digexp  47871  dig1  47872  nn0sumshdiglemB  47884