Theorem recn 8031

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7896  ℝcr 7897

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-resscn 7990

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  mulrid  8042  recnd  8074  pnfnre  8087  mnfnre  8088  cnegexlem1  8220  cnegexlem2  8221  cnegexlem3  8222  cnegex  8223  renegcl  8306  resubcl  8309  negf1o  8427  mul02lem2  8433  ltaddneg  8470  ltaddnegr  8471  ltaddsub2  8483  leaddsub2  8485  leltadd  8493  ltaddpos  8498  ltaddpos2  8499  posdif  8501  lenegcon1  8512  lenegcon2  8513  addge01  8518  addge02  8519  leaddle0  8523  mullt0  8526  recexre  8624  msqge0  8662  mulge0  8665  aprcl  8692  recexap  8699  rerecapb  8889  ltm1  8892  prodgt02  8899  prodge02  8901  ltmul2  8902  lemul2  8903  lemul2a  8905  ltmulgt12  8911  lemulge12  8913  gt0div  8916  ge0div  8917  ltmuldiv2  8921  ltdivmul  8922  ltdivmul2  8924  ledivmul2  8926  lemuldiv2  8928  negiso  9001  cju  9007  nnge1  9032  halfpos  9241  lt2halves  9246  addltmul  9247  avgle1  9251  avgle2  9252  div4p1lem1div2  9264  nnrecl  9266  elznn0  9360  elznn  9361  nzadd  9397  zmulcl  9398  difgtsumgt  9414  elz2  9416  gtndiv  9440  zeo  9450  supminfex  9690  eqreznegel  9707  negm  9708  irradd  9739  irrmul  9740  divlt1lt  9818  divle1le  9819  xnegneg  9927  rexsub  9947  xnegid  9953  xaddcom  9955  xaddid1  9956  xnegdi  9962  xaddass  9963  xleaddadd  9981  divelunit  10096  fzonmapblen  10282  infssuzex  10342  expgt1  10688  mulexpzap  10690  leexp1a  10705  expubnd  10707  sqgt0ap  10719  lt2sq  10724  le2sq  10725  sqge0  10727  sumsqeq0  10729  bernneq  10771  bernneq2  10772  nn0ltexp2  10820  crre  11041  crim  11042  reim0  11045  mulreap  11048  rere  11049  remul2  11057  redivap  11058  immul2  11064  imdivap  11065  cjre  11066  cjreim  11087  rennim  11186  sqrt0rlem  11187  resqrexlemover  11194  absreimsq  11251  absreim  11252  absnid  11257  leabs  11258  absre  11261  absresq  11262  sqabs  11266  ltabs  11271  absdiflt  11276  absdifle  11277  lenegsq  11279  abssuble0  11287  dfabsmax  11401  max0addsup  11403  negfi  11412  minclpr  11421  reefcl  11852  efgt0  11868  reeftlcl  11873  resinval  11899  recosval  11900  resin4p  11902  recos4p  11903  resincl  11904  recoscl  11905  retanclap  11906  efieq  11919  sinbnd  11936  cosbnd  11937  absefi  11953  odd2np1  12057  remetdval  14891  bl2ioo  14894  ioo2bl  14895  hoverb  14992  plyreres  15108  sincosq1sgn  15170  sincosq2sgn  15171  sincosq3sgn  15172  sincosq4sgn  15173  sinq12gt0  15174  relogoprlem  15212  logcxp  15241  rpcxpcl  15247  cxpcom  15282  rprelogbdiv  15301  gausslemma2dlem1a  15407  triap  15786  trirec0  15801