![]() |
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 10518 | . . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) | |
2 | 1 | ancoms 451 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) |
3 | 2 | con2bid 347 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 387 ∈ wcel 2051 class class class wbr 4926 ℝcr 10333 < clt 10473 ≤ cle 10474 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2745 ax-sep 5057 ax-nul 5064 ax-pr 5183 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-ral 3088 df-rex 3089 df-rab 3092 df-v 3412 df-dif 3827 df-un 3829 df-in 3831 df-ss 3838 df-nul 4174 df-if 4346 df-sn 4437 df-pr 4439 df-op 4443 df-br 4927 df-opab 4989 df-xp 5410 df-cnv 5412 df-xr 10477 df-le 10479 |
This theorem is referenced by: letric 10539 ltnled 10586 leaddsub 10916 mulge0b 11310 nnnle0 11472 nn0n0n1ge2b 11774 znnnlt1 11821 uzwo 12124 qsqueeze 12410 difreicc 12685 fzp1disj 12781 fzneuz 12803 fznuz 12804 uznfz 12805 difelfznle 12836 nelfzo 12858 ssfzoulel 12945 elfzonelfzo 12953 modfzo0difsn 13125 ssnn0fi 13167 discr1 13414 bcval5 13492 ccatsymb 13744 swrdnd 13821 swrdnnn0nd 13823 swrdnd0 13824 swrdsbslen 13840 swrdspsleq 13841 pfxnd0 13869 pfxccat3 13935 swrdccat3OLD 13936 swrdccat 13937 pfxccat3a 13941 repswswrd 14002 cnpart 14459 absmax 14549 rlimrege0 14796 rpnnen2lem12 15437 alzdvds 15529 algcvgblem 15776 prmndvdsfaclt 15922 pcprendvds 16032 pcdvdsb 16060 pcmpt 16083 prmunb 16105 prmreclem2 16108 prmgaplem5 16246 prmgaplem6 16247 prmlem1 16296 prmlem2 16308 lt6abl 18782 metdseq0 23181 xrhmeo 23269 ovolicc2lem3 23839 itg2seq 24062 dvne0 24327 coeeulem 24533 radcnvlt1 24725 argimgt0 24912 cxple2 24997 ressatans 25229 eldmgm 25317 basellem2 25377 issqf 25431 bpos1 25577 bposlem3 25580 bposlem6 25583 2sqreulem1 25740 2sqreunnlem1 25743 pntpbnd2 25881 ostth2lem4 25930 crctcshwlkn0 27323 crctcsh 27326 eucrctshift 27789 ltflcei 34354 poimirlem4 34370 poimirlem13 34379 poimirlem14 34380 poimirlem15 34381 poimirlem31 34397 mblfinlem1 34403 mbfposadd 34413 itgaddnclem2 34425 ftc1anclem1 34441 ftc1anclem5 34445 dvasin 34452 icccncfext 41630 stoweidlem14 41760 stoweidlem34 41780 ltnltne 42935 nnsum4primeseven 43363 nnsum4primesevenALTV 43364 ply1mulgsumlem2 43838 |
Copyright terms: Public domain | W3C validator |