Theorem nltled 11331

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 11327	. 2 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
5	1, 4	mpbird 257	1 ⊢ (𝜑 → 𝐴 ≤ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074   < clt 11215   ≤ cle 11216

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-xr 11219  df-le 11221

This theorem is referenced by:  dedekind  11344  suprub  12151  infrelb  12175  suprzub  12905  prodge0rd  13067  seqf1olem1  14013  bitsfzolem  16411  bitsmod  16413  reconnlem2  24723  ioombl1lem4  25469  dgrub  26146  dgrlb  26148  suppssnn0  32737  constrsqrtcl  33776  1smat1  33801  sn-suprubd  42489  imo72b2  44168  dvbdfbdioolem2  45934  stoweidlem14  46019  fourierdlem10  46122  fourierdlem12  46124  fourierdlem20  46132  fourierdlem24  46136  fourierdlem50  46161  fourierdlem54  46165  fourierdlem63  46174  fourierdlem65  46176  fourierdlem75  46186  fourierdlem79  46190  fouriersw  46236  etransclem3  46242  etransclem7  46246  etransclem10  46249  etransclem15  46254  etransclem20  46259  etransclem21  46260  etransclem22  46261  etransclem24  46263  etransclem25  46264  etransclem27  46266  etransclem32  46271