MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nn0cni Structured version   Visualization version   GIF version

Theorem nn0cni 11901
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.)
Hypothesis
Ref Expression
nn0rei.1 𝐴 ∈ ℕ0
Assertion
Ref Expression
nn0cni 𝐴 ∈ ℂ

Proof of Theorem nn0cni
StepHypRef Expression
1 nn0sscn 11894 . 2 0 ⊆ ℂ
2 nn0rei.1 . 2 𝐴 ∈ ℕ0
31, 2sselii 3915 1 𝐴 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  cc 10528  0cn0 11889
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-mulcl 10592  ax-i2m1 10598
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-nn 11630  df-n0 11890
This theorem is referenced by:  nn0le2xi  11943  num0u  12101  num0h  12102  numsuc  12104  numsucc  12130  numma  12134  nummac  12135  numma2c  12136  numadd  12137  numaddc  12138  nummul1c  12139  nummul2c  12140  decrmanc  12147  decrmac  12148  decaddi  12150  decaddci  12151  decsubi  12153  decmul1  12154  decmulnc  12157  11multnc  12158  decmul10add  12159  6p5lem  12160  4t3lem  12187  7t3e21  12200  7t6e42  12203  8t3e24  12206  8t4e32  12207  8t8e64  12211  9t3e27  12213  9t4e36  12214  9t5e45  12215  9t6e54  12216  9t7e63  12217  9t11e99  12220  decbin0  12230  decbin2  12231  sq10  13624  3dec  13626  nn0le2msqi  13627  nn0opthlem1  13628  nn0opthi  13630  nn0opth2i  13631  faclbnd4lem1  13653  cats1fvn  14215  bpoly4  15408  fsumcube  15409  3dvdsdec  15676  3dvds2dec  15677  divalglem2  15739  3lcm2e6  16065  phiprmpw  16106  dec5dvds  16393  dec5dvds2  16394  dec2nprm  16396  modxai  16397  mod2xi  16398  mod2xnegi  16400  modsubi  16401  gcdi  16402  decexp2  16404  numexp0  16405  numexp1  16406  numexpp1  16407  numexp2x  16408  decsplit0b  16409  decsplit0  16410  decsplit1  16411  decsplit  16412  karatsuba  16413  2exp8  16418  prmlem2  16448  83prm  16451  139prm  16452  163prm  16453  631prm  16455  1259lem1  16459  1259lem2  16460  1259lem3  16461  1259lem4  16462  1259lem5  16463  1259prm  16464  2503lem1  16465  2503lem2  16466  2503lem3  16467  2503prm  16468  4001lem1  16469  4001lem2  16470  4001lem3  16471  4001lem4  16472  4001prm  16473  log2ublem1  25535  log2ublem2  25536  log2ublem3  25537  log2ub  25538  birthday  25543  ppidif  25751  bpos1lem  25869  9p10ne21  28258  dfdec100  30575  dp20u  30583  dp20h  30584  dpmul10  30600  dpmul100  30602  dp3mul10  30603  dpmul1000  30604  dpexpp1  30613  0dp2dp  30614  dpadd2  30615  dpadd  30616  dpmul  30618  dpmul4  30619  lmatfvlem  31168  ballotlemfp1  31857  ballotth  31903  reprlt  31998  hgt750lemd  32027  hgt750lem2  32031  subfacp1lem1  32534  poimirlem26  35076  poimirlem28  35078  420gcd8e4  39287  lcmeprodgcdi  39288  12lcm5e60  39289  60lcm7e420  39291  3lexlogpow5ineq1  39334  decaddcom  39465  sqn5i  39466  decpmulnc  39468  decpmul  39469  sqdeccom12  39470  sq3deccom12  39471  235t711  39472  ex-decpmul  39473  resqrtvalex  40332  imsqrtvalex  40333  inductionexd  40845  unitadd  40888  fmtno5lem4  44060  257prm  44065  fmtno4prmfac  44076  fmtno5fac  44086  139prmALT  44100  127prm  44103  m11nprm  44106  11t31e341  44237  2exp340mod341  44238  ackval3012  45093
  Copyright terms: Public domain W3C validator