![]() |
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 10488 | . 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
2 | rexr 10488 | . 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*) | |
3 | xrlenlt 10508 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | |
4 | 1, 2, 3 | syl2an 586 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 387 ∈ wcel 2050 class class class wbr 4930 ℝcr 10336 ℝ*cxr 10475 < clt 10476 ≤ cle 10477 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5061 ax-nul 5068 ax-pr 5187 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-sn 4443 df-pr 4445 df-op 4449 df-br 4931 df-opab 4993 df-xp 5414 df-cnv 5416 df-xr 10480 df-le 10482 |
This theorem is referenced by: ltnle 10522 letri3 10528 leloe 10529 eqlelt 10530 ne0gt0 10547 lelttric 10549 lenlti 10562 lenltd 10588 ltaddsub 10917 leord1 10970 lediv1 11308 suprleub 11410 dfinfre 11425 infregelb 11428 nnge1 11471 nnnlt1 11475 avgle1 11690 avgle2 11691 nn0nlt0 11738 recnz 11873 btwnnz 11874 prime 11879 indstr 12133 uzsupss 12157 zbtwnre 12163 rpneg 12241 2resupmax 12401 fzn 12742 nelfzo 12862 fzonlt0 12878 fllt 12994 flflp1 12995 modifeq2int 13119 om2uzlt2i 13137 fsuppmapnn0fiub0 13179 suppssfz 13180 leexp2 13353 discr 13419 bcval4 13485 ccatsymb 13748 swrd0 13829 sqrtneglem 14490 harmonic 15077 efle 15334 dvdsle 15523 dfgcd2 15753 lcmf 15836 infpnlem1 16105 pgpssslw 18503 gsummoncoe1 20178 mp2pm2mplem4 21124 dvferm1 24288 dvferm2 24290 dgrlt 24562 logleb 24890 argrege0 24898 ellogdm 24926 cxple 24982 cxple3 24988 asinneg 25168 birthdaylem3 25236 ppieq0 25458 chpeq0 25489 chteq0 25490 lgsval2lem 25588 lgsneg 25602 lgsdilem 25605 gausslemma2dlem1a 25646 gausslemma2dlem3 25649 ostth2lem1 25899 ostth3 25919 rusgrnumwwlks 27483 rusgrnumwwlksOLD 27484 clwlkclwwlklem2a 27507 frgrreg 27954 friendship 27959 nmounbi 28333 nmlno0lem 28350 nmlnop0iALT 29556 supfz 32480 inffz 32481 fz0n 32482 nn0prpw 33192 leceifl 34322 poimirlem15 34348 poimirlem16 34349 poimirlem17 34350 poimirlem20 34353 poimirlem24 34357 poimirlem31 34364 poimirlem32 34365 ftc1anclem1 34408 nninfnub 34468 ellz1 38759 rencldnfilem 38813 limsup10ex 41486 icccncfext 41601 subsubelfzo0 42933 digexp 44036 reorelicc 44066 |
Copyright terms: Public domain | W3C validator |