Theorem eluzelcn 12838

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

Syntax hints:   → wi 4   ∈ wcel 2104  ‘cfv 6542  ℂcc 11110  ℤ_≥cuz 12826

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-cnex 11168  ax-resscn 11169

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-ov 7414  df-neg 11451  df-z 12563  df-uz 12827

This theorem is referenced by:  uzp1  12867  peano2uzr  12891  uzaddcl  12892  eluzgtdifelfzo  13698  fzosplitpr  13745  fldiv4lem1div2uz2  13805  mulp1mod1  13881  seqm1  13989  bcval5  14282  swrdfv2  14615  relexpaddg  15004  shftuz  15020  seqshft  15036  climshftlem  15522  climshft  15524  isumshft  15789  dvdsexp  16275  pclem  16775  efgtlen  19635  dvradcnv  26169  logbgcd1irr  26535  clwwlkext2edg  29576  clwwlknonex2lem1  29627  clwwlknonex2lem2  29628  clwwlknonex2  29629  2clwwlk2clwwlk  29870  numclwwlk1lem2foalem  29871  numclwwlk1lem2fo  29878  numclwwlk2  29901  nn0prpwlem  35510  aks4d1p1p1  41234  rmspecsqrtnq  41946  rmxm1  41975  rmym1  41976  rmxluc  41977  rmyluc  41978  rmyluc2  41979  jm2.17a  42001  relexpaddss  42771  trclfvdecomr  42781  binomcxplemnn0  43410  stoweidlem14  45028  fmtnorec3  46514  lighneallem4a  46574  lighneallem4b  46575  evengpop3  46764  evengpoap3  46765  nnsum4primeseven  46766  nnsum4primesevenALTV  46767  expnegico01  47286  dignn0ldlem  47375  dignnld  47376  digexp  47380  dig1  47381  nn0sumshdiglemB  47393