Axiom ax-resscn 11184

Description: The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by Theorem axresscn 11160. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11126	. 2 class ℝ
2		cc 11125	. 2 class ℂ
3	1, 2	wss 3902	1 wff ℝ ⊆ ℂ

This axiom is used by:  recn  11217  reex  11218  recni  11250  qsscn  13012  ioosscn  13463  unitsscn  13555  reexpcl  14144  rpexpcl  14146  reexpclz  14148  expge0  14164  expge1  14165  rlimrecl  15669  abscn2  15688  recn2  15690  imcn2  15691  climabs  15693  climre  15695  climim  15696  rlimabs  15698  rlimre  15700  rlimim  15701  caurcvgr  15763  caucvgrlem2  15764  caurcvg  15766  fsumrecl  15822  fsumrpcl  15825  fsumge0  15884  fsumre  15897  fsumim  15898  fprodrecl  16044  fprodrpcl  16047  fprodreclf  16050  fprodge0  16084  fprodge1  16086  rerisefaccl  16108  refallfaccl  16109  rprisefaccl  16114  reeff1  16212  nthruc  16344  regsumfsum  21649  rge0srg  21652  rebase  21820  re0g  21826  regsumsupp  21836  remet  25017  tgioo2  25030  xrsdsre  25038  recld2  25042  reperf  25047  iitopon  25108  dfii3  25112  abscncf  25130  recncf  25131  imcncf  25132  abscncfALT  25153  cnmptre  25156  icchmeo  25170  cnrehmeo  25182  evth  25188  evth2  25189  lebnumlem2  25191  lebnumii  25195  cphsqrtcl  25413  resscdrg  25587  ishl2  25599  recms  25609  reust  25610  evthicc  25688  evthicc2  25689  ovolfsf  25700  volcn  25835  volivth  25836  ismbf  25857  cncombf  25887  cnmbf  25888  0plef  25901  itg1ge0  25915  i1faddlem  25922  i1fmul  25925  itg1addlem4  25928  i1fsub  25937  itg1sub  25938  mbfi1fseqlem5  25948  xrge0f  25960  itg20  25966  itg2const  25969  itg2mulc  25976  itg2addlem  25987  i1fibl  26037  itgitg1  26038  iblabslem  26057  iblabs  26058  bddmulibl  26068  recnprss  26133  dvmptresicc  26145  dvcjbr  26178  dvfre  26180  dvnfre  26181  dvferm1  26214  dvferm2  26216  rolle  26219  cmvth  26220  mvth  26221  dvlip  26222  dvlipcn  26223  dvlip2  26224  c1liplem1  26225  c1lip2  26227  dvgt0lem1  26231  dvle  26236  dvivthlem1  26237  dvivth  26239  dvne0  26240  lhop1lem  26242  lhop1  26243  lhop2  26244  lhop  26245  dvcnvrelem1  26246  dvcnvrelem2  26247  dvcnvre  26248  dvcvx  26249  dvfsumle  26250  dvfsumge  26251  dvfsumabs  26252  dvfsumlem2  26256  dvfsumrlim  26260  ftc1a  26266  ftc1lem3  26267  ftc1lem6  26270  ftc1  26271  ftc1cn  26272  ftc2  26273  ftc2ditglem  26274  itgparts  26276  itgsubstlem  26277  itgsubst  26278  itgpowd  26279  plyn0mulidp  26512  plymulidp  26513  aacjcl  26560  aalioulem3  26567  taylthlem2  26607  taylth  26608  abelth2  26675  reeff1olem  26679  efcvx  26682  pilem3  26686  pige3ALT  26755  recosf1o  26770  resinf1o  26771  dvrelog  26872  relogcn  26873  logcnlem5  26881  logcn  26882  dvloglem  26883  dvlog2lem  26887  logccv  26898  dvcxp1  26975  cxpcn3  26983  resqrtcn  26984  loglesqrt  26996  ssscongptld  27057  ressatans  27169  rlimcnp  27200  efrlim  27204  jensenlem1  27221  jensenlem2  27222  jensen  27223  amgm  27225  lgamgulmlem2  27264  ftalem3  27309  basellem9  27323  efnnfsumcl  27337  efchtdvds  27393  lgsdchr  27589  dchrvmasumlem1  27729  dchrisum0lem3  27753  pntlem3  27843  cchhllem  29329  ex-fpar  30928  ipasslem7  31303  fprodex01  33282  indsumin  33294  rexdiv  33358  fsumrp0cl  33448  xrge0slmod  33775  ccfldsrarelvec  34168  ccfldextdgrr  34169  rmulccn  34425  raddcn  34426  xrge0iifhom  34434  lmlimxrge0  34445  rezh  34466  esumpfinvallem  34571  esumpfinval  34572  esumpfinvalf  34573  esumcvg  34583  signsplypnf  35045  signsply0  35046  iblidicc  35087  rpsqrtcn  35088  ftc2re  35093  fdvposlt  35094  fdvneggt  35095  fdvposle  35096  fdvnegge  35097  itgexpif  35101  circlemeth  35135  circlemethnat  35136  circlevma  35137  circlemethhgt  35138  logdivsqrle  35145  resconn  35812  ivthALT  36941  dnicn  37176  knoppcnlem10  37186  knoppcnlem11  37187  unbdqndv2  37195  knoppndv  37218  knoppcn2  37220  broucube  38390  mblfinlem2  38394  mbfresfi  38402  ftc1cnnclem  38427  ftc1cnnc  38428  ftc1anclem3  38431  ftc1anclem5  38433  ftc1anclem7  38435  ftc1anclem8  38436  ftc1anc  38437  ftc2nc  38438  asindmre  38439  dvreasin  38442  dvreacos  38443  areacirclem1  38444  areacirclem2  38445  areacirclem3  38446  areacirclem4  38447  areacirc  38449  repwsmet  38571  rrnequiv  38572  rrntotbnd  38573  reheibor  38576  iccbnd  38577  intlewftc  42914  dvrelog2  42917  dvrelog3  42918  aks4d1p1p5  42928  rpsscn  43161  redvmptabs  43222  readvrec2  43223  resuppsinopn  43225  readvcot  43226  resubeqsub  43292  subresre  43293  arearect  44043  areaquad  44044  k0004val0  44981  extoimad  44991  imo72b2lem0  44992  imo72b2lem2  44994  imo72b2lem1  44996  imo72b2  44999  ssrecnpr  45119  sblpnf  45121  radcnvrat  45125  lhe4.4ex1a  45140  refsumcn  45851  rr2sscn2  46182  uzsscn  46290  evthiccabs  46313  climreeq  46430  limciccioolb  46438  limcrecl  46446  limcicciooub  46452  limcleqr  46459  lptioo2cn  46460  lptioo1cn  46461  limclner  46466  liminflimsupclim  46622  resincncf  46690  cncficcgt0  46703  cncfiooicclem1  46708  cncfiooiccre  46710  jumpncnp  46713  dvcosre  46727  dvmptconst  46730  dvmptidg  46732  fperdvper  46734  dvresioo  46736  dvmulcncf  46740  dvdivcncf  46742  dvbdfbdioolem1  46743  ioodvbdlimc1lem1  46746  ioodvbdlimc1lem2  46747  ioodvbdlimc1  46748  ioodvbdlimc2lem  46749  ioodvbdlimc2  46750  itgsin0pilem1  46765  ibliccsinexp  46766  iblioosinexp  46768  itgsinexplem1  46769  itgsinexp  46770  itgcoscmulx  46784  itgsincmulx  46789  itgsubsticclem  46790  itgiccshift  46795  itgperiod  46796  itgsbtaddcnst  46797  dirkeritg  46917  dirkercncflem2  46919  dirkercncflem3  46920  dirkercncflem4  46921  dirkercncf  46922  fourierdlem16  46938  fourierdlem18  46940  fourierdlem21  46943  fourierdlem22  46944  fourierdlem39  46961  fourierdlem42  46964  fourierdlem48  46969  fourierdlem49  46970  fourierdlem53  46974  fourierdlem57  46978  fourierdlem58  46979  fourierdlem59  46980  fourierdlem60  46981  fourierdlem61  46982  fourierdlem62  46983  fourierdlem68  46989  fourierdlem70  46991  fourierdlem72  46993  fourierdlem73  46994  fourierdlem74  46995  fourierdlem75  46996  fourierdlem76  46997  fourierdlem78  46999  fourierdlem80  47001  fourierdlem83  47004  fourierdlem84  47005  fourierdlem85  47006  fourierdlem88  47009  fourierdlem89  47010  fourierdlem90  47011  fourierdlem91  47012  fourierdlem93  47014  fourierdlem94  47015  fourierdlem95  47016  fourierdlem96  47017  fourierdlem97  47018  fourierdlem98  47019  fourierdlem99  47020  fourierdlem101  47022  fourierdlem103  47024  fourierdlem104  47025  fourierdlem111  47032  fourierdlem112  47033  fourierdlem113  47034  fouriercnp  47041  sqwvfoura  47043  sqwvfourb  47044  fouriersw  47046  fouriercn  47047  etransclem2  47051  etransclem18  47067  etransclem23  47072  etransclem46  47095  rrxtopnfi  47102  rrndistlt  47105  sge0sn  47194  sge0tsms  47195  sge0f1o  47197  sge0pr  47209  sge0resplit  47221  sge0iunmptlemre  47230  sge0isummpt2  47247  hoicvr  47363  hoidmvlelem2  47411  lamberte  47743  refdivmptf  49459  refdivmptfv  49463  amgmlemALT  50808