Theorem recn 7900

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 7765  ℝcr 7766

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-resscn 7859

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  mulid1  7910  recnd  7941  pnfnre  7954  mnfnre  7955  cnegexlem1  8087  cnegexlem2  8088  cnegexlem3  8089  cnegex  8090  renegcl  8173  resubcl  8176  negf1o  8294  mul02lem2  8300  ltaddneg  8336  ltaddnegr  8337  ltaddsub2  8349  leaddsub2  8351  leltadd  8359  ltaddpos  8364  ltaddpos2  8365  posdif  8367  lenegcon1  8378  lenegcon2  8379  addge01  8384  addge02  8385  leaddle0  8389  mullt0  8392  recexre  8490  msqge0  8528  mulge0  8531  aprcl  8558  recexap  8564  ltm1  8755  prodgt02  8762  prodge02  8764  ltmul2  8765  lemul2  8766  lemul2a  8768  ltmulgt12  8774  lemulge12  8776  gt0div  8779  ge0div  8780  ltmuldiv2  8784  ltdivmul  8785  ltdivmul2  8787  ledivmul2  8789  lemuldiv2  8791  negiso  8864  cju  8870  nnge1  8894  halfpos  9102  lt2halves  9106  addltmul  9107  avgle1  9111  avgle2  9112  div4p1lem1div2  9124  nnrecl  9126  elznn0  9220  elznn  9221  nzadd  9257  zmulcl  9258  difgtsumgt  9274  elz2  9276  gtndiv  9300  zeo  9310  supminfex  9549  eqreznegel  9566  negm  9567  irradd  9598  irrmul  9599  divlt1lt  9674  divle1le  9675  xnegneg  9783  rexsub  9803  xnegid  9809  xaddcom  9811  xaddid1  9812  xnegdi  9818  xaddass  9819  xleaddadd  9837  divelunit  9952  fzonmapblen  10136  expgt1  10507  mulexpzap  10509  leexp1a  10524  expubnd  10526  sqgt0ap  10537  lt2sq  10542  le2sq  10543  sqge0  10545  sumsqeq0  10547  bernneq  10589  bernneq2  10590  nn0ltexp2  10637  crre  10814  crim  10815  reim0  10818  mulreap  10821  rere  10822  remul2  10830  redivap  10831  immul2  10837  imdivap  10838  cjre  10839  cjreim  10860  rennim  10959  sqrt0rlem  10960  resqrexlemover  10967  absreimsq  11024  absreim  11025  absnid  11030  leabs  11031  absre  11034  absresq  11035  sqabs  11039  ltabs  11044  absdiflt  11049  absdifle  11050  lenegsq  11052  abssuble0  11060  dfabsmax  11174  max0addsup  11176  negfi  11184  minclpr  11193  reefcl  11624  efgt0  11640  reeftlcl  11645  resinval  11671  recosval  11672  resin4p  11674  recos4p  11675  resincl  11676  recoscl  11677  retanclap  11678  efieq  11691  sinbnd  11708  cosbnd  11709  absefi  11724  odd2np1  11825  infssuzex  11897  remetdval  13298  bl2ioo  13301  ioo2bl  13302  sincosq1sgn  13506  sincosq2sgn  13507  sincosq3sgn  13508  sincosq4sgn  13509  sinq12gt0  13510  relogoprlem  13548  logcxp  13577  rpcxpcl  13583  cxpcom  13616  rprelogbdiv  13634  triap  14026  trirec0  14041