Theorem posdifd 11735

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 11641	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
4	1, 2, 3	syl2anc 590	1 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))

Syntax hints:   → wi 4   ↔ wb 207   ∈ wcel 2119   class class class wbr 5079  (class class class)co 7363  ℝcr 11035  0cc0 11036   < clt 11177   − cmin 11375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-ltxr 11182  df-sub 11377  df-neg 11378

This theorem is referenced by:  possumd  11773  ltmul1a  12002  cshwcsh2id  14788  01sqrexlem7  15208  fsumlt  15761  bpoly4  16022  sin01gt0  16155  nno  16349  pythagtriplem10  16789  evth  24951  minveclem4  25424  ismbf3d  25646  itg2seq  25734  dvferm1lem  25976  dvferm2lem  25978  mvth  25984  dvlip  25985  dvgt0  25996  dvlt0  25997  dvge0  25998  dvcvx  26012  ftc1lem4  26031  pilem2  26442  cosordlem  26519  lgamgulmlem2  27018  lgsquadlem1  27368  brbtwn2  28999  axpaschlem  29034  axcontlem8  29065  crctcshwlkn0  29914  clwlkclwwlklem2a4  30092  clwwlkext2edg  30151  minvecolem4  30976  sgnsub  32936  cycpmrn  33231  signslema  34753  fdvposlt  34790  tgoldbachgtde  34851  dnibndlem5  36795  unbdqndv2lem2  36823  knoppndvlem2  36826  knoppndvlem21  36845  poimirlem7  38001  itg2addnclem  38045  itg2gt0cn  38049  ftc1cnnclem  38065  areacirclem1  38082  areacirc  38087  posbezout  42592  hashscontpow1  42613  aks6d1c2  42622  aks6d1c5lem1  42628  aks6d1c5lem2  42630  sticksstones12a  42649  3cubeslem1  43140  irrapxlem3  43276  pell14qrgt0  43311  rmspecnonsq  43359  rmspecfund  43361  rmspecpos  43368  jm3.1lem1  43469  radcnvrat  44765  supxrgere  45785  supxrgelem  45789  dvbdfbdioolem1  46378  dvbdfbdioolem2  46379  ioodvbdlimc1lem1  46381  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvnxpaek  46392  wallispilem4  46518  wallispi2lem1  46521  stirlinglem11  46534  fourierdlem4  46561  fourierdlem6  46563  fourierdlem7  46564  fourierdlem19  46576  fourierdlem26  46583  fourierdlem41  46598  fourierdlem42  46599  fourierdlem48  46604  fourierdlem49  46605  fourierdlem51  46607  fourierdlem61  46617  fourierdlem63  46619  fourierdlem64  46620  fourierdlem65  46621  fourierdlem71  46627  fourierdlem79  46635  fourierdlem89  46645  fourierdlem90  46646  fourierdlem91  46647  fouriersw  46681  etransclem15  46699  etransclem24  46708  etransclem25  46709  etransclem35  46719  ioorrnopnlem  46754  hoidmvlelem2  47046  hoiqssbllem2  47073  iunhoiioolem  47125  zm1nn  47772  nnoALTV  48193  fllog2  49066  dignn0flhalflem1  49113  eenglngeehlnmlem2  49236  2itscp  49279