Theorem recn 11118

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11026  ℝcr 11027

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 11085

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

This theorem is referenced by:  mulrid  11132  recnd  11162  pnfnre  11175  mnfnre  11177  mul02  11312  ltaddneg  11350  ltaddnegr  11351  renegcli  11443  resubcl  11446  negn0  11567  negf1o  11568  ltaddsub2  11613  leaddsub2  11615  leltadd  11622  ltaddpos  11628  ltaddpos2  11629  posdif  11631  lenegcon1  11642  lenegcon2  11643  addge01  11648  addge02  11649  leaddle0  11653  mullt0  11657  recex  11770  ltm1  11984  prodgt02  11990  ltmul2  11993  lemul1  11994  lemul2  11995  lemul1a  11996  lemul2a  11997  ltmulgt12  12003  lemulge12  12006  gt0div  12009  ge0div  12010  mulge0b  12013  mulle0b  12014  ltmuldiv2  12017  ltdivmul  12018  ledivmul  12019  ltdivmul2  12020  lt2mul2div  12021  ledivmul2  12022  lemuldiv2  12024  ltdiv2  12029  ltrec1  12030  lerec2  12031  ledivdiv  12032  lediv2  12033  ltdiv23  12034  lediv23  12035  lediv12a  12036  recp1lt1  12041  ledivp1  12045  negfi  12092  infm3lem  12101  supmul  12115  riotaneg  12122  negiso  12123  cju  12142  nnge1  12174  halfpos  12372  lt2halves  12377  addltmul  12378  avgle1  12382  avgle2  12383  avgle  12384  div4p1lem1div2  12397  nnrecl  12400  difgtsumgt  12455  elznn0  12504  elznn  12505  elz2  12507  nzadd  12541  zmulcl  12542  gtndiv  12571  zeo  12580  eqreznegel  12853  supminf  12854  rebtwnz  12866  irradd  12892  irrmul  12893  divlt1lt  12982  divle1le  12983  max0sub  13116  xnegneg  13134  rexsub  13153  xnegid  13158  xaddcom  13160  xaddrid  13161  xnegdi  13168  xaddass  13169  rexmul  13191  xmulasslem3  13206  xadddilem  13214  divelunit  13415  fzonmapblen  13629  ico01fl0  13741  flzadd  13748  ltdifltdiv  13756  dfceil2  13761  intfrac2  13780  fldiv2  13783  flpmodeq  13796  mod0  13798  negmod0  13800  modlt  13802  modfrac  13806  flmod  13807  intfrac  13808  modmulnn  13811  modvalp1  13812  modid  13818  modcyc  13828  modcyc2  13829  modadd1  13830  modaddabs  13833  muladdmodid  13835  muladdmod  13837  negmod  13841  modadd2mod  13846  modmul1  13849  modmulmodr  13862  modaddmulmod  13863  moddi  13864  modsubdir  13865  modirr  13867  addmodlteq  13871  expgt1  14025  mulexpz  14027  sqgt0  14051  lt2sq  14058  le2sq  14059  sqge0  14061  expmordi  14092  leexp1a  14100  expubnd  14103  sumsqeq0  14104  sqlecan  14134  bernneq  14154  bernneq2  14155  expnbnd  14157  digit2  14161  digit1  14162  expnngt1  14166  swrdccatin2  14653  swrdccat3blem  14663  cshweqrep  14745  crre  15039  crim  15040  reim0  15043  mulre  15046  rere  15047  remul2  15055  rediv  15056  immul2  15062  imdiv  15063  cjre  15064  cjreim  15085  rennim  15164  resqrex  15175  resqreu  15177  resqrtcl  15178  resqrtthlem  15179  sqrtneglem  15191  sqrtneg  15192  absreimsq  15217  absreim  15218  absnid  15223  leabs  15224  absre  15226  absresq  15227  sqabs  15232  max0add  15235  absz  15236  absdiflt  15243  absdifle  15244  lenegsq  15246  abssuble0  15254  absmax  15255  rddif  15266  absrdbnd  15267  o1rlimmul  15544  caurcvg2  15603  reefcl  16012  efgt0  16030  reeftlcl  16035  resinval  16062  recosval  16063  resin4p  16065  recos4p  16066  resincl  16067  recoscl  16068  retancl  16069  resinhcl  16083  rpcoshcl  16084  retanhcl  16086  tanhlt1  16087  tanhbnd  16088  efieq  16090  sinbnd  16107  cosbnd  16108  absefi  16123  dvdsaddre2b  16236  odd2np1  16270  bezoutlem1  16468  xrsdsreclb  21338  remulg  21532  resubdrg  21533  remetdval  24693  bl2ioo  24696  ioo2bl  24697  cnperf  24725  icccvx  24864  tcphcph  25153  shft2rab  25425  volsup2  25522  volcn  25523  c1lip1  25918  plyreres  26206  aalioulem3  26258  taylthlem2  26298  taylthlem2OLD  26299  reeff1o  26373  reefgim  26376  sincosq1sgn  26423  sincosq2sgn  26424  sincosq3sgn  26425  sincosq4sgn  26426  sinq12gt0  26432  pige3ALT  26445  efif1olem4  26470  efifo  26472  relogrn  26486  logrnaddcl  26499  relogoprlem  26516  advlog  26579  advlogexp  26580  logtayl  26585  recxpcl  26600  rpcxpcl  26601  cxpge0  26608  cxpcom  26664  dvcxp1  26665  logreclem  26688  relogbreexp  26701  relogbcxp  26711  angpieqvd  26757  atanre  26811  basellem9  27015  gausslemma2dlem1a  27292  2sqnn0  27365  log2sumbnd  27471  brbtwn2  28868  colinearalglem4  28872  colinearalg  28873  crctcshwlkn0lem1  29773  nvsge0  30626  nmoub3i  30735  nmlnoubi  30758  isblo3i  30763  ipasslem3  30795  ipasslem9  30800  ipasslem11  30802  hmopm  31983  riesz1  32027  leopmuli  32095  leopmul  32096  leopmul2i  32097  leopnmid  32100  nmopleid  32101  cdj1i  32395  cdj3lem1  32396  cdj3i  32403  addltmulALT  32408  sgnneg  32791  dpfrac1  32845  rexdiv  32879  xdivid  32881  xdiv0  32882  lediv2aALT  35649  nndivlub  36431  irrdiff  37299  cos2h  37590  tan2h  37591  poimir  37632  mblfinlem2  37637  mblfinlem4  37639  itg2addnclem  37650  itg2addnclem2  37651  dvasin  37683  areacirclem1  37687  areacirclem2  37688  areacirclem4  37690  areacirclem5  37691  areacirc  37692  lcmineqlem12  42013  dvrelog2b  42039  aks4d1p1p6  42046  retire  42292  readvrec2  42334  readvrec  42335  resubeulem2  42349  renegneg  42385  renegid2  42387  sn-it0e0  42389  sn-negex12  42390  resubeqsub  42403  sn-mullid  42409  sn-mul02  42425  areaquad  43189  reabssgn  43609  radcnvrat  44287  lhe4.4ex1a  44302  expgrowthi  44306  mulltgt0  45000  refsum2cnlem1  45015  infnsuprnmpt  45228  dstregt0  45264  suplesup  45319  infleinflem1  45350  infleinflem2  45351  ltdiv23neg  45374  rexabslelem  45398  supminfrnmpt  45425  supminfxr  45444  fmul01lt1lem1  45566  lptre2pt  45622  cnrefiisplem  45811  dvcosre  45894  itgsin0pilem1  45932  itgsinexplem1  45936  volioc  45954  volico  45965  stoweidlem7  45989  stoweidlem10  45992  stoweidlem19  46001  stoweidlem34  46016  stoweid  46045  dirker2re  46074  dirkerdenne0  46075  dirkerper  46078  dirkertrigeq  46083  dirkeritg  46084  fourierdlem39  46128  fourierdlem42  46131  fourierdlem47  46135  fourierdlem56  46144  fourierdlem57  46145  fourierdlem58  46146  fourierdlem60  46148  fourierdlem61  46149  fourierdlem73  46161  fourierdlem76  46164  fourierdlem77  46165  fourierdlem92  46180  fourierdlem97  46185  etransclem46  46262  volico2  46623  smflimlem4  46756  smfinflem  46799  et-sqrtnegnre  46855  squeezedltsq  46871  2leaddle2  47283  ltsubsubaddltsub  47286  sqrtnegnre  47292  ceildivmod  47324  m1mod0mod1  47339  requad01  47606  requad1  47607  bgoldbtbndlem2  47791  flsubz  48508  rege1logbrege0  48544  nn0digval  48586  rrx2vlinest  48727  line2  48738  line2xlem  48739  line2x  48740  itscnhlc0yqe  48745  itsclc0yqsollem2  48749  itsclc0yqsol  48750  itscnhlc0xyqsol  48751  itschlc0xyqsol1  48752  itsclc0xyqsolr  48755  itsclquadb  48762  reseccl  49739  recsccl  49740  recotcl  49741