Theorem nltled 11440

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   class class class wbr 5166  ℝcr 11183   < clt 11324   ≤ cle 11325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-cnv 5708  df-xr 11328  df-le 11330

This theorem is referenced by:  dedekind  11453  suprub  12256  infrelb  12280  suprzub  13004  prodge0rd  13164  seqf1olem1  14092  bitsfzolem  16480  bitsmod  16482  reconnlem2  24868  ioombl1lem4  25615  dgrub  26293  dgrlb  26295  suppssnn0  32812  1smat1  33750  metakunt28  42189  metakunt30  42191  sn-suprubd  42450  imo72b2  44134  dvbdfbdioolem2  45850  stoweidlem14  45935  fourierdlem10  46038  fourierdlem12  46040  fourierdlem20  46048  fourierdlem24  46052  fourierdlem50  46077  fourierdlem54  46081  fourierdlem63  46090  fourierdlem65  46092  fourierdlem75  46102  fourierdlem79  46106  fouriersw  46152  etransclem3  46158  etransclem7  46162  etransclem10  46165  etransclem15  46170  etransclem20  46175  etransclem21  46176  etransclem22  46177  etransclem24  46179  etransclem25  46180  etransclem27  46182  etransclem32  46187