Theorem posdifd 11219

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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2108   class class class wbr 5057  (class class class)co 7148  ℝcr 10528  0cc0 10529   < clt 10667   − cmin 10862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-ltxr 10672  df-sub 10864  df-neg 10865

This theorem is referenced by:  possumd  11257  ltmul1a  11481  cshwcsh2id  14182  sqrlem7  14600  fsumlt  15147  bpoly4  15405  sin01gt0  15535  nno  15725  pythagtriplem10  16149  evth  23555  minveclem4  24027  ismbf3d  24247  itg2seq  24335  dvferm1lem  24573  dvferm2lem  24575  mvth  24581  dvlip  24582  dvgt0  24593  dvlt0  24594  dvge0  24595  dvcvx  24609  ftc1lem4  24628  pilem2  25032  cosordlem  25107  lgamgulmlem2  25599  lgsquadlem1  25948  brbtwn2  26683  axpaschlem  26718  axcontlem8  26749  crctcshwlkn0  27591  clwlkclwwlklem2a4  27767  clwwlkext2edg  27827  minvecolem4  28649  cycpmrn  30778  sgnsub  31795  signslema  31825  fdvposlt  31863  tgoldbachgtde  31924  dnibndlem5  33814  unbdqndv2lem2  33842  knoppndvlem2  33845  knoppndvlem21  33864  poimirlem7  34891  itg2addnclem  34935  itg2gt0cn  34939  ftc1cnnclem  34957  areacirclem1  34974  areacirc  34979  3cubeslem1  39272  irrapxlem3  39412  pell14qrgt0  39447  rmspecnonsq  39495  rmspecfund  39497  rmspecpos  39504  jm3.1lem1  39605  radcnvrat  40637  supxrgere  41591  supxrgelem  41595  dvbdfbdioolem1  42203  dvbdfbdioolem2  42204  ioodvbdlimc1lem1  42206  ioodvbdlimc1lem2  42207  ioodvbdlimc2lem  42209  dvnxpaek  42217  wallispilem4  42344  wallispi2lem1  42347  stirlinglem11  42360  fourierdlem4  42387  fourierdlem6  42389  fourierdlem7  42390  fourierdlem19  42402  fourierdlem26  42409  fourierdlem41  42424  fourierdlem42  42425  fourierdlem48  42430  fourierdlem49  42431  fourierdlem51  42433  fourierdlem61  42443  fourierdlem63  42445  fourierdlem64  42446  fourierdlem65  42447  fourierdlem71  42453  fourierdlem79  42461  fourierdlem89  42471  fourierdlem90  42472  fourierdlem91  42473  fouriersw  42507  etransclem15  42525  etransclem24  42534  etransclem25  42535  etransclem35  42545  ioorrnopnlem  42580  hoidmvlelem2  42869  hoiqssbllem2  42896  iunhoiioolem  42948  zm1nn  43493  nnoALTV  43851  fllog2  44619  dignn0flhalflem1  44666  eenglngeehlnmlem2  44716  2itscp  44759