Theorem eluzelcn 12747

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6482  ℂcc 11007  ℤ_≥cuz 12735

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-cnex 11065  ax-resscn 11066

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-fv 6490  df-ov 7352  df-neg 11350  df-z 12472  df-uz 12736

This theorem is referenced by:  uzp1  12776  peano2uzr  12804  uzaddcl  12805  ge2halflem1  13010  eluzgtdifelfzo  13630  fzosplitpr  13679  fldiv4lem1div2uz2  13740  mulp1mod1  13818  seqm1  13926  bcval5  14225  swrdfv2  14568  relexpaddg  14960  shftuz  14976  seqshft  14992  climshftlem  15481  climshft  15483  isumshft  15746  dvdsexp  16239  pclem  16750  efgtlen  19605  dvradcnv  26328  logbgcd1irr  26702  clwwlkext2edg  30000  clwwlknonex2lem1  30051  clwwlknonex2lem2  30052  clwwlknonex2  30053  2clwwlk2clwwlk  30294  numclwwlk1lem2foalem  30295  numclwwlk1lem2fo  30302  numclwwlk2  30325  nn0prpwlem  36306  aks4d1p1p1  42046  fimgmcyc  42517  rmspecsqrtnq  42889  rmxm1  42917  rmym1  42918  rmxluc  42919  rmyluc  42920  rmyluc2  42921  jm2.17a  42943  relexpaddss  43701  trclfvdecomr  43711  binomcxplemnn0  44332  stoweidlem14  46005  2tceilhalfelfzo1  47326  fmtnorec3  47542  lighneallem4a  47602  lighneallem4b  47603  evengpop3  47792  evengpoap3  47793  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  gpgedgvtx1  48056  expnegico01  48513  dignn0ldlem  48597  dignnld  48598  digexp  48602  dig1  48603  nn0sumshdiglemB  48615