Theorem eluzelcn 12795

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

Syntax hints:   → wi 4   ∈ wcel 2121  ‘cfv 6489  ℂcc 11031  ℤ_≥cuz 12783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pr 5365  ax-cnex 11089  ax-resscn 11090

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-fv 6497  df-ov 7363  df-neg 11375  df-z 12520  df-uz 12784

This theorem is referenced by:  uzp1  12820  peano2uzr  12848  uzaddcl  12849  ge2halflem1  13054  eluzgtdifelfzo  13677  fzosplitpr  13727  fldiv4lem1div2uz2  13790  mulp1mod1  13868  seqm1  13976  bcval5  14275  swrdfv2  14619  relexpaddg  15010  shftuz  15026  seqshft  15042  climshftlem  15531  climshft  15533  isumshft  15799  dvdsexp  16292  pclem  16804  efgtlen  19696  dvradcnv  26408  logbgcd1irr  26780  clwwlkext2edg  30148  clwwlknonex2lem1  30199  clwwlknonex2lem2  30200  clwwlknonex2  30201  2clwwlk2clwwlk  30442  numclwwlk1lem2foalem  30443  numclwwlk1lem2fo  30450  numclwwlk2  30473  nn0prpwlem  36565  aks4d1p1p1  42563  fimgmcyc  43035  rmspecsqrtnq  43366  rmxm1  43394  rmym1  43395  rmxluc  43396  rmyluc  43397  rmyluc2  43398  jm2.17a  43420  relexpaddss  44177  trclfvdecomr  44187  binomcxplemnn0  44808  stoweidlem14  46471  2tceilhalfelfzo1  47813  2timesltsqm1  47856  fmtnorec3  48040  lighneallem4a  48100  lighneallem4b  48101  ppivalnnprm  48117  ppivalnnnprmge6  48118  evengpop3  48303  evengpoap3  48304  nnsum4primeseven  48305  nnsum4primesevenALTV  48306  gpgedgvtx1  48567  expnegico01  49023  dignn0ldlem  49107  dignnld  49108  digexp  49112  dig1  49113  nn0sumshdiglemB  49125