Theorem eluzelcn 12744

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

Syntax hints:   → wi 4   ∈ wcel 2111  ‘cfv 6481  ℂcc 11004  ℤ_≥cuz 12732

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-cnex 11062  ax-resscn 11063

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489  df-ov 7349  df-neg 11347  df-z 12469  df-uz 12733

This theorem is referenced by:  uzp1  12773  peano2uzr  12801  uzaddcl  12802  ge2halflem1  13007  eluzgtdifelfzo  13627  fzosplitpr  13677  fldiv4lem1div2uz2  13740  mulp1mod1  13818  seqm1  13926  bcval5  14225  swrdfv2  14569  relexpaddg  14960  shftuz  14976  seqshft  14992  climshftlem  15481  climshft  15483  isumshft  15746  dvdsexp  16239  pclem  16750  efgtlen  19638  dvradcnv  26357  logbgcd1irr  26731  clwwlkext2edg  30036  clwwlknonex2lem1  30087  clwwlknonex2lem2  30088  clwwlknonex2  30089  2clwwlk2clwwlk  30330  numclwwlk1lem2foalem  30331  numclwwlk1lem2fo  30338  numclwwlk2  30361  nn0prpwlem  36366  aks4d1p1p1  42155  fimgmcyc  42626  rmspecsqrtnq  42998  rmxm1  43026  rmym1  43027  rmxluc  43028  rmyluc  43029  rmyluc2  43030  jm2.17a  43052  relexpaddss  43810  trclfvdecomr  43820  binomcxplemnn0  44441  stoweidlem14  46111  2tceilhalfelfzo1  47431  fmtnorec3  47647  lighneallem4a  47707  lighneallem4b  47708  evengpop3  47897  evengpoap3  47898  nnsum4primeseven  47899  nnsum4primesevenALTV  47900  gpgedgvtx1  48161  expnegico01  48618  dignn0ldlem  48702  dignnld  48703  digexp  48707  dig1  48708  nn0sumshdiglemB  48720