xrletri3 - Metamath Proof Explorer

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

Theorem xrletri3 13105

Description: Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)

**Assertion**
Ref	Expression
xrletri3	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))

**Proof of Theorem xrletri3**
Step	Hyp	Ref	Expression
1		xrlttri3 13094	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)))
2	1	biancomd 463	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 = 𝐵 ↔ (¬ 𝐵 < 𝐴 ∧ ¬ 𝐴 < 𝐵)))
3		xrlenlt 11210	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
4		xrlenlt 11210	. . . 4 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐴 ∈ ℝ^*) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
5	4	ancoms 458	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
6	3, 5	anbi12d 633	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴) ↔ (¬ 𝐵 < 𝐴 ∧ ¬ 𝐴 < 𝐵)))
7	2, 6	bitr4d 282	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 class class class wbr 5085 ℝ^*cxr 11178 < clt 11179 ≤ cle 11180

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-pre-lttri 11112 ax-pre-lttrn 11113

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-br 5086 df-opab 5148 df-mpt 5167 df-id 5526 df-po 5539 df-so 5540 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-er 8643 df-en 8894 df-dom 8895 df-sdom 8896 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185

This theorem is referenced by: xrletrid 13106 xrmaxeq 13131 xrmineq 13132 xleadd1a 13205 xsubge0 13213 xlemul1a 13240 hashle00 14362 limsupval2 15442 pc2dvds 16850 pc11 16851 letsr 18559 xrge0omnd 21425 isxmet2d 24292 xmetgt0 24323 prdsxmetlem 24333 xblss2 24367 nmo0 24700 nmoid 24707 xrsxmet 24775 ovolssnul 25454 ovolctb 25457 ovoliunnul 25474 ovolre 25492 volsup 25523 vitalilem5 25579 itg2mulc 25714 umgrislfupgrlem 29191 upgr2pthnlp 29800 xeqlelt 32849 xrstos 33070 metideq 34037 metider 34038 esumpad2 34200 esumrnmpt2 34212 measle0 34352 inelcarsg 34455 carsggect 34462 carsgclctun 34465 omsmeas 34467 ovoliunnfl 37983 volsupnfl 37986 iccintsng 45953 liminfval2 46196