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 10675 | . 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
2 | rexr 10675 | . 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*) | |
3 | xrlenlt 10694 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | |
4 | 1, 2, 3 | syl2an 595 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∈ wcel 2105 class class class wbr 5057 ℝcr 10524 ℝ*cxr 10662 < clt 10663 ≤ cle 10664 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-br 5058 df-opab 5120 df-xp 5554 df-cnv 5556 df-xr 10667 df-le 10669 |
This theorem is referenced by: ltnle 10708 letri3 10714 leloe 10715 eqlelt 10716 ne0gt0 10733 lelttric 10735 lenlti 10748 lenltd 10774 ltaddsub 11102 leord1 11155 lediv1 11493 suprleub 11595 dfinfre 11610 infregelb 11613 nnge1 11653 nnnlt1 11657 avgle1 11865 avgle2 11866 nn0nlt0 11911 recnz 12045 btwnnz 12046 prime 12051 indstr 12304 uzsupss 12328 zbtwnre 12334 rpneg 12409 2resupmax 12569 fzn 12911 nelfzo 13031 fzonlt0 13048 fllt 13164 flflp1 13165 modifeq2int 13289 om2uzlt2i 13307 fsuppmapnn0fiub0 13349 suppssfz 13350 leexp2 13523 discr 13589 bcval4 13655 ccatsymb 13924 swrd0 14008 sqrtneglem 14614 harmonic 15202 efle 15459 dvdsle 15648 dfgcd2 15882 lcmf 15965 infpnlem1 16234 pgpssslw 18668 gsummoncoe1 20400 mp2pm2mplem4 21345 dvferm1 24509 dvferm2 24511 dgrlt 24783 logleb 25113 argrege0 25121 ellogdm 25149 cxple 25205 cxple3 25211 asinneg 25391 birthdaylem3 25458 ppieq0 25680 chpeq0 25711 chteq0 25712 lgsval2lem 25810 lgsneg 25824 lgsdilem 25827 gausslemma2dlem1a 25868 gausslemma2dlem3 25871 ostth2lem1 26121 ostth3 26141 rusgrnumwwlks 27680 clwlkclwwlklem2a 27703 frgrreg 28100 friendship 28105 nmounbi 28480 nmlno0lem 28497 nmlnop0iALT 29699 supfz 32857 inffz 32858 fz0n 32859 nn0prpw 33568 leceifl 34762 poimirlem15 34788 poimirlem16 34789 poimirlem17 34790 poimirlem20 34793 poimirlem24 34797 poimirlem31 34804 poimirlem32 34805 ftc1anclem1 34848 nninfnub 34907 ellz1 39242 rencldnfilem 39295 limsup10ex 41930 icccncfext 42046 subsubelfzo0 43403 digexp 44595 reorelicc 44625 |
Copyright terms: Public domain | W3C validator |