xrre2 - Metamath Proof Explorer

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

Theorem xrre2 12203

Description: An extended real between two others is real. (Contributed by NM, 6-Feb-2007.)

**Assertion**
Ref	Expression
xrre2	⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ ℝ)

**Proof of Theorem xrre2**
Step	Hyp	Ref	Expression
1		mnfle 12169	. . . . . . 7 ⊢ (𝐴 ∈ ℝ^* → -∞ ≤ 𝐴)
2	1	adantr 472	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → -∞ ≤ 𝐴)
3		mnfxr 10350	. . . . . . 7 ⊢ -∞ ∈ ℝ^*
4		xrlelttr 12189	. . . . . . 7 ⊢ ((-∞ ∈ ℝ^* ∧ 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((-∞ ≤ 𝐴 ∧ 𝐴 < 𝐵) → -∞ < 𝐵))
5	3, 4	mp3an1 1572	. . . . . 6 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((-∞ ≤ 𝐴 ∧ 𝐴 < 𝐵) → -∞ < 𝐵))
6	2, 5	mpand 686	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 → -∞ < 𝐵))
7	6	3adant3 1162	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐴 < 𝐵 → -∞ < 𝐵))
8		pnfge 12164	. . . . . . 7 ⊢ (𝐶 ∈ ℝ^* → 𝐶 ≤ +∞)
9	8	adantl 473	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → 𝐶 ≤ +∞)
10		pnfxr 10346	. . . . . . 7 ⊢ +∞ ∈ ℝ^*
11		xrltletr 12190	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝐵 < 𝐶 ∧ 𝐶 ≤ +∞) → 𝐵 < +∞))
12	10, 11	mp3an3 1574	. . . . . 6 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐵 < 𝐶 ∧ 𝐶 ≤ +∞) → 𝐵 < +∞))
13	9, 12	mpan2d 685	. . . . 5 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐵 < 𝐶 → 𝐵 < +∞))
14	13	3adant1 1160	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐵 < 𝐶 → 𝐵 < +∞))
15	7, 14	anim12d 602	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → (-∞ < 𝐵 ∧ 𝐵 < +∞)))
16		xrrebnd 12201	. . . 4 ⊢ (𝐵 ∈ ℝ^* → (𝐵 ∈ ℝ ↔ (-∞ < 𝐵 ∧ 𝐵 < +∞)))
17	16	3ad2ant2 1164	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → (𝐵 ∈ ℝ ↔ (-∞ < 𝐵 ∧ 𝐵 < +∞)))
18	15, 17	sylibrd 250	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐵 ∈ ℝ))
19	18	imp 395	1 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → 𝐵 ∈ ℝ)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 197 ∧ wa 384 ∧ w3a 1107 ∈ wcel 2155 class class class wbr 4809 ℝcr 10188 +∞cpnf 10325 -∞cmnf 10326 ℝ^*cxr 10327 < clt 10328 ≤ cle 10329

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2070 ax-7 2105 ax-8 2157 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2352 ax-ext 2743 ax-sep 4941 ax-nul 4949 ax-pow 5001 ax-pr 5062 ax-un 7147 ax-cnex 10245 ax-resscn 10246 ax-pre-lttri 10263 ax-pre-lttrn 10264

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-3or 1108 df-3an 1109 df-tru 1656 df-ex 1875 df-nf 1879 df-sb 2063 df-mo 2565 df-eu 2582 df-clab 2752 df-cleq 2758 df-clel 2761 df-nfc 2896 df-ne 2938 df-nel 3041 df-ral 3060 df-rex 3061 df-rab 3064 df-v 3352 df-sbc 3597 df-csb 3692 df-dif 3735 df-un 3737 df-in 3739 df-ss 3746 df-nul 4080 df-if 4244 df-pw 4317 df-sn 4335 df-pr 4337 df-op 4341 df-uni 4595 df-br 4810 df-opab 4872 df-mpt 4889 df-id 5185 df-po 5198 df-so 5199 df-xp 5283 df-rel 5284 df-cnv 5285 df-co 5286 df-dm 5287 df-rn 5288 df-res 5289 df-ima 5290 df-iota 6031 df-fun 6070 df-fn 6071 df-f 6072 df-f1 6073 df-fo 6074 df-f1o 6075 df-fv 6076 df-er 7947 df-en 8161 df-dom 8162 df-sdom 8163 df-pnf 10330 df-mnf 10331 df-xr 10332 df-ltxr 10333 df-le 10334

This theorem is referenced by: elioore 12407 xrsdsreclblem 20065 pnfnei 21304 mnfnei 21305 tgioo 22878 ovolunnul 23558 icombl 23622 ioombl 23623 ioorcl2 23630 volivth 23665 dvferm2lem 24040 itg2gt0cn 33888 iccpartipre 42091

W3C validator