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

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

Proof of Theorem lenltd
StepHypRef Expression
1 ltd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 ltd.2 . 2 (𝜑𝐵 ∈ ℝ)
3 lenlt 9968 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
41, 2, 3syl2anc 691 1 (𝜑 → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wcel 1977   class class class wbr 4578  cr 9792   < clt 9931  cle 9932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4579  df-opab 4639  df-xp 5034  df-cnv 5036  df-xr 9935  df-le 9937
This theorem is referenced by:  ltnsymd  10038  nltled  10039  lensymd  10040  dedekind  10052  leadd1  10348  leord1  10407  prodge0  10722  lediv1  10740  lemuldiv  10755  lerec  10758  le2msq  10775  suprub  10836  suprleub  10839  supaddc  10840  supmul1  10842  infregelb  10857  suprfinzcl  11327  uzinfi  11603  zsupss  11612  suprzub  11614  rpnnen1lem5  11653  rpnnen1lem5OLD  11659  fzdisj  12197  uzdisj  12240  nn0disj  12282  fzouzdisj  12331  fleqceilz  12473  modsumfzodifsn  12563  addmodlteq  12565  seqf1olem1  12660  seqf1olem2  12661  leexp2  12735  hashf1  13053  seqcoll  13060  seqcoll2  13061  ccatsymb  13168  swrdccatin2  13287  rlimcld2  14106  rlimno1  14181  isercoll  14195  ruclem3  14750  bitsfzolem  14943  bitsmod  14945  sadcaddlem  14966  smupvallem  14992  pcfac  15390  4sqlem11  15446  ramcl2lem  15500  sylow1lem1  17785  fvmptnn04if  20421  chfacfisf  20426  chfacfisfcpmat  20427  recld2  22373  reconnlem2  22386  ivthlem2  22973  ivthlem3  22974  ovolicopnf  23044  ioombl1lem4  23081  ioorcl2  23091  itg1ge0a  23229  mbfi1fseqlem4  23236  itg2monolem1  23268  itg2cnlem1  23279  dvferm1lem  23496  dvferm2lem  23498  mdegmullem  23587  dgrub  23739  dgrlb  23741  dgreq0  23770  quotcan  23813  aaliou3lem9  23854  radcnvle  23923  abelthlem2  23935  logdivle  24117  cxple  24186  lgsval2lem  24777  gausslemma2dlem1a  24835  padicabv  25064  ssnnssfz  28731  smattr  28987  smatbl  28988  smatbr  28989  esumpcvgval  29261  eulerpartlems  29543  dstfrvunirn  29657  ballotlemodife  29680  erdszelem7  30227  erdszelem8  30228  unblimceq0  31462  unbdqndv2lem1  31464  poimirlem2  32375  poimirlem7  32380  poimirlem10  32383  poimirlem11  32384  areacirc  32469  rencldnfilem  36196  irrapxlem1  36198  monotoddzzfi  36319  radcnvrat  37329  reclt0d  38342  reclt0  38349  sqrlearg  38421  dvnxpaek  38626  volico  38670  sublevolico  38671  fourierdlem12  38806  fourierdlem42  38836  elaa2lem  38920  iundjiun  39147  hoidmvval0  39271  hoidmv1lelem2  39276  hoidmv1lelem3  39277  hoidmvlelem4  39282  hspdifhsp  39300  volico2  39325  ovolval2lem  39327  vonioo  39367  smfconst  39430  fzopredsuc  39741  stgoldbwt  39993  nnsum3primesle9  40005  bgoldbtbndlem1  40016  pthdlem1  40964  ssnn0ssfz  41912
  Copyright terms: Public domain W3C validator