Theorem recn 8029

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7894  ℝcr 7895

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 7988

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  8040  recnd  8072  pnfnre  8085  mnfnre  8086  cnegexlem1  8218  cnegexlem2  8219  cnegexlem3  8220  cnegex  8221  renegcl  8304  resubcl  8307  negf1o  8425  mul02lem2  8431  ltaddneg  8468  ltaddnegr  8469  ltaddsub2  8481  leaddsub2  8483  leltadd  8491  ltaddpos  8496  ltaddpos2  8497  posdif  8499  lenegcon1  8510  lenegcon2  8511  addge01  8516  addge02  8517  leaddle0  8521  mullt0  8524  recexre  8622  msqge0  8660  mulge0  8663  aprcl  8690  recexap  8697  rerecapb  8887  ltm1  8890  prodgt02  8897  prodge02  8899  ltmul2  8900  lemul2  8901  lemul2a  8903  ltmulgt12  8909  lemulge12  8911  gt0div  8914  ge0div  8915  ltmuldiv2  8919  ltdivmul  8920  ltdivmul2  8922  ledivmul2  8924  lemuldiv2  8926  negiso  8999  cju  9005  nnge1  9030  halfpos  9239  lt2halves  9244  addltmul  9245  avgle1  9249  avgle2  9250  div4p1lem1div2  9262  nnrecl  9264  elznn0  9358  elznn  9359  nzadd  9395  zmulcl  9396  difgtsumgt  9412  elz2  9414  gtndiv  9438  zeo  9448  supminfex  9688  eqreznegel  9705  negm  9706  irradd  9737  irrmul  9738  divlt1lt  9816  divle1le  9817  xnegneg  9925  rexsub  9945  xnegid  9951  xaddcom  9953  xaddid1  9954  xnegdi  9960  xaddass  9961  xleaddadd  9979  divelunit  10094  fzonmapblen  10280  infssuzex  10340  expgt1  10686  mulexpzap  10688  leexp1a  10703  expubnd  10705  sqgt0ap  10717  lt2sq  10722  le2sq  10723  sqge0  10725  sumsqeq0  10727  bernneq  10769  bernneq2  10770  nn0ltexp2  10818  crre  11039  crim  11040  reim0  11043  mulreap  11046  rere  11047  remul2  11055  redivap  11056  immul2  11062  imdivap  11063  cjre  11064  cjreim  11085  rennim  11184  sqrt0rlem  11185  resqrexlemover  11192  absreimsq  11249  absreim  11250  absnid  11255  leabs  11256  absre  11259  absresq  11260  sqabs  11264  ltabs  11269  absdiflt  11274  absdifle  11275  lenegsq  11277  abssuble0  11285  dfabsmax  11399  max0addsup  11401  negfi  11410  minclpr  11419  reefcl  11850  efgt0  11866  reeftlcl  11871  resinval  11897  recosval  11898  resin4p  11900  recos4p  11901  resincl  11902  recoscl  11903  retanclap  11904  efieq  11917  sinbnd  11934  cosbnd  11935  absefi  11951  odd2np1  12055  remetdval  14867  bl2ioo  14870  ioo2bl  14871  hoverb  14968  plyreres  15084  sincosq1sgn  15146  sincosq2sgn  15147  sincosq3sgn  15148  sincosq4sgn  15149  sinq12gt0  15150  relogoprlem  15188  logcxp  15217  rpcxpcl  15223  cxpcom  15258  rprelogbdiv  15277  gausslemma2dlem1a  15383  triap  15760  trirec0  15775