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 11197

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 5099	. . 3 ⊢ (𝐴 ≤ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≤ )
2		opelxpi 5661	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → ⟨𝐴, 𝐵⟩ ∈ (ℝ^ × ℝ^*))
3		df-le 11172	. . . . . . 7 ⊢ ≤ = ((ℝ^* × ℝ^*) ∖ ^◡ < )
4	3	eleq2i 2828	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ⟨𝐴, 𝐵⟩ ∈ ((ℝ^* × ℝ^*) ∖ ^◡ < ))
5		eldif 3911	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ ∈ ((ℝ^* × ℝ^) ∖ ^◡ < ) ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ^ × ℝ^*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
6	4, 5	bitri 275	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ^* × ℝ^*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
7	6	baib 535	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ ∈ (ℝ^* × ℝ^*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
8	2, 7	syl 17	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
9	1, 8	bitrid 283	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 ≤ 𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
10		df-br 5099	. . . 4 ⊢ (𝐵 < 𝐴 ↔ ⟨𝐵, 𝐴⟩ ∈ < )
11		opelcnvg 5829	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (⟨𝐴, 𝐵⟩ ∈ ^◡ < ↔ ⟨𝐵, 𝐴⟩ ∈ < ))
12	10, 11	bitr4id 290	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐵 < 𝐴 ↔ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
13	12	notbid 318	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (¬ 𝐵 < 𝐴 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
14	9, 13	bitr4d 282	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∈ wcel 2113 ∖ cdif 3898 ⟨cop 4586 class class class wbr 5098 × cxp 5622 ^◡ccnv 5623 ℝ^*cxr 11165 < clt 11166 ≤ cle 11167

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 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pr 5377

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2715 df-cleq 2728 df-clel 2811 df-ral 3052 df-rex 3061 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-ss 3918 df-nul 4286 df-if 4480 df-sn 4581 df-pr 4583 df-op 4587 df-br 5099 df-opab 5161 df-xp 5630 df-cnv 5632 df-le 11172

This theorem is referenced by: xrlenltd 11198 xrltnle 11199 lenlt 11211 pnfge 13044 mnfle 13049 xrleloe 13058 xrltlen 13060 xrletri3 13068 xgepnf 13080 xlemnf 13082 xralrple 13120 xleneg 13133 supxr2 13229 supxrbnd1 13236 supxrbnd2 13237 supxrleub 13241 supxrbnd 13243 xrsupssd 13248 infxrgelb 13251 ioon0 13287 iccid 13306 icc0 13309 icoun 13391 ioounsn 13393 snunico 13395 ioodisj 13398 ioojoin 13399 hashgt0elex 14324 hashgt12el 14345 hashgt12el2 14346 0ringnnzr 20458 lecldbas 23163 xmetgt0 24302 icopnfcld 24711 ioombl 25522 vitalilem4 25568 itg2gt0 25717 nmlnogt0 30872 xrlelttric 32832 xrge0infss 32840 joiniooico 32854 xeqlelt 32856 iocinif 32861 esumsnf 34221 esum2d 34250 oms0 34454 omssubadd 34457 cusgracyclt3v 35350 relowlpssretop 37569 mblfinlem3 37860 mblfinlem4 37861 ismblfin 37862 asindmre 37904 dvrelog2b 42320 iocmbl 43455 supxrgere 45578 iccdifprioo 45762 iccpartnel 47684 iccdisj2 49142

W3C validator