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

Theorem ltnled 10780
Description: 'Less than' in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
ltd.1 (𝜑𝐴 ∈ ℝ)
ltd.2 (𝜑𝐵 ∈ ℝ)
Assertion
Ref Expression
ltnled (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))

Proof of Theorem ltnled
StepHypRef Expression
1 ltd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 ltd.2 . 2 (𝜑𝐵 ∈ ℝ)
3 ltnle 10713 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
41, 2, 3syl2anc 587 1 (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wcel 2112   class class class wbr 5033  cr 10529   < clt 10668  cle 10669
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-xp 5529  df-cnv 5531  df-xr 10672  df-le 10674
This theorem is referenced by:  ltsub1  11129  ltsub2  11130  0mnnnnn0  11921  mul2lt0bi  12487  fzp1nel  12990  fzodisj  13070  elfznelfzob  13142  ccatsymb  13931  swrdnd  14011  cshwcsh2id  14185  sqrlem7  14603  sqrtlt  14616  lo1bdd2  14876  isercoll  15019  fprodntriv  15291  fzm1ndvds  15667  fzo0dvdseq  15668  bitsfzolem  15776  bitsfzo  15777  sadcaddlem  15799  smuval2  15824  bezoutlem3  15882  2mulprm  16030  isprm5  16044  odzdvds  16125  prm23ge5  16145  pc2dvds  16208  pockthg  16235  prmreclem1  16245  prmreclem5  16249  1arith  16256  4sqlem11  16284  vdwlem6  16315  vdwlem11  16320  ramlb  16348  oddvds  18670  gexdvds  18704  sylow1lem3  18720  zringlpirlem3  20182  coe1tmmul2  20908  iccntr  23429  icccmplem2  23431  reconnlem2  23435  evth  23567  lebnumlem3  23571  nmoleub2lem3  23723  minveclem3b  24035  minveclem4  24039  pmltpclem2  24056  ovolgelb  24087  ovolicc2lem2  24125  ovolicc2lem4  24127  mbfposr  24259  itg2const2  24348  itg2cnlem2  24369  itg2cn  24370  plyco0  24792  coeeulem  24824  dgradd2  24868  cxplt2  25292  fsumharmonic  25600  dmlogdmgm  25612  lgamgulmlem1  25617  lgamucov  25626  ftalem3  25663  ftalem5  25665  ftalem7  25667  ppiprm  25739  chtprm  25741  chpub  25807  perfectlem2  25817  bposlem1  25871  lgsdilem2  25920  lgsqrlem2  25934  lgsquadlem2  25968  2sqblem  26018  2sqmod  26023  2sqnn0  26025  pntpbnd1  26173  pntlem3  26196  nbusgrvtxm1  27172  crctcshwlkn0lem3  27601  frgrreggt1  28181  minvecolem4  28666  minvecolem5  28667  nndiffz1  30538  psgnfzto1stlem  30795  lmdvg  31304  eulerpartlems  31726  ballotlemfc0  31858  ballotlemfcc  31859  ballotlemrv2  31887  signsply0  31929  reprinfz1  32001  lpadmax  32061  lpadright  32063  0nn0m1nnn0  32459  erdszelem8  32553  bccolsum  33079  unbdqndv2lem1  33956  unbdqndv2lem2  33957  poimirlem2  35052  poimirlem3  35053  poimirlem6  35056  poimirlem7  35057  poimirlem8  35058  poimirlem16  35066  poimirlem17  35067  poimirlem19  35069  poimirlem20  35070  poimirlem21  35071  poimirlem22  35072  poimirlem23  35073  poimirlem26  35076  poimirlem31  35081  poimir  35083  mblfinlem2  35088  itg2addnclem  35101  itg2addnclem2  35102  itg2addnclem3  35103  iblabsnclem  35113  ftc1anclem5  35127  areacirclem4  35141  areacirclem5  35142  areacirc  35143  cntotbnd  35227  metakunt29  39369  metakunt30  39370  elpell1qr2  39800  pellfundglb  39813  pellfund14gap  39815  congabseq  39902  jm2.19  39921  jm2.26lem3  39929  dgraa0p  40080  dvgrat  41003  uzwo4  41674  divlt0gt0d  41904  supxrgere  41952  uzublem  42054  nleltd  42078  supminfxr  42090  xrpnf  42112  sqrlearg  42177  lptre2pt  42269  limsupubuzlem  42341  climxrrelem  42378  climxlim2lem  42474  icccncfext  42516  ioodvbdlimc1lem2  42561  ioodvbdlimc2lem  42563  volioore  42619  voliooico  42621  voliccico  42628  stoweidlem26  42655  stoweidlem34  42663  stoweidlem59  42688  stirlinglem5  42707  dirkercncflem1  42732  fourierdlem10  42746  fourierdlem19  42755  fourierdlem25  42761  fourierdlem35  42771  fourierdlem40  42776  fourierdlem42  42778  fourierdlem64  42799  fourierdlem65  42800  fourierdlem74  42809  fourierdlem75  42810  fourierdlem78  42813  fourierdlem79  42814  fourierdlem104  42839  fourierswlem  42859  fouriersw  42860  elaa2lem  42862  etransclem32  42895  etransclem41  42904  hsphoidmvle2  43211  hoidmv1lelem1  43217  hoidmv1lelem2  43218  hoidmv1lelem3  43219  hoidmvlelem2  43222  hoidmvlelem4  43224  hoidmvlelem5  43225  hoiqssbllem3  43250  hspmbllem1  43252  hspmbllem2  43253  vonicc  43311  pimdecfgtioo  43339  pimincfltioo  43340  fmtno4prmfac  44076  requad01  44126  requad1  44127  perfectALTVlem2  44227  itsclc0yqsol  45165  aacllem  45316
  Copyright terms: Public domain W3C validator