Theorem recn 11126

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℂcc 11034  ℝcr 11035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-resscn 11093

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2815  df-ss 3907

This theorem is referenced by:  mulrid  11140  recnd  11171  pnfnre  11184  mnfnre  11186  mul02  11322  ltaddneg  11360  ltaddnegr  11361  renegcli  11453  resubcl  11456  negn0  11577  negf1o  11578  ltaddsub2  11623  leaddsub2  11625  leltadd  11632  ltaddpos  11638  ltaddpos2  11639  posdif  11641  lenegcon1  11652  lenegcon2  11653  addge01  11658  addge02  11659  leaddle0  11663  mullt0  11667  recex  11780  ltm1  11995  prodgt02  12001  ltmul2  12004  lemul1  12005  lemul2  12006  lemul1a  12007  lemul2a  12008  ltmulgt12  12014  lemulge12  12017  gt0div  12020  ge0div  12021  mulge0b  12024  mulle0b  12025  ltmuldiv2  12028  ltdivmul  12029  ledivmul  12030  ltdivmul2  12031  lt2mul2div  12032  ledivmul2  12033  lemuldiv2  12035  ltdiv2  12040  ltrec1  12041  lerec2  12042  ledivdiv  12043  lediv2  12044  ltdiv23  12045  lediv23  12046  lediv12a  12047  recp1lt1  12052  ledivp1  12056  negfi  12103  infm3lem  12112  supmul  12126  riotaneg  12133  negiso  12134  cju  12153  nnge1  12203  halfpos  12405  lt2halves  12410  addltmul  12411  avgle1  12415  avgle2  12416  avgle  12417  div4p1lem1div2  12430  nnrecl  12433  difgtsumgt  12488  elznn0  12537  elznn  12538  elz2  12540  nzadd  12573  zmulcl  12574  gtndiv  12604  zeo  12613  eqreznegel  12882  supminf  12883  rebtwnz  12895  irradd  12921  irrmul  12922  divlt1lt  13011  divle1le  13012  max0sub  13146  xnegneg  13164  rexsub  13183  xnegid  13188  xaddcom  13190  xaddrid  13191  xnegdi  13198  xaddass  13199  rexmul  13221  xmulasslem3  13236  xadddilem  13244  divelunit  13445  fzonmapblen  13661  ico01fl0  13776  flzadd  13783  ltdifltdiv  13791  dfceil2  13796  intfrac2  13815  fldiv2  13818  flpmodeq  13831  mod0  13833  negmod0  13835  modlt  13837  modfrac  13841  flmod  13842  intfrac  13843  modmulnn  13846  modvalp1  13847  modid  13853  modcyc  13863  modcyc2  13864  modadd1  13865  modaddabs  13868  muladdmodid  13870  muladdmod  13872  negmod  13876  modadd2mod  13881  modmul1  13884  modmulmodr  13897  modaddmulmod  13898  moddi  13899  modsubdir  13900  modirr  13902  addmodlteq  13906  expgt1  14060  mulexpz  14062  sqgt0  14086  lt2sq  14093  le2sq  14094  sqge0  14096  expmordi  14127  leexp1a  14135  expubnd  14138  sumsqeq0  14139  sqlecan  14169  bernneq  14189  bernneq2  14190  expnbnd  14192  digit2  14196  digit1  14197  expnngt1  14201  swrdccatin2  14689  swrdccat3blem  14699  cshweqrep  14781  crre  15074  crim  15075  reim0  15078  mulre  15081  rere  15082  remul2  15090  rediv  15091  immul2  15097  imdiv  15098  cjre  15099  cjreim  15120  rennim  15199  resqrex  15210  resqreu  15212  resqrtcl  15213  resqrtthlem  15214  sqrtneglem  15226  sqrtneg  15227  absreimsq  15252  absreim  15253  absnid  15258  leabs  15259  absre  15261  absresq  15262  sqabs  15267  max0add  15270  absz  15271  absdiflt  15278  absdifle  15279  lenegsq  15281  abssuble0  15289  absmax  15290  rddif  15301  absrdbnd  15302  o1rlimmul  15579  caurcvg2  15638  reefcl  16050  efgt0  16068  reeftlcl  16073  resinval  16100  recosval  16101  resin4p  16103  recos4p  16104  resincl  16105  recoscl  16106  retancl  16107  resinhcl  16121  rpcoshcl  16122  retanhcl  16124  tanhlt1  16125  tanhbnd  16126  efieq  16128  sinbnd  16145  cosbnd  16146  absefi  16161  dvdsaddre2b  16274  odd2np1  16308  bezoutlem1  16506  xrsdsreclb  21396  remulg  21589  resubdrg  21590  remetdval  24779  bl2ioo  24782  ioo2bl  24783  cnperf  24811  icccvx  24942  tcphcph  25229  shft2rab  25500  volsup2  25597  volcn  25598  c1lip1  25989  plyreres  26274  aalioulem3  26325  taylthlem2  26364  reeff1o  26437  reefgim  26440  sincosq1sgn  26487  sincosq2sgn  26488  sincosq3sgn  26489  sincosq4sgn  26490  sinq12gt0  26496  pige3ALT  26509  efif1olem4  26534  efifo  26536  relogrn  26550  logrnaddcl  26563  relogoprlem  26580  advlog  26643  advlogexp  26644  logtayl  26649  recxpcl  26664  rpcxpcl  26665  cxpge0  26672  cxpcom  26728  dvcxp1  26729  logreclem  26751  relogbreexp  26764  relogbcxp  26774  angpieqvd  26820  atanre  26874  basellem9  27077  gausslemma2dlem1a  27353  2sqnn0  27426  log2sumbnd  27532  brbtwn2  28999  colinearalglem4  29003  colinearalg  29004  crctcshwlkn0lem1  29903  nvsge0  30760  nmoub3i  30869  nmlnoubi  30892  isblo3i  30897  ipasslem3  30929  ipasslem9  30934  ipasslem11  30936  hmopm  32117  riesz1  32161  leopmuli  32229  leopmul  32230  leopmul2i  32231  leopnmid  32234  nmopleid  32235  cdj1i  32529  cdj3lem1  32530  cdj3i  32537  addltmulALT  32542  sgnneg  32932  dpfrac1  32977  rexdiv  33011  xdivid  33013  xdiv0  33014  lediv2aALT  35912  nndivlub  36693  irrdiff  37693  cos2h  37985  tan2h  37986  poimir  38027  mblfinlem2  38032  mblfinlem4  38034  itg2addnclem  38045  itg2addnclem2  38046  dvasin  38078  areacirclem1  38082  areacirclem2  38083  areacirclem4  38085  areacirclem5  38086  areacirc  38087  lcmineqlem12  42532  dvrelog2b  42558  aks4d1p1p6  42565  retire  42803  readvrec2  42845  readvrec  42846  resubeulem2  42860  renegneg  42896  renegid2  42898  sn-it0e0  42900  sn-negex12  42901  resubeqsub  42914  sn-mullid  42920  sn-mul02  42949  areaquad  43668  reabssgn  44087  radcnvrat  44765  lhe4.4ex1a  44780  expgrowthi  44784  mulltgt0  45477  refsum2cnlem1  45492  infnsuprnmpt  45701  dstregt0  45737  suplesup  45791  infleinflem1  45821  infleinflem2  45822  ltdiv23neg  45845  rexabslelem  45868  supminfrnmpt  45895  supminfxr  45914  fmul01lt1lem1  46036  lptre2pt  46090  cnrefiisplem  46279  dvcosre  46362  itgsin0pilem1  46400  itgsinexplem1  46404  volioc  46422  volico  46433  stoweidlem7  46457  stoweidlem10  46460  stoweidlem19  46469  stoweidlem34  46484  stoweid  46513  dirker2re  46542  dirkerdenne0  46543  dirkerper  46546  dirkertrigeq  46551  dirkeritg  46552  fourierdlem39  46596  fourierdlem42  46599  fourierdlem47  46603  fourierdlem56  46612  fourierdlem57  46613  fourierdlem58  46614  fourierdlem60  46616  fourierdlem61  46617  fourierdlem73  46629  fourierdlem76  46632  fourierdlem77  46633  fourierdlem92  46648  fourierdlem97  46653  etransclem46  46730  volico2  47091  smflimlem4  47224  smfinflem  47267  et-sqrtnegnre  47323  squeezedltsq  47340  2leaddle2  47768  ltsubsubaddltsub  47771  sqrtnegnre  47777  ceildivmod  47815  m1mod0mod1  47830  requad01  48119  requad1  48120  bgoldbtbndlem2  48304  flsubz  49020  rege1logbrege0  49056  nn0digval  49098  rrx2vlinest  49239  line2  49250  line2xlem  49251  line2x  49252  itscnhlc0yqe  49257  itsclc0yqsollem2  49261  itsclc0yqsol  49262  itscnhlc0xyqsol  49263  itschlc0xyqsol1  49264  itsclc0xyqsolr  49267  itsclquadb  49274  reseccl  50250  recsccl  50251  recotcl  50252