Theorem nltled 11441

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2145   class class class wbr 5103  ℝcr 11180   < clt 11324   ≤ cle 11325

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-xr 11328  df-le 11330

This theorem is used by:  dedekind  11454  suprub  12259  infrelb  12283  suprzub  13047  prodge0rd  13210  seqf1olem1  14164  bitsfzolem  16584  bitsmod  16586  reconnlem2  25127  ioombl1lem4  25862  dgrub  26533  dgrlb  26535  suppssnn0  33379  constrsqrtcl  34393  1smat1  34418  sn-suprubd  43526  imo72b2  45131  dvbdfbdioolem2  46883  stoweidlem14  46968  fourierdlem10  47071  fourierdlem12  47073  fourierdlem20  47081  fourierdlem24  47085  fourierdlem50  47110  fourierdlem54  47114  fourierdlem63  47123  fourierdlem65  47125  fourierdlem75  47135  fourierdlem79  47139  fouriersw  47185  etransclem3  47191  etransclem7  47195  etransclem10  47198  etransclem15  47203  etransclem20  47208  etransclem21  47209  etransclem22  47210  etransclem24  47212  etransclem25  47213  etransclem27  47215  etransclem32  47220