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 11121 | . 2 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
5 | 1, 4 | mpbird 256 | 1 ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2106 class class class wbr 5074 ℝcr 10870 < clt 11009 ≤ cle 11010 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-br 5075 df-opab 5137 df-xp 5595 df-cnv 5597 df-xr 11013 df-le 11015 |
This theorem is referenced by: dedekind 11138 suprub 11936 infrelb 11960 suprzub 12679 prodge0rd 12837 seqf1olem1 13762 bitsfzolem 16141 bitsmod 16143 reconnlem2 23990 ioombl1lem4 24725 dgrub 25395 dgrlb 25397 1smat1 31754 metakunt28 40152 metakunt30 40154 imo72b2 41783 dvbdfbdioolem2 43470 stoweidlem14 43555 fourierdlem10 43658 fourierdlem12 43660 fourierdlem20 43668 fourierdlem24 43672 fourierdlem50 43697 fourierdlem54 43701 fourierdlem63 43710 fourierdlem65 43712 fourierdlem75 43722 fourierdlem79 43726 fouriersw 43772 etransclem3 43778 etransclem7 43782 etransclem10 43785 etransclem15 43790 etransclem20 43795 etransclem21 43796 etransclem22 43797 etransclem24 43799 etransclem25 43800 etransclem27 43802 etransclem32 43807 |
Copyright terms: Public domain | W3C validator |