Theorem recn 10908

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

Assertion

Ref	Expression
recn	⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)

Proof of Theorem recn

Step	Hyp	Ref	Expression
1		ax-resscn 10875	. 2 ⊢ ℝ ⊆ ℂ
2	1	sseli 3918	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 10816  ℝcr 10817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-resscn 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3429  df-in 3895  df-ss 3905

This theorem is referenced by:  mulid1  10920  recnd  10950  pnfnre  10963  mnfnre  10965  mul02  11099  ltaddneg  11136  ltaddnegr  11137  renegcli  11228  resubcl  11231  negn0  11350  negf1o  11351  ltaddsub2  11396  leaddsub2  11398  leltadd  11405  ltaddpos  11411  ltaddpos2  11412  posdif  11414  lenegcon1  11425  lenegcon2  11426  addge01  11431  addge02  11432  leaddle0  11436  mullt0  11440  recex  11553  ltm1  11763  prodgt02  11769  ltmul2  11772  lemul1  11773  lemul2  11774  lemul1a  11775  lemul2a  11776  ltmulgt12  11782  lemulge12  11784  gt0div  11787  ge0div  11788  mulge0b  11791  mulle0b  11792  ltmuldiv2  11795  ltdivmul  11796  ledivmul  11797  ltdivmul2  11798  lt2mul2div  11799  ledivmul2  11800  lemuldiv2  11802  ltdiv2  11807  ltrec1  11808  lerec2  11809  ledivdiv  11810  lediv2  11811  ltdiv23  11812  lediv23  11813  lediv12a  11814  recp1lt1  11819  ledivp1  11823  negfi  11870  infm3lem  11879  supmul  11893  riotaneg  11900  negiso  11901  cju  11915  nnge1  11947  halfpos  12149  lt2halves  12154  addltmul  12155  avgle1  12159  avgle2  12160  avgle  12161  div4p1lem1div2  12174  nnrecl  12177  difgtsumgt  12232  elznn0  12280  elznn  12281  elz2  12283  nzadd  12314  zmulcl  12315  gtndiv  12343  zeo  12352  eqreznegel  12619  supminf  12620  rebtwnz  12632  irradd  12658  irrmul  12659  divlt1lt  12744  divle1le  12745  max0sub  12875  xnegneg  12893  rexsub  12912  xnegid  12917  xaddcom  12919  xaddid1  12920  xnegdi  12927  xaddass  12928  rexmul  12950  xmulasslem3  12965  xadddilem  12973  divelunit  13171  fzonmapblen  13377  ico01fl0  13483  flzadd  13490  ltdifltdiv  13498  dfceil2  13503  intfrac2  13522  fldiv2  13525  flpmodeq  13538  mod0  13540  negmod0  13542  modlt  13544  modfrac  13548  flmod  13549  intfrac  13550  modmulnn  13553  modvalp1  13554  modid  13560  modcyc  13570  modcyc2  13571  modadd1  13572  modaddabs  13573  muladdmodid  13575  negmod  13580  modadd2mod  13585  modmul1  13588  modmulmodr  13601  modaddmulmod  13602  moddi  13603  modsubdir  13604  modirr  13606  addmodlteq  13610  expgt1  13765  mulexpz  13767  sqgt0  13789  lt2sq  13796  le2sq  13797  sqge0  13799  expmordi  13829  leexp1a  13837  expubnd  13839  sumsqeq0  13840  sqlecan  13869  bernneq  13888  bernneq2  13889  expnbnd  13891  digit2  13895  digit1  13896  expnngt1  13900  swrdccatin2  14386  swrdccat3blem  14396  cshweqrep  14478  crre  14769  crim  14770  reim0  14773  mulre  14776  rere  14777  remul2  14785  rediv  14786  immul2  14792  imdiv  14793  cjre  14794  cjreim  14815  rennim  14894  resqrex  14906  resqreu  14908  resqrtcl  14909  resqrtthlem  14910  sqrtneglem  14922  sqrtneg  14923  absreimsq  14948  absreim  14949  absnid  14954  leabs  14955  absre  14957  absresq  14958  sqabs  14963  max0add  14966  absz  14967  absdiflt  14973  absdifle  14974  lenegsq  14976  abssuble0  14984  absmax  14985  rddif  14996  absrdbnd  14997  o1rlimmul  15272  caurcvg2  15333  reefcl  15740  efgt0  15756  reeftlcl  15761  resinval  15788  recosval  15789  resin4p  15791  recos4p  15792  resincl  15793  recoscl  15794  retancl  15795  resinhcl  15809  rpcoshcl  15810  retanhcl  15812  tanhlt1  15813  tanhbnd  15814  efieq  15816  sinbnd  15833  cosbnd  15834  absefi  15849  dvdsaddre2b  15960  odd2np1  15994  bezoutlem1  16191  xrsdsreclb  20589  remulg  20756  resubdrg  20757  remetdval  23896  bl2ioo  23899  ioo2bl  23900  cnperf  23927  icccvx  24057  tcphcph  24344  shft2rab  24615  volsup2  24712  volcn  24713  c1lip1  25104  plyreres  25386  aalioulem3  25437  taylthlem2  25476  reeff1o  25549  reefgim  25552  sincosq1sgn  25598  sincosq2sgn  25599  sincosq3sgn  25600  sincosq4sgn  25601  sinq12gt0  25607  pige3ALT  25619  efif1olem4  25644  efifo  25646  relogrn  25660  logrnaddcl  25673  relogoprlem  25689  advlog  25752  advlogexp  25753  logtayl  25758  recxpcl  25773  rpcxpcl  25774  cxpge0  25781  cxpcom  25835  dvcxp1  25836  logreclem  25855  relogbreexp  25868  relogbcxp  25878  angpieqvd  25924  atanre  25978  basellem9  26181  gausslemma2dlem1a  26456  2sqnn0  26529  log2sumbnd  26635  brbtwn2  27216  colinearalglem4  27220  colinearalg  27221  crctcshwlkn0lem1  28116  nvsge0  28967  nmoub3i  29076  nmlnoubi  29099  isblo3i  29104  ipasslem3  29136  ipasslem9  29141  ipasslem11  29143  hmopm  30324  riesz1  30368  leopmuli  30436  leopmul  30437  leopmul2i  30438  leopnmid  30441  nmopleid  30442  cdj1i  30736  cdj3lem1  30737  cdj3i  30744  addltmulALT  30749  dpfrac1  31108  rexdiv  31142  xdivid  31144  xdiv0  31145  rmulccn  31820  sgnneg  32449  lediv2aALT  33577  nndivlub  34616  irrdiff  35466  cos2h  35737  tan2h  35738  poimir  35779  mblfinlem2  35784  mblfinlem4  35786  itg2addnclem  35797  itg2addnclem2  35798  dvasin  35830  areacirclem1  35834  areacirclem2  35835  areacirclem4  35837  areacirclem5  35838  areacirc  35839  lcmineqlem12  40018  dvrelog2b  40044  aks4d1p1p6  40051  2xp3dxp2ge1d  40132  resubeulem2  40322  renegneg  40357  renegid2  40359  sn-it0e0  40360  sn-negex12  40361  resubeqsub  40374  sn-mulid2  40380  sn-mul02  40385  areaquad  41005  reabssgn  41175  radcnvrat  41863  lhe4.4ex1a  41878  expgrowthi  41882  mulltgt0  42496  refsum2cnlem1  42511  infnsuprnmpt  42727  dstregt0  42751  suplesup  42810  infleinflem1  42841  infleinflem2  42842  ltdiv23neg  42866  rexabslelem  42890  supminfrnmpt  42917  supminfxr  42936  fmul01lt1lem1  43057  lptre2pt  43113  cnrefiisplem  43302  dvcosre  43385  itgsin0pilem1  43423  itgsinexplem1  43427  volioc  43445  volico  43456  stoweidlem7  43480  stoweidlem10  43483  stoweidlem19  43492  stoweidlem34  43507  stoweid  43536  dirker2re  43565  dirkerdenne0  43566  dirkerper  43569  dirkertrigeq  43574  dirkeritg  43575  fourierdlem39  43619  fourierdlem42  43622  fourierdlem47  43626  fourierdlem56  43635  fourierdlem57  43636  fourierdlem58  43637  fourierdlem60  43639  fourierdlem61  43640  fourierdlem73  43652  fourierdlem76  43655  fourierdlem77  43656  fourierdlem92  43671  fourierdlem97  43676  etransclem46  43753  volico2  44111  smflimlem4  44238  smfinflem  44279  2leaddle2  44720  ltsubsubaddltsub  44723  sqrtnegnre  44729  m1mod0mod1  44751  requad01  45003  requad1  45004  bgoldbtbndlem2  45188  flsubz  45793  rege1logbrege0  45834  nn0digval  45876  rrx2vlinest  46017  line2  46028  line2xlem  46029  line2x  46030  itscnhlc0yqe  46035  itsclc0yqsollem2  46039  itsclc0yqsol  46040  itscnhlc0xyqsol  46041  itschlc0xyqsol1  46042  itsclc0xyqsolr  46045  itsclquadb  46052  reseccl  46385  recsccl  46386  recotcl  46387