Theorem recn 8306

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

Syntax hints:   → wi 4   ∈ wcel 2209  ℂcc 8171  ℝcr 8172

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8265

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  mulrid  8317  recnd  8348  pnfnre  8361  mnfnre  8362  cnegexlem1  8495  cnegexlem2  8496  cnegexlem3  8497  cnegex  8498  renegcl  8581  resubcl  8584  negf1o  8703  mul02lem2  8709  ltaddneg  8746  ltaddnegr  8747  ltaddsub2  8759  leaddsub2  8761  leltadd  8769  ltaddpos  8774  ltaddpos2  8775  posdif  8777  lenegcon1  8788  lenegcon2  8789  addge01  8794  addge02  8795  leaddle0  8799  mullt0  8802  recexre  8900  msqge0  8938  mulge0  8941  aprcl  8968  recexap  8975  rerecapb  9167  ltm1  9170  prodgt02  9177  prodge02  9179  ltmul2  9180  lemul2  9181  lemul2a  9183  ltmulgt12  9189  lemulge12  9191  gt0div  9194  ge0div  9195  ltmuldiv2  9199  ltdivmul  9200  ltdivmul2  9202  ledivmul2  9204  lemuldiv2  9206  negiso  9279  cju  9285  nnge1  9310  halfpos  9519  lt2halves  9524  addltmul  9525  avgle1  9529  avgle2  9530  div4p1lem1div2  9542  nnrecl  9544  elznn0  9642  elznn  9643  nzadd  9680  zmulcl  9681  difgtsumgt  9697  elz2  9699  gtndiv  9724  zeo  9734  supminfex  9980  eqreznegel  9997  negm  9998  irradd  10029  irrmul  10030  divlt1lt  10108  divle1le  10109  xnegneg  10218  rexsub  10238  xnegid  10244  xaddcom  10246  xaddid1  10247  xnegdi  10253  xaddass  10254  xleaddadd  10272  divelunit  10387  fzonmapblen  10582  infssuzex  10649  expgt1  10997  mulexpzap  10999  leexp1a  11014  expubnd  11016  sqgt0ap  11028  lt2sq  11033  le2sq  11034  sqge0  11036  sumsqeq0  11038  bernneq  11081  bernneq2  11082  nn0ltexp2  11130  swrdccatin2  11484  swrdccat3blem  11494  crre  11605  crim  11606  reim0  11609  mulreap  11612  rere  11613  remul2  11621  redivap  11622  immul2  11628  imdivap  11629  cjre  11630  cjreim  11652  rennim  11751  sqrt0rlem  11752  resqrexlemover  11759  absreimsq  11816  absreim  11817  absnid  11822  leabs  11823  absre  11826  absresq  11827  sqabs  11831  ltabs  11836  absdiflt  11841  absdifle  11842  lenegsq  11844  abssuble0  11852  dfabsmax  11966  max0addsup  11968  negfi  11977  minclpr  11986  reefcl  12418  efgt0  12434  reeftlcl  12439  resinval  12465  recosval  12466  resin4p  12468  recos4p  12469  resincl  12470  recoscl  12471  retanclap  12472  efieq  12485  sinbnd  12502  cosbnd  12503  absefi  12519  odd2np1  12623  remetdval  15631  bl2ioo  15634  ioo2bl  15635  hoverb  15732  plyreres  15848  sincosq1sgn  15910  sincosq2sgn  15911  sincosq3sgn  15912  sincosq4sgn  15913  sinq12gt0  15914  relogoprlem  15952  logcxp  15982  rpcxpcl  15988  cxpcom  16023  rprelogbdiv  16042  gausslemma2dlem1a  16160  triap  17052  trirec0  17067