Theorem recn 8312

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℂcc 8177  ℝcr 8178

This proof depends on 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 8271

This proof 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 used by:  mulrid  8323  recnd  8354  pnfnre  8367  mnfnre  8368  cnegexlem1  8501  cnegexlem2  8502  cnegexlem3  8503  cnegex  8504  renegcl  8587  resubcl  8590  negf1o  8709  mul02lem2  8715  ltaddneg  8752  ltaddnegr  8753  ltaddsub2  8765  leaddsub2  8767  leltadd  8775  ltaddpos  8780  ltaddpos2  8781  posdif  8783  lenegcon1  8794  lenegcon2  8795  addge01  8800  addge02  8801  leaddle0  8805  mullt0  8808  recexre  8907  msqge0  8945  mulge0  8948  aprcl  8975  recexap  8982  rerecapb  9174  ltm1  9177  prodgt02  9184  prodge02  9186  ltmul2  9187  lemul2  9188  lemul2a  9190  ltmulgt12  9196  lemulge12  9198  gt0div  9201  ge0div  9202  ltmuldiv2  9206  ltdivmul  9207  ltdivmul2  9209  ledivmul2  9211  lemuldiv2  9213  negiso  9286  cju  9292  nnge1  9328  halfpos  9538  lt2halves  9543  addltmul  9544  avgle1  9548  avgle2  9549  div4p1lem1div2  9561  nnrecl  9563  elznn0  9661  elznn  9662  nzadd  9699  zmulcl  9700  difgtsumgt  9716  elz2  9718  gtndiv  9743  zeo  9753  supminfex  9999  eqreznegel  10016  negm  10017  irradd  10048  irrmul  10049  divlt1lt  10127  divle1le  10128  xnegneg  10237  rexsub  10257  xnegid  10263  xaddcom  10265  xaddid1  10266  xnegdi  10272  xaddass  10273  xleaddadd  10291  divelunit  10406  fzonmapblen  10601  infssuzex  10668  expgt1  11016  mulexpzap  11018  leexp1a  11033  expubnd  11035  sqgt0ap  11047  lt2sq  11052  le2sq  11053  sqge0  11055  sumsqeq0  11057  bernneq  11100  bernneq2  11101  nn0ltexp2  11149  swrdccatin2  11503  swrdccat3blem  11513  crre  11624  crim  11625  reim0  11628  mulreap  11631  rere  11632  remul2  11640  redivap  11641  immul2  11647  imdivap  11648  cjre  11649  cjreim  11671  rennim  11770  sqrt0rlem  11771  resqrexlemover  11778  absreimsq  11835  absreim  11836  absnid  11841  leabs  11842  absre  11845  absresq  11846  sqabs  11850  ltabs  11855  absdiflt  11860  absdifle  11861  lenegsq  11863  abssuble0  11871  dfabsmax  11985  max0addsup  11987  negfi  11996  minclpr  12005  reefcl  12437  efgt0  12453  reeftlcl  12458  resinval  12484  recosval  12485  resin4p  12487  recos4p  12488  resincl  12489  recoscl  12490  retanclap  12491  efieq  12504  sinbnd  12521  cosbnd  12522  absefi  12538  odd2np1  12642  remetdval  15650  bl2ioo  15653  ioo2bl  15654  hoverb  15751  plyreres  15867  sincosq1sgn  15930  sincosq2sgn  15931  sincosq3sgn  15932  sincosq4sgn  15933  sinq12gt0  15934  relogoprlem  15973  logcxp  16005  rpcxpcl  16011  cxpcom  16046  rprelogbdiv  16065  gausslemma2dlem1a  16189  triap  17090  trirec0  17105