MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  recn Structured version   Visualization version   GIF version

Theorem recn 10619
Description: A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
Assertion
Ref Expression
recn (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)

Proof of Theorem recn
StepHypRef Expression
1 ax-resscn 10586 . 2 ℝ ⊆ ℂ
21sseli 3961 1 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cc 10527  cr 10528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-resscn 10586
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-in 3941  df-ss 3950
This theorem is referenced by:  mulid1  10631  recnd  10661  pnfnre  10674  mnfnre  10676  mul02  10810  ltaddneg  10847  ltaddnegr  10848  renegcli  10939  resubcl  10942  negn0  11061  negf1o  11062  ltaddsub2  11107  leaddsub2  11109  leltadd  11116  ltaddpos  11122  ltaddpos2  11123  posdif  11125  lenegcon1  11136  lenegcon2  11137  addge01  11142  addge02  11143  leaddle0  11147  mullt0  11151  recex  11264  ltm1  11474  prodgt02  11480  ltmul2  11483  lemul1  11484  lemul2  11485  lemul1a  11486  lemul2a  11487  ltmulgt12  11493  lemulge12  11495  gt0div  11498  ge0div  11499  mulge0b  11502  mulle0b  11503  ltmuldiv2  11506  ltdivmul  11507  ledivmul  11508  ltdivmul2  11509  lt2mul2div  11510  ledivmul2  11511  lemuldiv2  11513  ltdiv2  11518  ltrec1  11519  lerec2  11520  ledivdiv  11521  lediv2  11522  ltdiv23  11523  lediv23  11524  lediv12a  11525  recp1lt1  11530  ledivp1  11534  negfi  11581  fiminreOLD  11582  infm3lem  11591  supmul  11605  riotaneg  11612  negiso  11613  cju  11626  nnge1  11657  halfpos  11859  lt2halves  11864  addltmul  11865  avgle1  11869  avgle2  11870  avgle  11871  div4p1lem1div2  11884  nnrecl  11887  difgtsumgt  11942  elznn0  11988  elznn  11989  elz2  11991  nzadd  12022  zmulcl  12023  gtndiv  12051  zeo  12060  eqreznegel  12326  supminf  12327  rebtwnz  12339  irradd  12364  irrmul  12365  divlt1lt  12450  divle1le  12451  max0sub  12581  xnegneg  12599  rexsub  12618  xnegid  12623  xaddcom  12625  xaddid1  12626  xnegdi  12633  xaddass  12634  rexmul  12656  xmulasslem3  12671  xadddilem  12679  divelunit  12872  fzonmapblen  13075  ico01fl0  13181  flzadd  13188  ltdifltdiv  13196  dfceil2  13201  intfrac2  13218  fldiv2  13221  flpmodeq  13234  mod0  13236  negmod0  13238  modlt  13240  modfrac  13244  flmod  13245  intfrac  13246  modmulnn  13249  modvalp1  13250  modid  13256  modcyc  13266  modcyc2  13267  modadd1  13268  modaddabs  13269  muladdmodid  13271  negmod  13276  modadd2mod  13281  modmul1  13284  modmulmodr  13297  modaddmulmod  13298  moddi  13299  modsubdir  13300  modirr  13302  addmodlteq  13306  expgt1  13459  mulexpz  13461  sqgt0  13483  lt2sq  13490  le2sq  13491  sqge0  13493  expmordi  13523  leexp1a  13531  expubnd  13533  sumsqeq0  13534  sqlecan  13563  bernneq  13582  bernneq2  13583  expnbnd  13585  digit2  13589  digit1  13590  expnngt1  13594  swrdccatin2  14083  swrdccat3blem  14093  cshweqrep  14175  crre  14465  crim  14466  reim0  14469  mulre  14472  rere  14473  remul2  14481  rediv  14482  immul2  14488  imdiv  14489  cjre  14490  cjreim  14511  rennim  14590  resqrex  14602  resqreu  14604  resqrtcl  14605  resqrtthlem  14606  sqrtneglem  14618  sqrtneg  14619  absreimsq  14644  absreim  14645  absnid  14650  leabs  14651  absre  14653  absresq  14654  sqabs  14659  max0add  14662  absz  14663  absdiflt  14669  absdifle  14670  lenegsq  14672  abssuble0  14680  absmax  14681  rddif  14692  absrdbnd  14693  o1rlimmul  14967  caurcvg2  15026  reefcl  15432  efgt0  15448  reeftlcl  15453  resinval  15480  recosval  15481  resin4p  15483  recos4p  15484  resincl  15485  recoscl  15486  retancl  15487  resinhcl  15501  rpcoshcl  15502  retanhcl  15504  tanhlt1  15505  tanhbnd  15506  efieq  15508  sinbnd  15525  cosbnd  15526  absefi  15541  dvdsaddre2b  15649  odd2np1  15682  bezoutlem1  15879  xrsdsreclb  20584  remulg  20743  resubdrg  20744  remetdval  23389  bl2ioo  23392  ioo2bl  23393  cnperf  23420  icccvx  23546  tcphcph  23832  shft2rab  24101  volsup2  24198  volcn  24199  c1lip1  24586  plyreres  24864  aalioulem3  24915  taylthlem2  24954  reeff1o  25027  reefgim  25030  sincosq1sgn  25076  sincosq2sgn  25077  sincosq3sgn  25078  sincosq4sgn  25079  sinq12gt0  25085  pige3ALT  25097  efif1olem4  25121  efifo  25123  relogrn  25137  logrnaddcl  25150  relogoprlem  25166  advlog  25229  advlogexp  25230  logtayl  25235  recxpcl  25250  rpcxpcl  25251  cxpge0  25258  cxpcom  25312  dvcxp1  25313  logreclem  25332  relogbreexp  25345  relogbcxp  25355  angpieqvd  25401  atanre  25455  basellem9  25658  gausslemma2dlem1a  25933  2sqnn0  26006  log2sumbnd  26112  brbtwn2  26683  colinearalglem4  26687  colinearalg  26688  crctcshwlkn0lem1  27580  nvsge0  28433  nmoub3i  28542  nmlnoubi  28565  isblo3i  28570  ipasslem3  28602  ipasslem9  28607  ipasslem11  28609  hmopm  29790  riesz1  29834  leopmuli  29902  leopmul  29903  leopmul2i  29904  leopnmid  29907  nmopleid  29908  cdj1i  30202  cdj3lem1  30203  cdj3i  30210  addltmulALT  30215  dpfrac1  30561  rexdiv  30595  xdivid  30597  xdiv0  30598  rmulccn  31164  sgnneg  31791  lediv2aALT  32913  nndivlub  33799  cos2h  34875  tan2h  34876  poimir  34917  mblfinlem2  34922  mblfinlem4  34924  itg2addnclem  34935  itg2addnclem2  34936  dvasin  34970  areacirclem1  34974  areacirclem2  34975  areacirclem4  34977  areacirclem5  34978  areacirc  34979  resubeulem2  39196  renegneg  39231  areaquad  39813  radcnvrat  40636  lhe4.4ex1a  40651  expgrowthi  40655  mulltgt0  41269  refsum2cnlem1  41284  infnsuprnmpt  41511  dstregt0  41536  suplesup  41596  infleinflem1  41627  infleinflem2  41628  ltdiv23neg  41655  rexabslelem  41681  supminfrnmpt  41708  supminfxr  41729  fmul01lt1lem1  41854  lptre2pt  41910  cnrefiisplem  42099  dvcosre  42185  itgsin0pilem1  42224  itgsinexplem1  42228  volioc  42246  volico  42258  stoweidlem7  42282  stoweidlem10  42285  stoweidlem19  42294  stoweidlem34  42309  stoweid  42338  dirker2re  42367  dirkerdenne0  42368  dirkerper  42371  dirkertrigeq  42376  dirkeritg  42377  fourierdlem39  42421  fourierdlem42  42424  fourierdlem47  42428  fourierdlem56  42437  fourierdlem57  42438  fourierdlem58  42439  fourierdlem60  42441  fourierdlem61  42442  fourierdlem73  42454  fourierdlem76  42457  fourierdlem77  42458  fourierdlem92  42473  fourierdlem97  42478  etransclem46  42555  volico2  42913  smflimlem4  43040  smfinflem  43081  2leaddle2  43488  ltsubsubaddltsub  43491  sqrtnegnre  43497  m1mod0mod1  43519  requad01  43776  requad1  43777  bgoldbtbndlem2  43961  flsubz  44567  rege1logbrege0  44608  nn0digval  44650  rrx2vlinest  44718  line2  44729  line2xlem  44730  line2x  44731  itscnhlc0yqe  44736  itsclc0yqsollem2  44740  itsclc0yqsol  44741  itscnhlc0xyqsol  44742  itschlc0xyqsol1  44743  itsclc0xyqsolr  44746  itsclquadb  44753  reseccl  44842  recsccl  44843  recotcl  44844
  Copyright terms: Public domain W3C validator