![]() |
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 11191 | . . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) | |
2 | 1 | ancoms 459 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) |
3 | 2 | con2bid 354 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∈ wcel 2106 class class class wbr 5103 ℝcr 11008 < clt 11147 ≤ cle 11148 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2708 ax-sep 5254 ax-nul 5261 ax-pr 5382 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-br 5104 df-opab 5166 df-xp 5637 df-cnv 5639 df-xr 11151 df-le 11153 |
This theorem is referenced by: letric 11213 ltnled 11260 leaddsub 11589 mulge0b 11983 nnnle0 12144 nn0n0n1ge2b 12439 znnnlt1 12488 uzwo 12790 qsqueeze 13074 difreicc 13355 fzp1disj 13454 fzneuz 13476 fznuz 13477 uznfz 13478 difelfznle 13509 nelfzo 13531 ssfzoulel 13620 elfzonelfzo 13628 modfzo0difsn 13802 ssnn0fi 13844 discr1 14096 bcval5 14172 swrdnd 14500 swrdnnn0nd 14502 swrdnd0 14503 swrdsbslen 14510 swrdspsleq 14511 pfxnd0 14534 pfxccat3 14580 swrdccat 14581 pfxccat3a 14584 repswswrd 14630 cnpart 15085 absmax 15174 rlimrege0 15421 rpnnen2lem12 16067 alzdvds 16162 algcvgblem 16413 prmndvdsfaclt 16561 pcprendvds 16672 pcdvdsb 16701 pcmpt 16724 prmunb 16746 prmreclem2 16749 prmgaplem5 16887 prmgaplem6 16888 prmlem1 16940 prmlem2 16952 lt6abl 19631 metdseq0 24169 xrhmeo 24261 ovolicc2lem3 24835 itg2seq 25059 dvne0 25327 coeeulem 25537 radcnvlt1 25729 argimgt0 25919 cxple2 26004 ressatans 26236 eldmgm 26323 basellem2 26383 issqf 26437 bpos1 26583 bposlem3 26586 bposlem6 26589 2sqreulem1 26746 2sqreunnlem1 26749 pntpbnd2 26887 ostth2lem4 26936 crctcshwlkn0 28595 crctcsh 28598 eucrctshift 29016 ltflcei 36004 poimirlem4 36020 poimirlem13 36029 poimirlem14 36030 poimirlem15 36031 poimirlem31 36047 mblfinlem1 36053 mbfposadd 36063 itgaddnclem2 36075 ftc1anclem1 36089 ftc1anclem5 36093 dvasin 36100 reabsifnpos 41816 reabsifnneg 41818 icccncfext 44029 stoweidlem14 44156 stoweidlem34 44176 ltnltne 45432 nnsum4primeseven 45893 nnsum4primesevenALTV 45894 ply1mulgsumlem2 46369 |
Copyright terms: Public domain | W3C validator |