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

Theorem nncnd 8757
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 8748 . 2  |-  NN  C_  CC
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3099 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1481   CCcc 7641   NNcn 8743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4053  ax-cnex 7734  ax-resscn 7735  ax-1re 7737  ax-addrcl 7740
This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-v 2691  df-in 3081  df-ss 3088  df-int 3779  df-inn 8744
This theorem is referenced by:  peano5uzti  9182  qapne  9457  qtri3or  10050  exbtwnzlemstep  10055  intfracq  10123  flqdiv  10124  modqmulnn  10145  addmodid  10175  modaddmodup  10190  modsumfzodifsn  10199  addmodlteq  10201  facdiv  10515  facndiv  10516  faclbnd  10518  faclbnd6  10521  facubnd  10522  facavg  10523  bccmpl  10531  bcn0  10532  bcn1  10535  bcm1k  10537  bcp1n  10538  bcp1nk  10539  bcval5  10540  bcpasc  10543  permnn  10548  cvg1nlemcxze  10785  cvg1nlemcau  10787  resqrexlemcalc3  10819  binom11  11286  binom1dif  11287  divcnv  11297  arisum2  11299  trireciplem  11300  trirecip  11301  expcnvap0  11302  geo2sum  11314  geo2lim  11316  cvgratnnlembern  11323  cvgratnnlemnexp  11324  cvgratnnlemmn  11325  cvgratnnlemsumlt  11328  cvgratnnlemfm  11329  cvgratnnlemrate  11330  cvgratz  11332  eftcl  11395  eftabs  11397  efcllemp  11399  ege2le3  11412  efcj  11414  efaddlem  11415  eftlub  11431  eirraplem  11517  oexpneg  11608  divalglemnn  11649  dvdsgcdidd  11716  bezoutlemnewy  11718  mulgcd  11738  rplpwr  11749  sqgcd  11751  lcmgcdlem  11792  3lcm2e6woprm  11801  cncongr1  11818  cncongr2  11819  prmind2  11835  divgcdodd  11855  prmdvdsexpr  11862  sqrt2irrlem  11873  oddpwdclemxy  11881  oddpwdclemodd  11884  oddpwdclemdc  11885  oddpwdc  11886  sqpweven  11887  2sqpwodd  11888  sqrt2irraplemnn  11891  sqrt2irrap  11892  qmuldeneqnum  11907  divnumden  11908  qnumgt0  11910  numdensq  11914  hashdvds  11931  phiprmpw  11932  oddennn  11939  evenennn  11940  logbgcd1irraplemap  13092  trilpolemeq1  13406  trilpolemlt1  13407  redcwlpolemeq1  13419
  Copyright terms: Public domain W3C validator