Theorem eluzelcn 12777

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6502  ℂcc 11038  ℤ_≥cuz 12765

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 5245  ax-nul 5255  ax-pr 5381  ax-cnex 11096  ax-resscn 11097

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 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-fv 6510  df-ov 7373  df-neg 11381  df-z 12503  df-uz 12766

This theorem is referenced by:  uzp1  12802  peano2uzr  12830  uzaddcl  12831  ge2halflem1  13036  eluzgtdifelfzo  13657  fzosplitpr  13707  fldiv4lem1div2uz2  13770  mulp1mod1  13848  seqm1  13956  bcval5  14255  swrdfv2  14599  relexpaddg  14990  shftuz  15006  seqshft  15022  climshftlem  15511  climshft  15513  isumshft  15776  dvdsexp  16269  pclem  16780  efgtlen  19672  dvradcnv  26403  logbgcd1irr  26777  clwwlkext2edg  30149  clwwlknonex2lem1  30200  clwwlknonex2lem2  30201  clwwlknonex2  30202  2clwwlk2clwwlk  30443  numclwwlk1lem2foalem  30444  numclwwlk1lem2fo  30451  numclwwlk2  30474  nn0prpwlem  36544  aks4d1p1p1  42462  fimgmcyc  42933  rmspecsqrtnq  43292  rmxm1  43320  rmym1  43321  rmxluc  43322  rmyluc  43323  rmyluc2  43324  jm2.17a  43346  relexpaddss  44103  trclfvdecomr  44113  binomcxplemnn0  44734  stoweidlem14  46401  2tceilhalfelfzo1  47721  fmtnorec3  47937  lighneallem4a  47997  lighneallem4b  47998  evengpop3  48187  evengpoap3  48188  nnsum4primeseven  48189  nnsum4primesevenALTV  48190  gpgedgvtx1  48451  expnegico01  48907  dignn0ldlem  48991  dignnld  48992  digexp  48996  dig1  48997  nn0sumshdiglemB  49009