Theorem nltled 11296

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   class class class wbr 5085  ℝcr 11037   < clt 11179   ≤ cle 11180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-cnv 5639  df-xr 11183  df-le 11185

This theorem is referenced by:  dedekind  11309  suprub  12117  infrelb  12141  suprzub  12889  prodge0rd  13051  seqf1olem1  14003  bitsfzolem  16403  bitsmod  16405  reconnlem2  24793  ioombl1lem4  25528  dgrub  26199  dgrlb  26201  suppssnn0  32878  constrsqrtcl  33923  1smat1  33948  sn-suprubd  42939  imo72b2  44599  dvbdfbdioolem2  46357  stoweidlem14  46442  fourierdlem10  46545  fourierdlem12  46547  fourierdlem20  46555  fourierdlem24  46559  fourierdlem50  46584  fourierdlem54  46588  fourierdlem63  46597  fourierdlem65  46599  fourierdlem75  46609  fourierdlem79  46613  fouriersw  46659  etransclem3  46665  etransclem7  46669  etransclem10  46672  etransclem15  46677  etransclem20  46682  etransclem21  46683  etransclem22  46684  etransclem24  46686  etransclem25  46687  etransclem27  46689  etransclem32  46694