Theorem eluzelcn 11905

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

Syntax hints:   → wi 4   ∈ wcel 2145  ‘cfv 6030  ℂcc 10140  ℤ_≥cuz 11893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-cnex 10198  ax-resscn 10199

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-fv 6038  df-ov 6799  df-neg 10475  df-z 11585  df-uz 11894

This theorem is referenced by:  uzp1  11928  peano2uzr  11950  uzaddcl  11951  eluzgtdifelfzo  12738  fzosplitpr  12785  fldiv4lem1div2uz2  12845  mulp1mod1  12919  seqm1  13025  bcval5  13309  swrdfv2  13655  relexpaddg  14001  shftuz  14017  seqshft  14033  climshftlem  14513  climshft  14515  isumshft  14778  dvdsexp  15258  pclem  15750  efgtlen  18346  dvradcnv  24395  clwwlkext2edg  27213  clwwlknonex2lem1  27283  clwwlknonex2lem2  27284  clwwlknonex2  27285  extwwlkfablem1OLD  27524  2clwwlk2clwwlk  27534  numclwwlk1lem2foalem  27537  numclwwlk1lem2fo  27544  numclwwlk2  27572  numclwwlk2OLD  27579  nn0prpwlem  32654  rmspecsqrtnq  37996  rmspecsqrtnqOLD  37997  rmxm1  38025  rmym1  38026  rmxluc  38027  rmyluc  38028  rmyluc2  38029  jm2.17a  38053  relexpaddss  38536  trclfvdecomr  38546  binomcxplemnn0  39074  stoweidlem14  40745  fmtnorec3  41985  lighneallem4a  42050  lighneallem4b  42051  evengpop3  42211  evengpoap3  42212  nnsum4primeseven  42213  nnsum4primesevenALTV  42214  expnegico01  42833  dignn0ldlem  42921  dignnld  42922  digexp  42926  dig1  42927  nn0sumshdiglemB  42939