Theorem eluzelcn 13001

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ‘cfv 6555  ℂcc 11222  ℤ_≥cuz 12989

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-cnex 11280  ax-resscn 11281

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-fv 6563  df-ov 7443  df-neg 11568  df-z 12718  df-uz 12990

This theorem is used by:  uzp1  13026  peano2uzr  13054  uzaddcl  13055  ge2halflem1  13261  eluzgtdifelfzo  13886  fzosplitpr  13936  fldiv4lem1div2uz2  14000  mulp1mod1  14078  seqm1  14186  bcval5  14486  swrdfv2  14836  relexpaddg  15232  shftuz  15248  seqshft  15264  climshftlem  15767  climshft  15769  isumshft  16034  dvdsexp  16524  pclem  17042  efgtlen  19967  dvradcnv  26775  logbgcd1irr  27149  clwwlkext2edg  30674  clwwlknonex2lem1  30725  clwwlknonex2lem2  30726  clwwlknonex2  30727  2clwwlk2clwwlk  30978  numclwwlk1lem2foalem  30979  numclwwlk1lem2fo  30986  numclwwlk2  31009  nn0prpwlem  37287  aks4d1p1p1  43304  fimgmcyc  43789  rmspecsqrtnq  44104  rmxm1  44132  rmym1  44133  rmxluc  44134  rmyluc  44135  rmyluc2  44136  jm2.17a  44158  relexpaddss  44908  trclfvdecomr  44918  binomcxplemnn0  45523  stoweidlem14  47227  2tceilhalfelfzo1  48609  2timesltsqm1  48652  fmtnorec3  48836  lighneallem4a  48896  lighneallem4b  48897  ppivalnnprm  48913  ppivalnnnprmge6  48914  evengpop3  49099  evengpoap3  49100  nnsum4primeseven  49101  nnsum4primesevenALTV  49102  gpgedgvtx1  49363  expnegico01  49833  dignn0ldlem  49917  dignnld  49918  digexp  49922  dig1  49923  nn0sumshdiglemB  49935