![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eluzelcn | Structured version Visualization version GIF version |
Description: A member of an upper set of integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Ref | Expression |
---|---|
eluzelcn | ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluzelre 12871 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ) | |
2 | 1 | recnd 11279 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 ‘cfv 6549 ℂcc 11143 ℤ≥cuz 12860 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 ax-cnex 11201 ax-resscn 11202 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-iota 6501 df-fun 6551 df-fn 6552 df-f 6553 df-fv 6557 df-ov 7422 df-neg 11484 df-z 12597 df-uz 12861 |
This theorem is referenced by: uzp1 12901 peano2uzr 12925 uzaddcl 12926 eluzgtdifelfzo 13734 fzosplitpr 13782 fldiv4lem1div2uz2 13842 mulp1mod1 13918 seqm1 14025 bcval5 14321 swrdfv2 14655 relexpaddg 15044 shftuz 15060 seqshft 15076 climshftlem 15562 climshft 15564 isumshft 15829 dvdsexp 16316 pclem 16826 efgtlen 19710 dvradcnv 26419 logbgcd1irr 26791 clwwlkext2edg 29958 clwwlknonex2lem1 30009 clwwlknonex2lem2 30010 clwwlknonex2 30011 2clwwlk2clwwlk 30252 numclwwlk1lem2foalem 30253 numclwwlk1lem2fo 30260 numclwwlk2 30283 nn0prpwlem 35957 aks4d1p1p1 41686 rmspecsqrtnq 42473 rmxm1 42502 rmym1 42503 rmxluc 42504 rmyluc 42505 rmyluc2 42506 jm2.17a 42528 relexpaddss 43295 trclfvdecomr 43305 binomcxplemnn0 43933 stoweidlem14 45545 fmtnorec3 47030 lighneallem4a 47090 lighneallem4b 47091 evengpop3 47280 evengpoap3 47281 nnsum4primeseven 47282 nnsum4primesevenALTV 47283 expnegico01 47777 dignn0ldlem 47866 dignnld 47867 digexp 47871 dig1 47872 nn0sumshdiglemB 47884 |
Copyright terms: Public domain | W3C validator |