Theorem lesub0i 8420

Description: Lemma to show a nonnegative number is zero. (Contributed by NM, 8-Oct-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)

Hypotheses

Ref	Expression
lt2.1	|- A e. RR
lt2.2	|- B e. RR

Assertion

Ref	Expression
lesub0i	|- ( ( 0 <_ A /\ B <_ ( B - A ) ) <-> A = 0 )

Proof of Theorem lesub0i

Step	Hyp	Ref	Expression
1		lt2.1	. 2 |- A e. RR
2		lt2.2	. 2 |- B e. RR
3		lesub0 8403	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <_ A /\ B <_ ( B - A ) ) <-> A = 0 ) )
4	1, 2, 3	mp2an 425	1 |- ( ( 0 <_ A /\ B <_ ( B - A ) ) <-> A = 0 )

Syntax hints:   /\ wa 103   <-> wb 104   = wceq 1350   e. wcel 2143   class class class wbr 3991  (class class class)co 5858   RRcr 7778   0cc0 7779   <_ cle 7960   - cmin 8095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 611  ax-in2 612  ax-io 706  ax-5 1442  ax-7 1443  ax-gen 1444  ax-ie1 1488  ax-ie2 1489  ax-8 1499  ax-10 1500  ax-11 1501  ax-i12 1502  ax-bndl 1504  ax-4 1505  ax-17 1521  ax-i9 1525  ax-ial 1529  ax-i5r 1530  ax-13 2145  ax-14 2146  ax-ext 2154  ax-sep 4109  ax-pow 4162  ax-pr 4196  ax-un 4420  ax-setind 4523  ax-cnex 7870  ax-resscn 7871  ax-1cn 7872  ax-1re 7873  ax-icn 7874  ax-addcl 7875  ax-addrcl 7876  ax-mulcl 7877  ax-addcom 7879  ax-addass 7881  ax-distr 7883  ax-i2m1 7884  ax-0id 7887  ax-rnegex 7888  ax-cnre 7890  ax-pre-ltirr 7891  ax-pre-apti 7894  ax-pre-ltadd 7895

This theorem depends on definitions:  df-bi 116  df-3an 977  df-tru 1353  df-fal 1356  df-nf 1456  df-sb 1758  df-eu 2024  df-mo 2025  df-clab 2159  df-cleq 2165  df-clel 2168  df-nfc 2303  df-ne 2343  df-nel 2438  df-ral 2455  df-rex 2456  df-reu 2457  df-rab 2459  df-v 2734  df-sbc 2958  df-dif 3125  df-un 3127  df-in 3129  df-ss 3136  df-pw 3570  df-sn 3591  df-pr 3592  df-op 3594  df-uni 3799  df-br 3992  df-opab 4053  df-id 4280  df-xp 4619  df-rel 4620  df-cnv 4621  df-co 4622  df-dm 4623  df-iota 5163  df-fun 5203  df-fv 5209  df-riota 5814  df-ov 5861  df-oprab 5862  df-mpo 5863  df-pnf 7961  df-mnf 7962  df-xr 7963  df-ltxr 7964  df-le 7965  df-sub 8097  df-neg 8098

This theorem is referenced by: (None)