Theorem nltled 11295

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

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

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 2709  ax-sep 5243  ax-pr 5379

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 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-xr 11182  df-le 11184

This theorem is referenced by:  dedekind  11308  suprub  12115  infrelb  12139  suprzub  12864  prodge0rd  13026  seqf1olem1  13976  bitsfzolem  16373  bitsmod  16375  reconnlem2  24784  ioombl1lem4  25530  dgrub  26207  dgrlb  26209  suppssnn0  32895  constrsqrtcl  33956  1smat1  33981  sn-suprubd  42861  imo72b2  44525  dvbdfbdioolem2  46284  stoweidlem14  46369  fourierdlem10  46472  fourierdlem12  46474  fourierdlem20  46482  fourierdlem24  46486  fourierdlem50  46511  fourierdlem54  46515  fourierdlem63  46524  fourierdlem65  46526  fourierdlem75  46536  fourierdlem79  46540  fouriersw  46586  etransclem3  46592  etransclem7  46596  etransclem10  46599  etransclem15  46604  etransclem20  46609  etransclem21  46610  etransclem22  46611  etransclem24  46613  etransclem25  46614  etransclem27  46616  etransclem32  46621