Theorem nltled 11283

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113   class class class wbr 5098  ℝcr 11025   < clt 11166   ≤ cle 11167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-xr 11170  df-le 11172

This theorem is referenced by:  dedekind  11296  suprub  12103  infrelb  12127  suprzub  12852  prodge0rd  13014  seqf1olem1  13964  bitsfzolem  16361  bitsmod  16363  reconnlem2  24772  ioombl1lem4  25518  dgrub  26195  dgrlb  26197  suppssnn0  32885  constrsqrtcl  33936  1smat1  33961  sn-suprubd  42749  imo72b2  44413  dvbdfbdioolem2  46173  stoweidlem14  46258  fourierdlem10  46361  fourierdlem12  46363  fourierdlem20  46371  fourierdlem24  46375  fourierdlem50  46400  fourierdlem54  46404  fourierdlem63  46413  fourierdlem65  46415  fourierdlem75  46425  fourierdlem79  46429  fouriersw  46475  etransclem3  46481  etransclem7  46485  etransclem10  46488  etransclem15  46493  etransclem20  46498  etransclem21  46499  etransclem22  46500  etransclem24  46502  etransclem25  46503  etransclem27  46505  etransclem32  46510