![]() |
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 12732 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℝ) | |
2 | 1 | recnd 11141 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 ‘cfv 6493 ℂcc 11007 ℤ≥cuz 12721 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5254 ax-nul 5261 ax-pr 5382 ax-cnex 11065 ax-resscn 11066 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-mpt 5187 df-id 5529 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6445 df-fun 6495 df-fn 6496 df-f 6497 df-fv 6501 df-ov 7354 df-neg 11346 df-z 12458 df-uz 12722 |
This theorem is referenced by: uzp1 12758 peano2uzr 12782 uzaddcl 12783 eluzgtdifelfzo 13588 fzosplitpr 13635 fldiv4lem1div2uz2 13695 mulp1mod1 13771 seqm1 13879 bcval5 14172 swrdfv2 14503 relexpaddg 14892 shftuz 14908 seqshft 14924 climshftlem 15410 climshft 15412 isumshft 15678 dvdsexp 16164 pclem 16664 efgtlen 19461 dvradcnv 25726 logbgcd1irr 26090 clwwlkext2edg 28845 clwwlknonex2lem1 28896 clwwlknonex2lem2 28897 clwwlknonex2 28898 2clwwlk2clwwlk 29139 numclwwlk1lem2foalem 29140 numclwwlk1lem2fo 29147 numclwwlk2 29170 nn0prpwlem 34726 aks4d1p1p1 40452 rmspecsqrtnq 41132 rmxm1 41161 rmym1 41162 rmxluc 41163 rmyluc 41164 rmyluc2 41165 jm2.17a 41187 relexpaddss 41895 trclfvdecomr 41905 binomcxplemnn0 42534 stoweidlem14 44150 fmtnorec3 45635 lighneallem4a 45695 lighneallem4b 45696 evengpop3 45885 evengpoap3 45886 nnsum4primeseven 45887 nnsum4primesevenALTV 45888 expnegico01 46494 dignn0ldlem 46583 dignnld 46584 digexp 46588 dig1 46589 nn0sumshdiglemB 46601 |
Copyright terms: Public domain | W3C validator |