Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lenlt | Structured version Visualization version GIF version |
Description: 'Less than or equal to' expressed in terms of 'less than'. (Contributed by NM, 13-May-1999.) |
Ref | Expression |
---|---|
lenlt | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexr 9964 | . 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
2 | rexr 9964 | . 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*) | |
3 | xrlenlt 9982 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | |
4 | 1, 2, 3 | syl2an 493 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∈ wcel 1977 class class class wbr 4583 ℝcr 9814 ℝ*cxr 9952 < clt 9953 ≤ cle 9954 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 df-opab 4644 df-xp 5044 df-cnv 5046 df-xr 9957 df-le 9959 |
This theorem is referenced by: ltnle 9996 letri3 10002 leloe 10003 eqlelt 10004 ne0gt0 10021 lelttric 10023 lenlti 10036 lenltd 10062 ltaddsub 10381 leord1 10434 lediv1 10767 suprleub 10866 dfinfre 10881 infregelb 10884 nnge1 10923 nnnlt1 10927 avgle1 11149 avgle2 11150 nn0nlt0 11196 recnz 11328 btwnnz 11329 prime 11334 indstr 11632 uzsupss 11656 zbtwnre 11662 rpneg 11739 2resupmax 11893 fzn 12228 nelfzo 12344 fzonlt0 12360 fllt 12469 flflp1 12470 modifeq2int 12594 om2uzlt2i 12612 fsuppmapnn0fiub0 12655 suppssfz 12656 leexp2 12777 discr 12863 bcval4 12956 ccatsymb 13219 swrd0 13286 sqrtneglem 13855 harmonic 14430 efle 14687 dvdsle 14870 dfgcd2 15101 lcmf 15184 infpnlem1 15452 pgpssslw 17852 gsummoncoe1 19495 mp2pm2mplem4 20433 dvferm1 23552 dvferm2 23554 dgrlt 23826 logleb 24153 argrege0 24161 ellogdm 24185 dvlog2lem 24198 cxple 24241 cxple3 24247 asinneg 24413 birthdaylem3 24480 ppieq0 24702 chpeq0 24733 chteq0 24734 lgsval2lem 24832 lgsneg 24846 lgsdilem 24849 gausslemma2dlem1a 24890 gausslemma2dlem3 24893 ostth2lem1 25107 ostth3 25127 clwlkisclwwlklem2a 26313 rusgranumwlks 26483 frgrareg 26644 friendship 26649 nmounbi 27015 nmlno0lem 27032 nmlnop0iALT 28238 supfz 30866 inffz 30867 inffzOLD 30868 fz0n 30869 nn0prpw 31488 leceifl 32568 poimirlem15 32594 poimirlem16 32595 poimirlem17 32596 poimirlem20 32599 poimirlem24 32603 poimirlem31 32610 poimirlem32 32611 ftc1anclem1 32655 nninfnub 32717 ellz1 36348 rencldnfilem 36402 icccncfext 38773 subsubelfzo0 40359 upgrewlkle2 40808 rusgrnumwwlks 41177 clwlkclwwlklem2a 41207 av-frgrareg 41548 av-friendship 41553 digexp 42199 |
Copyright terms: Public domain | W3C validator |