| 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 11339 | . . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) | |
| 2 | 1 | ancoms 458 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) |
| 3 | 2 | con2bid 354 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∈ wcel 2108 class class class wbr 5143 ℝcr 11154 < clt 11295 ≤ cle 11296 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-br 5144 df-opab 5206 df-xp 5691 df-cnv 5693 df-xr 11299 df-le 11301 |
| This theorem is referenced by: letric 11361 ltnled 11408 leaddsub 11739 mulge0b 12138 nnnle0 12299 nn0n0n1ge2b 12595 znnnlt1 12644 uzwo 12953 qsqueeze 13243 difreicc 13524 fzp1disj 13623 fzneuz 13648 fznuz 13649 uznfz 13650 difelfznle 13682 nelfzo 13704 ssfzoulel 13799 elfzonelfzo 13808 modfzo0difsn 13984 ssnn0fi 14026 discr1 14278 bcval5 14357 swrdnd 14692 swrdnnn0nd 14694 swrdnd0 14695 swrdsbslen 14702 swrdspsleq 14703 pfxnd0 14726 pfxccat3 14772 swrdccat 14773 pfxccat3a 14776 repswswrd 14822 cnpart 15279 absmax 15368 rlimrege0 15615 rpnnen2lem12 16261 alzdvds 16357 algcvgblem 16614 prmndvdsfaclt 16762 pcprendvds 16878 pcdvdsb 16907 pcmpt 16930 prmunb 16952 prmreclem2 16955 prmgaplem5 17093 prmgaplem6 17094 prmlem1 17145 prmlem2 17157 lt6abl 19913 metdseq0 24876 xrhmeo 24977 ovolicc2lem3 25554 itg2seq 25777 dvne0 26050 coeeulem 26263 radcnvlt1 26461 argimgt0 26654 cxple2 26739 ressatans 26977 eldmgm 27065 basellem2 27125 issqf 27179 bpos1 27327 bposlem3 27330 bposlem6 27333 2sqreulem1 27490 2sqreunnlem1 27493 pntpbnd2 27631 ostth2lem4 27680 crctcshwlkn0 29841 crctcsh 29844 eucrctshift 30262 ltflcei 37615 poimirlem4 37631 poimirlem13 37640 poimirlem14 37641 poimirlem15 37642 poimirlem31 37658 mblfinlem1 37664 mbfposadd 37674 itgaddnclem2 37686 ftc1anclem1 37700 ftc1anclem5 37704 dvasin 37711 reabsifnpos 43646 reabsifnneg 43648 icccncfext 45902 stoweidlem14 46029 stoweidlem34 46049 ltnltne 47311 nnsum4primeseven 47787 nnsum4primesevenALTV 47788 ply1mulgsumlem2 48304 |
| Copyright terms: Public domain | W3C validator |