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

Theorem recn 10238
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 10205 . 2 ℝ ⊆ ℂ
21sseli 3740 1 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  cc 10146  cr 10147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-resscn 10205
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729
This theorem is referenced by:  mulid1  10249  recnd  10280  pnfnre  10293  mnfnre  10294  mul02  10426  ltaddneg  10463  ltaddnegr  10464  renegcli  10554  resubcl  10557  negn0  10671  negf1o  10672  ltaddsub2  10715  leaddsub2  10717  leltadd  10724  ltaddpos  10730  ltaddpos2  10731  posdif  10733  lenegcon1  10744  lenegcon2  10745  addge01  10750  addge02  10751  leaddle0  10755  mullt0  10759  recex  10871  ltm1  11075  prodgt02  11081  prodge02  11083  ltmul2  11086  lemul1  11087  lemul2  11088  lemul1a  11089  lemul2a  11090  ltmulgt12  11096  lemulge12  11098  gt0div  11101  ge0div  11102  mulge0b  11105  mulle0b  11106  ltmuldiv2  11109  ltdivmul  11110  ledivmul  11111  ltdivmul2  11112  lt2mul2div  11113  ledivmul2  11114  lemuldiv2  11116  ltdiv2  11121  ltrec1  11122  lerec2  11123  ledivdiv  11124  lediv2  11125  ltdiv23  11126  lediv23  11127  lediv12a  11128  recp1lt1  11133  ledivp1  11137  negfi  11183  fiminre  11184  infm3lem  11193  supmul  11207  riotaneg  11214  negiso  11215  cju  11228  nnge1  11258  halfpos  11474  lt2halves  11479  addltmul  11480  avgle1  11484  avgle2  11485  avgle  11486  div4p1lem1div2  11499  nnrecl  11502  difgtsumgt  11558  elznn0  11604  elznn  11605  elz2  11606  nzadd  11637  zmulcl  11638  gtndiv  11666  zeo  11675  eqreznegel  11987  supminf  11988  rebtwnz  12000  irradd  12025  irrmul  12026  divlt1lt  12112  divle1le  12113  max0sub  12240  xnegneg  12258  rexsub  12277  xnegid  12282  xaddcom  12284  xaddid1  12285  xnegdi  12291  xaddass  12292  rexmul  12314  xmulasslem3  12329  xadddilem  12337  divelunit  12527  fzonmapblen  12728  ico01fl0  12834  flzadd  12841  ltdifltdiv  12849  dfceil2  12854  intfrac2  12871  fldiv2  12874  flpmodeq  12887  mod0  12889  negmod0  12891  modlt  12893  modfrac  12897  flmod  12898  intfrac  12899  modmulnn  12902  modvalp1  12903  modid  12909  modcyc  12919  modcyc2  12920  modadd1  12921  modaddabs  12922  muladdmodid  12924  negmod  12929  modadd2mod  12934  modmul1  12937  modmulmodr  12950  modaddmulmod  12951  moddi  12952  modsubdir  12953  modirr  12955  addmodlteq  12959  expgt1  13112  mulexpz  13114  leexp1a  13133  expubnd  13135  sqgt0  13146  lt2sq  13151  le2sq  13152  sqge0  13154  sumsqeq0  13156  sqlecan  13185  bernneq  13204  bernneq2  13205  expnbnd  13207  digit2  13211  digit1  13212  swrdccatin2  13707  swrdccat3blem  13715  cshweqrep  13787  crre  14073  crim  14074  reim0  14077  mulre  14080  rere  14081  remul2  14089  rediv  14090  immul2  14096  imdiv  14097  cjre  14098  cjreim  14119  rennim  14198  resqrex  14210  resqreu  14212  resqrtcl  14213  resqrtthlem  14214  sqrtneglem  14226  sqrtneg  14227  absreimsq  14251  absreim  14252  absnid  14257  leabs  14258  absre  14260  absresq  14261  sqabs  14266  max0add  14269  absz  14270  absdiflt  14276  absdifle  14277  lenegsq  14279  abssuble0  14287  absmax  14288  rddif  14299  absrdbnd  14300  o1rlimmul  14568  caurcvg2  14627  reefcl  15036  efgt0  15052  reeftlcl  15057  resinval  15084  recosval  15085  resin4p  15087  recos4p  15088  resincl  15089  recoscl  15090  retancl  15091  resinhcl  15105  rpcoshcl  15106  retanhcl  15108  tanhlt1  15109  tanhbnd  15110  efieq  15112  sinbnd  15129  cosbnd  15130  absefi  15145  dvdsaddre2b  15251  odd2np1  15287  bezoutlem1  15478  xrsdsreclb  20015  remulg  20175  resubdrg  20176  remetdval  22813  bl2ioo  22816  ioo2bl  22817  cnperf  22844  icccvx  22970  tchcph  23256  shft2rab  23496  volsup2  23593  volcn  23594  c1lip1  23979  plyreres  24257  aalioulem3  24308  taylthlem2  24347  reeff1o  24420  reefgim  24423  sincosq1sgn  24470  sincosq2sgn  24471  sincosq3sgn  24472  sincosq4sgn  24473  sinq12gt0  24479  pige3  24489  efif1olem4  24511  efifo  24513  relogrn  24528  logrnaddcl  24541  relogoprlem  24557  advlog  24620  advlogexp  24621  logtayl  24626  recxpcl  24641  rpcxpcl  24642  cxpge0  24649  dvcxp1  24701  logreclem  24720  relogbreexp  24733  relogbcxp  24743  angpieqvd  24778  atanre  24832  basellem9  25035  gausslemma2dlem1a  25310  log2sumbnd  25453  brbtwn2  26005  colinearalglem4  26009  colinearalg  26010  crctcshwlkn0lem1  26934  nvsge0  27849  nmoub3i  27958  nmlnoubi  27981  isblo3i  27986  ipasslem3  28018  ipasslem9  28023  ipasslem11  28025  hmopm  29210  riesz1  29254  leopmuli  29322  leopmul  29323  leopmul2i  29324  leopnmid  29327  nmopleid  29328  cdj1i  29622  cdj3lem1  29623  cdj3i  29630  addltmulALT  29635  dpfrac1  29929  dpfrac1OLD  29930  rexdiv  29964  xdivid  29966  xdiv0  29967  rmulccn  30304  sgnneg  30932  lediv2aALT  31899  nndivlub  32784  cos2h  33731  tan2h  33732  poimir  33773  mblfinlem2  33778  mblfinlem4  33780  itg2addnclem  33792  itg2addnclem2  33793  dvasin  33827  areacirclem1  33831  areacirclem2  33832  areacirclem4  33834  areacirclem5  33835  areacirc  33836  expmordi  38032  areaquad  38322  radcnvrat  39033  lhe4.4ex1a  39048  expgrowthi  39052  mulltgt0  39698  refsum2cnlem1  39713  infnsuprnmpt  39982  dstregt0  40010  suplesup  40071  infleinflem1  40102  infleinflem2  40103  ltdiv23neg  40133  rexabslelem  40161  supminfrnmpt  40188  supminfxr  40210  fmul01lt1lem1  40337  lptre2pt  40393  cnrefiisplem  40576  dvcosre  40647  itgsin0pilem1  40686  itgsinexplem1  40690  volioc  40709  volico  40721  stoweidlem7  40745  stoweidlem10  40748  stoweidlem19  40757  stoweidlem34  40772  stoweid  40801  dirker2re  40830  dirkerdenne0  40831  dirkerper  40834  dirkertrigeq  40839  dirkeritg  40840  fourierdlem39  40884  fourierdlem42  40887  fourierdlem47  40891  fourierdlem56  40900  fourierdlem57  40901  fourierdlem58  40902  fourierdlem60  40904  fourierdlem61  40905  fourierdlem73  40917  fourierdlem76  40920  fourierdlem77  40921  fourierdlem92  40936  fourierdlem97  40941  etransclem46  41018  volico2  41379  smflimlem4  41506  smfinflem  41547  2leaddle2  41840  ltsubsubaddltsub  41843  m1mod0mod1  41867  bgoldbtbndlem2  42222  flsubz  42840  rege1logbrege0  42880  nn0digval  42922  reseccl  43025  recsccl  43026  recotcl  43027
  Copyright terms: Public domain W3C validator