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

Theorem nn0cni 10881
Description: A nonnegative integer is a complex number. (Contributed by NM, 14-May-2003.)
Hypothesis
Ref Expression
nn0rei.1  |-  A  e. 
NN0
Assertion
Ref Expression
nn0cni  |-  A  e.  CC

Proof of Theorem nn0cni
StepHypRef Expression
1 nn0rei.1 . . 3  |-  A  e. 
NN0
21nn0rei 10880 . 2  |-  A  e.  RR
32recni 9655 1  |-  A  e.  CC
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1868   CCcc 9537   NN0cn0 10869
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-i2m1 9607  ax-1ne0 9608  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-ov 6304  df-om 6703  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-nn 10610  df-n0 10870
This theorem is referenced by:  nn0le2xi  10921  num0u  11060  num0h  11061  numsuc  11063  numsucc  11077  numma  11082  nummac  11083  numma2c  11084  numadd  11085  numaddc  11086  nummul1c  11087  nummul2c  11088  decaddi  11095  decaddci  11096  6p5lem  11100  4t3lem  11122  6t5e30  11131  7t3e21  11134  7t6e42  11137  8t3e24  11140  8t4e32  11141  8t8e64  11145  9t3e27  11147  9t4e36  11148  9t5e45  11149  9t6e54  11150  9t7e63  11151  decbin0  11154  decbin2  11155  nn0le2msqi  12452  nn0opthlem1  12453  nn0opthi  12455  nn0opth2i  12456  faclbnd4lem1  12477  cats1fvn  12942  bpoly4  14097  fsumcube  14098  divalglem2  14358  divalglem2OLD  14359  3lcm2e6  14666  phiprmpw  14709  dec5dvds  15021  dec5dvds2  15022  dec2nprm  15024  modxai  15025  mod2xi  15026  mod2xnegi  15028  modsubi  15029  gcdi  15030  decexp2  15032  numexp0  15033  numexp1  15034  numexpp1  15035  numexp2x  15036  decsplit0b  15037  decsplit0  15038  decsplit1  15039  decsplit  15040  karatsuba  15041  2exp6OLD  15044  2exp8  15045  prmlem2  15076  83prm  15079  139prm  15080  163prm  15081  631prm  15083  1259lem1  15087  1259lem2  15088  1259lem3  15089  1259lem4  15090  1259lem5  15091  1259prm  15092  2503lem1  15093  2503lem2  15094  2503lem3  15095  2503prm  15096  4001lem1  15097  4001lem2  15098  4001lem3  15099  4001lem4  15100  4001prm  15101  log2ublem1  23856  log2ublem2  23857  log2ublem3  23858  log2ub  23859  birthday  23864  ppidif  24074  bpos1lem  24194  vdegp1ai  25695  lmatfvlem  28634  ballotlemfp1  29317  ballotth  29363  ballotthOLD  29401  subfacp1lem1  29895  poimirlem26  31877  poimirlem28  31879  inductionexd  36448  unitadd  36497
  Copyright terms: Public domain W3C validator