Theorem recn 11236

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

Syntax hints:   → wi 4   ∈ wcel 2099  ℂcc 11144  ℝcr 11145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-resscn 11203

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-clel 2803  df-ss 3963

This theorem is referenced by:  mulrid  11250  recnd  11280  pnfnre  11293  mnfnre  11295  mul02  11430  ltaddneg  11467  ltaddnegr  11468  renegcli  11559  resubcl  11562  negn0  11681  negf1o  11682  ltaddsub2  11727  leaddsub2  11729  leltadd  11736  ltaddpos  11742  ltaddpos2  11743  posdif  11745  lenegcon1  11756  lenegcon2  11757  addge01  11762  addge02  11763  leaddle0  11767  mullt0  11771  recex  11884  ltm1  12098  prodgt02  12104  ltmul2  12107  lemul1  12108  lemul2  12109  lemul1a  12110  lemul2a  12111  ltmulgt12  12117  lemulge12  12120  gt0div  12123  ge0div  12124  mulge0b  12127  mulle0b  12128  ltmuldiv2  12131  ltdivmul  12132  ledivmul  12133  ltdivmul2  12134  lt2mul2div  12135  ledivmul2  12136  lemuldiv2  12138  ltdiv2  12143  ltrec1  12144  lerec2  12145  ledivdiv  12146  lediv2  12147  ltdiv23  12148  lediv23  12149  lediv12a  12150  recp1lt1  12155  ledivp1  12159  negfi  12206  infm3lem  12215  supmul  12229  riotaneg  12236  negiso  12237  cju  12251  nnge1  12283  halfpos  12485  lt2halves  12490  addltmul  12491  avgle1  12495  avgle2  12496  avgle  12497  div4p1lem1div2  12510  nnrecl  12513  difgtsumgt  12568  elznn0  12616  elznn  12617  elz2  12619  nzadd  12653  zmulcl  12654  gtndiv  12682  zeo  12691  eqreznegel  12961  supminf  12962  rebtwnz  12974  irradd  13000  irrmul  13001  divlt1lt  13088  divle1le  13089  max0sub  13220  xnegneg  13238  rexsub  13257  xnegid  13262  xaddcom  13264  xaddrid  13265  xnegdi  13272  xaddass  13273  rexmul  13295  xmulasslem3  13310  xadddilem  13318  divelunit  13516  fzonmapblen  13723  ico01fl0  13830  flzadd  13837  ltdifltdiv  13845  dfceil2  13850  intfrac2  13869  fldiv2  13872  flpmodeq  13885  mod0  13887  negmod0  13889  modlt  13891  modfrac  13895  flmod  13896  intfrac  13897  modmulnn  13900  modvalp1  13901  modid  13907  modcyc  13917  modcyc2  13918  modadd1  13919  modaddabs  13920  muladdmodid  13922  negmod  13927  modadd2mod  13932  modmul1  13935  modmulmodr  13948  modaddmulmod  13949  moddi  13950  modsubdir  13951  modirr  13953  addmodlteq  13957  expgt1  14111  mulexpz  14113  sqgt0  14136  lt2sq  14143  le2sq  14144  sqge0  14146  expmordi  14177  leexp1a  14185  expubnd  14187  sumsqeq0  14188  sqlecan  14218  bernneq  14238  bernneq2  14239  expnbnd  14241  digit2  14245  digit1  14246  expnngt1  14250  swrdccatin2  14729  swrdccat3blem  14739  cshweqrep  14821  crre  15111  crim  15112  reim0  15115  mulre  15118  rere  15119  remul2  15127  rediv  15128  immul2  15134  imdiv  15135  cjre  15136  cjreim  15157  rennim  15236  resqrex  15247  resqreu  15249  resqrtcl  15250  resqrtthlem  15251  sqrtneglem  15263  sqrtneg  15264  absreimsq  15289  absreim  15290  absnid  15295  leabs  15296  absre  15298  absresq  15299  sqabs  15304  max0add  15307  absz  15308  absdiflt  15314  absdifle  15315  lenegsq  15317  abssuble0  15325  absmax  15326  rddif  15337  absrdbnd  15338  o1rlimmul  15613  caurcvg2  15674  reefcl  16081  efgt0  16097  reeftlcl  16102  resinval  16129  recosval  16130  resin4p  16132  recos4p  16133  resincl  16134  recoscl  16135  retancl  16136  resinhcl  16150  rpcoshcl  16151  retanhcl  16153  tanhlt1  16154  tanhbnd  16155  efieq  16157  sinbnd  16174  cosbnd  16175  absefi  16190  dvdsaddre2b  16301  odd2np1  16335  bezoutlem1  16532  xrsdsreclb  21403  remulg  21596  resubdrg  21597  remetdval  24790  bl2ioo  24793  ioo2bl  24794  cnperf  24821  icccvx  24960  tcphcph  25250  shft2rab  25522  volsup2  25619  volcn  25620  c1lip1  26015  plyreres  26304  aalioulem3  26356  taylthlem2  26396  taylthlem2OLD  26397  reeff1o  26471  reefgim  26474  sincosq1sgn  26520  sincosq2sgn  26521  sincosq3sgn  26522  sincosq4sgn  26523  sinq12gt0  26529  pige3ALT  26541  efif1olem4  26566  efifo  26568  relogrn  26582  logrnaddcl  26595  relogoprlem  26612  advlog  26675  advlogexp  26676  logtayl  26681  recxpcl  26696  rpcxpcl  26697  cxpge0  26704  cxpcom  26760  dvcxp1  26761  logreclem  26784  relogbreexp  26797  relogbcxp  26807  angpieqvd  26853  atanre  26907  basellem9  27111  gausslemma2dlem1a  27388  2sqnn0  27461  log2sumbnd  27567  brbtwn2  28833  colinearalglem4  28837  colinearalg  28838  crctcshwlkn0lem1  29738  nvsge0  30591  nmoub3i  30700  nmlnoubi  30723  isblo3i  30728  ipasslem3  30760  ipasslem9  30765  ipasslem11  30767  hmopm  31948  riesz1  31992  leopmuli  32060  leopmul  32061  leopmul2i  32062  leopnmid  32065  nmopleid  32066  cdj1i  32360  cdj3lem1  32361  cdj3i  32368  addltmulALT  32373  dpfrac1  32753  rexdiv  32787  xdivid  32789  xdiv0  32790  sgnneg  34384  lediv2aALT  35515  nndivlub  36180  irrdiff  37043  cos2h  37322  tan2h  37323  poimir  37364  mblfinlem2  37369  mblfinlem4  37371  itg2addnclem  37382  itg2addnclem2  37383  dvasin  37415  areacirclem1  37419  areacirclem2  37420  areacirclem4  37422  areacirclem5  37423  areacirc  37424  lcmineqlem12  41749  dvrelog2b  41775  aks4d1p1p6  41782  2xp3dxp2ge1d  41946  retire  42044  resubeulem2  42084  renegneg  42119  renegid2  42121  sn-it0e0  42123  sn-negex12  42124  resubeqsub  42137  sn-mullid  42143  sn-mul02  42148  areaquad  42915  reabssgn  43337  radcnvrat  44022  lhe4.4ex1a  44037  expgrowthi  44041  mulltgt0  44655  refsum2cnlem1  44670  infnsuprnmpt  44892  dstregt0  44929  suplesup  44987  infleinflem1  45018  infleinflem2  45019  ltdiv23neg  45042  rexabslelem  45066  supminfrnmpt  45093  supminfxr  45112  fmul01lt1lem1  45238  lptre2pt  45294  cnrefiisplem  45483  dvcosre  45566  itgsin0pilem1  45604  itgsinexplem1  45608  volioc  45626  volico  45637  stoweidlem7  45661  stoweidlem10  45664  stoweidlem19  45673  stoweidlem34  45688  stoweid  45717  dirker2re  45746  dirkerdenne0  45747  dirkerper  45750  dirkertrigeq  45755  dirkeritg  45756  fourierdlem39  45800  fourierdlem42  45803  fourierdlem47  45807  fourierdlem56  45816  fourierdlem57  45817  fourierdlem58  45818  fourierdlem60  45820  fourierdlem61  45821  fourierdlem73  45833  fourierdlem76  45836  fourierdlem77  45837  fourierdlem92  45852  fourierdlem97  45857  etransclem46  45934  volico2  46295  smflimlem4  46428  smfinflem  46471  et-sqrtnegnre  46527  2leaddle2  46944  ltsubsubaddltsub  46947  sqrtnegnre  46953  m1mod0mod1  46974  requad01  47226  requad1  47227  bgoldbtbndlem2  47411  flsubz  47938  rege1logbrege0  47979  nn0digval  48021  rrx2vlinest  48162  line2  48173  line2xlem  48174  line2x  48175  itscnhlc0yqe  48180  itsclc0yqsollem2  48184  itsclc0yqsol  48185  itscnhlc0xyqsol  48186  itschlc0xyqsol1  48187  itsclc0xyqsolr  48190  itsclquadb  48197  reseccl  48532  recsccl  48533  recotcl  48534