Theorem recn 10026

Description: A real number is a complex number. (Contributed by NM, 10-Aug-1999.)

Assertion

Ref	Expression
recn	|- ( A e. RR -> A e. CC )

Proof of Theorem recn

Step	Hyp	Ref	Expression
1		ax-resscn 9993	. 2 |- RR C_ CC
2	1	sseli 3599	1 |- ( A e. RR -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 1990   CCcc 9934   RRcr 9935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  mulid1  10037  recnd  10068  pnfnre  10081  mnfnre  10082  mul02  10214  ltaddneg  10251  ltaddnegr  10252  renegcli  10342  resubcl  10345  negn0  10459  negf1o  10460  ltaddsub2  10503  leaddsub2  10505  leltadd  10512  ltaddpos  10518  ltaddpos2  10519  posdif  10521  lenegcon1  10532  lenegcon2  10533  addge01  10538  addge02  10539  leaddle0  10543  mullt0  10547  recex  10659  ltm1  10863  prodgt02  10869  prodge02  10871  ltmul2  10874  lemul1  10875  lemul2  10876  lemul1a  10877  lemul2a  10878  ltmulgt12  10884  lemulge12  10886  gt0div  10889  ge0div  10890  mulge0b  10893  mulle0b  10894  ltmuldiv2  10897  ltdivmul  10898  ledivmul  10899  ltdivmul2  10900  lt2mul2div  10901  ledivmul2  10902  lemuldiv2  10904  ltdiv2  10909  ltrec1  10910  lerec2  10911  ledivdiv  10912  lediv2  10913  ltdiv23  10914  lediv23  10915  lediv12a  10916  recp1lt1  10921  ledivp1  10925  negfi  10971  fiminre  10972  infm3lem  10981  supmul  10995  riotaneg  11002  negiso  11003  cju  11016  nnge1  11046  halfpos  11262  lt2halves  11267  addltmul  11268  avgle1  11272  avgle2  11273  avgle  11274  div4p1lem1div2  11287  nnrecl  11290  difgtsumgt  11346  elznn0  11392  elznn  11393  elz2  11394  nzadd  11425  zmulcl  11426  gtndiv  11454  zeo  11463  eqreznegel  11774  supminf  11775  rebtwnz  11787  irradd  11812  irrmul  11813  divlt1lt  11899  divle1le  11900  max0sub  12027  xnegneg  12045  rexsub  12064  xnegid  12069  xaddcom  12071  xaddid1  12072  xnegdi  12078  xaddass  12079  rexmul  12101  xmulasslem3  12116  xadddilem  12124  divelunit  12314  fzonmapblen  12513  ico01fl0  12620  flzadd  12627  ltdifltdiv  12635  dfceil2  12640  intfrac2  12657  fldiv2  12660  flpmodeq  12673  mod0  12675  negmod0  12677  modlt  12679  modfrac  12683  flmod  12684  intfrac  12685  modmulnn  12688  modvalp1  12689  modid  12695  modcyc  12705  modcyc2  12706  modadd1  12707  modaddabs  12708  muladdmodid  12710  negmod  12715  modadd2mod  12720  modmul1  12723  modmulmodr  12736  modaddmulmod  12737  moddi  12738  modsubdir  12739  modirr  12741  addmodlteq  12745  expgt1  12898  mulexpz  12900  leexp1a  12919  expubnd  12921  sqgt0  12932  lt2sq  12937  le2sq  12938  sqge0  12940  sumsqeq0  12942  sqlecan  12971  bernneq  12990  bernneq2  12991  expnbnd  12993  digit2  12997  digit1  12998  swrdccatin2  13487  swrdccat3blem  13495  cshweqrep  13567  crre  13854  crim  13855  reim0  13858  mulre  13861  rere  13862  remul2  13870  rediv  13871  immul2  13877  imdiv  13878  cjre  13879  cjreim  13900  rennim  13979  resqrex  13991  resqreu  13993  resqrtcl  13994  resqrtthlem  13995  sqrtneglem  14007  sqrtneg  14008  absreimsq  14032  absreim  14033  absnid  14038  leabs  14039  absre  14041  absresq  14042  sqabs  14047  max0add  14050  absz  14051  absdiflt  14057  absdifle  14058  lenegsq  14060  abssuble0  14068  absmax  14069  rddif  14080  absrdbnd  14081  o1rlimmul  14349  caurcvg2  14408  reefcl  14817  efgt0  14833  reeftlcl  14838  resinval  14865  recosval  14866  resin4p  14868  recos4p  14869  resincl  14870  recoscl  14871  retancl  14872  resinhcl  14886  rpcoshcl  14887  retanhcl  14889  tanhlt1  14890  tanhbnd  14891  efieq  14893  sinbnd  14910  cosbnd  14911  absefi  14926  dvdsaddre2b  15029  odd2np1  15065  bezoutlem1  15256  xrsdsreclb  19793  remulg  19953  resubdrg  19954  remetdval  22592  bl2ioo  22595  ioo2bl  22596  cnperf  22623  icccvx  22749  tchcph  23036  shft2rab  23276  volsup2  23373  volcn  23374  c1lip1  23760  plyreres  24038  aalioulem3  24089  taylthlem2  24128  reeff1o  24201  reefgim  24204  sincosq1sgn  24250  sincosq2sgn  24251  sincosq3sgn  24252  sincosq4sgn  24253  sinq12gt0  24259  pige3  24269  efif1olem4  24291  efifo  24293  relogrn  24308  logrnaddcl  24321  relogoprlem  24337  advlog  24400  advlogexp  24401  logtayl  24406  recxpcl  24421  rpcxpcl  24422  cxpge0  24429  dvcxp1  24481  logreclem  24500  relogbreexp  24513  relogbcxp  24523  angpieqvd  24558  atanre  24612  basellem9  24815  gausslemma2dlem1a  25090  log2sumbnd  25233  brbtwn2  25785  colinearalglem4  25789  colinearalg  25790  crctcshwlkn0lem1  26702  nvsge0  27519  nmoub3i  27628  nmlnoubi  27651  isblo3i  27656  ipasslem3  27688  ipasslem9  27693  ipasslem11  27695  hmopm  28880  riesz1  28924  leopmuli  28992  leopmul  28993  leopmul2i  28994  leopnmid  28997  nmopleid  28998  cdj1i  29292  cdj3lem1  29293  cdj3i  29300  addltmulALT  29305  dpfrac1  29599  dpfrac1OLD  29600  rexdiv  29634  xdivid  29636  xdiv0  29637  rmulccn  29974  sgnneg  30602  lediv2aALT  31571  nndivlub  32457  cos2h  33400  tan2h  33401  poimir  33442  mblfinlem2  33447  mblfinlem4  33449  itg2addnclem  33461  itg2addnclem2  33462  dvasin  33496  areacirclem1  33500  areacirclem2  33501  areacirclem4  33503  areacirclem5  33504  areacirc  33505  expmordi  37512  areaquad  37802  radcnvrat  38513  lhe4.4ex1a  38528  expgrowthi  38532  mulltgt0  39181  refsum2cnlem1  39196  infnsuprnmpt  39465  dstregt0  39493  suplesup  39555  infleinflem1  39586  infleinflem2  39587  ltdiv23neg  39617  rexabslelem  39645  supminfrnmpt  39672  supminfxr  39694  fmul01lt1lem1  39816  lptre2pt  39872  cnrefiisplem  40055  dvcosre  40126  itgsin0pilem1  40165  itgsinexplem1  40169  volioc  40188  volico  40200  stoweidlem7  40224  stoweidlem10  40227  stoweidlem19  40236  stoweidlem34  40251  stoweid  40280  dirker2re  40309  dirkerdenne0  40310  dirkerper  40313  dirkertrigeq  40318  dirkeritg  40319  fourierdlem39  40363  fourierdlem42  40366  fourierdlem47  40370  fourierdlem56  40379  fourierdlem57  40380  fourierdlem58  40381  fourierdlem60  40383  fourierdlem61  40384  fourierdlem73  40396  fourierdlem76  40399  fourierdlem77  40400  fourierdlem92  40415  fourierdlem97  40420  etransclem46  40497  volico2  40855  smflimlem4  40982  smfinflem  41023  2leaddle2  41312  ltsubsubaddltsub  41315  m1mod0mod1  41339  bgoldbtbndlem2  41694  flsubz  42312  rege1logbrege0  42352  nn0digval  42394  reseccl  42494  recsccl  42495  recotcl  42496