ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  resubcld Unicode version

Theorem resubcld 8328
Description: Closure law for subtraction of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
renegcld.1  |-  ( ph  ->  A  e.  RR )
resubcld.2  |-  ( ph  ->  B  e.  RR )
Assertion
Ref Expression
resubcld  |-  ( ph  ->  ( A  -  B
)  e.  RR )

Proof of Theorem resubcld
StepHypRef Expression
1 renegcld.1 . 2  |-  ( ph  ->  A  e.  RR )
2 resubcld.2 . 2  |-  ( ph  ->  B  e.  RR )
3 resubcl 8211 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  -  B
)  e.  RR )
41, 2, 3syl2anc 411 1  |-  ( ph  ->  ( A  -  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 2148  (class class class)co 5869   RRcr 7801    - cmin 8118
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-setind 4533  ax-resscn 7894  ax-1cn 7895  ax-icn 7897  ax-addcl 7898  ax-addrcl 7899  ax-mulcl 7900  ax-addcom 7902  ax-addass 7904  ax-distr 7906  ax-i2m1 7907  ax-0id 7910  ax-rnegex 7911  ax-cnre 7913
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-opab 4062  df-id 4290  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-iota 5174  df-fun 5214  df-fv 5220  df-riota 5825  df-ov 5872  df-oprab 5873  df-mpo 5874  df-sub 8120  df-neg 8121
This theorem is referenced by:  ltsubadd  8379  lesubadd  8381  ltaddsub  8383  leaddsub  8385  lesub1  8403  lesub2  8404  ltsub1  8405  ltsub2  8406  lt2sub  8407  le2sub  8408  rereim  8533  ltmul1a  8538  cru  8549  lemul1a  8804  ztri3or  9285  lincmb01cmp  9990  iccf1o  9991  rebtwn2z  10241  qbtwnrelemcalc  10242  qbtwnre  10243  intfracq  10306  modqval  10310  modqlt  10319  modqsubdir  10379  ser3le  10504  expnbnd  10629  crre  10850  remullem  10864  recvguniqlem  10987  resqrexlemover  11003  resqrexlemcalc2  11008  resqrexlemcalc3  11009  resqrexlemnmsq  11010  resqrexlemnm  11011  resqrexlemcvg  11012  resqrexlemglsq  11015  resqrexlemga  11016  fzomaxdiflem  11105  caubnd2  11110  amgm2  11111  icodiamlt  11173  qdenre  11195  maxabslemab  11199  maxabslemlub  11200  maxltsup  11211  bdtrilem  11231  bdtri  11232  mulcn2  11304  reccn2ap  11305  climle  11326  climsqz  11327  climsqz2  11328  climcvg1nlem  11341  fsumle  11455  cvgratnnlembern  11515  cvgratnnlemsumlt  11520  cvgratnnlemfm  11521  cvgratnnlemrate  11522  cvgratnn  11523  efltim  11690  sin01bnd  11749  sin01gt0  11753  cos12dec  11759  uzwodc  12021  pythagtriplem12  12258  pythagtriplem14  12260  blss2ps  13573  blss2  13574  blssps  13594  blss  13595  ivthinclemlopn  13781  ivthinclemuopn  13783  dvcjbr  13839  reeff1oleme  13860  efltlemlt  13862  sin0pilem1  13869  tangtx  13926  cosordlem  13937  cosq34lt1  13938  cvgcmp2nlemabs  14436  iooref1o  14438  trilpolemlt1  14445  trirec0  14448  apdifflemf  14450
  Copyright terms: Public domain W3C validator