Theorem recn 11116

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11024  ℝcr 11025

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-resscn 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2811  df-ss 3918

This theorem is referenced by:  mulrid  11130  recnd  11160  pnfnre  11173  mnfnre  11175  mul02  11311  ltaddneg  11349  ltaddnegr  11350  renegcli  11442  resubcl  11445  negn0  11566  negf1o  11567  ltaddsub2  11612  leaddsub2  11614  leltadd  11621  ltaddpos  11627  ltaddpos2  11628  posdif  11630  lenegcon1  11641  lenegcon2  11642  addge01  11647  addge02  11648  leaddle0  11652  mullt0  11656  recex  11769  ltm1  11983  prodgt02  11989  ltmul2  11992  lemul1  11993  lemul2  11994  lemul1a  11995  lemul2a  11996  ltmulgt12  12002  lemulge12  12005  gt0div  12008  ge0div  12009  mulge0b  12012  mulle0b  12013  ltmuldiv2  12016  ltdivmul  12017  ledivmul  12018  ltdivmul2  12019  lt2mul2div  12020  ledivmul2  12021  lemuldiv2  12023  ltdiv2  12028  ltrec1  12029  lerec2  12030  ledivdiv  12031  lediv2  12032  ltdiv23  12033  lediv23  12034  lediv12a  12035  recp1lt1  12040  ledivp1  12044  negfi  12091  infm3lem  12100  supmul  12114  riotaneg  12121  negiso  12122  cju  12141  nnge1  12173  halfpos  12371  lt2halves  12376  addltmul  12377  avgle1  12381  avgle2  12382  avgle  12383  div4p1lem1div2  12396  nnrecl  12399  difgtsumgt  12454  elznn0  12503  elznn  12504  elz2  12506  nzadd  12539  zmulcl  12540  gtndiv  12569  zeo  12578  eqreznegel  12847  supminf  12848  rebtwnz  12860  irradd  12886  irrmul  12887  divlt1lt  12976  divle1le  12977  max0sub  13111  xnegneg  13129  rexsub  13148  xnegid  13153  xaddcom  13155  xaddrid  13156  xnegdi  13163  xaddass  13164  rexmul  13186  xmulasslem3  13201  xadddilem  13209  divelunit  13410  fzonmapblen  13624  ico01fl0  13739  flzadd  13746  ltdifltdiv  13754  dfceil2  13759  intfrac2  13778  fldiv2  13781  flpmodeq  13794  mod0  13796  negmod0  13798  modlt  13800  modfrac  13804  flmod  13805  intfrac  13806  modmulnn  13809  modvalp1  13810  modid  13816  modcyc  13826  modcyc2  13827  modadd1  13828  modaddabs  13831  muladdmodid  13833  muladdmod  13835  negmod  13839  modadd2mod  13844  modmul1  13847  modmulmodr  13860  modaddmulmod  13861  moddi  13862  modsubdir  13863  modirr  13865  addmodlteq  13869  expgt1  14023  mulexpz  14025  sqgt0  14049  lt2sq  14056  le2sq  14057  sqge0  14059  expmordi  14090  leexp1a  14098  expubnd  14101  sumsqeq0  14102  sqlecan  14132  bernneq  14152  bernneq2  14153  expnbnd  14155  digit2  14159  digit1  14160  expnngt1  14164  swrdccatin2  14652  swrdccat3blem  14662  cshweqrep  14744  crre  15037  crim  15038  reim0  15041  mulre  15044  rere  15045  remul2  15053  rediv  15054  immul2  15060  imdiv  15061  cjre  15062  cjreim  15083  rennim  15162  resqrex  15173  resqreu  15175  resqrtcl  15176  resqrtthlem  15177  sqrtneglem  15189  sqrtneg  15190  absreimsq  15215  absreim  15216  absnid  15221  leabs  15222  absre  15224  absresq  15225  sqabs  15230  max0add  15233  absz  15234  absdiflt  15241  absdifle  15242  lenegsq  15244  abssuble0  15252  absmax  15253  rddif  15264  absrdbnd  15265  o1rlimmul  15542  caurcvg2  15601  reefcl  16010  efgt0  16028  reeftlcl  16033  resinval  16060  recosval  16061  resin4p  16063  recos4p  16064  resincl  16065  recoscl  16066  retancl  16067  resinhcl  16081  rpcoshcl  16082  retanhcl  16084  tanhlt1  16085  tanhbnd  16086  efieq  16088  sinbnd  16105  cosbnd  16106  absefi  16121  dvdsaddre2b  16234  odd2np1  16268  bezoutlem1  16466  xrsdsreclb  21368  remulg  21562  resubdrg  21563  remetdval  24733  bl2ioo  24736  ioo2bl  24737  cnperf  24765  icccvx  24904  tcphcph  25193  shft2rab  25465  volsup2  25562  volcn  25563  c1lip1  25958  plyreres  26246  aalioulem3  26298  taylthlem2  26338  taylthlem2OLD  26339  reeff1o  26413  reefgim  26416  sincosq1sgn  26463  sincosq2sgn  26464  sincosq3sgn  26465  sincosq4sgn  26466  sinq12gt0  26472  pige3ALT  26485  efif1olem4  26510  efifo  26512  relogrn  26526  logrnaddcl  26539  relogoprlem  26556  advlog  26619  advlogexp  26620  logtayl  26625  recxpcl  26640  rpcxpcl  26641  cxpge0  26648  cxpcom  26704  dvcxp1  26705  logreclem  26728  relogbreexp  26741  relogbcxp  26751  angpieqvd  26797  atanre  26851  basellem9  27055  gausslemma2dlem1a  27332  2sqnn0  27405  log2sumbnd  27511  brbtwn2  28978  colinearalglem4  28982  colinearalg  28983  crctcshwlkn0lem1  29883  nvsge0  30739  nmoub3i  30848  nmlnoubi  30871  isblo3i  30876  ipasslem3  30908  ipasslem9  30913  ipasslem11  30915  hmopm  32096  riesz1  32140  leopmuli  32208  leopmul  32209  leopmul2i  32210  leopnmid  32213  nmopleid  32214  cdj1i  32508  cdj3lem1  32509  cdj3i  32516  addltmulALT  32521  sgnneg  32914  dpfrac1  32973  rexdiv  33007  xdivid  33009  xdiv0  33010  lediv2aALT  35871  nndivlub  36652  irrdiff  37527  cos2h  37808  tan2h  37809  poimir  37850  mblfinlem2  37855  mblfinlem4  37857  itg2addnclem  37868  itg2addnclem2  37869  dvasin  37901  areacirclem1  37905  areacirclem2  37906  areacirclem4  37908  areacirclem5  37909  areacirc  37910  lcmineqlem12  42290  dvrelog2b  42316  aks4d1p1p6  42323  retire  42570  readvrec2  42612  readvrec  42613  resubeulem2  42627  renegneg  42663  renegid2  42665  sn-it0e0  42667  sn-negex12  42668  resubeqsub  42681  sn-mullid  42687  sn-mul02  42703  areaquad  43454  reabssgn  43873  radcnvrat  44551  lhe4.4ex1a  44566  expgrowthi  44570  mulltgt0  45263  refsum2cnlem1  45278  infnsuprnmpt  45490  dstregt0  45526  suplesup  45580  infleinflem1  45610  infleinflem2  45611  ltdiv23neg  45634  rexabslelem  45658  supminfrnmpt  45685  supminfxr  45704  fmul01lt1lem1  45826  lptre2pt  45880  cnrefiisplem  46069  dvcosre  46152  itgsin0pilem1  46190  itgsinexplem1  46194  volioc  46212  volico  46223  stoweidlem7  46247  stoweidlem10  46250  stoweidlem19  46259  stoweidlem34  46274  stoweid  46303  dirker2re  46332  dirkerdenne0  46333  dirkerper  46336  dirkertrigeq  46341  dirkeritg  46342  fourierdlem39  46386  fourierdlem42  46389  fourierdlem47  46393  fourierdlem56  46402  fourierdlem57  46403  fourierdlem58  46404  fourierdlem60  46406  fourierdlem61  46407  fourierdlem73  46419  fourierdlem76  46422  fourierdlem77  46423  fourierdlem92  46438  fourierdlem97  46443  etransclem46  46520  volico2  46881  smflimlem4  47014  smfinflem  47057  et-sqrtnegnre  47113  squeezedltsq  47128  2leaddle2  47540  ltsubsubaddltsub  47543  sqrtnegnre  47549  ceildivmod  47581  m1mod0mod1  47596  requad01  47863  requad1  47864  bgoldbtbndlem2  48048  flsubz  48764  rege1logbrege0  48800  nn0digval  48842  rrx2vlinest  48983  line2  48994  line2xlem  48995  line2x  48996  itscnhlc0yqe  49001  itsclc0yqsollem2  49005  itsclc0yqsol  49006  itscnhlc0xyqsol  49007  itschlc0xyqsol1  49008  itsclc0xyqsolr  49011  itsclquadb  49018  reseccl  49994  recsccl  49995  recotcl  49996