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 11896 | . 2 ⊢ ℕ0 ⊆ ℂ | |
2 | nn0rei.1 | . 2 ⊢ 𝐴 ∈ ℕ0 | |
3 | 1, 2 | sselii 3963 | 1 ⊢ 𝐴 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 ℂcc 10529 ℕ0cn0 11891 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-mulcl 10593 ax-i2m1 10599 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-iun 4913 df-br 5059 df-opab 5121 df-mpt 5139 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-pred 6142 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-ov 7153 df-om 7575 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-nn 11633 df-n0 11892 |
This theorem is referenced by: nn0le2xi 11945 num0u 12103 num0h 12104 numsuc 12106 numsucc 12132 numma 12136 nummac 12137 numma2c 12138 numadd 12139 numaddc 12140 nummul1c 12141 nummul2c 12142 decrmanc 12149 decrmac 12150 decaddi 12152 decaddci 12153 decsubi 12155 decmul1 12156 decmulnc 12159 11multnc 12160 decmul10add 12161 6p5lem 12162 4t3lem 12189 7t3e21 12202 7t6e42 12205 8t3e24 12208 8t4e32 12209 8t8e64 12213 9t3e27 12215 9t4e36 12216 9t5e45 12217 9t6e54 12218 9t7e63 12219 9t11e99 12222 decbin0 12232 decbin2 12233 sq10 13618 3dec 13620 nn0le2msqi 13621 nn0opthlem1 13622 nn0opthi 13624 nn0opth2i 13625 faclbnd4lem1 13647 cats1fvn 14214 bpoly4 15407 fsumcube 15408 3dvdsdec 15675 3dvds2dec 15676 divalglem2 15740 3lcm2e6 16066 phiprmpw 16107 dec5dvds 16394 dec5dvds2 16395 dec2nprm 16397 modxai 16398 mod2xi 16399 mod2xnegi 16401 modsubi 16402 gcdi 16403 decexp2 16405 numexp0 16406 numexp1 16407 numexpp1 16408 numexp2x 16409 decsplit0b 16410 decsplit0 16411 decsplit1 16412 decsplit 16413 karatsuba 16414 2exp8 16417 prmlem2 16447 83prm 16450 139prm 16451 163prm 16452 631prm 16454 1259lem1 16458 1259lem2 16459 1259lem3 16460 1259lem4 16461 1259lem5 16462 1259prm 16463 2503lem1 16464 2503lem2 16465 2503lem3 16466 2503prm 16467 4001lem1 16468 4001lem2 16469 4001lem3 16470 4001lem4 16471 4001prm 16472 log2ublem1 25518 log2ublem2 25519 log2ublem3 25520 log2ub 25521 birthday 25526 ppidif 25734 bpos1lem 25852 9p10ne21 28243 dfdec100 30541 dp20u 30549 dp20h 30550 dpmul10 30566 dpmul100 30568 dp3mul10 30569 dpmul1000 30570 dpexpp1 30579 0dp2dp 30580 dpadd2 30581 dpadd 30582 dpmul 30584 dpmul4 30585 lmatfvlem 31075 ballotlemfp1 31744 ballotth 31790 reprlt 31885 hgt750lemd 31914 hgt750lem2 31918 subfacp1lem1 32421 poimirlem26 34912 poimirlem28 34914 decaddcom 39163 sqn5i 39164 decpmulnc 39166 decpmul 39167 sqdeccom12 39168 sq3deccom12 39169 235t711 39170 ex-decpmul 39171 inductionexd 40498 unitadd 40541 fmtno5lem4 43712 257prm 43717 fmtno4prmfac 43728 fmtno5fac 43738 139prmALT 43753 127prm 43757 m11nprm 43760 11t31e341 43891 2exp340mod341 43892 |
Copyright terms: Public domain | W3C validator |