![]() |
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 12529 | . 2 ⊢ ℕ0 ⊆ ℂ | |
2 | nn0rei.1 | . 2 ⊢ 𝐴 ∈ ℕ0 | |
3 | 1, 2 | sselii 3976 | 1 ⊢ 𝐴 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 ℂcc 11156 ℕ0cn0 12524 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5304 ax-nul 5311 ax-pr 5433 ax-un 7746 ax-1cn 11216 ax-icn 11217 ax-addcl 11218 ax-mulcl 11220 ax-i2m1 11226 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-ral 3052 df-rex 3061 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3967 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-iun 5003 df-br 5154 df-opab 5216 df-mpt 5237 df-tr 5271 df-id 5580 df-eprel 5586 df-po 5594 df-so 5595 df-fr 5637 df-we 5639 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-pred 6312 df-ord 6379 df-on 6380 df-lim 6381 df-suc 6382 df-iota 6506 df-fun 6556 df-fn 6557 df-f 6558 df-f1 6559 df-fo 6560 df-f1o 6561 df-fv 6562 df-ov 7427 df-om 7877 df-2nd 8004 df-frecs 8296 df-wrecs 8327 df-recs 8401 df-rdg 8440 df-nn 12265 df-n0 12525 |
This theorem is referenced by: nn0le2xi 12578 num0u 12740 num0h 12741 numsuc 12743 numsucc 12769 numma 12773 nummac 12774 numma2c 12775 numadd 12776 numaddc 12777 nummul1c 12778 nummul2c 12779 decrmanc 12786 decrmac 12787 decaddi 12789 decaddci 12790 decsubi 12792 decmul1 12793 decmulnc 12796 11multnc 12797 decmul10add 12798 6p5lem 12799 4t3lem 12826 7t3e21 12839 7t6e42 12842 8t3e24 12845 8t4e32 12846 8t8e64 12850 9t3e27 12852 9t4e36 12853 9t5e45 12854 9t6e54 12855 9t7e63 12856 9t11e99 12859 decbin0 12869 decbin2 12870 sq10 14281 3dec 14283 nn0le2msqi 14284 nn0opthlem1 14285 nn0opthi 14287 nn0opth2i 14288 faclbnd4lem1 14310 cats1fvn 14867 bpoly4 16061 fsumcube 16062 3dvdsdec 16334 3dvds2dec 16335 divalglem2 16397 3lcm2e6 16734 phiprmpw 16778 dec5dvds 17066 dec5dvds2 17067 dec2nprm 17069 modxai 17070 mod2xi 17071 mod2xnegi 17073 modsubi 17074 gcdi 17075 decexp2 17077 numexp0 17078 numexp1 17079 numexpp1 17080 numexp2x 17081 decsplit0b 17082 decsplit0 17083 decsplit1 17084 decsplit 17085 karatsuba 17086 2exp8 17091 prmlem2 17122 83prm 17125 139prm 17126 163prm 17127 631prm 17129 1259lem1 17133 1259lem2 17134 1259lem3 17135 1259lem4 17136 1259lem5 17137 1259prm 17138 2503lem1 17139 2503lem2 17140 2503lem3 17141 2503prm 17142 4001lem1 17143 4001lem2 17144 4001lem3 17145 4001lem4 17146 4001prm 17147 psdmul 22160 log2ublem1 26974 log2ublem2 26975 log2ublem3 26976 log2ub 26977 birthday 26982 ppidif 27191 bpos1lem 27311 9p10ne21 30403 dfdec100 32731 dp20u 32739 dp20h 32740 dpmul10 32756 dpmul100 32758 dp3mul10 32759 dpmul1000 32760 dpexpp1 32769 0dp2dp 32770 dpadd2 32771 dpadd 32772 dpmul 32774 dpmul4 32775 lmatfvlem 33630 ballotlemfp1 34325 ballotth 34371 reprlt 34465 hgt750lemd 34494 hgt750lem2 34498 subfacp1lem1 35007 poimirlem26 37347 poimirlem28 37349 420gcd8e4 41705 lcmeprodgcdi 41706 12lcm5e60 41707 60lcm7e420 41709 3exp7 41752 3lexlogpow5ineq1 41753 3lexlogpow5ineq5 41759 aks4d1p1p7 41773 aks4d1p1 41775 decaddcom 42097 sqn5i 42098 decpmulnc 42100 decpmul 42101 sqdeccom12 42102 sq3deccom12 42103 235t711 42106 ex-decpmul 42107 sq45 42325 sum9cubes 42326 resqrtvalex 43312 imsqrtvalex 43313 inductionexd 43822 unitadd 43862 fmtno5lem4 47128 257prm 47133 fmtno4prmfac 47144 fmtno5fac 47154 139prmALT 47168 127prm 47171 m11nprm 47173 11t31e341 47304 2exp340mod341 47305 ackval3012 48080 |
Copyright terms: Public domain | W3C validator |