xrltnle - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > xrltnle		Structured version Visualization version GIF version

Theorem xrltnle 11305

Description: "Less than" expressed in terms of "less than or equal to", for extended reals. (Contributed by NM, 6-Feb-2007.)

**Assertion**
Ref	Expression
xrltnle	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

**Proof of Theorem xrltnle**
Step	Hyp	Ref	Expression
1		xrlenlt 11303	. . 3 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐴 ∈ ℝ^*) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
2	1	con2bid 354	. 2 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐴 ∈ ℝ^*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))
3	2	ancoms 458	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∈ wcel 2099 class class class wbr 5142 ℝ^*cxr 11271 < clt 11272 ≤ cle 11273

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-sep 5293 ax-nul 5300 ax-pr 5423

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ral 3058 df-rex 3067 df-rab 3429 df-v 3472 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4319 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-br 5143 df-opab 5205 df-xp 5678 df-cnv 5680 df-le 11278

This theorem is referenced by: xrletri 13158 qextltlem 13207 xralrple 13210 xltadd1 13261 xsubge0 13266 xposdif 13267 xltmul1 13297 ioo0 13375 ico0 13396 ioc0 13397 snunioo 13481 snunioc 13483 difreicc 13487 hashbnd 14321 limsuplt 15449 pcadd 16851 pcadd2 16852 ramubcl 16980 ramlb 16981 leordtvallem1 23107 leordtvallem2 23108 leordtval2 23109 leordtval 23110 lecldbas 23116 blcld 24407 stdbdbl 24419 tmsxpsval2 24441 iocmnfcld 24678 xrsxmet 24718 metdsge 24758 bndth 24877 ovolgelb 25402 ovolunnul 25422 ioombl 25487 volsup2 25527 mbfmax 25571 ismbf3d 25576 itg2seq 25665 itg2monolem2 25674 itg2monolem3 25675 lhop2 25941 mdegleb 25993 deg1ge 26027 deg1add 26032 ig1pdvds 26107 plypf1 26139 radcnvlt1 26347 upgrfi 28897 xrdifh 32542 xrge00 32736 gsumesum 33672 itg2gt0cn 37142 asindmre 37170 dvasin 37171 aks6d1c6lem3 41638 aks6d1c7lem2 41647 radcnvrat 43745 supxrgelem 44713 infrpge 44727 xrlexaddrp 44728 xrltnled 44739 xrpnf 44862 gtnelioc 44870 ltnelicc 44876 gtnelicc 44879 snunioo1 44891 eliccnelico 44908 xrgtnelicc 44917 lptioo2 45013 stoweidlem34 45416 fourierdlem20 45509 fouriersw 45613 nltle2tri 46687 iccelpart 46767

	
		OSZAR »