Theorem recn 11208

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℂcc 11116  ℝcr 11117

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-resscn 11175

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2841  df-ss 3925

This theorem is used by:  mulrid  11224  recnd  11255  pnfnre  11268  mnfnre  11270  mul02  11406  ltaddneg  11444  ltaddnegr  11445  renegcli  11537  resubcl  11540  negn0  11661  negf1o  11662  ltaddsub2  11707  leaddsub2  11709  leltadd  11716  ltaddpos  11722  ltaddpos2  11723  posdif  11725  lenegcon1  11736  lenegcon2  11737  addge01  11742  addge02  11743  leaddle0  11747  mullt0  11751  recex  11864  ltm1  12075  prodgt02  12081  ltmul2  12084  lemul1  12085  lemul2  12086  lemul1a  12087  lemul2a  12088  ltmulgt12  12093  lemulge12  12096  gt0div  12099  ge0div  12100  mulge0b  12103  mulle0b  12104  ltmuldiv2  12107  ltdivmul  12108  ledivmul  12109  ltdivmul2  12110  lt2mul2div  12111  ledivmul2  12112  lemuldiv2  12114  ltdiv2  12119  ltrec1  12120  lerec2  12121  ledivdiv  12122  lediv2  12123  ltdiv23  12124  lediv23  12125  lediv12a  12126  recp1lt1  12131  ledivp1  12135  negfi  12182  infm3lem  12191  supmul  12205  riotaneg  12212  negiso  12213  cju  12232  nnge1  12282  halfpos  12492  lt2halves  12497  addltmul  12498  avgle1  12502  avgle2  12503  avgle  12504  div4p1lem1div2  12517  nnrecl  12520  difgtsumgt  12575  elznn0  12624  elznn  12625  elz2  12627  nzadd  12660  zmulcl  12661  gtndiv  12691  zeo  12700  eqreznegel  12976  supminf  12977  rebtwnz  12989  irradd  13015  irrmul  13016  divlt1lt  13105  divle1le  13106  max0sub  13240  xnegneg  13258  rexsub  13277  xnegid  13282  xaddcom  13284  xaddrid  13285  xnegdi  13292  xaddass  13293  rexmul  13315  xmulasslem3  13330  xadddilem  13338  divelunit  13539  fzonmapblen  13756  ico01fl0  13872  flzadd  13879  ltdifltdiv  13887  dfceil2  13892  intfrac2  13911  fldiv2  13914  flpmodeq  13927  mod0  13929  negmod0  13931  modlt  13933  modfrac  13937  flmod  13938  intfrac  13939  modmulnn  13942  modvalp1  13943  modid  13949  modcyc  13959  modcyc2  13960  modadd1  13961  modaddabs  13964  muladdmodid  13966  muladdmod  13968  negmod  13972  modadd2mod  13977  modmul1  13980  modmulmodr  13993  modaddmulmod  13994  moddi  13995  modsubdir  13996  modirr  13998  addmodlteq  14002  expgt1  14156  mulexpz  14158  sqgt0  14182  lt2sq  14189  le2sq  14190  sqge0  14192  expmordi  14223  leexp1a  14231  expubnd  14234  sumsqeq0  14235  sqlecan  14265  bernneq  14285  bernneq2  14286  expnbnd  14288  digit2  14292  digit1  14293  expnngt1  14297  swrdccatin2  14790  swrdccat3blem  14800  cshweqrep  14884  sgnneg  15163  crre  15191  crim  15192  reim0  15195  mulre  15198  rere  15199  remul2  15207  rediv  15208  immul2  15214  imdiv  15215  cjre  15216  cjreim  15237  rennim  15316  resqrex  15327  resqreu  15329  resqrtcl  15330  resqrtthlem  15331  sqrtneglem  15343  sqrtneg  15344  absreimsq  15369  absreim  15370  absnid  15375  leabs  15376  absre  15378  absresq  15379  sqabs  15384  max0add  15387  absz  15388  absdiflt  15395  absdifle  15396  lenegsq  15398  abssuble0  15406  absmax  15407  rddif  15418  absrdbnd  15419  o1rlimmul  15696  caurcvg2  15755  reefcl  16166  efgt0  16184  reeftlcl  16189  resinval  16216  recosval  16217  resin4p  16219  recos4p  16220  resincl  16221  recoscl  16222  retancl  16223  resinhcl  16237  rpcoshcl  16238  retanhcl  16240  tanhlt1  16241  tanhbnd  16242  efieq  16244  sinbnd  16261  cosbnd  16262  absefi  16277  dvdsaddre2b  16390  odd2np1  16424  bezoutlem1  16622  xrsdsreclb  21601  remulg  21794  resubdrg  21795  remetdval  24983  bl2ioo  24986  ioo2bl  24987  cnperf  25015  icccvx  25146  tcphcph  25433  shft2rab  25704  volsup2  25801  volcn  25802  c1lip1  26193  plyreres  26481  aalioulem3  26534  taylthlem2  26574  reeff1o  26647  reefgim  26650  sincosq1sgn  26700  sincosq2sgn  26701  sincosq3sgn  26702  sincosq4sgn  26703  sinq12gt0  26709  pige3ALT  26722  efif1olem4  26747  efifo  26749  relogrn  26763  logrnaddcl  26776  relogoprlem  26793  advlog  26856  advlogexp  26857  logtayl  26862  recxpcl  26877  rpcxpcl  26878  cxpge0  26885  cxpcom  26941  dvcxp1  26942  logreclem  26964  relogbreexp  26977  relogbcxp  26987  angpieqvd  27033  atanre  27087  basellem9  27290  gausslemma2dlem1a  27566  2sqnn0  27639  log2sumbnd  27745  brbtwn2  29292  colinearalglem4  29296  colinearalg  29297  crctcshwlkn0lem1  30196  nvsge0  31053  nmoub3i  31162  nmlnoubi  31185  isblo3i  31190  ipasslem3  31222  ipasslem9  31227  ipasslem11  31229  hmopm  32410  riesz1  32454  leopmuli  32522  leopmul  32523  leopmul2i  32524  leopnmid  32527  nmopleid  32528  cdj1i  32822  cdj3lem1  32823  cdj3i  32830  addltmulALT  32835  dpfrac1  33248  rexdiv  33282  xdivid  33284  xdiv0  33285  lediv2aALT  36190  nndivlub  37010  irrdiff  38011  cos2h  38303  tan2h  38304  poimir  38345  mblfinlem2  38350  mblfinlem4  38352  itg2addnclem  38363  itg2addnclem2  38364  dvasin  38396  areacirclem1  38400  areacirclem2  38401  areacirclem4  38403  areacirclem5  38404  areacirc  38405  lcmineqlem12  42848  dvrelog2b  42874  aks4d1p1p6  42881  retire  43121  readvrec2  43163  readvrec  43164  resubeulem2  43178  renegneg  43214  renegid2  43216  sn-it0e0  43218  sn-negex12  43219  resubeqsub  43232  sn-mullid  43238  sn-mul02  43267  areaquad  43984  reabssgn  44403  radcnvrat  45065  lhe4.4ex1a  45080  expgrowthi  45084  mulltgt0  45783  refsum2cnlem1  45798  infnsuprnmpt  46006  dstregt0  46042  suplesup  46096  infleinflem1  46126  infleinflem2  46127  ltdiv23neg  46150  rexabslelem  46173  supminfrnmpt  46200  supminfxr  46219  fmul01lt1lem1  46341  lptre2pt  46395  cnrefiisplem  46584  dvcosre  46667  itgsin0pilem1  46705  itgsinexplem1  46709  volioc  46727  volico  46738  stoweidlem7  46762  stoweidlem10  46765  stoweidlem19  46774  stoweidlem34  46789  stoweid  46818  dirker2re  46847  dirkerdenne0  46848  dirkerper  46851  dirkertrigeq  46856  dirkeritg  46857  fourierdlem39  46901  fourierdlem42  46904  fourierdlem47  46908  fourierdlem56  46917  fourierdlem57  46918  fourierdlem58  46919  fourierdlem60  46921  fourierdlem61  46922  fourierdlem73  46934  fourierdlem76  46937  fourierdlem77  46938  fourierdlem92  46953  fourierdlem97  46958  etransclem46  47035  volico2  47396  smflimlem4  47529  smfinflem  47572  et-sqrtnegnre  47628  squeezedltsq  47644  2leaddle2  48076  ltsubsubaddltsub  48079  sqrtnegnre  48085  ceildivmod  48123  m1mod0mod1  48138  requad01  48427  requad1  48428  bgoldbtbndlem2  48612  flsubz  49343  rege1logbrege0  49379  nn0digval  49421  rrx2vlinest  49562  line2  49573  line2xlem  49574  line2x  49575  itscnhlc0yqe  49580  itsclc0yqsollem2  49584  itsclc0yqsol  49585  itscnhlc0xyqsol  49586  itschlc0xyqsol1  49587  itsclc0xyqsolr  49590  itsclquadb  49597  reseccl  50572  recsccl  50573  recotcl  50574