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 12351 | . 2 ⊢ ℕ0 ⊆ ℂ | |
2 | nn0rei.1 | . 2 ⊢ 𝐴 ∈ ℕ0 | |
3 | 1, 2 | sselii 3939 | 1 ⊢ 𝐴 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 ℂcc 10982 ℕ0cn0 12346 |
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 2708 ax-sep 5254 ax-nul 5261 ax-pr 5382 ax-un 7662 ax-1cn 11042 ax-icn 11043 ax-addcl 11044 ax-mulcl 11046 ax-i2m1 11052 |
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 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-reu 3352 df-rab 3406 df-v 3445 df-sbc 3738 df-csb 3854 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3927 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-iun 4954 df-br 5104 df-opab 5166 df-mpt 5187 df-tr 5221 df-id 5528 df-eprel 5534 df-po 5542 df-so 5543 df-fr 5585 df-we 5587 df-xp 5636 df-rel 5637 df-cnv 5638 df-co 5639 df-dm 5640 df-rn 5641 df-res 5642 df-ima 5643 df-pred 6249 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6443 df-fun 6493 df-fn 6494 df-f 6495 df-f1 6496 df-fo 6497 df-f1o 6498 df-fv 6499 df-ov 7352 df-om 7793 df-2nd 7912 df-frecs 8179 df-wrecs 8210 df-recs 8284 df-rdg 8323 df-nn 12087 df-n0 12347 |
This theorem is referenced by: nn0le2xi 12400 num0u 12561 num0h 12562 numsuc 12564 numsucc 12590 numma 12594 nummac 12595 numma2c 12596 numadd 12597 numaddc 12598 nummul1c 12599 nummul2c 12600 decrmanc 12607 decrmac 12608 decaddi 12610 decaddci 12611 decsubi 12613 decmul1 12614 decmulnc 12617 11multnc 12618 decmul10add 12619 6p5lem 12620 4t3lem 12647 7t3e21 12660 7t6e42 12663 8t3e24 12666 8t4e32 12667 8t8e64 12671 9t3e27 12673 9t4e36 12674 9t5e45 12675 9t6e54 12676 9t7e63 12677 9t11e99 12680 decbin0 12690 decbin2 12691 sq10 14091 3dec 14093 nn0le2msqi 14094 nn0opthlem1 14095 nn0opthi 14097 nn0opth2i 14098 faclbnd4lem1 14120 cats1fvn 14678 bpoly4 15876 fsumcube 15877 3dvdsdec 16148 3dvds2dec 16149 divalglem2 16211 3lcm2e6 16541 phiprmpw 16582 dec5dvds 16870 dec5dvds2 16871 dec2nprm 16873 modxai 16874 mod2xi 16875 mod2xnegi 16877 modsubi 16878 gcdi 16879 decexp2 16881 numexp0 16882 numexp1 16883 numexpp1 16884 numexp2x 16885 decsplit0b 16886 decsplit0 16887 decsplit1 16888 decsplit 16889 karatsuba 16890 2exp8 16895 prmlem2 16926 83prm 16929 139prm 16930 163prm 16931 631prm 16933 1259lem1 16937 1259lem2 16938 1259lem3 16939 1259lem4 16940 1259lem5 16941 1259prm 16942 2503lem1 16943 2503lem2 16944 2503lem3 16945 2503prm 16946 4001lem1 16947 4001lem2 16948 4001lem3 16949 4001lem4 16950 4001prm 16951 log2ublem1 26218 log2ublem2 26219 log2ublem3 26220 log2ub 26221 birthday 26226 ppidif 26434 bpos1lem 26552 9p10ne21 29212 dfdec100 31520 dp20u 31528 dp20h 31529 dpmul10 31545 dpmul100 31547 dp3mul10 31548 dpmul1000 31549 dpexpp1 31558 0dp2dp 31559 dpadd2 31560 dpadd 31561 dpmul 31563 dpmul4 31564 lmatfvlem 32169 ballotlemfp1 32864 ballotth 32910 reprlt 33005 hgt750lemd 33034 hgt750lem2 33038 subfacp1lem1 33546 poimirlem26 35999 poimirlem28 36001 420gcd8e4 40358 lcmeprodgcdi 40359 12lcm5e60 40360 60lcm7e420 40362 3exp7 40405 3lexlogpow5ineq1 40406 3lexlogpow5ineq5 40412 aks4d1p1p7 40426 aks4d1p1 40428 decaddcom 40666 sqn5i 40667 decpmulnc 40669 decpmul 40670 sqdeccom12 40671 sq3deccom12 40672 235t711 40673 ex-decpmul 40674 resqrtvalex 41679 imsqrtvalex 41680 inductionexd 42191 unitadd 42232 fmtno5lem4 45497 257prm 45502 fmtno4prmfac 45513 fmtno5fac 45523 139prmALT 45537 127prm 45540 m11nprm 45542 11t31e341 45673 2exp340mod341 45674 ackval3012 46527 |
Copyright terms: Public domain | W3C validator |