![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ltnle | Structured version Visualization version GIF version |
Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.) |
Ref | Expression |
---|---|
ltnle | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lenlt 11342 | . . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) | |
2 | 1 | ancoms 457 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) |
3 | 2 | con2bid 353 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∈ wcel 2099 class class class wbr 5153 ℝcr 11157 < clt 11298 ≤ cle 11299 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-sep 5304 ax-nul 5311 ax-pr 5433 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-br 5154 df-opab 5216 df-xp 5688 df-cnv 5690 df-xr 11302 df-le 11304 |
This theorem is referenced by: letric 11364 ltnled 11411 leaddsub 11740 mulge0b 12136 nnnle0 12297 nn0n0n1ge2b 12592 znnnlt1 12641 uzwo 12947 qsqueeze 13234 difreicc 13515 fzp1disj 13614 fzneuz 13636 fznuz 13637 uznfz 13638 difelfznle 13669 nelfzo 13691 ssfzoulel 13780 elfzonelfzo 13789 modfzo0difsn 13963 ssnn0fi 14005 discr1 14256 bcval5 14335 swrdnd 14662 swrdnnn0nd 14664 swrdnd0 14665 swrdsbslen 14672 swrdspsleq 14673 pfxnd0 14696 pfxccat3 14742 swrdccat 14743 pfxccat3a 14746 repswswrd 14792 cnpart 15245 absmax 15334 rlimrege0 15581 rpnnen2lem12 16227 alzdvds 16322 algcvgblem 16578 prmndvdsfaclt 16727 pcprendvds 16842 pcdvdsb 16871 pcmpt 16894 prmunb 16916 prmreclem2 16919 prmgaplem5 17057 prmgaplem6 17058 prmlem1 17110 prmlem2 17122 lt6abl 19893 metdseq0 24861 xrhmeo 24962 ovolicc2lem3 25539 itg2seq 25763 dvne0 26035 coeeulem 26251 radcnvlt1 26447 argimgt0 26639 cxple2 26724 ressatans 26962 eldmgm 27050 basellem2 27110 issqf 27164 bpos1 27312 bposlem3 27315 bposlem6 27318 2sqreulem1 27475 2sqreunnlem1 27478 pntpbnd2 27616 ostth2lem4 27665 crctcshwlkn0 29755 crctcsh 29758 eucrctshift 30176 ltflcei 37309 poimirlem4 37325 poimirlem13 37334 poimirlem14 37335 poimirlem15 37336 poimirlem31 37352 mblfinlem1 37358 mbfposadd 37368 itgaddnclem2 37380 ftc1anclem1 37394 ftc1anclem5 37398 dvasin 37405 reabsifnpos 43300 reabsifnneg 43302 icccncfext 45508 stoweidlem14 45635 stoweidlem34 45655 ltnltne 46912 nnsum4primeseven 47372 nnsum4primesevenALTV 47373 ply1mulgsumlem2 47770 |
Copyright terms: Public domain | W3C validator |