![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > resubcl | Unicode version |
Description: Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997.) |
Ref | Expression |
---|---|
resubcl |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recn 7465 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | recn 7465 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | negsub 7720 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | syl2an 283 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | renegcl 7733 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | readdcl 7458 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | sylan2 280 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 4, 7 | eqeltrrd 2165 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 579 ax-in2 580 ax-io 665 ax-5 1381 ax-7 1382 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-8 1440 ax-10 1441 ax-11 1442 ax-i12 1443 ax-bndl 1444 ax-4 1445 ax-14 1450 ax-17 1464 ax-i9 1468 ax-ial 1472 ax-i5r 1473 ax-ext 2070 ax-sep 3955 ax-pow 4007 ax-pr 4034 ax-setind 4351 ax-resscn 7427 ax-1cn 7428 ax-icn 7430 ax-addcl 7431 ax-addrcl 7432 ax-mulcl 7433 ax-addcom 7435 ax-addass 7437 ax-distr 7439 ax-i2m1 7440 ax-0id 7443 ax-rnegex 7444 ax-cnre 7446 |
This theorem depends on definitions: df-bi 115 df-3an 926 df-tru 1292 df-fal 1295 df-nf 1395 df-sb 1693 df-eu 1951 df-mo 1952 df-clab 2075 df-cleq 2081 df-clel 2084 df-nfc 2217 df-ne 2256 df-ral 2364 df-rex 2365 df-reu 2366 df-rab 2368 df-v 2621 df-sbc 2841 df-dif 3001 df-un 3003 df-in 3005 df-ss 3012 df-pw 3429 df-sn 3450 df-pr 3451 df-op 3453 df-uni 3652 df-br 3844 df-opab 3898 df-id 4118 df-xp 4442 df-rel 4443 df-cnv 4444 df-co 4445 df-dm 4446 df-iota 4975 df-fun 5012 df-fv 5018 df-riota 5600 df-ov 5647 df-oprab 5648 df-mpt2 5649 df-sub 7645 df-neg 7646 |
This theorem is referenced by: peano2rem 7739 resubcld 7849 posdif 7923 lt2sub 7928 le2sub 7929 cju 8411 elz2 8808 difrp 9160 iooshf 9360 iccshftl 9403 lincmb01cmp 9410 uzsubsubfz 9451 difelfzle 9533 fzonmapblen 9586 eluzgtdifelfzo 9596 subfzo0 9641 modfzo0difsn 9790 expubnd 10000 absdiflt 10513 absdifle 10514 elicc4abs 10515 abssubge0 10523 abs2difabs 10529 maxabsle 10625 resin4p 10996 recos4p 10997 cos01bnd 11036 cos01gt0 11040 |
Copyright terms: Public domain | W3C validator |