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

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

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 9227 . 2
2 cc 9226 . 2
31, 2wss 3305 1
Colors of variables: wff setvar class
This axiom is referenced by:  recn  9318  reex  9319  recni  9344  nnsscn  10273  nn0sscn  10530  qsscn  10909  reexpcl  11823  rpexpcl  11825  reexpclz  11826  expge0  11841  expge1  11842  rlimrecl  12999  abscn2  13017  recn2  13019  imcn2  13020  climabs  13022  climre  13024  climim  13025  rlimabs  13027  rlimre  13029  rlimim  13030  caurcvgr  13092  caucvgrlem2  13093  caurcvg  13095  fsumrecl  13152  fsumrpcl  13155  fsumge0  13198  fsumre  13211  fsumim  13212  reeff1  13344  nthruc  13473  rebase  17744  re0g  17750  regsumsupp  17760  remet  20067  tgioo2  20080  xrsdsre  20087  recld2  20091  reperf  20096  iitopon  20155  dfii3  20159  abscncf  20177  recncf  20178  imcncf  20179  abscncfALT  20196  cnmptre  20199  iimulcn  20210  icchmeo  20213  cnrehmeo  20225  evth  20231  evth2  20232  lebnumlem2  20234  lebnumii  20238  reparphti  20269  cphsqrcl  20403  resscdrg  20570  ishl2  20582  recms  20584  reust  20585  evthicc  20643  evthicc2  20644  ovolfsf  20655  volcn  20786  volivth  20787  ismbf  20808  cncombf  20836  cnmbf  20837  0plef  20850  itg1ge0  20864  i1faddlem  20871  i1fmul  20874  itg1addlem4  20877  i1fsub  20886  itg1sub  20887  mbfi1fseqlem5  20897  xrge0f  20909  itg20  20915  itg2const  20918  itg2mulc  20925  itg2addlem  20936  i1fibl  20985  itgitg1  20986  iblabslem  21005  iblabs  21006  bddmulibl  21016  recnprss  21079  dvcjbr  21123  dvfre  21125  dvnfre  21126  dvferm1  21157  dvferm2  21159  rolle  21162  cmvth  21163  mvth  21164  dvlip  21165  dvlipcn  21166  dvlip2  21167  c1liplem1  21168  c1lip2  21170  dvgt0lem1  21174  dvle  21179  dvivthlem1  21180  dvivth  21182  dvne0  21183  lhop1lem  21185  lhop1  21186  lhop2  21187  lhop  21188  dvcnvrelem1  21189  dvcnvrelem2  21190  dvcnvre  21191  dvcvx  21192  dvfsumle  21193  dvfsumge  21194  dvfsumabs  21195  dvfsumlem2  21199  dvfsumrlim  21203  ftc1a  21209  ftc1lem3  21210  ftc1lem6  21213  ftc1  21214  ftc1cn  21215  ftc2  21216  ftc2ditglem  21217  itgparts  21219  itgsubstlem  21220  itgsubst  21221  aacjcl  21534  aalioulem3  21541  taylthlem2  21580  taylth  21581  abelth2  21648  reeff1olem  21652  efcvx  21655  pilem3  21659  pige3  21720  recosf1o  21732  resinf1o  21733  dvrelog  21823  relogcn  21824  logcnlem5  21832  logcn  21833  dvloglem  21834  dvlog2lem  21838  logccv  21849  dvcxp1  21921  cxpcn3  21927  resqrcn  21928  loglesqr  21937  ssscongptld  21961  ressatans  22070  rlimcnp  22100  efrlim  22104  jensenlem1  22121  jensenlem2  22122  jensen  22123  amgm  22125  ftalem3  22153  basellem9  22167  efnnfsumcl  22181  efchtdvds  22238  lgsdchr  22428  dchrvmasumlem1  22485  dchrisum0lem3  22509  pntlem3  22599  cchhllem  22812  readdsubgo  23519  circgrp  23540  ipasslem7  23915  rexdiv  25779  fsumrp0cl  25837  rge0srg  25919  regsumfsum  25958  xrge0slmod  26021  unitsscn  26035  rmulccn  26067  raddcn  26068  xrge0iifhom  26076  lmlimxrge0  26087  rezh  26109  esumpfinvallem  26232  esumpfinval  26233  esumpfinvalf  26234  esumcvg  26244  plymulx0  26651  plymulx  26652  signsplypnf  26654  signsply0  26655  lgamgulmlem2  26719  cvxpcon  26834  cvxscon  26835  rescon  26838  fprodrecl  27168  fprodrpcl  27171  rerisefaccl  27222  refallfaccl  27223  rprisefaccl  27228  mblfinlem2  28100  mbfresfi  28109  ftc1cnnclem  28136  ftc1cnnc  28137  ftc1anclem3  28140  ftc1anclem5  28142  ftc1anclem7  28144  ftc1anclem8  28145  ftc1anc  28146  ftc2nc  28147  asindmre  28150  dvreasin  28153  dvreacos  28154  areacirclem1  28155  areacirclem2  28156  areacirclem3  28157  areacirclem4  28158  areacirc  28160  ivthALT  28201  repwsmet  28404  rrnequiv  28405  rrntotbnd  28406  reheibor  28409  iccbnd  28410  itgpowd  29263  arearect  29264  areaquad  29265  ssrecnpr  29267  sblpnf  29269  lhe4.4ex1a  29276  refsumcn  29425  climreeq  29460  dvcosre  29462  itgsin0pilem1  29464  ibliccsinexp  29465  iblioosinexp  29467  itgsinexplem1  29468  itgsinexp  29469  wallispilem2  29535
  Copyright terms: Public domain W3C validator