![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ltnlei | Structured version Visualization version GIF version |
Description: 'Less than' in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.) |
Ref | Expression |
---|---|
lt.1 | ⊢ 𝐴 ∈ ℝ |
lt.2 | ⊢ 𝐵 ∈ ℝ |
Ref | Expression |
---|---|
ltnlei | ⊢ (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lt.2 | . . 3 ⊢ 𝐵 ∈ ℝ | |
2 | lt.1 | . . 3 ⊢ 𝐴 ∈ ℝ | |
3 | 1, 2 | lenlti 11366 | . 2 ⊢ (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵) |
4 | 3 | con2bii 356 | 1 ⊢ (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∈ wcel 2098 class class class wbr 5149 ℝcr 11139 < clt 11280 ≤ cle 11281 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5150 df-opab 5212 df-xp 5684 df-cnv 5686 df-xr 11284 df-le 11286 |
This theorem is referenced by: letrii 11371 nn0ge2m1nn 12574 0nelfz1 13555 fzpreddisj 13585 hashnn0n0nn 14386 hashge2el2dif 14477 divalglem5 16377 divalglem6 16378 sadcadd 16436 htpycc 24950 pco1 24986 pcohtpylem 24990 pcopt 24993 pcopt2 24994 pcoass 24995 pcorevlem 24997 vitalilem5 25585 vieta1lem2 26291 ppiltx 27154 ppiublem1 27180 chtub 27190 axlowdimlem16 28840 axlowdim 28844 lfgrnloop 29010 lfuhgr1v0e 29139 lfgrwlkprop 29573 ballotlem2 34239 subfacp1lem1 34920 subfacp1lem5 34925 bcneg1 35461 poimirlem9 37233 poimirlem16 37240 poimirlem17 37241 poimirlem19 37243 poimirlem20 37244 poimirlem22 37246 fdc 37349 pellexlem6 42396 jm2.23 42559 |
Copyright terms: Public domain | W3C validator |