![]() |
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 11710 | . 2 ⊢ ℕ0 ⊆ ℂ | |
2 | nn0rei.1 | . 2 ⊢ 𝐴 ∈ ℕ0 | |
3 | 1, 2 | sselii 3848 | 1 ⊢ 𝐴 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2051 ℂcc 10331 ℕ0cn0 11705 |
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 2743 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 ax-1cn 10391 ax-icn 10392 ax-addcl 10393 ax-mulcl 10395 ax-i2m1 10401 |
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 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-ne 2961 df-ral 3086 df-rex 3087 df-reu 3088 df-rab 3090 df-v 3410 df-sbc 3675 df-csb 3780 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-pss 3838 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4709 df-iun 4790 df-br 4926 df-opab 4988 df-mpt 5005 df-tr 5027 df-id 5308 df-eprel 5313 df-po 5322 df-so 5323 df-fr 5362 df-we 5364 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-pred 5983 df-ord 6029 df-on 6030 df-lim 6031 df-suc 6032 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-ov 6977 df-om 7395 df-wrecs 7748 df-recs 7810 df-rdg 7848 df-nn 11438 df-n0 11706 |
This theorem is referenced by: nn0le2xi 11761 num0u 11920 num0h 11921 numsuc 11923 numsucc 11950 numma 11954 nummac 11955 numma2c 11956 numadd 11957 numaddc 11958 nummul1c 11959 nummul2c 11960 decrmanc 11967 decrmac 11968 decaddi 11970 decaddci 11971 decsubi 11973 decmul1 11974 decmul1OLD 11975 decmulnc 11978 11multnc 11979 decmul10add 11980 6p5lem 11981 4t3lem 12008 7t3e21 12021 7t6e42 12024 8t3e24 12027 8t4e32 12028 8t8e64 12032 9t3e27 12034 9t4e36 12035 9t5e45 12036 9t6e54 12037 9t7e63 12038 9t11e99 12041 decbin0 12051 decbin2 12052 sq10 13437 3dec 13439 nn0le2msqi 13440 nn0opthlem1 13441 nn0opthi 13443 nn0opth2i 13444 faclbnd4lem1 13466 cats1fvn 14080 bpoly4 15271 fsumcube 15272 3dvdsdec 15539 3dvds2dec 15540 divalglem2 15604 3lcm2e6 15926 phiprmpw 15967 dec5dvds 16254 dec5dvds2 16255 dec2nprm 16257 modxai 16258 mod2xi 16259 mod2xnegi 16261 modsubi 16262 gcdi 16263 decexp2 16265 numexp0 16266 numexp1 16267 numexpp1 16268 numexp2x 16269 decsplit0b 16270 decsplit0 16271 decsplit1 16272 decsplit 16273 karatsuba 16274 2exp8 16277 prmlem2 16307 83prm 16310 139prm 16311 163prm 16312 631prm 16314 1259lem1 16318 1259lem2 16319 1259lem3 16320 1259lem4 16321 1259lem5 16322 1259prm 16323 2503lem1 16324 2503lem2 16325 2503lem3 16326 2503prm 16327 4001lem1 16328 4001lem2 16329 4001lem3 16330 4001lem4 16331 4001prm 16332 log2ublem1 25241 log2ublem2 25242 log2ublem3 25243 log2ub 25244 birthday 25249 ppidif 25457 bpos1lem 25575 9p10ne21 28041 dfdec100 30316 dp20u 30324 dp20h 30325 dpmul10 30341 dpmul100 30343 dp3mul10 30344 dpmul1000 30345 dpexpp1 30354 0dp2dp 30355 dpadd2 30356 dpadd 30357 dpmul 30359 dpmul4 30360 lmatfvlem 30754 ballotlemfp1 31427 ballotth 31473 reprlt 31570 hgt750lemd 31599 hgt750lem2 31603 subfacp1lem1 32048 poimirlem26 34396 poimirlem28 34398 decaddcom 38640 sqn5i 38641 decpmulnc 38643 decpmul 38644 sqdeccom12 38645 sq3deccom12 38646 235t711 38647 ex-decpmul 38648 inductionexd 39906 unitadd 39951 fmtno5lem4 43120 257prm 43125 fmtno4prmfac 43136 fmtno5fac 43146 139prmALT 43161 127prm 43165 m11nprm 43168 11t31e341 43299 2exp340mod341 43300 |
Copyright terms: Public domain | W3C validator |