Theorem eluzelcn 12795

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6494  ℂcc 11031  ℤ_≥cuz 12783

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 5232  ax-nul 5242  ax-pr 5372  ax-cnex 11089  ax-resscn 11090

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5521  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-fv 6502  df-ov 7365  df-neg 11375  df-z 12520  df-uz 12784

This theorem is referenced by:  uzp1  12820  peano2uzr  12848  uzaddcl  12849  ge2halflem1  13054  eluzgtdifelfzo  13677  fzosplitpr  13727  fldiv4lem1div2uz2  13790  mulp1mod1  13868  seqm1  13976  bcval5  14275  swrdfv2  14619  relexpaddg  15010  shftuz  15026  seqshft  15042  climshftlem  15531  climshft  15533  isumshft  15799  dvdsexp  16292  pclem  16804  efgtlen  19696  dvradcnv  26403  logbgcd1irr  26775  clwwlkext2edg  30145  clwwlknonex2lem1  30196  clwwlknonex2lem2  30197  clwwlknonex2  30198  2clwwlk2clwwlk  30439  numclwwlk1lem2foalem  30440  numclwwlk1lem2fo  30447  numclwwlk2  30470  nn0prpwlem  36524  aks4d1p1p1  42520  fimgmcyc  42997  rmspecsqrtnq  43356  rmxm1  43384  rmym1  43385  rmxluc  43386  rmyluc  43387  rmyluc2  43388  jm2.17a  43410  relexpaddss  44167  trclfvdecomr  44177  binomcxplemnn0  44798  stoweidlem14  46464  2tceilhalfelfzo1  47800  2timesltsqm1  47843  fmtnorec3  48027  lighneallem4a  48087  lighneallem4b  48088  ppivalnnprm  48104  ppivalnnnprmge6  48105  evengpop3  48290  evengpoap3  48291  nnsum4primeseven  48292  nnsum4primesevenALTV  48293  gpgedgvtx1  48554  expnegico01  49010  dignn0ldlem  49094  dignnld  49095  digexp  49099  dig1  49100  nn0sumshdiglemB  49112