Theorem subclt 5354

Description: Closure law for subtraction.

Assertion

Ref	Expression
subclt	|- ((A e. CC /\ B e. CC) -> (A - B) e. CC)

Proof of Theorem subclt

Step	Hyp	Ref	Expression
1		opreq1 3965	. . 3 |- (A = if(A e. CC, A, 0) -> (A - B) = (if(A e. CC, A, 0) - B))
2	1	eleq1d 1539	. 2 |- (A = if(A e. CC, A, 0) -> ((A - B) e. CC <-> (if(A e. CC, A, 0) - B) e. CC))
3		opreq2 3966	. . 3 |- (B = if(B e. CC, B, 0) -> (if(A e. CC, A, 0) - B) = (if(A e. CC, A, 0) - if(B e. CC, B, 0)))
4	3	eleq1d 1539	. 2 |- (B = if(B e. CC, B, 0) -> ((if(A e. CC, A, 0) - B) e. CC <-> (if(A e. CC, A, 0) - if(B e. CC, B, 0)) e. CC))
5		0cn 5315	. . . 4 |- 0 e. CC
6	5	elimel 2392	. . 3 |- if(A e. CC, A, 0) e. CC
7	5	elimel 2392	. . 3 |- if(B e. CC, B, 0) e. CC
8	6, 7	subcl 5353	. 2 |- (if(A e. CC, A, 0) - if(B e. CC, B, 0)) e. CC
9	2, 4, 8	dedth2h 2385	1 |- ((A e. CC /\ B e. CC) -> (A - B) e. CC)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 955   e. wcel 957  ifcif 2359  (class class class)co 3960  CCcc 5219  0cc0 5221   - cmin 5279

This theorem is referenced by:  negclt 5355  subopr 5357  pncan3t 5364  addsubt 5371  addsub12t 5373  npncant 5387  nppcant 5388  subdit 5414  subdirt 5415  subsub2t 5448  subsub4t 5451  nnncant 5453  nnncan1t 5454  nnncan2t 5455  subadd4t 5462  pnpcant 5465  recextlem1 5669  recext 5671  muleqaddt 5683  halfaddsubcl 6001  halfaddsubt 6002  elnnnn0 6133  uzindOLD 6170  shftval2t 6302  2shft 6307  shftcan2t 6308  seq1seq02t 6493  seqzp1 6498  seq0p1 6501  seqzval2t 6503  subsqt 6592  subsq2t 6593  cjclt 6717  sqabssubt 6811  abs3dift 6864  abs2dift 6867  abs2difabst 6868  caubnd 6892  caure 6893  cauim 6894  ser1absdiflem 6895  fsumconst 7006  clm4le 7049  2climnn 7070  2climnn0 7071  climrecl 7078  climaddlem3 7085  climmullem3 7091  climmullem4 7092  climmullem5 7093  climabslem 7117  climcj 7119  climre 7120  climim 7121  climcau 7125  serzf0 7140  ser1f0 7141  cvgcmp3c 7157  georeclim 7211  geoisumr 7214  geoisum1c 7216  abscncflem 7245  recncf 7247  imcncf 7248  cjcncf 7249  mulc1cncf 7250  efaddlem16 7331  sinclt 7409  sinnegt 7420  efivalt 7425  addsint 7435  subcost 7438  cnmet 7887  ioo2bl 7895  subcn 7970  sm1cnilem 8333  ipval2 8343  4ipval2 8344  4ipval3 8348  ipcj 8353  sinco 8650  efimpi 8679  hvmulcan2t 8924  occllem6 9166  pjthlem8 9214  lnfncon 9981  mslb1 10580  2wsms 10581

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2690  ax-sep 2700  ax-nul 2707  ax-pow 2739  ax-pr 2776  ax-un 2863  ax-inf2 4612

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-ral 1648  df-rex 1649  df-reu 1650  df-rab 1651  df-v 1810  df-sbc 1940  df-csb 2000  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-pss 2053  df-nul 2279  df-if 2360  df-pw 2400  df-sn 2410  df-pr 2411  df-tp 2413  df-op 2414  df-uni 2501  df-int 2531  df-iun 2565  df-br 2617  df-opab 2664  df-tr 2678  df-eprel 2829  df-id 2832  df-po 2837  df-so 2847  df-fr 2914  df-we 2931  df-ord 2948  df-on 2949  df-lim 2950  df-suc 2951  df-om 3129  df-xp 3181  df-rel 3182  df-cnv 3183  df-co 3184  df-dm 3185  df-rn 3186  df-res 3187  df-ima 3188  df-fun 3189  df-fn 3190  df-f 3191  df-fv 3195  df-rdg 3929  df-opr 3962  df-oprab 3963  df-1st 4076  df-2nd 4077  df-1o 4130  df-oadd 4132  df-omul 4133  df-er 4258  df-ec 4260  df-qs 4263  df-ni 4987  df-pli 4988  df-mi 4989  df-lti 4990  df-plpq 5022  df-mpq 5023  df-enq 5024  df-nq 5025  df-plq 5026  df-mq 5027  df-rq 5028  df-ltq 5029  df-1q 5030  df-np 5073  df-1p 5074  df-plp 5075  df-mp 5076  df-ltp 5077  df-plpr 5151  df-mpr 5152  df-enr 5153  df-nr 5154  df-plr 5155  df-mr 5156  df-0r 5158  df-1r 5159  df-m1r 5160  df-c 5227  df-0 5228  df-1 5229  df-i 5230  df-r 5231  df-plus 5232  df-mul 5233  df-sub 5343

Copyright terms: Public domain