Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nn0cni | Structured version Visualization version GIF version |
Description: A nonnegative integer is a complex number. (Contributed by NM, 14-May-2003.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 8-Oct-2022.) |
Ref | Expression |
---|---|
nn0rei.1 | ⊢ 𝐴 ∈ ℕ0 |
Ref | Expression |
---|---|
nn0cni | ⊢ 𝐴 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0sscn 11890 | . 2 ⊢ ℕ0 ⊆ ℂ | |
2 | nn0rei.1 | . 2 ⊢ 𝐴 ∈ ℕ0 | |
3 | 1, 2 | sselii 3961 | 1 ⊢ 𝐴 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 ℂcc 10523 ℕ0cn0 11885 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7450 ax-1cn 10583 ax-icn 10584 ax-addcl 10585 ax-mulcl 10587 ax-i2m1 10593 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3or 1080 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ne 3014 df-ral 3140 df-rex 3141 df-reu 3142 df-rab 3144 df-v 3494 df-sbc 3770 df-csb 3881 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-pss 3951 df-nul 4289 df-if 4464 df-pw 4537 df-sn 4558 df-pr 4560 df-tp 4562 df-op 4564 df-uni 4831 df-iun 4912 df-br 5058 df-opab 5120 df-mpt 5138 df-tr 5164 df-id 5453 df-eprel 5458 df-po 5467 df-so 5468 df-fr 5507 df-we 5509 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-pred 6141 df-ord 6187 df-on 6188 df-lim 6189 df-suc 6190 df-iota 6307 df-fun 6350 df-fn 6351 df-f 6352 df-f1 6353 df-fo 6354 df-f1o 6355 df-fv 6356 df-ov 7148 df-om 7570 df-wrecs 7936 df-recs 7997 df-rdg 8035 df-nn 11627 df-n0 11886 |
This theorem is referenced by: nn0le2xi 11939 num0u 12097 num0h 12098 numsuc 12100 numsucc 12126 numma 12130 nummac 12131 numma2c 12132 numadd 12133 numaddc 12134 nummul1c 12135 nummul2c 12136 decrmanc 12143 decrmac 12144 decaddi 12146 decaddci 12147 decsubi 12149 decmul1 12150 decmulnc 12153 11multnc 12154 decmul10add 12155 6p5lem 12156 4t3lem 12183 7t3e21 12196 7t6e42 12199 8t3e24 12202 8t4e32 12203 8t8e64 12207 9t3e27 12209 9t4e36 12210 9t5e45 12211 9t6e54 12212 9t7e63 12213 9t11e99 12216 decbin0 12226 decbin2 12227 sq10 13612 3dec 13614 nn0le2msqi 13615 nn0opthlem1 13616 nn0opthi 13618 nn0opth2i 13619 faclbnd4lem1 13641 cats1fvn 14208 bpoly4 15401 fsumcube 15402 3dvdsdec 15669 3dvds2dec 15670 divalglem2 15734 3lcm2e6 16060 phiprmpw 16101 dec5dvds 16388 dec5dvds2 16389 dec2nprm 16391 modxai 16392 mod2xi 16393 mod2xnegi 16395 modsubi 16396 gcdi 16397 decexp2 16399 numexp0 16400 numexp1 16401 numexpp1 16402 numexp2x 16403 decsplit0b 16404 decsplit0 16405 decsplit1 16406 decsplit 16407 karatsuba 16408 2exp8 16411 prmlem2 16441 83prm 16444 139prm 16445 163prm 16446 631prm 16448 1259lem1 16452 1259lem2 16453 1259lem3 16454 1259lem4 16455 1259lem5 16456 1259prm 16457 2503lem1 16458 2503lem2 16459 2503lem3 16460 2503prm 16461 4001lem1 16462 4001lem2 16463 4001lem3 16464 4001lem4 16465 4001prm 16466 log2ublem1 25451 log2ublem2 25452 log2ublem3 25453 log2ub 25454 birthday 25459 ppidif 25667 bpos1lem 25785 9p10ne21 28176 dfdec100 30473 dp20u 30481 dp20h 30482 dpmul10 30498 dpmul100 30500 dp3mul10 30501 dpmul1000 30502 dpexpp1 30511 0dp2dp 30512 dpadd2 30513 dpadd 30514 dpmul 30516 dpmul4 30517 lmatfvlem 30979 ballotlemfp1 31648 ballotth 31694 reprlt 31789 hgt750lemd 31818 hgt750lem2 31822 subfacp1lem1 32323 poimirlem26 34799 poimirlem28 34801 decaddcom 39048 sqn5i 39049 decpmulnc 39051 decpmul 39052 sqdeccom12 39053 sq3deccom12 39054 235t711 39055 ex-decpmul 39056 inductionexd 40383 unitadd 40426 fmtno5lem4 43595 257prm 43600 fmtno4prmfac 43611 fmtno5fac 43621 139prmALT 43636 127prm 43640 m11nprm 43643 11t31e341 43774 2exp340mod341 43775 |
Copyright terms: Public domain | W3C validator |