Theorem nltled 11411

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

Step	Hyp	Ref	Expression
1		nltled.1	. 2 ⊢ (𝜑 → ¬ 𝐵 < 𝐴)
2		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4	2, 3	lenltd 11407	. 2 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
5	1, 4	mpbird 257	1 ⊢ (𝜑 → 𝐴 ≤ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   class class class wbr 5143  ℝcr 11154   < clt 11295   ≤ cle 11296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-xr 11299  df-le 11301

This theorem is referenced by:  dedekind  11424  suprub  12229  infrelb  12253  suprzub  12981  prodge0rd  13142  seqf1olem1  14082  bitsfzolem  16471  bitsmod  16473  reconnlem2  24849  ioombl1lem4  25596  dgrub  26273  dgrlb  26275  suppssnn0  32809  1smat1  33803  metakunt28  42233  metakunt30  42235  sn-suprubd  42504  imo72b2  44185  dvbdfbdioolem2  45944  stoweidlem14  46029  fourierdlem10  46132  fourierdlem12  46134  fourierdlem20  46142  fourierdlem24  46146  fourierdlem50  46171  fourierdlem54  46175  fourierdlem63  46184  fourierdlem65  46186  fourierdlem75  46196  fourierdlem79  46200  fouriersw  46246  etransclem3  46252  etransclem7  46256  etransclem10  46259  etransclem15  46264  etransclem20  46269  etransclem21  46270  etransclem22  46271  etransclem24  46273  etransclem25  46274  etransclem27  46276  etransclem32  46281