MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  posdifd Structured version   Visualization version   GIF version

Theorem posdifd 11227
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
StepHypRef Expression
1 leidd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 ltnegd.2 . 2 (𝜑𝐵 ∈ ℝ)
3 posdif 11133 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
41, 2, 3syl2anc 587 1 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wcel 2115   class class class wbr 5053  (class class class)co 7151  cr 10536  0cc0 10537   < clt 10675  cmin 10870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7457  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5054  df-opab 5116  df-mpt 5134  df-id 5448  df-po 5462  df-so 5463  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-iota 6304  df-fun 6347  df-fn 6348  df-f 6349  df-f1 6350  df-fo 6351  df-f1o 6352  df-fv 6353  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-er 8287  df-en 8508  df-dom 8509  df-sdom 8510  df-pnf 10677  df-mnf 10678  df-ltxr 10680  df-sub 10872  df-neg 10873
This theorem is referenced by:  possumd  11265  ltmul1a  11489  cshwcsh2id  14192  sqrlem7  14610  fsumlt  15157  bpoly4  15415  sin01gt0  15545  nno  15733  pythagtriplem10  16157  evth  23573  minveclem4  24045  ismbf3d  24267  itg2seq  24355  dvferm1lem  24596  dvferm2lem  24598  mvth  24604  dvlip  24605  dvgt0  24616  dvlt0  24617  dvge0  24618  dvcvx  24632  ftc1lem4  24651  pilem2  25056  cosordlem  25131  lgamgulmlem2  25624  lgsquadlem1  25973  brbtwn2  26708  axpaschlem  26743  axcontlem8  26774  crctcshwlkn0  27616  clwlkclwwlklem2a4  27791  clwwlkext2edg  27850  minvecolem4  28672  cycpmrn  30827  sgnsub  31887  signslema  31917  fdvposlt  31955  tgoldbachgtde  32016  dnibndlem5  33906  unbdqndv2lem2  33934  knoppndvlem2  33937  knoppndvlem21  33956  poimirlem7  35036  itg2addnclem  35080  itg2gt0cn  35084  ftc1cnnclem  35100  areacirclem1  35117  areacirc  35122  3cubeslem1  39569  irrapxlem3  39709  pell14qrgt0  39744  rmspecnonsq  39792  rmspecfund  39794  rmspecpos  39801  jm3.1lem1  39902  radcnvrat  40966  supxrgere  41918  supxrgelem  41922  dvbdfbdioolem1  42523  dvbdfbdioolem2  42524  ioodvbdlimc1lem1  42526  ioodvbdlimc1lem2  42527  ioodvbdlimc2lem  42529  dvnxpaek  42537  wallispilem4  42663  wallispi2lem1  42666  stirlinglem11  42679  fourierdlem4  42706  fourierdlem6  42708  fourierdlem7  42709  fourierdlem19  42721  fourierdlem26  42728  fourierdlem41  42743  fourierdlem42  42744  fourierdlem48  42749  fourierdlem49  42750  fourierdlem51  42752  fourierdlem61  42762  fourierdlem63  42764  fourierdlem64  42765  fourierdlem65  42766  fourierdlem71  42772  fourierdlem79  42780  fourierdlem89  42790  fourierdlem90  42791  fourierdlem91  42792  fouriersw  42826  etransclem15  42844  etransclem24  42853  etransclem25  42854  etransclem35  42864  ioorrnopnlem  42899  hoidmvlelem2  43188  hoiqssbllem2  43215  iunhoiioolem  43267  zm1nn  43812  nnoALTV  44166  fllog2  44935  dignn0flhalflem1  44982  eenglngeehlnmlem2  45105  2itscp  45148
  Copyright terms: Public domain W3C validator