MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-resscn Structured version   GIF version

Axiom ax-resscn 9085
Description: The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by theorem axresscn 9061. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-resscn ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 9027 . 2 class
2 cc 9026 . 2 class
31, 2wss 3309 1 wff ℝ ⊆ ℂ
Colors of variables: wff set class
This axiom is referenced by:  recn  9118  reex  9119  recni  9140  nnsscn  10043  nn0sscn  10264  qsscn  10623  reexpcl  11436  rpexpcl  11438  reexpclz  11439  expge0  11454  expge1  11455  rlimrecl  12412  abscn2  12430  recn2  12432  imcn2  12433  climabs  12435  climre  12437  climim  12438  rlimabs  12440  rlimre  12442  rlimim  12443  caurcvgr  12505  caucvgrlem2  12506  caurcvg  12508  fsumrecl  12566  fsumrpcl  12569  fsumge0  12612  fsumre  12625  fsumim  12626  reeff1  12759  nthruc  12888  remet  18859  tgioo2  18872  xrsdsre  18879  recld2  18883  reperf  18888  iitopon  18947  dfii3  18951  abscncf  18969  recncf  18970  imcncf  18971  abscncfALT  18988  cnmptre  18990  iimulcn  19001  icchmeo  19004  cnrehmeo  19016  evth  19022  evth2  19023  lebnumlem2  19025  lebnumii  19029  reparphti  19060  cphsqrcl  19185  resscdrg  19350  ishl2  19362  evthicc  19394  evthicc2  19395  ovolfsf  19406  volcn  19536  volivth  19537  ismbf  19558  cncombf  19586  cnmbf  19587  0plef  19600  itg1ge0  19614  i1faddlem  19621  i1fmul  19624  itg1addlem4  19627  i1fsub  19636  itg1sub  19637  mbfi1fseqlem5  19647  xrge0f  19659  itg20  19665  itg2const  19668  itg2mulc  19675  itg2addlem  19686  i1fibl  19735  itgitg1  19736  iblabslem  19755  iblabs  19756  bddmulibl  19766  recnprss  19829  dvcjbr  19873  dvfre  19875  dvnfre  19876  dvferm1  19907  dvferm2  19909  rolle  19912  cmvth  19913  mvth  19914  dvlip  19915  dvlipcn  19916  dvlip2  19917  c1liplem1  19918  c1lip2  19920  dvgt0lem1  19924  dvle  19929  dvivthlem1  19930  dvivth  19932  dvne0  19933  lhop1lem  19935  lhop1  19936  lhop2  19937  lhop  19938  dvcnvrelem1  19939  dvcnvrelem2  19940  dvcnvre  19941  dvcvx  19942  dvfsumle  19943  dvfsumge  19944  dvfsumabs  19945  dvfsumlem2  19949  dvfsumrlim  19953  ftc1a  19959  ftc1lem3  19960  ftc1lem6  19963  ftc1  19964  ftc1cn  19965  ftc2  19966  ftc2ditglem  19967  itgparts  19969  itgsubstlem  19970  itgsubst  19971  aacjcl  20282  aalioulem3  20289  taylthlem2  20328  taylth  20329  abelth2  20396  reeff1olem  20400  efcvx  20403  pilem3  20407  pige3  20463  recosf1o  20475  resinf1o  20476  dvrelog  20566  relogcn  20567  logcnlem5  20575  logcn  20576  dvloglem  20577  dvlog2lem  20581  logccv  20592  dvcxp1  20664  cxpcn3  20670  resqrcn  20671  loglesqr  20680  ssscongptld  20704  ressatans  20812  rlimcnp  20842  efrlim  20846  jensenlem1  20863  jensenlem2  20864  jensen  20865  amgm  20867  ftalem3  20895  basellem9  20909  efnnfsumcl  20923  efchtdvds  20980  lgsdchr  21170  dchrvmasumlem1  21227  dchrisum0lem3  21251  pntlem3  21341  readdsubgo  21979  circgrp  22000  ipasslem7  22375  rexdiv  24207  fsumrp0cl  24252  rebase  24304  re0g  24308  unitsscn  24329  rmulccn  24349  raddcn  24350  xrge0iifhom  24358  lmlimxrge0  24369  recms  24378  reust  24379  rezh  24390  rrhre  24422  esumpfinvallem  24499  esumpfinval  24500  esumpfinvalf  24501  esumcvg  24511  lgamgulmlem2  24849  cvxpcon  24964  cvxscon  24965  rescon  24968  fprodrecl  25314  fprodrpcl  25317  rerisefaccl  25368  refallfaccl  25369  rprisefaccl  25374  mblfinlem2  26284  mbfresfi  26293  ftc1cnnclem  26320  ftc1cnnc  26321  ftc1anclem3  26324  ftc1anclem5  26326  ftc1anclem7  26328  ftc1anclem8  26329  ftc1anc  26330  ftc2nc  26331  dvreasin  26332  dvreacos  26333  areacirclem1  26334  areacirclem2  26335  areacirclem3  26336  areacirclem4  26337  areacirc  26339  ivthALT  26380  repwsmet  26585  rrnequiv  26586  rrntotbnd  26587  reheibor  26590  iccbnd  26591  ssrecnpr  27626  sblpnf  27628  lhe4.4ex1a  27635  refsumcn  27789  climreeq  27827  dvcosre  27829  itgsin0pilem1  27832  ibliccsinexp  27833  iblioosinexp  27835  itgsinexplem1  27836  itgsinexp  27837  wallispilem2  27903
  Copyright terms: Public domain W3C validator