Theorem eluzelcn 11534

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

Syntax hints:   → wi 4   ∈ wcel 1977  ‘cfv 5790  ℂcc 9791  ℤ_≥cuz 11522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-cnex 9849  ax-resscn 9850

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-br 4579  df-opab 4639  df-mpt 4640  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-fv 5798  df-ov 6530  df-neg 10121  df-z 11214  df-uz 11523

This theorem is referenced by:  uzp1  11556  peano2uzr  11578  uzaddcl  11579  eluzgtdifelfzo  12355  fldiv4lem1div2uz2  12457  mulp1mod1  12531  seqm1  12638  bcval5  12925  swrdfv2  13247  relexpaddg  13590  shftuz  13606  seqshft  13622  climshftlem  14102  climshft  14104  isumshft  14359  dvdsexp  14836  pclem  15330  efgtlen  17911  dvradcnv  23924  clwwlkext2edg  26124  extwwlkfablem1  26395  extwwlkfablem2  26399  numclwwlkovf2ex  26407  numclwlk1lem2foa  26412  numclwlk1lem2fo  26416  numclwwlk2  26428  nn0prpwlem  31281  rmspecsqrtnq  36282  rmspecsqrtnqOLD  36283  rmxm1  36311  rmym1  36312  rmxluc  36313  rmyluc  36314  rmyluc2  36315  jm2.17a  36339  relexpaddss  36823  trclfvdecomr  36833  binomcxplemnn0  37364  stoweidlem14  38701  fmtnorec3  39793  lighneallem4a  39858  lighneallem4b  39859  evengpop3  40009  evengpoap3  40010  nnsum4primeseven  40011  nnsum4primesevenALTV  40012  fzosplitpr  40179  clwwlksext2edg  41222  av-extwwlkfablem1  41500  av-extwwlkfablem2  41502  av-numclwwlkovf2ex  41509  av-numclwlk1lem2foa  41513  av-numclwlk1lem2fo  41517  av-numclwwlk2  41529  expnegico01  42094  dignn0ldlem  42186  dignnld  42187  digexp  42191  dig1  42192  nn0sumshdiglemB  42204