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 12352 | . 2 ⊢ ℕ0 ⊆ ℂ | |
2 | nn0rei.1 | . 2 ⊢ 𝐴 ∈ ℕ0 | |
3 | 1, 2 | sselii 3940 | 1 ⊢ 𝐴 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 ℂcc 10983 ℕ0cn0 12347 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2709 ax-sep 5255 ax-nul 5262 ax-pr 5383 ax-un 7663 ax-1cn 11043 ax-icn 11044 ax-addcl 11045 ax-mulcl 11047 ax-i2m1 11053 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2888 df-ne 2943 df-ral 3064 df-rex 3073 df-reu 3353 df-rab 3407 df-v 3446 df-sbc 3739 df-csb 3855 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-pss 3928 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-iun 4955 df-br 5105 df-opab 5167 df-mpt 5188 df-tr 5222 df-id 5529 df-eprel 5535 df-po 5543 df-so 5544 df-fr 5586 df-we 5588 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6250 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6444 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7353 df-om 7794 df-2nd 7913 df-frecs 8180 df-wrecs 8211 df-recs 8285 df-rdg 8324 df-nn 12088 df-n0 12348 |
This theorem is referenced by: nn0le2xi 12401 num0u 12562 num0h 12563 numsuc 12565 numsucc 12591 numma 12595 nummac 12596 numma2c 12597 numadd 12598 numaddc 12599 nummul1c 12600 nummul2c 12601 decrmanc 12608 decrmac 12609 decaddi 12611 decaddci 12612 decsubi 12614 decmul1 12615 decmulnc 12618 11multnc 12619 decmul10add 12620 6p5lem 12621 4t3lem 12648 7t3e21 12661 7t6e42 12664 8t3e24 12667 8t4e32 12668 8t8e64 12672 9t3e27 12674 9t4e36 12675 9t5e45 12676 9t6e54 12677 9t7e63 12678 9t11e99 12681 decbin0 12691 decbin2 12692 sq10 14092 3dec 14094 nn0le2msqi 14095 nn0opthlem1 14096 nn0opthi 14098 nn0opth2i 14099 faclbnd4lem1 14121 cats1fvn 14679 bpoly4 15877 fsumcube 15878 3dvdsdec 16149 3dvds2dec 16150 divalglem2 16212 3lcm2e6 16542 phiprmpw 16583 dec5dvds 16871 dec5dvds2 16872 dec2nprm 16874 modxai 16875 mod2xi 16876 mod2xnegi 16878 modsubi 16879 gcdi 16880 decexp2 16882 numexp0 16883 numexp1 16884 numexpp1 16885 numexp2x 16886 decsplit0b 16887 decsplit0 16888 decsplit1 16889 decsplit 16890 karatsuba 16891 2exp8 16896 prmlem2 16927 83prm 16930 139prm 16931 163prm 16932 631prm 16934 1259lem1 16938 1259lem2 16939 1259lem3 16940 1259lem4 16941 1259lem5 16942 1259prm 16943 2503lem1 16944 2503lem2 16945 2503lem3 16946 2503prm 16947 4001lem1 16948 4001lem2 16949 4001lem3 16950 4001lem4 16951 4001prm 16952 log2ublem1 26218 log2ublem2 26219 log2ublem3 26220 log2ub 26221 birthday 26226 ppidif 26434 bpos1lem 26552 9p10ne21 29200 dfdec100 31508 dp20u 31516 dp20h 31517 dpmul10 31533 dpmul100 31535 dp3mul10 31536 dpmul1000 31537 dpexpp1 31546 0dp2dp 31547 dpadd2 31548 dpadd 31549 dpmul 31551 dpmul4 31552 lmatfvlem 32157 ballotlemfp1 32852 ballotth 32898 reprlt 32993 hgt750lemd 33022 hgt750lem2 33026 subfacp1lem1 33534 poimirlem26 35990 poimirlem28 35992 420gcd8e4 40349 lcmeprodgcdi 40350 12lcm5e60 40351 60lcm7e420 40353 3exp7 40396 3lexlogpow5ineq1 40397 3lexlogpow5ineq5 40403 aks4d1p1p7 40417 aks4d1p1 40419 decaddcom 40645 sqn5i 40646 decpmulnc 40648 decpmul 40649 sqdeccom12 40650 sq3deccom12 40651 235t711 40652 ex-decpmul 40653 resqrtvalex 41648 imsqrtvalex 41649 inductionexd 42160 unitadd 42201 fmtno5lem4 45448 257prm 45453 fmtno4prmfac 45464 fmtno5fac 45474 139prmALT 45488 127prm 45491 m11nprm 45493 11t31e341 45624 2exp340mod341 45625 ackval3012 46478 |
Copyright terms: Public domain | W3C validator |