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 10898 | . . 3 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵)) | |
2 | 1 | con2bid 358 | . 2 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
3 | 2 | ancoms 462 | 1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∈ wcel 2110 class class class wbr 5053 ℝ*cxr 10866 < clt 10867 ≤ cle 10868 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 ax-sep 5192 ax-nul 5199 ax-pr 5322 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3410 df-dif 3869 df-un 3871 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-op 4548 df-br 5054 df-opab 5116 df-xp 5557 df-cnv 5559 df-le 10873 |
This theorem is referenced by: xrletri 12743 qextltlem 12792 xralrple 12795 xltadd1 12846 xsubge0 12851 xposdif 12852 xltmul1 12882 ioo0 12960 ico0 12981 ioc0 12982 snunioo 13066 snunioc 13068 difreicc 13072 hashbnd 13902 limsuplt 15040 pcadd 16442 pcadd2 16443 ramubcl 16571 ramlb 16572 leordtvallem1 22107 leordtvallem2 22108 leordtval2 22109 leordtval 22110 lecldbas 22116 blcld 23403 stdbdbl 23415 tmsxpsval2 23437 iocmnfcld 23666 xrsxmet 23706 metdsge 23746 bndth 23855 ovolgelb 24377 ovolunnul 24397 ioombl 24462 volsup2 24502 mbfmax 24546 ismbf3d 24551 itg2seq 24640 itg2monolem2 24649 itg2monolem3 24650 lhop2 24912 mdegleb 24962 deg1ge 24996 deg1add 25001 ig1pdvds 25074 plypf1 25106 radcnvlt1 25310 upgrfi 27182 xrdifh 30821 xrge00 31014 gsumesum 31739 itg2gt0cn 35569 asindmre 35597 dvasin 35598 radcnvrat 41605 supxrgelem 42549 infrpge 42563 xrlexaddrp 42564 xrltnled 42575 xrpnf 42701 gtnelioc 42704 ltnelicc 42710 gtnelicc 42713 snunioo1 42725 eliccnelico 42742 xrgtnelicc 42751 lptioo2 42847 stoweidlem34 43250 fourierdlem20 43343 fouriersw 43447 nltle2tri 44478 iccelpart 44558 |
Copyright terms: Public domain | W3C validator |