![]() |
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 10609 | . 2 ⊢ (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵) |
4 | 3 | con2bii 359 | 1 ⊢ (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 ∈ wcel 2080 class class class wbr 4964 ℝcr 10385 < clt 10524 ≤ cle 10525 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-13 2343 ax-ext 2768 ax-sep 5097 ax-nul 5104 ax-pr 5224 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-mo 2575 df-eu 2611 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-ral 3109 df-rex 3110 df-rab 3113 df-v 3438 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-nul 4214 df-if 4384 df-sn 4475 df-pr 4477 df-op 4481 df-br 4965 df-opab 5027 df-xp 5452 df-cnv 5454 df-xr 10528 df-le 10530 |
This theorem is referenced by: letrii 10614 nn0ge2m1nn 11814 0nelfz1 12776 fzpreddisj 12806 hashnn0n0nn 13600 hashge2el2dif 13684 n2dvds1OLD 15551 divalglem5 15581 divalglem6 15582 sadcadd 15640 htpycc 23267 pco1 23302 pcohtpylem 23306 pcopt 23309 pcopt2 23310 pcoass 23311 pcorevlem 23313 vitalilem5 23896 vieta1lem2 24583 ppiltx 25436 ppiublem1 25460 chtub 25470 axlowdimlem16 26426 axlowdim 26430 lfgrnloop 26593 lfuhgr1v0e 26719 lfgrwlkprop 27151 ballotlem2 31355 subfacp1lem1 32028 subfacp1lem5 32033 bcneg1 32570 poimirlem9 34445 poimirlem16 34452 poimirlem17 34453 poimirlem19 34455 poimirlem20 34456 poimirlem22 34458 fdc 34565 pellexlem6 38929 jm2.23 39091 |
Copyright terms: Public domain | W3C validator |