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.) |
Ref | Expression |
---|---|
nn0rei.1 | ⊢ 𝐴 ∈ ℕ0 |
Ref | Expression |
---|---|
nn0cni | ⊢ 𝐴 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0rei.1 | . . 3 ⊢ 𝐴 ∈ ℕ0 | |
2 | 1 | nn0rei 11180 | . 2 ⊢ 𝐴 ∈ ℝ |
3 | 2 | recni 9931 | 1 ⊢ 𝐴 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1977 ℂcc 9813 ℕ0cn0 11169 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-i2m1 9883 ax-1ne0 9884 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-ov 6552 df-om 6958 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-nn 10898 df-n0 11170 |
This theorem is referenced by: nn0le2xi 11224 num0u 11384 num0h 11385 numsuc 11387 numsucc 11425 numma 11433 nummac 11434 numma2c 11435 numadd 11436 numaddc 11437 nummul1c 11438 nummul2c 11439 decrmanc 11452 decrmac 11453 decaddi 11455 decaddci 11456 decsubi 11459 decsubiOLD 11460 decmul1 11461 decmul1OLD 11462 decmulnc 11467 11multnc 11468 decmul10add 11469 decmul10addOLD 11470 6p5lem 11471 4t3lem 11507 6t5e30OLD 11521 7t3e21 11525 7t6e42 11528 8t3e24 11531 8t4e32 11532 8t8e64 11538 9t3e27 11540 9t4e36 11541 9t5e45 11542 9t6e54 11543 9t7e63 11544 9t11e99 11547 decbin0 11558 decbin2 11559 sq10 12910 3dec 12912 3decOLD 12915 nn0le2msqi 12916 nn0opthlem1 12917 nn0opthi 12919 nn0opth2i 12920 faclbnd4lem1 12942 cats1fvn 13454 bpoly4 14629 fsumcube 14630 3dvdsdec 14892 3dvdsdecOLD 14893 3dvds2dec 14894 3dvds2decOLD 14895 divalglem2 14956 3lcm2e6 15278 phiprmpw 15319 dec5dvds 15606 dec5dvds2 15607 dec2nprm 15609 modxai 15610 mod2xi 15611 mod2xnegi 15613 modsubi 15614 gcdi 15615 decexp2 15617 numexp0 15618 numexp1 15619 numexpp1 15620 numexp2x 15621 decsplit0b 15622 decsplit0 15623 decsplit1 15624 decsplit 15625 decsplit0bOLD 15626 decsplit0OLD 15627 decsplit1OLD 15628 decsplitOLD 15629 karatsuba 15630 karatsubaOLD 15631 2exp8 15634 prmlem2 15665 83prm 15668 139prm 15669 163prm 15670 631prm 15672 1259lem1 15676 1259lem2 15677 1259lem3 15678 1259lem4 15679 1259lem5 15680 1259prm 15681 2503lem1 15682 2503lem2 15683 2503lem3 15684 2503prm 15685 4001lem1 15686 4001lem2 15687 4001lem3 15688 4001lem4 15689 4001prm 15690 log2ublem1 24473 log2ublem2 24474 log2ublem3 24475 log2ub 24476 birthday 24481 ppidif 24689 bpos1lem 24807 vdegp1ai 26511 lmatfvlem 29209 ballotlemfp1 29880 ballotth 29926 subfacp1lem1 30415 poimirlem26 32605 poimirlem28 32607 inductionexd 37473 unitadd 37520 fmtno5lem4 40006 257prm 40011 fmtno4prmfac 40022 fmtno5fac 40032 139prmALT 40049 127prm 40053 m11nprm 40056 |
Copyright terms: Public domain | W3C validator |