![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nltled | Structured version Visualization version GIF version |
Description: 'Not less than ' implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
ltd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
ltd.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
nltled.1 | ⊢ (𝜑 → ¬ 𝐵 < 𝐴) |
Ref | Expression |
---|---|
nltled | ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nltled.1 | . 2 ⊢ (𝜑 → ¬ 𝐵 < 𝐴) | |
2 | ltd.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
3 | ltd.2 | . . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
4 | 2, 3 | lenltd 11405 | . 2 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
5 | 1, 4 | mpbird 257 | 1 ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2106 class class class wbr 5148 ℝcr 11152 < clt 11293 ≤ cle 11294 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pr 5438 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ral 3060 df-rex 3069 df-rab 3434 df-v 3480 df-dif 3966 df-un 3968 df-ss 3980 df-nul 4340 df-if 4532 df-sn 4632 df-pr 4634 df-op 4638 df-br 5149 df-opab 5211 df-xp 5695 df-cnv 5697 df-xr 11297 df-le 11299 |
This theorem is referenced by: dedekind 11422 suprub 12227 infrelb 12251 suprzub 12979 prodge0rd 13140 seqf1olem1 14079 bitsfzolem 16468 bitsmod 16470 reconnlem2 24863 ioombl1lem4 25610 dgrub 26288 dgrlb 26290 suppssnn0 32815 1smat1 33765 metakunt28 42214 metakunt30 42216 sn-suprubd 42481 imo72b2 44162 dvbdfbdioolem2 45885 stoweidlem14 45970 fourierdlem10 46073 fourierdlem12 46075 fourierdlem20 46083 fourierdlem24 46087 fourierdlem50 46112 fourierdlem54 46116 fourierdlem63 46125 fourierdlem65 46127 fourierdlem75 46137 fourierdlem79 46141 fouriersw 46187 etransclem3 46193 etransclem7 46197 etransclem10 46200 etransclem15 46205 etransclem20 46210 etransclem21 46211 etransclem22 46212 etransclem24 46214 etransclem25 46215 etransclem27 46217 etransclem32 46222 |
Copyright terms: Public domain | W3C validator |