Theorem eluzelcn 12767

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6493  ℂcc 11028  ℤ_≥cuz 12755

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 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378  ax-cnex 11086  ax-resscn 11087

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7363  df-neg 11371  df-z 12493  df-uz 12756

This theorem is referenced by:  uzp1  12792  peano2uzr  12820  uzaddcl  12821  ge2halflem1  13026  eluzgtdifelfzo  13647  fzosplitpr  13697  fldiv4lem1div2uz2  13760  mulp1mod1  13838  seqm1  13946  bcval5  14245  swrdfv2  14589  relexpaddg  14980  shftuz  14996  seqshft  15012  climshftlem  15501  climshft  15503  isumshft  15766  dvdsexp  16259  pclem  16770  efgtlen  19659  dvradcnv  26390  logbgcd1irr  26764  clwwlkext2edg  30135  clwwlknonex2lem1  30186  clwwlknonex2lem2  30187  clwwlknonex2  30188  2clwwlk2clwwlk  30429  numclwwlk1lem2foalem  30430  numclwwlk1lem2fo  30437  numclwwlk2  30460  nn0prpwlem  36518  aks4d1p1p1  42385  fimgmcyc  42856  rmspecsqrtnq  43215  rmxm1  43243  rmym1  43244  rmxluc  43245  rmyluc  43246  rmyluc2  43247  jm2.17a  43269  relexpaddss  44026  trclfvdecomr  44036  binomcxplemnn0  44657  stoweidlem14  46325  2tceilhalfelfzo1  47645  fmtnorec3  47861  lighneallem4a  47921  lighneallem4b  47922  evengpop3  48111  evengpoap3  48112  nnsum4primeseven  48113  nnsum4primesevenALTV  48114  gpgedgvtx1  48375  expnegico01  48831  dignn0ldlem  48915  dignnld  48916  digexp  48920  dig1  48921  nn0sumshdiglemB  48933