xrlenlt - Metamath Proof Explorer

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

Theorem xrlenlt 11262

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 5105	. . 3 ⊢ (𝐴 ≤ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≤ )
2		opelxpi 5688	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → ⟨𝐴, 𝐵⟩ ∈ (ℝ^ × ℝ^*))
3		df-le 11237	. . . . . . 7 ⊢ ≤ = ((ℝ^* × ℝ^*) ∖ ^◡ < )
4	3	eleq2i 2857	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ⟨𝐴, 𝐵⟩ ∈ ((ℝ^* × ℝ^*) ∖ ^◡ < ))
5		eldif 3917	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ ∈ ((ℝ^* × ℝ^) ∖ ^◡ < ) ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ^ × ℝ^*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
6	4, 5	bitri 278	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ^* × ℝ^*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
7	6	baib 544	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ ∈ (ℝ^* × ℝ^*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
8	2, 7	syl 18	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
9	1, 8	bitrid 286	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 ≤ 𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
10		df-br 5105	. . . 4 ⊢ (𝐵 < 𝐴 ↔ ⟨𝐵, 𝐴⟩ ∈ < )
11		opelcnvg 5856	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (⟨𝐴, 𝐵⟩ ∈ ^◡ < ↔ ⟨𝐵, 𝐴⟩ ∈ < ))
12	10, 11	bitr4id 293	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐵 < 𝐴 ↔ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
13	12	notbid 321	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (¬ 𝐵 < 𝐴 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
14	9, 13	bitr4d 285	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∈ wcel 2145 ∖ cdif 3904 ⟨cop 4591 class class class wbr 5104 × cxp 5649 ^◡ccnv 5650 ℝ^*cxr 11230 < clt 11231 ≤ cle 11232

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 ax-sep 5250 ax-pr 5394

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-br 5105 df-opab 5167 df-xp 5657 df-cnv 5659 df-le 11237

This theorem is referenced by: xrlenltd 11263 xrltnle 11264 lenlt 11276 pnfge 13143 mnfle 13148 xrleloe 13157 xrltlen 13159 xrletri3 13167 xgepnf 13179 xlemnf 13181 xralrple 13219 xleneg 13232 supxr2 13328 supxrbnd1 13335 supxrbnd2 13336 supxrleub 13340 supxrbnd 13342 xrsupssd 13347 infxrgelb 13350 ioon0 13386 iccid 13405 icc0 13408 icoun 13490 ioounsn 13492 snunico 13494 ioodisj 13497 ioojoin 13498 hashgt0elex 14425 hashgt12el 14447 hashgt12el2 14448 0ringnnzr 20597 lecldbas 23333 xmetgt0 24472 icopnfcld 24881 ioombl 25681 vitalilem4 25727 itg2gt0 25876 nmlnogt0 31054 xrlelttric 33005 xrge0infss 33013 joiniooico 33027 xeqlelt 33029 iocinif 33034 esumsnf 34366 esum2d 34395 oms0 34599 omssubadd 34602 cusgracyclt3v 35514 relowlpssretop 37865 mblfinlem3 38165 mblfinlem4 38166 ismblfin 38167 asindmre 38209 dvrelog2b 42690 iocmbl 43797 hashnnltb 45591 supxrgere 45908 iccdifprioo 46091 iccpartnel 48043 iccdisj2 49527

W3C validator