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

Theorem ltnled 10479
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 10412 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
41, 2, 3syl2anc 575 1 (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wcel 2157   class class class wbr 4855  cr 10230   < clt 10369  cle 10370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pr 5109
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-br 4856  df-opab 4918  df-xp 5330  df-cnv 5332  df-xr 10373  df-le 10375
This theorem is referenced by:  ltsub1  10819  ltsub2  10820  0mnnnnn0  11611  mul2lt0bi  12170  fzp1nel  12667  fzodisj  12746  elfznelfzob  12818  swrdnd  13676  cshwcsh2id  13818  sqrlem7  14232  sqrtlt  14245  lo1bdd2  14498  isercoll  14641  fprodntriv  14913  fzm1ndvds  15287  fzo0dvdseq  15288  bitsfzolem  15395  bitsfzo  15396  sadcaddlem  15418  smuval2  15443  bezoutlem3  15497  isprm5  15656  odzdvds  15737  prm23ge5  15757  pc2dvds  15820  pockthg  15847  prmreclem1  15857  prmreclem5  15861  1arith  15868  4sqlem11  15896  vdwlem6  15927  vdwlem11  15932  ramlb  15960  oddvds  18187  gexdvds  18220  sylow1lem3  18236  coe1tmmul2  19874  zringlpirlem3  20062  iccntr  22858  icccmplem2  22860  reconnlem2  22864  evth  22992  lebnumlem3  22996  nmoleub2lem3  23148  minveclem3b  23434  minveclem4  23438  pmltpclem2  23453  ovolgelb  23484  ovolicc2lem2  23522  ovolicc2lem4  23524  mbfposr  23656  itg2const2  23745  itg2cnlem2  23766  itg2cn  23767  plyco0  24185  coeeulem  24217  dgradd2  24261  pilem3OLD  24445  cxplt2  24681  fsumharmonic  24975  dmlogdmgm  24987  lgamgulmlem1  24992  lgamucov  25001  ftalem3  25038  ftalem5  25040  ftalem7  25042  ppiprm  25114  chtprm  25116  chpub  25182  perfectlem2  25192  bposlem1  25246  lgsdilem2  25295  lgsqrlem2  25309  lgsquadlem2  25343  2sqblem  25393  pntpbnd1  25512  pntlem3  25535  nbusgrvtxm1  26520  crctcshwlkn0lem3  26956  frgrreggt1  27604  minvecolem4  28087  minvecolem5  28088  nndiffz1  29898  2sqmod  29996  psgnfzto1stlem  30198  lmdvg  30347  eulerpartlems  30770  ballotlemfc0  30902  ballotlemfcc  30903  ballotlemrv2  30931  signsply0  30976  reprinfz1  31048  erdszelem8  31525  bccolsum  31969  unbdqndv2lem1  32839  unbdqndv2lem2  32840  poimirlem2  33743  poimirlem3  33744  poimirlem6  33747  poimirlem7  33748  poimirlem8  33749  poimirlem16  33757  poimirlem17  33758  poimirlem19  33760  poimirlem20  33761  poimirlem21  33762  poimirlem22  33763  poimirlem23  33764  poimirlem26  33767  poimirlem31  33772  poimir  33774  mblfinlem2  33779  itg2addnclem  33792  itg2addnclem2  33793  itg2addnclem3  33794  iblabsnclem  33804  ftc1anclem5  33820  areacirclem4  33834  areacirclem5  33835  areacirc  33836  cntotbnd  33925  elpell1qr2  37956  pellfundglb  37969  pellfund14gap  37971  congabseq  38060  jm2.19  38079  jm2.26lem3  38087  dgraa0p  38238  dvgrat  39029  uzwo4  39732  divlt0gt0d  39998  supxrgere  40047  uzublem  40154  nleltd  40178  supminfxr  40191  xrpnf  40213  sqrlearg  40278  lptre2pt  40370  limsupubuzlem  40442  climxrrelem  40479  climxlim2lem  40569  icccncfext  40598  ioodvbdlimc1lem2  40645  ioodvbdlimc2lem  40647  volioore  40704  voliooico  40706  voliccico  40713  stoweidlem26  40740  stoweidlem34  40748  stoweidlem59  40773  stirlinglem5  40792  dirkercncflem1  40817  fourierdlem10  40831  fourierdlem19  40840  fourierdlem25  40846  fourierdlem35  40856  fourierdlem40  40861  fourierdlem42  40863  fourierdlem64  40884  fourierdlem65  40885  fourierdlem74  40894  fourierdlem75  40895  fourierdlem78  40898  fourierdlem79  40899  fourierdlem104  40924  fourierswlem  40944  fouriersw  40945  elaa2lem  40947  etransclem32  40980  etransclem41  40989  hsphoidmvle2  41299  hoidmv1lelem1  41305  hoidmv1lelem2  41306  hoidmv1lelem3  41307  hoidmvlelem2  41310  hoidmvlelem4  41312  hoidmvlelem5  41313  hoiqssbllem3  41338  hspmbllem1  41340  hspmbllem2  41341  vonicc  41399  pimdecfgtioo  41427  pimincfltioo  41428  fmtno4prmfac  42077  perfectALTVlem2  42224  aacllem  43136
  Copyright terms: Public domain W3C validator