ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nncnd Unicode version

Theorem nncnd 8109
Description: A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nnred.1  |-  ( ph  ->  A  e.  NN )
Assertion
Ref Expression
nncnd  |-  ( ph  ->  A  e.  CC )

Proof of Theorem nncnd
StepHypRef Expression
1 nnsscn 8100 . 2  |-  NN  C_  CC
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 2998 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434   CCcc 7030   NNcn 8095
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-sep 3898  ax-cnex 7118  ax-resscn 7119  ax-1re 7121  ax-addrcl 7124
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ral 2354  df-v 2604  df-in 2980  df-ss 2987  df-int 3639  df-inn 8096
This theorem is referenced by:  peano5uzti  8525  qapne  8794  qtri3or  9318  exbtwnzlemstep  9323  intfracq  9391  flqdiv  9392  modqmulnn  9413  addmodid  9443  modaddmodup  9458  modsumfzodifsn  9467  addmodlteq  9469  facdiv  9751  facndiv  9752  faclbnd  9754  faclbnd6  9757  facubnd  9758  facavg  9759  bccmpl  9767  bcn0  9768  bcn1  9771  bcm1k  9773  bcp1n  9774  bcp1nk  9775  ibcval5  9776  bcpasc  9779  permnn  9784  cvg1nlemcxze  9995  cvg1nlemcau  9997  resqrexlemcalc3  10029  oexpneg  10410  divalglemnn  10451  bezoutlemnewy  10518  mulgcd  10538  rplpwr  10549  sqgcd  10551  lcmgcdlem  10592  3lcm2e6woprm  10601  cncongr1  10618  cncongr2  10619  prmind2  10635  divgcdodd  10655  prmdvdsexpr  10662  sqrt2irrlem  10673  oddpwdclemxy  10680  oddpwdclemodd  10683  oddpwdclemdc  10684  oddpwdc  10685  sqpweven  10686  2sqpwodd  10687  sqrt2irraplemnn  10690  sqrt2irrap  10691  oddennn  10692
  Copyright terms: Public domain W3C validator