xrlenlt - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > xrlenlt		GIF version

Theorem xrlenlt 8222

Description: 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.)

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

**Proof of Theorem xrlenlt**
Step	Hyp	Ref	Expression
1		df-br 4084	. . 3 ⊢ (𝐴 ≤ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≤ )
2		opelxpi 4751	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → ⟨𝐴, 𝐵⟩ ∈ (ℝ^ × ℝ^*))
3		df-le 8198	. . . . . . 7 ⊢ ≤ = ((ℝ^* × ℝ^*) ∖ ^◡ < )
4	3	eleq2i 2296	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ⟨𝐴, 𝐵⟩ ∈ ((ℝ^* × ℝ^*) ∖ ^◡ < ))
5		eldif 3206	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ ∈ ((ℝ^* × ℝ^) ∖ ^◡ < ) ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ^ × ℝ^*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
6	4, 5	bitri 184	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ^* × ℝ^*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
7	6	baib 924	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ ∈ (ℝ^* × ℝ^*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
8	2, 7	syl 14	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
9	1, 8	bitrid 192	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 ≤ 𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
10		df-br 4084	. . . 4 ⊢ (𝐵 < 𝐴 ↔ ⟨𝐵, 𝐴⟩ ∈ < )
11		opelcnvg 4902	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (⟨𝐴, 𝐵⟩ ∈ ^◡ < ↔ ⟨𝐵, 𝐴⟩ ∈ < ))
12	10, 11	bitr4id 199	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐵 < 𝐴 ↔ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
13	12	notbid 671	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (¬ 𝐵 < 𝐴 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
14	9, 13	bitr4d 191	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∈ wcel 2200 ∖ cdif 3194 ⟨cop 3669 class class class wbr 4083 × cxp 4717 ^◡ccnv 4718 ℝ^*cxr 8191 < clt 8192 ≤ cle 8193

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-14 2203 ax-ext 2211 ax-sep 4202 ax-pow 4258 ax-pr 4293

This theorem depends on definitions: df-bi 117 df-3an 1004 df-tru 1398 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ral 2513 df-rex 2514 df-v 2801 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-br 4084 df-opab 4146 df-xp 4725 df-cnv 4727 df-le 8198

This theorem is referenced by: lenlt 8233 pnfge 9997 mnfle 10000 xrltle 10006 xrleid 10008 xnn0dcle 10010 xrletri3 10012 xrlelttr 10014 xrltletr 10015 xrletr 10016 xgepnf 10024 xleneg 10045 xltadd1 10084 xsubge0 10089 xleaddadd 10095 iccid 10133 icc0r 10134 icodisj 10200 ioodisj 10201 ioo0 10491 ico0 10493 ioc0 10494 leisorel 11072 xrmaxleim 11770 xrmaxiflemval 11776 xrmaxlesup 11785 xrmaxaddlem 11786 xrminmax 11791 pcadd 12878 bldisj 15090 bdxmet 15190 bdbl 15192

W3C validator