![]() |
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 10320 | . 2 ⊢ (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵) |
4 | 3 | con2bii 346 | 1 ⊢ (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 ∈ wcel 2127 class class class wbr 4792 ℝcr 10098 < clt 10237 ≤ cle 10238 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 ax-sep 4921 ax-nul 4929 ax-pr 5043 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-eu 2599 df-mo 2600 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-ral 3043 df-rex 3044 df-rab 3047 df-v 3330 df-dif 3706 df-un 3708 df-in 3710 df-ss 3717 df-nul 4047 df-if 4219 df-sn 4310 df-pr 4312 df-op 4316 df-br 4793 df-opab 4853 df-xp 5260 df-cnv 5262 df-xr 10241 df-le 10243 |
This theorem is referenced by: letrii 10325 nn0ge2m1nn 11523 zgt1rpn0n1 12035 0nelfz1 12524 fzpreddisj 12554 hashnn0n0nn 13343 hashge2el2dif 13425 n2dvds1 15277 divalglem5 15293 divalglem6 15294 sadcadd 15353 strlemor1OLD 16142 htpycc 22951 pco1 22986 pcohtpylem 22990 pcopt 22993 pcopt2 22994 pcoass 22995 pcorevlem 22997 vitalilem5 23551 vieta1lem2 24236 ppiltx 25073 ppiublem1 25097 chtub 25107 axlowdimlem16 26007 axlowdim 26011 lfgrnloop 26190 lfuhgr1v0e 26316 lfgrwlkprop 26765 ballotlem2 30830 subfacp1lem1 31439 subfacp1lem5 31444 bcneg1 31900 poimirlem9 33700 poimirlem16 33707 poimirlem17 33708 poimirlem19 33710 poimirlem20 33711 poimirlem22 33713 fdc 33823 pellexlem6 37869 jm2.23 38034 |
Copyright terms: Public domain | W3C validator |