Theorem resubcl 8215

Description: Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997.)

Assertion

Ref	Expression
resubcl	|- ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )

Proof of Theorem resubcl

Step	Hyp	Ref	Expression
1		recn 7939	. . 3 |- ( A e. RR -> A e. CC )
2		recn 7939	. . 3 |- ( B e. RR -> B e. CC )
3		negsub 8199	. . 3 |- ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
4	1, 2, 3	syl2an 289	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A + -u B ) = ( A - B ) )
5		renegcl 8212	. . 3 |- ( B e. RR -> -u B e. RR )
6		readdcl 7932	. . 3 |- ( ( A e. RR /\ -u B e. RR ) -> ( A + -u B ) e. RR )
7	5, 6	sylan2 286	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A + -u B ) e. RR )
8	4, 7	eqeltrrd 2255	1 |- ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1353   e. wcel 2148  (class class class)co 5870   CCcc 7804   RRcr 7805   + caddc 7809   - cmin 8122   -ucneg 8123

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 4119  ax-pow 4172  ax-pr 4207  ax-setind 4534  ax-resscn 7898  ax-1cn 7899  ax-icn 7901  ax-addcl 7902  ax-addrcl 7903  ax-mulcl 7904  ax-addcom 7906  ax-addass 7908  ax-distr 7910  ax-i2m1 7911  ax-0id 7914  ax-rnegex 7915  ax-cnre 7917

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 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-br 4002  df-opab 4063  df-id 4291  df-xp 4630  df-rel 4631  df-cnv 4632  df-co 4633  df-dm 4634  df-iota 5175  df-fun 5215  df-fv 5221  df-riota 5826  df-ov 5873  df-oprab 5874  df-mpo 5875  df-sub 8124  df-neg 8125

This theorem is referenced by:  peano2rem  8218  resubcld  8332  posdif  8406  lt2sub  8411  le2sub  8412  cju  8912  elz2  9318  difrp  9686  iooshf  9946  iccshftl  9990  lincmb01cmp  9997  uzsubsubfz  10040  difelfzle  10127  fzonmapblen  10180  eluzgtdifelfzo  10190  subfzo0  10235  modfzo0difsn  10388  expubnd  10570  absdiflt  11092  absdifle  11093  elicc4abs  11094  abssubge0  11102  abs2difabs  11108  maxabsle  11204  resin4p  11717  recos4p  11718  cos01bnd  11757  cos01gt0  11761  pythagtriplem12  12265  pythagtriplem14  12267  pythagtriplem16  12269  fldivp1  12336  bl2ioo  13824  ioo2bl  13825  ioo2blex  13826  blssioo  13827  sincosq1sgn  14029  sincosq2sgn  14030  sincosq3sgn  14031  sincosq4sgn  14032  sinq12gt0  14033  cosq14gt0  14035  tangtx  14041  relogdiv  14073  logdivlti  14084  redc0  14576  reap0  14577