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

Theorem recn 9970
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 9937 . 2 ℝ ⊆ ℂ
21sseli 3579 1 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  cc 9878  cr 9879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-resscn 9937
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3562  df-ss 3569
This theorem is referenced by:  mulid1  9981  recnd  10012  pnfnre  10025  mnfnre  10026  mul02  10158  ltaddneg  10195  ltaddnegr  10196  renegcli  10286  resubcl  10289  negn0  10403  negf1o  10404  ltaddsub2  10447  leaddsub2  10449  leltadd  10456  ltaddpos  10462  ltaddpos2  10463  posdif  10465  lenegcon1  10476  lenegcon2  10477  addge01  10482  addge02  10483  leaddle0  10487  mullt0  10491  recex  10603  ltm1  10807  prodgt02  10813  prodge02  10815  ltmul2  10818  lemul1  10819  lemul2  10820  lemul1a  10821  lemul2a  10822  ltmulgt12  10828  lemulge12  10830  gt0div  10833  ge0div  10834  mulge0b  10837  mulle0b  10838  ltmuldiv2  10841  ltdivmul  10842  ledivmul  10843  ltdivmul2  10844  lt2mul2div  10845  ledivmul2  10846  lemuldiv2  10848  ltdiv2  10853  ltrec1  10854  lerec2  10855  ledivdiv  10856  lediv2  10857  ltdiv23  10858  lediv23  10859  lediv12a  10860  recp1lt1  10865  ledivp1  10869  negfi  10915  fiminre  10916  infm3lem  10925  supmul  10939  riotaneg  10946  negiso  10947  cju  10960  nnge1  10990  halfpos  11206  lt2halves  11211  addltmul  11212  avgle1  11216  avgle2  11217  avgle  11218  div4p1lem1div2  11231  nnrecl  11234  difgtsumgt  11290  elznn0  11336  elznn  11337  elz2  11338  nzadd  11369  zmulcl  11370  gtndiv  11398  zeo  11407  eqreznegel  11718  supminf  11719  rebtwnz  11731  irradd  11756  irrmul  11757  divlt1lt  11843  divle1le  11844  max0sub  11970  xnegneg  11988  rexsub  12007  xnegid  12012  xaddcom  12014  xaddid1  12015  xnegdi  12021  xaddass  12022  rexmul  12044  xmulasslem3  12059  xadddilem  12067  divelunit  12256  fzonmapblen  12454  ico01fl0  12560  flzadd  12567  ltdifltdiv  12575  dfceil2  12580  intfrac2  12597  fldiv2  12600  flpmodeq  12613  mod0  12615  negmod0  12617  modlt  12619  modfrac  12623  flmod  12624  intfrac  12625  modmulnn  12628  modvalp1  12629  modid  12635  modcyc  12645  modcyc2  12646  modadd1  12647  modaddabs  12648  muladdmodid  12650  negmod  12655  modadd2mod  12660  modmul1  12663  modmulmodr  12676  modaddmulmod  12677  moddi  12678  modsubdir  12679  modirr  12681  addmodlteq  12685  expgt1  12838  mulexpz  12840  leexp1a  12859  expubnd  12861  sqgt0  12872  lt2sq  12877  le2sq  12878  sqge0  12880  sumsqeq0  12882  sqlecan  12911  bernneq  12930  bernneq2  12931  expnbnd  12933  digit2  12937  digit1  12938  swrdccatin2  13424  swrdccat3blem  13432  cshweqrep  13504  crre  13788  crim  13789  reim0  13792  mulre  13795  rere  13796  remul2  13804  rediv  13805  immul2  13811  imdiv  13812  cjre  13813  cjreim  13834  rennim  13913  resqrex  13925  resqreu  13927  resqrtcl  13928  resqrtthlem  13929  sqrtneglem  13941  sqrtneg  13942  absreimsq  13966  absreim  13967  absnid  13972  leabs  13973  absre  13975  absresq  13976  sqabs  13981  max0add  13984  absz  13985  absdiflt  13991  absdifle  13992  lenegsq  13994  abssuble0  14002  absmax  14003  rddif  14014  absrdbnd  14015  o1rlimmul  14283  caurcvg2  14342  reefcl  14742  efgt0  14758  reeftlcl  14763  resinval  14790  recosval  14791  resin4p  14793  recos4p  14794  resincl  14795  recoscl  14796  retancl  14797  resinhcl  14811  rpcoshcl  14812  retanhcl  14814  tanhlt1  14815  tanhbnd  14816  efieq  14818  sinbnd  14835  cosbnd  14836  absefi  14851  dvdsaddre2b  14953  odd2np1  14989  bezoutlem1  15180  xrsdsreclb  19712  remulg  19872  resubdrg  19873  remetdval  22500  bl2ioo  22503  ioo2bl  22504  cnperf  22531  icccvx  22657  tchcph  22944  shft2rab  23183  volsup2  23279  volcn  23280  c1lip1  23664  plyreres  23942  aalioulem3  23993  taylthlem2  24032  reeff1o  24105  reefgim  24108  sincosq1sgn  24154  sincosq2sgn  24155  sincosq3sgn  24156  sincosq4sgn  24157  sinq12gt0  24163  pige3  24173  efif1olem4  24195  efifo  24197  relogrn  24212  logrnaddcl  24225  relogoprlem  24241  advlog  24300  advlogexp  24301  logtayl  24306  recxpcl  24321  rpcxpcl  24322  cxpge0  24329  dvcxp1  24381  logreclem  24400  relogbreexp  24413  relogbcxp  24423  angpieqvd  24458  atanre  24512  basellem9  24715  gausslemma2dlem1a  24990  log2sumbnd  25133  brbtwn2  25685  colinearalglem4  25689  colinearalg  25690  crctcshwlkn0lem1  26571  nvsge0  27368  nmoub3i  27477  nmlnoubi  27500  isblo3i  27505  ipasslem3  27537  ipasslem9  27542  ipasslem11  27544  hmopm  28729  riesz1  28773  leopmuli  28841  leopmul  28842  leopmul2i  28843  leopnmid  28846  nmopleid  28847  cdj1i  29141  cdj3lem1  29142  cdj3i  29149  addltmulALT  29154  rexdiv  29419  xdivid  29421  xdiv0  29422  rmulccn  29756  sgnneg  30383  lediv2aALT  31279  nndivlub  32099  cos2h  33032  tan2h  33033  poimir  33074  mblfinlem2  33079  mblfinlem4  33081  itg2addnclem  33093  itg2addnclem2  33094  dvasin  33128  areacirclem1  33132  areacirclem2  33133  areacirclem4  33135  areacirclem5  33136  areacirc  33137  expmordi  36992  areaquad  37283  radcnvrat  37995  lhe4.4ex1a  38010  expgrowthi  38014  mulltgt0  38664  refsum2cnlem1  38679  infnsuprnmpt  38941  dstregt0  38957  suplesup  39019  infleinflem1  39050  infleinflem2  39051  ltdiv23neg  39081  rexabslelem  39109  fmul01lt1lem1  39220  lptre2pt  39276  dvcosre  39430  itgsin0pilem1  39472  itgsinexplem1  39476  volioc  39495  volico  39507  stoweidlem7  39531  stoweidlem10  39534  stoweidlem19  39543  stoweidlem34  39558  stoweid  39587  dirker2re  39616  dirkerdenne0  39617  dirkerper  39620  dirkertrigeq  39625  dirkeritg  39626  fourierdlem39  39670  fourierdlem42  39673  fourierdlem47  39677  fourierdlem56  39686  fourierdlem57  39687  fourierdlem58  39688  fourierdlem60  39690  fourierdlem61  39691  fourierdlem73  39703  fourierdlem76  39706  fourierdlem77  39707  fourierdlem92  39722  fourierdlem97  39727  etransclem46  39804  volico2  40162  smflimlem4  40289  smfinflem  40330  2leaddle2  40609  ltsubsubaddltsub  40612  m1mod0mod1  40637  bgoldbtbndlem2  40983  flsubz  41600  rege1logbrege0  41644  nn0digval  41686  reseccl  41787  recsccl  41788  recotcl  41789  dpfrac1  41806  dpfrac1OLD  41807
  Copyright terms: Public domain W3C validator