Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xrltnle | Structured version Visualization version GIF version |
Description: "Less than" expressed in terms of "less than or equal to", for extended reals. (Contributed by NM, 6-Feb-2007.) |
Ref | Expression |
---|---|
xrltnle | ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xrlenlt 10708 | . . 3 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) | |
2 | 1 | con2bid 357 | . 2 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
3 | 2 | ancoms 461 | 1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∈ wcel 2114 class class class wbr 5068 ℝ*cxr 10676 < clt 10677 ≤ cle 10678 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-sep 5205 ax-nul 5212 ax-pr 5332 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ral 3145 df-rex 3146 df-rab 3149 df-v 3498 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-sn 4570 df-pr 4572 df-op 4576 df-br 5069 df-opab 5131 df-xp 5563 df-cnv 5565 df-le 10683 |
This theorem is referenced by: xrletri 12549 qextltlem 12598 xralrple 12601 xltadd1 12652 xsubge0 12657 xposdif 12658 xltmul1 12688 ioo0 12766 ico0 12787 ioc0 12788 snunioo 12867 snunioc 12869 difreicc 12873 hashbnd 13699 limsuplt 14838 pcadd 16227 pcadd2 16228 ramubcl 16356 ramlb 16357 leordtvallem1 21820 leordtvallem2 21821 leordtval2 21822 leordtval 21823 lecldbas 21829 blcld 23117 stdbdbl 23129 tmsxpsval2 23151 iocmnfcld 23379 xrsxmet 23419 metdsge 23459 bndth 23564 ovolgelb 24083 ovolunnul 24103 ioombl 24168 volsup2 24208 mbfmax 24252 ismbf3d 24257 itg2seq 24345 itg2monolem2 24354 itg2monolem3 24355 lhop2 24614 mdegleb 24660 deg1ge 24694 deg1add 24699 ig1pdvds 24772 plypf1 24804 radcnvlt1 25008 upgrfi 26878 xrdifh 30505 xrge00 30675 gsumesum 31320 itg2gt0cn 34949 asindmre 34979 dvasin 34980 radcnvrat 40653 supxrgelem 41612 infrpge 41626 xrlexaddrp 41627 xrltnled 41638 xrpnf 41769 gtnelioc 41772 ltnelicc 41779 gtnelicc 41782 snunioo1 41795 eliccnelico 41812 xrgtnelicc 41821 lptioo2 41919 stoweidlem34 42326 fourierdlem20 42419 fouriersw 42523 nltle2tri 43520 iccelpart 43600 |
Copyright terms: Public domain | W3C validator |