Theorem recn 11165

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 11132	. 2 ⊢ ℝ ⊆ ℂ
2	1	sseli 3945	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11073  ℝcr 11074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-resscn 11132

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2804  df-ss 3934

This theorem is referenced by:  mulrid  11179  recnd  11209  pnfnre  11222  mnfnre  11224  mul02  11359  ltaddneg  11397  ltaddnegr  11398  renegcli  11490  resubcl  11493  negn0  11614  negf1o  11615  ltaddsub2  11660  leaddsub2  11662  leltadd  11669  ltaddpos  11675  ltaddpos2  11676  posdif  11678  lenegcon1  11689  lenegcon2  11690  addge01  11695  addge02  11696  leaddle0  11700  mullt0  11704  recex  11817  ltm1  12031  prodgt02  12037  ltmul2  12040  lemul1  12041  lemul2  12042  lemul1a  12043  lemul2a  12044  ltmulgt12  12050  lemulge12  12053  gt0div  12056  ge0div  12057  mulge0b  12060  mulle0b  12061  ltmuldiv2  12064  ltdivmul  12065  ledivmul  12066  ltdivmul2  12067  lt2mul2div  12068  ledivmul2  12069  lemuldiv2  12071  ltdiv2  12076  ltrec1  12077  lerec2  12078  ledivdiv  12079  lediv2  12080  ltdiv23  12081  lediv23  12082  lediv12a  12083  recp1lt1  12088  ledivp1  12092  negfi  12139  infm3lem  12148  supmul  12162  riotaneg  12169  negiso  12170  cju  12189  nnge1  12221  halfpos  12419  lt2halves  12424  addltmul  12425  avgle1  12429  avgle2  12430  avgle  12431  div4p1lem1div2  12444  nnrecl  12447  difgtsumgt  12502  elznn0  12551  elznn  12552  elz2  12554  nzadd  12588  zmulcl  12589  gtndiv  12618  zeo  12627  eqreznegel  12900  supminf  12901  rebtwnz  12913  irradd  12939  irrmul  12940  divlt1lt  13029  divle1le  13030  max0sub  13163  xnegneg  13181  rexsub  13200  xnegid  13205  xaddcom  13207  xaddrid  13208  xnegdi  13215  xaddass  13216  rexmul  13238  xmulasslem3  13253  xadddilem  13261  divelunit  13462  fzonmapblen  13676  ico01fl0  13788  flzadd  13795  ltdifltdiv  13803  dfceil2  13808  intfrac2  13827  fldiv2  13830  flpmodeq  13843  mod0  13845  negmod0  13847  modlt  13849  modfrac  13853  flmod  13854  intfrac  13855  modmulnn  13858  modvalp1  13859  modid  13865  modcyc  13875  modcyc2  13876  modadd1  13877  modaddabs  13880  muladdmodid  13882  muladdmod  13884  negmod  13888  modadd2mod  13893  modmul1  13896  modmulmodr  13909  modaddmulmod  13910  moddi  13911  modsubdir  13912  modirr  13914  addmodlteq  13918  expgt1  14072  mulexpz  14074  sqgt0  14098  lt2sq  14105  le2sq  14106  sqge0  14108  expmordi  14139  leexp1a  14147  expubnd  14150  sumsqeq0  14151  sqlecan  14181  bernneq  14201  bernneq2  14202  expnbnd  14204  digit2  14208  digit1  14209  expnngt1  14213  swrdccatin2  14701  swrdccat3blem  14711  cshweqrep  14793  crre  15087  crim  15088  reim0  15091  mulre  15094  rere  15095  remul2  15103  rediv  15104  immul2  15110  imdiv  15111  cjre  15112  cjreim  15133  rennim  15212  resqrex  15223  resqreu  15225  resqrtcl  15226  resqrtthlem  15227  sqrtneglem  15239  sqrtneg  15240  absreimsq  15265  absreim  15266  absnid  15271  leabs  15272  absre  15274  absresq  15275  sqabs  15280  max0add  15283  absz  15284  absdiflt  15291  absdifle  15292  lenegsq  15294  abssuble0  15302  absmax  15303  rddif  15314  absrdbnd  15315  o1rlimmul  15592  caurcvg2  15651  reefcl  16060  efgt0  16078  reeftlcl  16083  resinval  16110  recosval  16111  resin4p  16113  recos4p  16114  resincl  16115  recoscl  16116  retancl  16117  resinhcl  16131  rpcoshcl  16132  retanhcl  16134  tanhlt1  16135  tanhbnd  16136  efieq  16138  sinbnd  16155  cosbnd  16156  absefi  16171  dvdsaddre2b  16284  odd2np1  16318  bezoutlem1  16516  xrsdsreclb  21337  remulg  21523  resubdrg  21524  remetdval  24684  bl2ioo  24687  ioo2bl  24688  cnperf  24716  icccvx  24855  tcphcph  25144  shft2rab  25416  volsup2  25513  volcn  25514  c1lip1  25909  plyreres  26197  aalioulem3  26249  taylthlem2  26289  taylthlem2OLD  26290  reeff1o  26364  reefgim  26367  sincosq1sgn  26414  sincosq2sgn  26415  sincosq3sgn  26416  sincosq4sgn  26417  sinq12gt0  26423  pige3ALT  26436  efif1olem4  26461  efifo  26463  relogrn  26477  logrnaddcl  26490  relogoprlem  26507  advlog  26570  advlogexp  26571  logtayl  26576  recxpcl  26591  rpcxpcl  26592  cxpge0  26599  cxpcom  26655  dvcxp1  26656  logreclem  26679  relogbreexp  26692  relogbcxp  26702  angpieqvd  26748  atanre  26802  basellem9  27006  gausslemma2dlem1a  27283  2sqnn0  27356  log2sumbnd  27462  brbtwn2  28839  colinearalglem4  28843  colinearalg  28844  crctcshwlkn0lem1  29747  nvsge0  30600  nmoub3i  30709  nmlnoubi  30732  isblo3i  30737  ipasslem3  30769  ipasslem9  30774  ipasslem11  30776  hmopm  31957  riesz1  32001  leopmuli  32069  leopmul  32070  leopmul2i  32071  leopnmid  32074  nmopleid  32075  cdj1i  32369  cdj3lem1  32370  cdj3i  32377  addltmulALT  32382  sgnneg  32765  dpfrac1  32819  rexdiv  32853  xdivid  32855  xdiv0  32856  lediv2aALT  35671  nndivlub  36453  irrdiff  37321  cos2h  37612  tan2h  37613  poimir  37654  mblfinlem2  37659  mblfinlem4  37661  itg2addnclem  37672  itg2addnclem2  37673  dvasin  37705  areacirclem1  37709  areacirclem2  37710  areacirclem4  37712  areacirclem5  37713  areacirc  37714  lcmineqlem12  42035  dvrelog2b  42061  aks4d1p1p6  42068  retire  42314  readvrec2  42356  readvrec  42357  resubeulem2  42371  renegneg  42407  renegid2  42409  sn-it0e0  42411  sn-negex12  42412  resubeqsub  42425  sn-mullid  42431  sn-mul02  42447  areaquad  43212  reabssgn  43632  radcnvrat  44310  lhe4.4ex1a  44325  expgrowthi  44329  mulltgt0  45023  refsum2cnlem1  45038  infnsuprnmpt  45251  dstregt0  45287  suplesup  45342  infleinflem1  45373  infleinflem2  45374  ltdiv23neg  45397  rexabslelem  45421  supminfrnmpt  45448  supminfxr  45467  fmul01lt1lem1  45589  lptre2pt  45645  cnrefiisplem  45834  dvcosre  45917  itgsin0pilem1  45955  itgsinexplem1  45959  volioc  45977  volico  45988  stoweidlem7  46012  stoweidlem10  46015  stoweidlem19  46024  stoweidlem34  46039  stoweid  46068  dirker2re  46097  dirkerdenne0  46098  dirkerper  46101  dirkertrigeq  46106  dirkeritg  46107  fourierdlem39  46151  fourierdlem42  46154  fourierdlem47  46158  fourierdlem56  46167  fourierdlem57  46168  fourierdlem58  46169  fourierdlem60  46171  fourierdlem61  46172  fourierdlem73  46184  fourierdlem76  46187  fourierdlem77  46188  fourierdlem92  46203  fourierdlem97  46208  etransclem46  46285  volico2  46646  smflimlem4  46779  smfinflem  46822  et-sqrtnegnre  46878  squeezedltsq  46894  2leaddle2  47303  ltsubsubaddltsub  47306  sqrtnegnre  47312  ceildivmod  47344  m1mod0mod1  47359  requad01  47626  requad1  47627  bgoldbtbndlem2  47811  flsubz  48515  rege1logbrege0  48551  nn0digval  48593  rrx2vlinest  48734  line2  48745  line2xlem  48746  line2x  48747  itscnhlc0yqe  48752  itsclc0yqsollem2  48756  itsclc0yqsol  48757  itscnhlc0xyqsol  48758  itschlc0xyqsol1  48759  itsclc0xyqsolr  48762  itsclquadb  48769  reseccl  49746  recsccl  49747  recotcl  49748