Theorem recn 8012

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7877  ℝcr 7878

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 7971

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  8023  recnd  8055  pnfnre  8068  mnfnre  8069  cnegexlem1  8201  cnegexlem2  8202  cnegexlem3  8203  cnegex  8204  renegcl  8287  resubcl  8290  negf1o  8408  mul02lem2  8414  ltaddneg  8451  ltaddnegr  8452  ltaddsub2  8464  leaddsub2  8466  leltadd  8474  ltaddpos  8479  ltaddpos2  8480  posdif  8482  lenegcon1  8493  lenegcon2  8494  addge01  8499  addge02  8500  leaddle0  8504  mullt0  8507  recexre  8605  msqge0  8643  mulge0  8646  aprcl  8673  recexap  8680  rerecapb  8870  ltm1  8873  prodgt02  8880  prodge02  8882  ltmul2  8883  lemul2  8884  lemul2a  8886  ltmulgt12  8892  lemulge12  8894  gt0div  8897  ge0div  8898  ltmuldiv2  8902  ltdivmul  8903  ltdivmul2  8905  ledivmul2  8907  lemuldiv2  8909  negiso  8982  cju  8988  nnge1  9013  halfpos  9222  lt2halves  9227  addltmul  9228  avgle1  9232  avgle2  9233  div4p1lem1div2  9245  nnrecl  9247  elznn0  9341  elznn  9342  nzadd  9378  zmulcl  9379  difgtsumgt  9395  elz2  9397  gtndiv  9421  zeo  9431  supminfex  9671  eqreznegel  9688  negm  9689  irradd  9720  irrmul  9721  divlt1lt  9799  divle1le  9800  xnegneg  9908  rexsub  9928  xnegid  9934  xaddcom  9936  xaddid1  9937  xnegdi  9943  xaddass  9944  xleaddadd  9962  divelunit  10077  fzonmapblen  10263  infssuzex  10323  expgt1  10669  mulexpzap  10671  leexp1a  10686  expubnd  10688  sqgt0ap  10700  lt2sq  10705  le2sq  10706  sqge0  10708  sumsqeq0  10710  bernneq  10752  bernneq2  10753  nn0ltexp2  10801  crre  11022  crim  11023  reim0  11026  mulreap  11029  rere  11030  remul2  11038  redivap  11039  immul2  11045  imdivap  11046  cjre  11047  cjreim  11068  rennim  11167  sqrt0rlem  11168  resqrexlemover  11175  absreimsq  11232  absreim  11233  absnid  11238  leabs  11239  absre  11242  absresq  11243  sqabs  11247  ltabs  11252  absdiflt  11257  absdifle  11258  lenegsq  11260  abssuble0  11268  dfabsmax  11382  max0addsup  11384  negfi  11393  minclpr  11402  reefcl  11833  efgt0  11849  reeftlcl  11854  resinval  11880  recosval  11881  resin4p  11883  recos4p  11884  resincl  11885  recoscl  11886  retanclap  11887  efieq  11900  sinbnd  11917  cosbnd  11918  absefi  11934  odd2np1  12038  remetdval  14783  bl2ioo  14786  ioo2bl  14787  hoverb  14884  plyreres  15000  sincosq1sgn  15062  sincosq2sgn  15063  sincosq3sgn  15064  sincosq4sgn  15065  sinq12gt0  15066  relogoprlem  15104  logcxp  15133  rpcxpcl  15139  cxpcom  15174  rprelogbdiv  15193  gausslemma2dlem1a  15299  triap  15673  trirec0  15688