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

Theorem nltled 11312
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 11308 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
51, 4mpbird 257 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2107   class class class wbr 5110  cr 11057   < clt 11196  cle 11197
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-xp 5644  df-cnv 5646  df-xr 11200  df-le 11202
This theorem is referenced by:  dedekind  11325  suprub  12123  infrelb  12147  suprzub  12871  prodge0rd  13029  seqf1olem1  13954  bitsfzolem  16321  bitsmod  16323  reconnlem2  24206  ioombl1lem4  24941  dgrub  25611  dgrlb  25613  1smat1  32425  metakunt28  40633  metakunt30  40635  imo72b2  42519  dvbdfbdioolem2  44244  stoweidlem14  44329  fourierdlem10  44432  fourierdlem12  44434  fourierdlem20  44442  fourierdlem24  44446  fourierdlem50  44471  fourierdlem54  44475  fourierdlem63  44484  fourierdlem65  44486  fourierdlem75  44496  fourierdlem79  44500  fouriersw  44546  etransclem3  44552  etransclem7  44556  etransclem10  44559  etransclem15  44564  etransclem20  44569  etransclem21  44570  etransclem22  44571  etransclem24  44573  etransclem25  44574  etransclem27  44576  etransclem32  44581
  Copyright terms: Public domain W3C validator