| 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 11307 | . 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
| 2 | rexr 11307 | . 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*) | |
| 3 | xrlenlt 11326 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | |
| 4 | 1, 2, 3 | syl2an 596 | 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 ℝ*cxr 11294 < 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: ltnle 11340 letri3 11346 leloe 11347 eqlelt 11348 ne0gt0 11366 lelttric 11368 lenlti 11381 lenltd 11407 ltaddsub 11737 leord1 11790 lediv1 12133 suprleub 12234 dfinfre 12249 infregelb 12252 nnge1 12294 nnnlt1 12298 avgle1 12506 avgle2 12507 nn0nlt0 12552 recnz 12693 btwnnz 12694 prime 12699 indstr 12958 uzsupss 12982 zbtwnre 12988 rpneg 13067 2resupmax 13230 fzn 13580 nelfzo 13704 fzonlt0 13722 fllt 13846 flflp1 13847 modifeq2int 13974 om2uzlt2i 13992 fsuppmapnn0fiub0 14034 suppssfz 14035 leexp2 14211 discr 14279 bcval4 14346 ccatsymb 14620 swrd0 14696 sqrtneglem 15305 harmonic 15895 efle 16154 dvdsle 16347 dfgcd2 16583 lcmf 16670 infpnlem1 16948 pgpssslw 19632 gsummoncoe1 22312 mp2pm2mplem4 22815 dvferm1 26023 dvferm2 26025 dgrlt 26306 logleb 26645 argrege0 26653 ellogdm 26681 cxple 26737 cxple3 26743 asinneg 26929 birthdaylem3 26996 ppieq0 27219 chpeq0 27252 chteq0 27253 lgsval2lem 27351 lgsneg 27365 lgsdilem 27368 gausslemma2dlem1a 27409 gausslemma2dlem3 27412 ostth2lem1 27662 ostth3 27682 rusgrnumwwlks 29994 clwlkclwwlklem2a 30017 frgrreg 30413 friendship 30418 nmounbi 30795 nmlno0lem 30812 nmlnop0iALT 32014 supfz 35729 inffz 35730 fz0n 35731 nn0prpw 36324 leceifl 37616 poimirlem15 37642 poimirlem16 37643 poimirlem17 37644 poimirlem20 37647 poimirlem24 37651 poimirlem31 37658 poimirlem32 37659 ftc1anclem1 37700 nninfnub 37758 metakunt22 42227 ellz1 42778 rencldnfilem 42831 icccncfext 45902 subsubelfzo0 47338 digexp 48528 reorelicc 48631 |
| Copyright terms: Public domain | W3C validator |