![]() |
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 10321 | . . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) | |
2 | 1 | ancoms 446 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) |
3 | 2 | con2bid 343 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 382 ∈ wcel 2145 class class class wbr 4787 ℝcr 10140 < clt 10279 ≤ cle 10280 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4916 ax-nul 4924 ax-pr 5035 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4227 df-sn 4318 df-pr 4320 df-op 4324 df-br 4788 df-opab 4848 df-xp 5256 df-cnv 5258 df-xr 10283 df-le 10285 |
This theorem is referenced by: letric 10342 ltnled 10389 leaddsub 10709 mulge0b 11098 nnnle0 11256 nn0n0n1ge2b 11565 znnnlt1 11610 uzwo 11958 qsqueeze 12236 difreicc 12510 fzp1disj 12605 fzneuz 12627 fznuz 12628 uznfz 12629 difelfznle 12660 nelfzo 12682 ssfzoulel 12769 elfzonelfzo 12777 modfzo0difsn 12949 ssnn0fi 12991 discr1 13206 facdiv 13277 bcval5 13308 ccatsymb 13563 swrdnd 13640 swrdsbslen 13656 swrdspsleq 13657 swrdccat3 13700 repswswrd 13739 cnpart 14187 absmax 14276 rlimrege0 14517 znnenlem 15145 rpnnen2lem12 15159 alzdvds 15250 algcvgblem 15497 prmndvdsfaclt 15641 pcprendvds 15751 pcdvdsb 15779 pcmpt 15802 prmunb 15824 prmreclem2 15827 prmgaplem5 15965 prmgaplem6 15966 prmlem1 16020 prmlem2 16033 lt6abl 18502 metdseq0 22876 xrhmeo 22964 ovolicc2lem3 23506 itg2seq 23728 dvne0 23993 coeeulem 24199 radcnvlt1 24391 argimgt0 24578 cxple2 24663 ressatans 24881 eldmgm 24968 basellem2 25028 issqf 25082 bpos1 25228 bposlem3 25231 bposlem6 25234 pntpbnd2 25496 ostth2lem4 25545 crctcshwlkn0 26948 crctcsh 26951 eucrctshift 27422 ltflcei 33729 poimirlem4 33745 poimirlem13 33754 poimirlem14 33755 poimirlem15 33756 poimirlem31 33772 mblfinlem1 33778 mbfposadd 33788 itgaddnclem2 33800 ftc1anclem1 33816 ftc1anclem5 33820 dvasin 33827 icccncfext 40615 stoweidlem14 40745 stoweidlem34 40765 ltnltne 41838 pfxccat3 41951 pfxccat3a 41954 nnsum4primeseven 42213 nnsum4primesevenALTV 42214 ply1mulgsumlem2 42700 |
Copyright terms: Public domain | W3C validator |