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 10876 | . 2 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
5 | 1, 4 | mpbird 260 | 1 ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2114 class class class wbr 5040 ℝcr 10626 < clt 10765 ≤ cle 10766 |
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 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 ax-sep 5177 ax-nul 5184 ax-pr 5306 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-ral 3059 df-rex 3060 df-v 3402 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4222 df-if 4425 df-sn 4527 df-pr 4529 df-op 4533 df-br 5041 df-opab 5103 df-xp 5541 df-cnv 5543 df-xr 10769 df-le 10771 |
This theorem is referenced by: dedekind 10893 suprub 11691 infrelb 11715 suprzub 12433 prodge0rd 12591 seqf1olem1 13513 bitsfzolem 15889 bitsmod 15891 reconnlem2 23591 ioombl1lem4 24325 dgrub 24995 dgrlb 24997 1smat1 31338 metakunt28 39783 metakunt30 39785 imo72b2 41370 dvbdfbdioolem2 43052 stoweidlem14 43137 fourierdlem10 43240 fourierdlem12 43242 fourierdlem20 43250 fourierdlem24 43254 fourierdlem50 43279 fourierdlem54 43283 fourierdlem63 43292 fourierdlem65 43294 fourierdlem75 43304 fourierdlem79 43308 fouriersw 43354 etransclem3 43360 etransclem7 43364 etransclem10 43367 etransclem15 43372 etransclem20 43377 etransclem21 43378 etransclem22 43379 etransclem24 43381 etransclem25 43382 etransclem27 43384 etransclem32 43389 |
Copyright terms: Public domain | W3C validator |