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

Theorem nltled 11125
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 11121 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
51, 4mpbird 256 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2106   class class class wbr 5074  cr 10870   < clt 11009  cle 11010
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-cnv 5597  df-xr 11013  df-le 11015
This theorem is referenced by:  dedekind  11138  suprub  11936  infrelb  11960  suprzub  12679  prodge0rd  12837  seqf1olem1  13762  bitsfzolem  16141  bitsmod  16143  reconnlem2  23990  ioombl1lem4  24725  dgrub  25395  dgrlb  25397  1smat1  31754  metakunt28  40152  metakunt30  40154  imo72b2  41783  dvbdfbdioolem2  43470  stoweidlem14  43555  fourierdlem10  43658  fourierdlem12  43660  fourierdlem20  43668  fourierdlem24  43672  fourierdlem50  43697  fourierdlem54  43701  fourierdlem63  43710  fourierdlem65  43712  fourierdlem75  43722  fourierdlem79  43726  fouriersw  43772  etransclem3  43778  etransclem7  43782  etransclem10  43785  etransclem15  43790  etransclem20  43795  etransclem21  43796  etransclem22  43797  etransclem24  43799  etransclem25  43800  etransclem27  43802  etransclem32  43807
  Copyright terms: Public domain W3C validator