Theorem nltled 11294

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2119   class class class wbr 5079  ℝcr 11035   < clt 11177   ≤ cle 11178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-xp 5631  df-cnv 5633  df-xr 11181  df-le 11183

This theorem is referenced by:  dedekind  11307  suprub  12115  infrelb  12139  suprzub  12887  prodge0rd  13049  seqf1olem1  14001  bitsfzolem  16401  bitsmod  16403  reconnlem2  24818  ioombl1lem4  25553  dgrub  26224  dgrlb  26226  suppssnn0  32904  constrsqrtcl  33970  1smat1  33995  sn-suprubd  42991  imo72b2  44623  dvbdfbdioolem2  46379  stoweidlem14  46464  fourierdlem10  46567  fourierdlem12  46569  fourierdlem20  46577  fourierdlem24  46581  fourierdlem50  46606  fourierdlem54  46610  fourierdlem63  46619  fourierdlem65  46621  fourierdlem75  46631  fourierdlem79  46635  fouriersw  46681  etransclem3  46687  etransclem7  46691  etransclem10  46694  etransclem15  46699  etransclem20  46704  etransclem21  46705  etransclem22  46706  etransclem24  46708  etransclem25  46709  etransclem27  46711  etransclem32  46716