Theorem recn 8007

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℂcc 7872  ℝcr 7873

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-resscn 7966

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  mulrid  8018  recnd  8050  pnfnre  8063  mnfnre  8064  cnegexlem1  8196  cnegexlem2  8197  cnegexlem3  8198  cnegex  8199  renegcl  8282  resubcl  8285  negf1o  8403  mul02lem2  8409  ltaddneg  8445  ltaddnegr  8446  ltaddsub2  8458  leaddsub2  8460  leltadd  8468  ltaddpos  8473  ltaddpos2  8474  posdif  8476  lenegcon1  8487  lenegcon2  8488  addge01  8493  addge02  8494  leaddle0  8498  mullt0  8501  recexre  8599  msqge0  8637  mulge0  8640  aprcl  8667  recexap  8674  rerecapb  8864  ltm1  8867  prodgt02  8874  prodge02  8876  ltmul2  8877  lemul2  8878  lemul2a  8880  ltmulgt12  8886  lemulge12  8888  gt0div  8891  ge0div  8892  ltmuldiv2  8896  ltdivmul  8897  ltdivmul2  8899  ledivmul2  8901  lemuldiv2  8903  negiso  8976  cju  8982  nnge1  9007  halfpos  9216  lt2halves  9221  addltmul  9222  avgle1  9226  avgle2  9227  div4p1lem1div2  9239  nnrecl  9241  elznn0  9335  elznn  9336  nzadd  9372  zmulcl  9373  difgtsumgt  9389  elz2  9391  gtndiv  9415  zeo  9425  supminfex  9665  eqreznegel  9682  negm  9683  irradd  9714  irrmul  9715  divlt1lt  9793  divle1le  9794  xnegneg  9902  rexsub  9922  xnegid  9928  xaddcom  9930  xaddid1  9931  xnegdi  9937  xaddass  9938  xleaddadd  9956  divelunit  10071  fzonmapblen  10257  expgt1  10651  mulexpzap  10653  leexp1a  10668  expubnd  10670  sqgt0ap  10682  lt2sq  10687  le2sq  10688  sqge0  10690  sumsqeq0  10692  bernneq  10734  bernneq2  10735  nn0ltexp2  10783  crre  11004  crim  11005  reim0  11008  mulreap  11011  rere  11012  remul2  11020  redivap  11021  immul2  11027  imdivap  11028  cjre  11029  cjreim  11050  rennim  11149  sqrt0rlem  11150  resqrexlemover  11157  absreimsq  11214  absreim  11215  absnid  11220  leabs  11221  absre  11224  absresq  11225  sqabs  11229  ltabs  11234  absdiflt  11239  absdifle  11240  lenegsq  11242  abssuble0  11250  dfabsmax  11364  max0addsup  11366  negfi  11374  minclpr  11383  reefcl  11814  efgt0  11830  reeftlcl  11835  resinval  11861  recosval  11862  resin4p  11864  recos4p  11865  resincl  11866  recoscl  11867  retanclap  11868  efieq  11881  sinbnd  11898  cosbnd  11899  absefi  11915  odd2np1  12017  infssuzex  12089  remetdval  14726  bl2ioo  14729  ioo2bl  14730  hoverb  14827  plyreres  14942  sincosq1sgn  15002  sincosq2sgn  15003  sincosq3sgn  15004  sincosq4sgn  15005  sinq12gt0  15006  relogoprlem  15044  logcxp  15073  rpcxpcl  15079  cxpcom  15112  rprelogbdiv  15130  gausslemma2dlem1a  15215  triap  15589  trirec0  15604