Theorem eluzelcn 12523

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6418  ℂcc 10800  ℤ_≥cuz 12511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-cnex 10858  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-ov 7258  df-neg 11138  df-z 12250  df-uz 12512

This theorem is referenced by:  uzp1  12548  peano2uzr  12572  uzaddcl  12573  eluzgtdifelfzo  13377  fzosplitpr  13424  fldiv4lem1div2uz2  13484  mulp1mod1  13560  seqm1  13668  bcval5  13960  swrdfv2  14302  relexpaddg  14692  shftuz  14708  seqshft  14724  climshftlem  15211  climshft  15213  isumshft  15479  dvdsexp  15965  pclem  16467  efgtlen  19247  dvradcnv  25485  logbgcd1irr  25849  clwwlkext2edg  28321  clwwlknonex2lem1  28372  clwwlknonex2lem2  28373  clwwlknonex2  28374  2clwwlk2clwwlk  28615  numclwwlk1lem2foalem  28616  numclwwlk1lem2fo  28623  numclwwlk2  28646  nn0prpwlem  34438  aks4d1p1p1  39999  rmspecsqrtnq  40644  rmxm1  40672  rmym1  40673  rmxluc  40674  rmyluc  40675  rmyluc2  40676  jm2.17a  40698  relexpaddss  41215  trclfvdecomr  41225  binomcxplemnn0  41856  stoweidlem14  43445  fmtnorec3  44888  lighneallem4a  44948  lighneallem4b  44949  evengpop3  45138  evengpoap3  45139  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  expnegico01  45747  dignn0ldlem  45836  dignnld  45837  digexp  45841  dig1  45842  nn0sumshdiglemB  45854