Theorem eluzelcn 12977

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ‘cfv 6538  ℂcc 11198  ℤ_≥cuz 12965

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-cnex 11256  ax-resscn 11257

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7423  df-neg 11544  df-z 12694  df-uz 12966

This theorem is used by:  uzp1  13002  peano2uzr  13030  uzaddcl  13031  ge2halflem1  13237  eluzgtdifelfzo  13862  fzosplitpr  13912  fldiv4lem1div2uz2  13976  mulp1mod1  14054  seqm1  14162  bcval5  14462  swrdfv2  14811  relexpaddg  15206  shftuz  15222  seqshft  15238  climshftlem  15741  climshft  15743  isumshft  16008  dvdsexp  16498  pclem  17016  efgtlen  19940  dvradcnv  26748  logbgcd1irr  27122  clwwlkext2edg  30647  clwwlknonex2lem1  30698  clwwlknonex2lem2  30699  clwwlknonex2  30700  2clwwlk2clwwlk  30951  numclwwlk1lem2foalem  30952  numclwwlk1lem2fo  30959  numclwwlk2  30982  nn0prpwlem  37110  aks4d1p1p1  43114  fimgmcyc  43599  rmspecsqrtnq  43913  rmxm1  43941  rmym1  43942  rmxluc  43943  rmyluc  43944  rmyluc2  43945  jm2.17a  43967  relexpaddss  44718  trclfvdecomr  44728  binomcxplemnn0  45333  stoweidlem14  47024  2tceilhalfelfzo1  48406  2timesltsqm1  48449  fmtnorec3  48633  lighneallem4a  48693  lighneallem4b  48694  ppivalnnprm  48710  ppivalnnnprmge6  48711  evengpop3  48896  evengpoap3  48897  nnsum4primeseven  48898  nnsum4primesevenALTV  48899  gpgedgvtx1  49160  expnegico01  49630  dignn0ldlem  49714  dignnld  49715  digexp  49719  dig1  49720  nn0sumshdiglemB  49732