Theorem recn 8265

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℂcc 8130  ℝcr 8131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8224

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3219  df-ss 3226

This theorem is referenced by:  mulrid  8276  recnd  8307  pnfnre  8320  mnfnre  8321  cnegexlem1  8453  cnegexlem2  8454  cnegexlem3  8455  cnegex  8456  renegcl  8539  resubcl  8542  negf1o  8660  mul02lem2  8666  ltaddneg  8703  ltaddnegr  8704  ltaddsub2  8716  leaddsub2  8718  leltadd  8726  ltaddpos  8731  ltaddpos2  8732  posdif  8734  lenegcon1  8745  lenegcon2  8746  addge01  8751  addge02  8752  leaddle0  8756  mullt0  8759  recexre  8857  msqge0  8895  mulge0  8898  aprcl  8925  recexap  8932  rerecapb  9122  ltm1  9125  prodgt02  9132  prodge02  9134  ltmul2  9135  lemul2  9136  lemul2a  9138  ltmulgt12  9144  lemulge12  9146  gt0div  9149  ge0div  9150  ltmuldiv2  9154  ltdivmul  9155  ltdivmul2  9157  ledivmul2  9159  lemuldiv2  9161  negiso  9234  cju  9240  nnge1  9265  halfpos  9474  lt2halves  9479  addltmul  9480  avgle1  9484  avgle2  9485  div4p1lem1div2  9497  nnrecl  9499  elznn0  9597  elznn  9598  nzadd  9635  zmulcl  9636  difgtsumgt  9652  elz2  9654  gtndiv  9679  zeo  9689  supminfex  9935  eqreznegel  9952  negm  9953  irradd  9984  irrmul  9985  divlt1lt  10063  divle1le  10064  xnegneg  10172  rexsub  10192  xnegid  10198  xaddcom  10200  xaddid1  10201  xnegdi  10207  xaddass  10208  xleaddadd  10226  divelunit  10341  fzonmapblen  10533  infssuzex  10600  expgt1  10946  mulexpzap  10948  leexp1a  10963  expubnd  10965  sqgt0ap  10977  lt2sq  10982  le2sq  10983  sqge0  10985  sumsqeq0  10987  bernneq  11030  bernneq2  11031  nn0ltexp2  11079  swrdccatin2  11429  swrdccat3blem  11439  crre  11550  crim  11551  reim0  11554  mulreap  11557  rere  11558  remul2  11566  redivap  11567  immul2  11573  imdivap  11574  cjre  11575  cjreim  11596  rennim  11695  sqrt0rlem  11696  resqrexlemover  11703  absreimsq  11760  absreim  11761  absnid  11766  leabs  11767  absre  11770  absresq  11771  sqabs  11775  ltabs  11780  absdiflt  11785  absdifle  11786  lenegsq  11788  abssuble0  11796  dfabsmax  11910  max0addsup  11912  negfi  11921  minclpr  11930  reefcl  12362  efgt0  12378  reeftlcl  12383  resinval  12409  recosval  12410  resin4p  12412  recos4p  12413  resincl  12414  recoscl  12415  retanclap  12416  efieq  12429  sinbnd  12446  cosbnd  12447  absefi  12463  odd2np1  12567  remetdval  15461  bl2ioo  15464  ioo2bl  15465  hoverb  15562  plyreres  15678  sincosq1sgn  15740  sincosq2sgn  15741  sincosq3sgn  15742  sincosq4sgn  15743  sinq12gt0  15744  relogoprlem  15782  logcxp  15811  rpcxpcl  15817  cxpcom  15852  rprelogbdiv  15871  gausslemma2dlem1a  15980  triap  16862  trirec0  16877