Theorem recn 8148

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8013  ℝcr 8014

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8107

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  mulrid  8159  recnd  8191  pnfnre  8204  mnfnre  8205  cnegexlem1  8337  cnegexlem2  8338  cnegexlem3  8339  cnegex  8340  renegcl  8423  resubcl  8426  negf1o  8544  mul02lem2  8550  ltaddneg  8587  ltaddnegr  8588  ltaddsub2  8600  leaddsub2  8602  leltadd  8610  ltaddpos  8615  ltaddpos2  8616  posdif  8618  lenegcon1  8629  lenegcon2  8630  addge01  8635  addge02  8636  leaddle0  8640  mullt0  8643  recexre  8741  msqge0  8779  mulge0  8782  aprcl  8809  recexap  8816  rerecapb  9006  ltm1  9009  prodgt02  9016  prodge02  9018  ltmul2  9019  lemul2  9020  lemul2a  9022  ltmulgt12  9028  lemulge12  9030  gt0div  9033  ge0div  9034  ltmuldiv2  9038  ltdivmul  9039  ltdivmul2  9041  ledivmul2  9043  lemuldiv2  9045  negiso  9118  cju  9124  nnge1  9149  halfpos  9358  lt2halves  9363  addltmul  9364  avgle1  9368  avgle2  9369  div4p1lem1div2  9381  nnrecl  9383  elznn0  9477  elznn  9478  nzadd  9515  zmulcl  9516  difgtsumgt  9532  elz2  9534  gtndiv  9558  zeo  9568  supminfex  9809  eqreznegel  9826  negm  9827  irradd  9858  irrmul  9859  divlt1lt  9937  divle1le  9938  xnegneg  10046  rexsub  10066  xnegid  10072  xaddcom  10074  xaddid1  10075  xnegdi  10081  xaddass  10082  xleaddadd  10100  divelunit  10215  fzonmapblen  10404  infssuzex  10470  expgt1  10816  mulexpzap  10818  leexp1a  10833  expubnd  10835  sqgt0ap  10847  lt2sq  10852  le2sq  10853  sqge0  10855  sumsqeq0  10857  bernneq  10899  bernneq2  10900  nn0ltexp2  10948  swrdccatin2  11282  swrdccat3blem  11292  crre  11389  crim  11390  reim0  11393  mulreap  11396  rere  11397  remul2  11405  redivap  11406  immul2  11412  imdivap  11413  cjre  11414  cjreim  11435  rennim  11534  sqrt0rlem  11535  resqrexlemover  11542  absreimsq  11599  absreim  11600  absnid  11605  leabs  11606  absre  11609  absresq  11610  sqabs  11614  ltabs  11619  absdiflt  11624  absdifle  11625  lenegsq  11627  abssuble0  11635  dfabsmax  11749  max0addsup  11751  negfi  11760  minclpr  11769  reefcl  12200  efgt0  12216  reeftlcl  12221  resinval  12247  recosval  12248  resin4p  12250  recos4p  12251  resincl  12252  recoscl  12253  retanclap  12254  efieq  12267  sinbnd  12284  cosbnd  12285  absefi  12301  odd2np1  12405  remetdval  15242  bl2ioo  15245  ioo2bl  15246  hoverb  15343  plyreres  15459  sincosq1sgn  15521  sincosq2sgn  15522  sincosq3sgn  15523  sincosq4sgn  15524  sinq12gt0  15525  relogoprlem  15563  logcxp  15592  rpcxpcl  15598  cxpcom  15633  rprelogbdiv  15652  gausslemma2dlem1a  15758  triap  16511  trirec0  16526