Theorem recn 7974

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

Syntax hints:   → wi 4   ∈ wcel 2160  ℂcc 7839  ℝcr 7840

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 2171  ax-resscn 7933

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3150  df-ss 3157

This theorem is referenced by:  mulrid  7984  recnd  8016  pnfnre  8029  mnfnre  8030  cnegexlem1  8162  cnegexlem2  8163  cnegexlem3  8164  cnegex  8165  renegcl  8248  resubcl  8251  negf1o  8369  mul02lem2  8375  ltaddneg  8411  ltaddnegr  8412  ltaddsub2  8424  leaddsub2  8426  leltadd  8434  ltaddpos  8439  ltaddpos2  8440  posdif  8442  lenegcon1  8453  lenegcon2  8454  addge01  8459  addge02  8460  leaddle0  8464  mullt0  8467  recexre  8565  msqge0  8603  mulge0  8606  aprcl  8633  recexap  8640  rerecapb  8830  ltm1  8833  prodgt02  8840  prodge02  8842  ltmul2  8843  lemul2  8844  lemul2a  8846  ltmulgt12  8852  lemulge12  8854  gt0div  8857  ge0div  8858  ltmuldiv2  8862  ltdivmul  8863  ltdivmul2  8865  ledivmul2  8867  lemuldiv2  8869  negiso  8942  cju  8948  nnge1  8972  halfpos  9180  lt2halves  9184  addltmul  9185  avgle1  9189  avgle2  9190  div4p1lem1div2  9202  nnrecl  9204  elznn0  9298  elznn  9299  nzadd  9335  zmulcl  9336  difgtsumgt  9352  elz2  9354  gtndiv  9378  zeo  9388  supminfex  9627  eqreznegel  9644  negm  9645  irradd  9676  irrmul  9677  divlt1lt  9754  divle1le  9755  xnegneg  9863  rexsub  9883  xnegid  9889  xaddcom  9891  xaddid1  9892  xnegdi  9898  xaddass  9899  xleaddadd  9917  divelunit  10032  fzonmapblen  10217  expgt1  10589  mulexpzap  10591  leexp1a  10606  expubnd  10608  sqgt0ap  10620  lt2sq  10625  le2sq  10626  sqge0  10628  sumsqeq0  10630  bernneq  10672  bernneq2  10673  nn0ltexp2  10721  crre  10898  crim  10899  reim0  10902  mulreap  10905  rere  10906  remul2  10914  redivap  10915  immul2  10921  imdivap  10922  cjre  10923  cjreim  10944  rennim  11043  sqrt0rlem  11044  resqrexlemover  11051  absreimsq  11108  absreim  11109  absnid  11114  leabs  11115  absre  11118  absresq  11119  sqabs  11123  ltabs  11128  absdiflt  11133  absdifle  11134  lenegsq  11136  abssuble0  11144  dfabsmax  11258  max0addsup  11260  negfi  11268  minclpr  11277  reefcl  11708  efgt0  11724  reeftlcl  11729  resinval  11755  recosval  11756  resin4p  11758  recos4p  11759  resincl  11760  recoscl  11761  retanclap  11762  efieq  11775  sinbnd  11792  cosbnd  11793  absefi  11808  odd2np1  11910  infssuzex  11982  remetdval  14496  bl2ioo  14499  ioo2bl  14500  sincosq1sgn  14704  sincosq2sgn  14705  sincosq3sgn  14706  sincosq4sgn  14707  sinq12gt0  14708  relogoprlem  14746  logcxp  14775  rpcxpcl  14781  cxpcom  14814  rprelogbdiv  14832  triap  15236  trirec0  15251