Theorem posdifd 11767

Description: Comparison of two numbers whose difference is positive. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
leidd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltnegd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
posdifd	⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))

Proof of Theorem posdifd

Step	Hyp	Ref	Expression
1		leidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		ltnegd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		posdif 11673	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
4	1, 2, 3	syl2anc 593	1 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2141   class class class wbr 5097  (class class class)co 7390  ℝcr 11065  0cc0 11066   < clt 11209   − cmin 11407

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-resscn 11123  ax-1cn 11124  ax-icn 11125  ax-addcl 11126  ax-addrcl 11127  ax-mulcl 11128  ax-mulrcl 11129  ax-mulcom 11130  ax-addass 11131  ax-mulass 11132  ax-distr 11133  ax-i2m1 11134  ax-1ne0 11135  ax-1rid 11136  ax-rnegex 11137  ax-rrecex 11138  ax-cnre 11139  ax-pre-lttri 11140  ax-pre-lttrn 11141  ax-pre-ltadd 11142

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-po 5551  df-so 5552  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8671  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11211  df-mnf 11212  df-ltxr 11214  df-sub 11409  df-neg 11410

This theorem is referenced by:  possumd  11805  ltmul1a  12033  cshwcsh2id  14834  sgnsub  15109  01sqrexlem7  15265  fsumlt  15818  bpoly4  16079  sin01gt0  16212  nno  16406  pythagtriplem10  16846  evth  25008  minveclem4  25481  ismbf3d  25703  itg2seq  25791  dvferm1lem  26033  dvferm2lem  26035  mvth  26041  dvlip  26042  dvgt0  26053  dvlt0  26054  dvge0  26055  dvcvx  26069  ftc1lem4  26088  pilem2  26502  cosordlem  26582  lgamgulmlem2  27081  lgsquadlem1  27431  brbtwn2  29062  axpaschlem  29097  axcontlem8  29128  crctcshwlkn0  29977  clwlkclwwlklem2a4  30155  clwwlkext2edg  30214  minvecolem4  31039  cycpmrn  33283  signslema  34816  fdvposlt  34853  tgoldbachgtde  34914  dnibndlem5  36880  unbdqndv2lem2  36908  knoppndvlem2  36911  knoppndvlem21  36930  poimirlem7  38086  itg2addnclem  38130  itg2gt0cn  38134  ftc1cnnclem  38150  areacirclem1  38167  areacirc  38172  posbezout  42677  hashscontpow1  42698  aks6d1c2  42707  aks6d1c5lem1  42713  aks6d1c5lem2  42715  sticksstones12a  42734  3cubeslem1  43225  irrapxlem3  43361  pell14qrgt0  43396  rmspecnonsq  43444  rmspecfund  43446  rmspecpos  43453  jm3.1lem1  43554  radcnvrat  44850  supxrgere  45869  supxrgelem  45873  dvbdfbdioolem1  46462  dvbdfbdioolem2  46463  ioodvbdlimc1lem1  46465  ioodvbdlimc1lem2  46466  ioodvbdlimc2lem  46468  dvnxpaek  46476  wallispilem4  46602  wallispi2lem1  46605  stirlinglem11  46618  fourierdlem4  46645  fourierdlem6  46647  fourierdlem7  46648  fourierdlem19  46660  fourierdlem26  46667  fourierdlem41  46682  fourierdlem42  46683  fourierdlem48  46688  fourierdlem49  46689  fourierdlem51  46691  fourierdlem61  46701  fourierdlem63  46703  fourierdlem64  46704  fourierdlem65  46705  fourierdlem71  46711  fourierdlem79  46719  fourierdlem89  46729  fourierdlem90  46730  fourierdlem91  46731  fouriersw  46765  etransclem15  46783  etransclem24  46792  etransclem25  46793  etransclem35  46803  ioorrnopnlem  46838  hoidmvlelem2  47130  hoiqssbllem2  47157  iunhoiioolem  47209  zm1nn  47856  nnoALTV  48277  fllog2  49150  dignn0flhalflem1  49197  eenglngeehlnmlem2  49320  2itscp  49363