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

Theorem nltled 10784
Description: 'Not less than ' implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
ltd.1 (𝜑𝐴 ∈ ℝ)
ltd.2 (𝜑𝐵 ∈ ℝ)
nltled.1 (𝜑 → ¬ 𝐵 < 𝐴)
Assertion
Ref Expression
nltled (𝜑𝐴𝐵)

Proof of Theorem nltled
StepHypRef Expression
1 nltled.1 . 2 (𝜑 → ¬ 𝐵 < 𝐴)
2 ltd.1 . . 3 (𝜑𝐴 ∈ ℝ)
3 ltd.2 . . 3 (𝜑𝐵 ∈ ℝ)
42, 3lenltd 10780 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
51, 4mpbird 258 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2107   class class class wbr 5063  cr 10530   < clt 10669  cle 10670
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-br 5064  df-opab 5126  df-xp 5560  df-cnv 5562  df-xr 10673  df-le 10675
This theorem is referenced by:  dedekind  10797  suprub  11596  infrelb  11620  suprzub  12333  prodge0rd  12491  seqf1olem1  13404  bitsfzolem  15778  bitsmod  15780  reconnlem2  23369  ioombl1lem4  24096  dgrub  24758  dgrlb  24760  1smat1  30974  imo72b2  40410  dvbdfbdioolem2  42098  stoweidlem14  42184  fourierdlem10  42287  fourierdlem12  42289  fourierdlem20  42297  fourierdlem24  42301  fourierdlem50  42326  fourierdlem54  42330  fourierdlem63  42339  fourierdlem65  42341  fourierdlem75  42351  fourierdlem79  42355  fouriersw  42401  etransclem3  42407  etransclem7  42411  etransclem10  42414  etransclem15  42419  etransclem20  42424  etransclem21  42425  etransclem22  42426  etransclem24  42428  etransclem25  42429  etransclem27  42431  etransclem32  42436
  Copyright terms: Public domain W3C validator