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

Theorem recn 9603
Description: A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
Assertion
Ref Expression
recn

Proof of Theorem recn
StepHypRef Expression
1 ax-resscn 9570 . 2
21sseli 3499 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cc 9511   cr 9512
This theorem is referenced by:  mulid1  9614  recnd  9643  pnfnre  9656  mnfnre  9657  mul02  9779  renegcli  9903  resubcl  9906  ltaddsub2  10052  leaddsub2  10054  leltadd  10061  ltaddpos  10067  ltaddpos2  10068  posdif  10070  lenegcon1  10081  lenegcon2  10082  addge01  10087  addge02  10088  leaddle0  10092  mullt0  10097  recex  10206  ltm1  10407  prodgt02  10413  prodge02  10415  ltmul2  10418  lemul1  10419  lemul2  10420  lemul1a  10421  lemul2a  10422  ltmulgt12  10428  lemulge12  10430  gt0div  10433  ge0div  10434  mulge0b  10437  mulle0b  10438  ltmuldiv2  10441  ltdivmul  10442  ledivmul  10443  ledivmulOLD  10444  ltdivmul2  10445  lt2mul2div  10446  ledivmul2  10447  ledivmul2OLD  10448  lemuldiv2  10450  ltdiv2  10455  ltrec1  10457  lerec2  10458  ledivdiv  10459  lediv2  10460  ltdiv23  10461  lediv23  10462  lediv12a  10463  recp1lt1  10468  ledivp1  10472  infm3lem  10526  supmul  10536  riotaneg  10543  negiso  10544  cju  10557  nnge1  10587  halfpos  10794  lt2halves  10798  addltmul  10799  avgle1  10803  avgle2  10804  avgle  10805  nnrecl  10818  elznn0  10904  elznn  10905  elz2  10906  zmulcl  10937  gtndiv  10965  zeo  10973  uzindOLD  10982  eqreznegel  11196  negn0  11197  supminf  11198  rebtwnz  11210  irradd  11235  irrmul  11236  max0sub  11424  xnegneg  11442  rexsub  11461  xnegid  11464  xaddcom  11466  xaddid1  11467  xnegdi  11469  xaddass  11470  rexmul  11492  xmulasslem3  11507  xadddilem  11515  divelunit  11691  fzonmapblen  11868  flzadd  11959  ltdifltdiv  11966  dfceil2  11968  intfrac2  11985  fldiv2  11988  flpmodeq  12001  mod0  12003  negmod0  12004  modlt  12006  modfrac  12009  flmod  12010  intfrac  12011  modmulnn  12013  modvalp1  12014  modid  12020  modcyc  12031  modcyc2  12032  modadd1  12033  modaddabs  12034  modadd2mod  12037  modmul1  12040  modaddmulmod  12053  moddi  12054  modsubdir  12055  modirr  12057  expgt1  12204  mulexpz  12206  leexp1a  12224  expubnd  12226  sqgt0  12236  lt2sq  12241  le2sq  12242  sqge0  12244  sumsqeq0  12246  sqlecan  12274  bernneq  12292  bernneq2  12293  expnbnd  12295  digit2  12299  digit1  12300  swrdccatin2  12712  swrdccat3blem  12720  cshweqrep  12789  crre  12947  crim  12948  reim0  12951  mulre  12954  rere  12955  remul2  12963  rediv  12964  immul2  12970  imdiv  12971  cjre  12972  cjreim  12993  rennim  13072  resqrex  13084  resqreu  13086  resqrtcl  13087  resqrtthlem  13088  sqrtneglem  13100  sqrtneg  13101  absreimsq  13125  absreim  13126  absnid  13131  leabs  13132  absre  13134  absresq  13135  sqabs  13140  max0add  13143  absz  13144  absdiflt  13150  absdifle  13151  lenegsq  13153  abssuble0  13161  absmax  13162  rddif  13173  absrdbnd  13174  o1rlimmul  13441  caurcvg2  13500  reefcl  13822  efgt0  13838  reeftlcl  13843  resinval  13870  recosval  13871  resin4p  13873  recos4p  13874  resincl  13875  recoscl  13876  retancl  13877  resinhcl  13891  rpcoshcl  13892  retanhcl  13894  tanhlt1  13895  tanhbnd  13896  efieq  13898  sinbnd  13915  cosbnd  13916  absefi  13931  odd2np1  14046  bezoutlem1  14176  xrsdsreclb  18465  remulg  18643  resubdrg  18644  remetdval  21294  bl2ioo  21297  ioo2bl  21298  cnperf  21325  icccvx  21450  tchcph  21680  shft2rab  21919  volsup2  22014  volcn  22015  c1lip1  22398  plyreres  22679  aalioulem3  22730  taylthlem2  22769  reeff1o  22842  reefgim  22845  sincosq1sgn  22891  sincosq2sgn  22892  sincosq3sgn  22893  sincosq4sgn  22894  sinq12gt0  22900  pige3  22910  efif1olem4  22932  efifo  22934  relogrn  22949  logrnaddcl  22962  relogoprlem  22975  advlog  23035  advlogexp  23036  logtayl  23041  recxpcl  23056  rpcxpcl  23057  cxpge0  23064  dvcxp1  23116  logreclem  23150  angpieqvd  23162  atanre  23216  basellem9  23362  log2sumbnd  23729  brbtwn2  24208  colinearalglem4  24212  colinearalg  24213  readdsubgo  25355  nvsge0  25566  nmoub3i  25688  nmlnoubi  25711  isblo3i  25716  ipasslem3  25748  ipasslem9  25753  ipasslem11  25755  hmopm  26940  riesz1  26984  leopmuli  27052  leopmul  27053  leopmul2i  27054  leopnmid  27057  nmopleid  27058  cdj1i  27352  cdj3lem1  27353  cdj3i  27360  addltmulALT  27365  rexdiv  27622  xdivid  27624  xdiv0  27625  rmulccn  27910  sgnneg  28479  lediv2aALT  29043  nndivlub  29923  cos2h  30046  tan2h  30047  mblfinlem2  30052  mblfinlem4  30054  dvtanlem  30064  itg2addnclem  30066  itg2addnclem2  30067  dvasin  30103  areacirclem1  30107  areacirclem2  30108  areacirclem4  30110  areacirclem5  30111  areacirc  30112  expmordi  30883  areaquad  31184  radcnvrat  31195  lhe4.4ex1a  31234  expgrowthi  31238  mulltgt0  31397  refsum2cnlem1  31412  dstregt0  31463  ltaddneg  31484  fmul01lt1lem1  31578  lptre2pt  31646  dvcosre  31706  itgsin0pilem1  31748  itgsinexplem1  31752  volioc  31771  stoweidlem7  31789  stoweidlem10  31792  stoweidlem19  31801  stoweidlem34  31816  stoweid  31845  dirker2re  31874  dirkerdenne0  31875  dirkerper  31878  dirkertrigeq  31883  dirkeritg  31884  fourierdlem39  31928  fourierdlem42  31931  fourierdlem47  31936  fourierdlem56  31945  fourierdlem57  31946  fourierdlem58  31947  fourierdlem60  31949  fourierdlem61  31950  fourierdlem73  31962  fourierdlem76  31965  fourierdlem77  31966  fourierdlem92  31981  fourierdlem97  31986  etransclem46  32063  2leaddle2  32320  ltsubsubaddltsub  32324  reseccl  33147  recsccl  33148  recotcl  33149  dpfrac1  33166  bj-flbi3  34608
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-resscn 9570
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator