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

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

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 9086 . 2 class
2 cc 9085 . 2 class
31, 2wss 3350 1 wff ℝ ⊆ ℂ
Colors of variables: wff set class
This axiom is referenced by:  recn  9177  reex  9178  recni  9199  nnsscn  10103  nn0sscn  10324  qsscn  10685  reexpcl  11502  rpexpcl  11504  reexpclz  11505  expge0  11520  expge1  11521  rlimrecl  12494  abscn2  12512  recn2  12514  imcn2  12515  climabs  12517  climre  12519  climim  12520  rlimabs  12522  rlimre  12524  rlimim  12525  caurcvgr  12587  caucvgrlem2  12588  caurcvg  12590  fsumrecl  12648  fsumrpcl  12651  fsumge0  12694  fsumre  12707  fsumim  12708  reeff1  12841  nthruc  12970  remet  18953  tgioo2  18966  xrsdsre  18973  recld2  18977  reperf  18982  iitopon  19041  dfii3  19045  abscncf  19063  recncf  19064  imcncf  19065  abscncfALT  19082  cnmptre  19084  iimulcn  19095  icchmeo  19098  cnrehmeo  19110  evth  19116  evth2  19117  lebnumlem2  19119  lebnumii  19123  reparphti  19154  cphsqrcl  19279  resscdrg  19444  ishl2  19456  evthicc  19488  evthicc2  19489  ovolfsf  19500  volcn  19630  volivth  19631  ismbf  19652  cncombf  19680  cnmbf  19681  0plef  19694  itg1ge0  19708  i1faddlem  19715  i1fmul  19718  itg1addlem4  19721  i1fsub  19730  itg1sub  19731  mbfi1fseqlem5  19741  xrge0f  19753  itg20  19759  itg2const  19762  itg2mulc  19769  itg2addlem  19780  i1fibl  19829  itgitg1  19830  iblabslem  19849  iblabs  19850  bddmulibl  19860  recnprss  19923  dvcjbr  19967  dvfre  19969  dvnfre  19970  dvferm1  20001  dvferm2  20003  rolle  20006  cmvth  20007  mvth  20008  dvlip  20009  dvlipcn  20010  dvlip2  20011  c1liplem1  20012  c1lip2  20014  dvgt0lem1  20018  dvle  20023  dvivthlem1  20024  dvivth  20026  dvne0  20027  lhop1lem  20029  lhop1  20030  lhop2  20031  lhop  20032  dvcnvrelem1  20033  dvcnvrelem2  20034  dvcnvre  20035  dvcvx  20036  dvfsumle  20037  dvfsumge  20038  dvfsumabs  20039  dvfsumlem2  20043  dvfsumrlim  20047  ftc1a  20053  ftc1lem3  20054  ftc1lem6  20057  ftc1  20058  ftc1cn  20059  ftc2  20060  ftc2ditglem  20061  itgparts  20063  itgsubstlem  20064  itgsubst  20065  aacjcl  20376  aalioulem3  20383  taylthlem2  20422  taylth  20423  abelth2  20490  reeff1olem  20494  efcvx  20497  pilem3  20501  pige3  20557  recosf1o  20569  resinf1o  20570  dvrelog  20660  relogcn  20661  logcnlem5  20669  logcn  20670  dvloglem  20671  dvlog2lem  20675  logccv  20686  dvcxp1  20758  cxpcn3  20764  resqrcn  20765  loglesqr  20774  ssscongptld  20798  ressatans  20906  rlimcnp  20936  efrlim  20940  jensenlem1  20957  jensenlem2  20958  jensen  20959  amgm  20961  ftalem3  20989  basellem9  21003  efnnfsumcl  21017  efchtdvds  21074  lgsdchr  21264  dchrvmasumlem1  21321  dchrisum0lem3  21345  pntlem3  21435  readdsubgo  22073  circgrp  22094  ipasslem7  22469  rexdiv  24349  fsumrp0cl  24408  rge0srg  24490  regsumfsum  24529  rebase  24594  re0g  24598  xrge0slmod  24609  unitsscn  24623  rmulccn  24655  raddcn  24656  xrge0iifhom  24664  lmlimxrge0  24675  recms  24686  reust  24687  rezh  24698  esumpfinvallem  24821  esumpfinval  24822  esumpfinvalf  24823  esumcvg  24833  plymulx0  25217  plymulx  25218  signsplypnf  25220  signsply0  25221  lgamgulmlem2  25280  cvxpcon  25395  cvxscon  25396  rescon  25399  fprodrecl  25736  fprodrpcl  25739  rerisefaccl  25790  refallfaccl  25791  rprisefaccl  25796  mblfinlem2  26698  mbfresfi  26707  ftc1cnnclem  26734  ftc1cnnc  26735  ftc1anclem3  26738  ftc1anclem5  26740  ftc1anclem7  26742  ftc1anclem8  26743  ftc1anc  26744  ftc2nc  26745  dvreasin  26746  dvreacos  26747  areacirclem1  26748  areacirclem2  26749  areacirclem3  26750  areacirclem4  26751  areacirc  26753  ivthALT  26794  repwsmet  26999  rrnequiv  27000  rrntotbnd  27001  reheibor  27004  iccbnd  27005  ssrecnpr  28036  sblpnf  28038  lhe4.4ex1a  28045  refsumcn  28196  climreeq  28233  dvcosre  28235  itgsin0pilem1  28238  ibliccsinexp  28239  iblioosinexp  28241  itgsinexplem1  28242  itgsinexp  28243  wallispilem2  28309
  Copyright terms: Public domain W3C validator