Theorem eluzelcn 12932

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6528  ℂcc 11155  ℤ_≥cuz 12920

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-cnex 11213  ax-resscn 11214

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-fv 6536  df-ov 7412  df-neg 11501  df-z 12649  df-uz 12921

This theorem is used by:  uzp1  12957  peano2uzr  12985  uzaddcl  12986  ge2halflem1  13192  eluzgtdifelfzo  13816  fzosplitpr  13866  fldiv4lem1div2uz2  13930  mulp1mod1  14008  seqm1  14116  bcval5  14415  swrdfv2  14764  relexpaddg  15159  shftuz  15175  seqshft  15191  climshftlem  15694  climshft  15696  isumshft  15961  dvdsexp  16451  pclem  16963  efgtlen  19887  dvradcnv  26697  logbgcd1irr  27071  clwwlkext2edg  30566  clwwlknonex2lem1  30617  clwwlknonex2lem2  30618  clwwlknonex2  30619  2clwwlk2clwwlk  30870  numclwwlk1lem2foalem  30871  numclwwlk1lem2fo  30878  numclwwlk2  30901  nn0prpwlem  37026  aks4d1p1p1  43027  fimgmcyc  43514  rmspecsqrtnq  43845  rmxm1  43873  rmym1  43874  rmxluc  43875  rmyluc  43876  rmyluc2  43877  jm2.17a  43899  relexpaddss  44656  trclfvdecomr  44666  binomcxplemnn0  45271  stoweidlem14  46940  2tceilhalfelfzo1  48322  2timesltsqm1  48365  fmtnorec3  48549  lighneallem4a  48609  lighneallem4b  48610  ppivalnnprm  48626  ppivalnnnprmge6  48627  evengpop3  48812  evengpoap3  48813  nnsum4primeseven  48814  nnsum4primesevenALTV  48815  gpgedgvtx1  49076  expnegico01  49546  dignn0ldlem  49630  dignnld  49631  digexp  49635  dig1  49636  nn0sumshdiglemB  49648