Theorem recn 8319

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

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

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 8278

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  8330  recnd  8361  pnfnre  8374  mnfnre  8375  cnegexlem1  8509  cnegexlem2  8510  cnegexlem3  8511  cnegex  8512  renegcl  8595  resubcl  8598  negf1o  8717  mul02lem2  8723  ltaddneg  8760  ltaddnegr  8761  ltaddsub2  8773  leaddsub2  8775  leltadd  8783  ltaddpos  8788  ltaddpos2  8789  posdif  8791  lenegcon1  8802  lenegcon2  8803  addge01  8808  addge02  8809  leaddle0  8813  mullt0  8816  recexre  8915  msqge0  8953  mulge0  8956  aprcl  8983  recexap  8990  rerecapb  9182  ltm1  9185  prodgt02  9192  prodge02  9194  ltmul2  9195  lemul2  9196  lemul2a  9198  ltmulgt12  9204  lemulge12  9206  gt0div  9209  ge0div  9210  ltmuldiv2  9214  ltdivmul  9215  ltdivmul2  9217  ledivmul2  9219  lemuldiv2  9221  negiso  9294  cju  9300  nnge1  9337  halfpos  9548  lt2halves  9553  addltmul  9554  avgle1  9558  avgle2  9559  div4p1lem1div2  9571  nnrecl  9573  elznn0  9671  elznn  9672  nzadd  9709  zmulcl  9710  difgtsumgt  9726  elz2  9728  gtndiv  9753  zeo  9763  supminfex  10014  eqreznegel  10031  negm  10032  irradd  10063  irrmul  10065  divlt1lt  10143  divle1le  10144  xnegneg  10253  rexsub  10273  xnegid  10279  xaddcom  10281  xaddid1  10282  xnegdi  10288  xaddass  10289  xleaddadd  10307  divelunit  10422  fzonmapblen  10617  infssuzex  10684  expgt1  11036  mulexpzap  11038  leexp1a  11053  expubnd  11055  sqgt0ap  11067  lt2sq  11072  le2sq  11073  sqge0  11075  sumsqeq0  11077  bernneq  11120  bernneq2  11121  nn0ltexp2  11170  swrdccatin2  11524  swrdccat3blem  11534  crre  11645  crim  11646  reim0  11649  mulreap  11652  rere  11653  remul2  11661  redivap  11662  immul2  11668  imdivap  11669  cjre  11670  cjreim  11692  rennim  11791  sqrt0rlem  11792  resqrexlemover  11799  absreimsq  11856  absreim  11857  absnid  11862  leabs  11863  absre  11867  absresq  11868  sqabs  11872  ltabs  11877  absdiflt  11882  absdifle  11883  lenegsq  11885  abssuble0  11893  dfabsmax  12007  max0addsup  12009  negfi  12018  minclpr  12028  reefcl  12461  efgt0  12477  reeftlcl  12482  resinval  12508  recosval  12509  resin4p  12511  recos4p  12512  resincl  12513  recoscl  12514  retanclap  12515  efieq  12528  sinbnd  12545  cosbnd  12546  absefi  12562  odd2np1  12666  remetdval  15785  bl2ioo  15788  ioo2bl  15789  hoverb  15886  plyreres  16002  sincosq1sgn  16065  sincosq2sgn  16066  sincosq3sgn  16067  sincosq4sgn  16068  sinq12gt0  16069  relogoprlem  16110  logcxp  16142  rpcxpcl  16148  cxpcom  16185  rprelogbdiv  16205  gausslemma2dlem1a  16394  triap  17296  trirec0  17312