Theorem recn 11191

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℂcc 11099  ℝcr 11100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-resscn 11158

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clel 2838  df-ss 3923

This theorem is referenced by:  mulrid  11207  recnd  11238  pnfnre  11251  mnfnre  11253  mul02  11389  ltaddneg  11427  ltaddnegr  11428  renegcli  11520  resubcl  11523  negn0  11644  negf1o  11645  ltaddsub2  11690  leaddsub2  11692  leltadd  11699  ltaddpos  11705  ltaddpos2  11706  posdif  11708  lenegcon1  11719  lenegcon2  11720  addge01  11725  addge02  11726  leaddle0  11730  mullt0  11734  recex  11847  ltm1  12058  prodgt02  12064  ltmul2  12067  lemul1  12068  lemul2  12069  lemul1a  12070  lemul2a  12071  ltmulgt12  12076  lemulge12  12079  gt0div  12082  ge0div  12083  mulge0b  12086  mulle0b  12087  ltmuldiv2  12090  ltdivmul  12091  ledivmul  12092  ltdivmul2  12093  lt2mul2div  12094  ledivmul2  12095  lemuldiv2  12097  ltdiv2  12102  ltrec1  12103  lerec2  12104  ledivdiv  12105  lediv2  12106  ltdiv23  12107  lediv23  12108  lediv12a  12109  recp1lt1  12114  ledivp1  12118  negfi  12165  infm3lem  12174  supmul  12188  riotaneg  12195  negiso  12196  cju  12215  nnge1  12265  halfpos  12475  lt2halves  12480  addltmul  12481  avgle1  12485  avgle2  12486  avgle  12487  div4p1lem1div2  12500  nnrecl  12503  difgtsumgt  12558  elznn0  12607  elznn  12608  elz2  12610  nzadd  12643  zmulcl  12644  gtndiv  12674  zeo  12683  eqreznegel  12959  supminf  12960  rebtwnz  12972  irradd  12998  irrmul  12999  divlt1lt  13088  divle1le  13089  max0sub  13223  xnegneg  13241  rexsub  13260  xnegid  13265  xaddcom  13267  xaddrid  13268  xnegdi  13275  xaddass  13276  rexmul  13298  xmulasslem3  13313  xadddilem  13321  divelunit  13522  fzonmapblen  13739  ico01fl0  13854  flzadd  13861  ltdifltdiv  13869  dfceil2  13874  intfrac2  13893  fldiv2  13896  flpmodeq  13909  mod0  13911  negmod0  13913  modlt  13915  modfrac  13919  flmod  13920  intfrac  13921  modmulnn  13924  modvalp1  13925  modid  13931  modcyc  13941  modcyc2  13942  modadd1  13943  modaddabs  13946  muladdmodid  13948  muladdmod  13950  negmod  13954  modadd2mod  13959  modmul1  13962  modmulmodr  13975  modaddmulmod  13976  moddi  13977  modsubdir  13978  modirr  13980  addmodlteq  13984  expgt1  14138  mulexpz  14140  sqgt0  14164  lt2sq  14171  le2sq  14172  sqge0  14174  expmordi  14205  leexp1a  14213  expubnd  14216  sumsqeq0  14217  sqlecan  14247  bernneq  14267  bernneq2  14268  expnbnd  14270  digit2  14274  digit1  14275  expnngt1  14279  swrdccatin2  14768  swrdccat3blem  14778  cshweqrep  14860  sgnneg  15139  crre  15167  crim  15168  reim0  15171  mulre  15174  rere  15175  remul2  15183  rediv  15184  immul2  15190  imdiv  15191  cjre  15192  cjreim  15213  rennim  15292  resqrex  15303  resqreu  15305  resqrtcl  15306  resqrtthlem  15307  sqrtneglem  15319  sqrtneg  15320  absreimsq  15345  absreim  15346  absnid  15351  leabs  15352  absre  15354  absresq  15355  sqabs  15360  max0add  15363  absz  15364  absdiflt  15371  absdifle  15372  lenegsq  15374  abssuble0  15382  absmax  15383  rddif  15394  absrdbnd  15395  o1rlimmul  15672  caurcvg2  15731  reefcl  16142  efgt0  16160  reeftlcl  16165  resinval  16192  recosval  16193  resin4p  16195  recos4p  16196  resincl  16197  recoscl  16198  retancl  16199  resinhcl  16213  rpcoshcl  16214  retanhcl  16216  tanhlt1  16217  tanhbnd  16218  efieq  16220  sinbnd  16237  cosbnd  16238  absefi  16253  dvdsaddre2b  16366  odd2np1  16400  bezoutlem1  16598  xrsdsreclb  21545  remulg  21738  resubdrg  21739  remetdval  24927  bl2ioo  24930  ioo2bl  24931  cnperf  24959  icccvx  25090  tcphcph  25377  shft2rab  25648  volsup2  25745  volcn  25746  c1lip1  26137  plyreres  26425  aalioulem3  26476  taylthlem2  26515  reeff1o  26588  reefgim  26591  sincosq1sgn  26641  sincosq2sgn  26642  sincosq3sgn  26643  sincosq4sgn  26644  sinq12gt0  26650  pige3ALT  26663  efif1olem4  26688  efifo  26690  relogrn  26704  logrnaddcl  26717  relogoprlem  26734  advlog  26797  advlogexp  26798  logtayl  26803  recxpcl  26818  rpcxpcl  26819  cxpge0  26826  cxpcom  26882  dvcxp1  26883  logreclem  26905  relogbreexp  26918  relogbcxp  26928  angpieqvd  26974  atanre  27028  basellem9  27231  gausslemma2dlem1a  27507  2sqnn0  27580  log2sumbnd  27686  brbtwn2  29233  colinearalglem4  29237  colinearalg  29238  crctcshwlkn0lem1  30137  nvsge0  30994  nmoub3i  31103  nmlnoubi  31126  isblo3i  31131  ipasslem3  31163  ipasslem9  31168  ipasslem11  31170  hmopm  32351  riesz1  32395  leopmuli  32463  leopmul  32464  leopmul2i  32465  leopnmid  32468  nmopleid  32469  cdj1i  32763  cdj3lem1  32764  cdj3i  32771  addltmulALT  32776  dpfrac1  33189  rexdiv  33223  xdivid  33225  xdiv0  33226  lediv2aALT  36147  nndivlub  36947  irrdiff  37948  cos2h  38240  tan2h  38241  poimir  38282  mblfinlem2  38287  mblfinlem4  38289  itg2addnclem  38300  itg2addnclem2  38301  dvasin  38333  areacirclem1  38337  areacirclem2  38338  areacirclem4  38340  areacirclem5  38341  areacirc  38342  lcmineqlem12  42785  dvrelog2b  42811  aks4d1p1p6  42818  retire  43058  readvrec2  43100  readvrec  43101  resubeulem2  43115  renegneg  43151  renegid2  43153  sn-it0e0  43155  sn-negex12  43156  resubeqsub  43169  sn-mullid  43175  sn-mul02  43204  areaquad  43923  reabssgn  44342  radcnvrat  45004  lhe4.4ex1a  45019  expgrowthi  45023  mulltgt0  45722  refsum2cnlem1  45737  infnsuprnmpt  45945  dstregt0  45981  suplesup  46035  infleinflem1  46065  infleinflem2  46066  ltdiv23neg  46089  rexabslelem  46112  supminfrnmpt  46139  supminfxr  46158  fmul01lt1lem1  46280  lptre2pt  46334  cnrefiisplem  46523  dvcosre  46606  itgsin0pilem1  46644  itgsinexplem1  46648  volioc  46666  volico  46677  stoweidlem7  46701  stoweidlem10  46704  stoweidlem19  46713  stoweidlem34  46728  stoweid  46757  dirker2re  46786  dirkerdenne0  46787  dirkerper  46790  dirkertrigeq  46795  dirkeritg  46796  fourierdlem39  46840  fourierdlem42  46843  fourierdlem47  46847  fourierdlem56  46856  fourierdlem57  46857  fourierdlem58  46858  fourierdlem60  46860  fourierdlem61  46861  fourierdlem73  46873  fourierdlem76  46876  fourierdlem77  46877  fourierdlem92  46892  fourierdlem97  46897  etransclem46  46974  volico2  47335  smflimlem4  47468  smfinflem  47511  et-sqrtnegnre  47567  squeezedltsq  47584  2leaddle2  48012  ltsubsubaddltsub  48015  sqrtnegnre  48021  ceildivmod  48059  m1mod0mod1  48074  requad01  48363  requad1  48364  bgoldbtbndlem2  48548  flsubz  49279  rege1logbrege0  49315  nn0digval  49357  rrx2vlinest  49498  line2  49509  line2xlem  49510  line2x  49511  itscnhlc0yqe  49516  itsclc0yqsollem2  49520  itsclc0yqsol  49521  itscnhlc0xyqsol  49522  itschlc0xyqsol1  49523  itsclc0xyqsolr  49526  itsclquadb  49533  reseccl  50508  recsccl  50509  recotcl  50510