Theorem nltled 11378

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2146   class class class wbr 5114  ℝcr 11117   < clt 11261   ≤ cle 11262

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

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 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672  df-cnv 5674  df-xr 11265  df-le 11267

This theorem is used by:  dedekind  11391  suprub  12194  infrelb  12218  suprzub  12981  prodge0rd  13143  seqf1olem1  14097  bitsfzolem  16517  bitsmod  16519  reconnlem2  25022  ioombl1lem4  25757  dgrub  26428  dgrlb  26430  suppssnn0  33187  constrsqrtcl  34200  1smat1  34225  sn-suprubd  43309  imo72b2  44939  dvbdfbdioolem2  46684  stoweidlem14  46769  fourierdlem10  46872  fourierdlem12  46874  fourierdlem20  46882  fourierdlem24  46886  fourierdlem50  46911  fourierdlem54  46915  fourierdlem63  46924  fourierdlem65  46926  fourierdlem75  46936  fourierdlem79  46940  fouriersw  46986  etransclem3  46992  etransclem7  46996  etransclem10  46999  etransclem15  47004  etransclem20  47009  etransclem21  47010  etransclem22  47011  etransclem24  47013  etransclem25  47014  etransclem27  47016  etransclem32  47021