Theorem eluzelcn 12765

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6491  ℂcc 11026  ℤ_≥cuz 12753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pr 5376  ax-cnex 11084  ax-resscn 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-fv 6499  df-ov 7361  df-neg 11369  df-z 12491  df-uz 12754

This theorem is referenced by:  uzp1  12790  peano2uzr  12818  uzaddcl  12819  ge2halflem1  13024  eluzgtdifelfzo  13645  fzosplitpr  13695  fldiv4lem1div2uz2  13758  mulp1mod1  13836  seqm1  13944  bcval5  14243  swrdfv2  14587  relexpaddg  14978  shftuz  14994  seqshft  15010  climshftlem  15499  climshft  15501  isumshft  15764  dvdsexp  16257  pclem  16768  efgtlen  19657  dvradcnv  26388  logbgcd1irr  26762  clwwlkext2edg  30112  clwwlknonex2lem1  30163  clwwlknonex2lem2  30164  clwwlknonex2  30165  2clwwlk2clwwlk  30406  numclwwlk1lem2foalem  30407  numclwwlk1lem2fo  30414  numclwwlk2  30437  nn0prpwlem  36495  aks4d1p1p1  42352  fimgmcyc  42826  rmspecsqrtnq  43185  rmxm1  43213  rmym1  43214  rmxluc  43215  rmyluc  43216  rmyluc2  43217  jm2.17a  43239  relexpaddss  43996  trclfvdecomr  44006  binomcxplemnn0  44627  stoweidlem14  46295  2tceilhalfelfzo1  47615  fmtnorec3  47831  lighneallem4a  47891  lighneallem4b  47892  evengpop3  48081  evengpoap3  48082  nnsum4primeseven  48083  nnsum4primesevenALTV  48084  gpgedgvtx1  48345  expnegico01  48801  dignn0ldlem  48885  dignnld  48886  digexp  48890  dig1  48891  nn0sumshdiglemB  48903