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 10695

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 5031	. . 3 ⊢ (𝐴 ≤ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≤ )
2		opelxpi 5556	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → ⟨𝐴, 𝐵⟩ ∈ (ℝ^ × ℝ^*))
3		df-le 10670	. . . . . . 7 ⊢ ≤ = ((ℝ^* × ℝ^*) ∖ ^◡ < )
4	3	eleq2i 2881	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ⟨𝐴, 𝐵⟩ ∈ ((ℝ^* × ℝ^*) ∖ ^◡ < ))
5		eldif 3891	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ ∈ ((ℝ^* × ℝ^) ∖ ^◡ < ) ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ^ × ℝ^*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
6	4, 5	bitri 278	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ^* × ℝ^*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
7	6	baib 539	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ ∈ (ℝ^* × ℝ^*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
8	2, 7	syl 17	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
9	1, 8	syl5bb 286	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 ≤ 𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ^◡ < ))
10		df-br 5031	. . . 4 ⊢ (𝐵 < 𝐴 ↔ ⟨𝐵, 𝐴⟩ ∈ < )
11		opelcnvg 5715	. . . 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 399 ∈ wcel 2111 ∖ cdif 3878 ⟨cop 4531 class class class wbr 5030 × cxp 5517 ^◡ccnv 5518 ℝ^*cxr 10663 < clt 10664 ≤ cle 10665

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-br 5031 df-opab 5093 df-xp 5525 df-cnv 5527 df-le 10670

This theorem is referenced by: xrlenltd 10696 xrltnle 10697 lenlt 10708 pnfge 12513 mnfle 12517 xrleloe 12525 xrltlen 12527 xrletri3 12535 xgepnf 12546 xlemnf 12548 xralrple 12586 xleneg 12599 supxr2 12695 supxrbnd1 12702 supxrbnd2 12703 supxrleub 12707 supxrbnd 12709 infxrgelb 12716 ioon0 12752 iccid 12771 icc0 12774 icoun 12853 ioounsn 12855 snunico 12857 ioodisj 12860 ioojoin 12861 hashgt0elex 13758 hashgt12el 13779 hashgt12el2 13780 0ringnnzr 20035 lecldbas 21824 xmetgt0 22965 icopnfcld 23373 ioombl 24169 vitalilem4 24215 itg2gt0 24364 nmlnogt0 28580 xrlelttric 30502 xrsupssd 30509 xrge0infss 30510 joiniooico 30523 xeqlelt 30525 iocinif 30530 esumsnf 31433 esum2d 31462 oms0 31665 omssubadd 31668 cusgracyclt3v 32516 relowlpssretop 34781 mblfinlem3 35096 mblfinlem4 35097 ismblfin 35098 asindmre 35140 iocmbl 40163 supxrgere 41965 iccdifprioo 42153 iccpartnel 43955

W3C validator