![]() |
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 12068 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ) | |
2 | 1 | recnd 10467 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2051 ‘cfv 6186 ℂcc 10332 ℤ≥cuz 12057 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2745 ax-sep 5057 ax-nul 5064 ax-pow 5116 ax-pr 5183 ax-cnex 10390 ax-resscn 10391 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-ne 2963 df-ral 3088 df-rex 3089 df-rab 3092 df-v 3412 df-sbc 3677 df-dif 3827 df-un 3829 df-in 3831 df-ss 3838 df-nul 4174 df-if 4346 df-pw 4419 df-sn 4437 df-pr 4439 df-op 4443 df-uni 4710 df-br 4927 df-opab 4989 df-mpt 5006 df-id 5309 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-rn 5415 df-res 5416 df-ima 5417 df-iota 6150 df-fun 6188 df-fn 6189 df-f 6190 df-fv 6194 df-ov 6978 df-neg 10672 df-z 11793 df-uz 12058 |
This theorem is referenced by: uzp1 12092 peano2uzr 12116 uzaddcl 12117 eluzgtdifelfzo 12913 fzosplitpr 12960 fldiv4lem1div2uz2 13020 mulp1mod1 13094 seqm1 13201 bcval5 13492 swrdfv2 13837 relexpaddg 14272 shftuz 14288 seqshft 14304 climshftlem 14791 climshft 14793 isumshft 15053 dvdsexp 15536 pclem 16030 efgtlen 18623 dvradcnv 24728 logbgcd1irr 25089 clwwlkext2edg 27595 clwwlknonex2lem1 27651 clwwlknonex2lem2 27652 clwwlknonex2 27653 2clwwlk2clwwlk 27903 2clwwlk2clwwlkOLD 27904 numclwwlk1lem2foalem 27905 numclwwlk1lem2foalemOLD 27906 numclwwlk1lem2fo 27916 numclwwlk1lem2foOLD 27921 numclwwlk2 27954 nn0prpwlem 33224 rmspecsqrtnq 38933 rmxm1 38961 rmym1 38962 rmxluc 38963 rmyluc 38964 rmyluc2 38965 jm2.17a 38987 relexpaddss 39460 trclfvdecomr 39470 binomcxplemnn0 40131 stoweidlem14 41760 fmtnorec3 43108 lighneallem4a 43171 lighneallem4b 43172 evengpop3 43361 evengpoap3 43362 nnsum4primeseven 43363 nnsum4primesevenALTV 43364 expnegico01 43971 dignn0ldlem 44060 dignnld 44061 digexp 44065 dig1 44066 nn0sumshdiglemB 44078 |
Copyright terms: Public domain | W3C validator |