xrrebnd - Metamath Proof Explorer

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

Theorem xrrebnd 13069

Description: An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.)

**Assertion**
Ref	Expression
xrrebnd	⊢ (𝐴 ∈ ℝ^* → (𝐴 ∈ ℝ ↔ (-∞ < 𝐴 ∧ 𝐴 < +∞)))

**Proof of Theorem xrrebnd**
Step	Hyp	Ref	Expression
1		mnflt 13024	. . 3 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)
2		ltpnf 13021	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)
3	1, 2	jca 511	. 2 ⊢ (𝐴 ∈ ℝ → (-∞ < 𝐴 ∧ 𝐴 < +∞))
4		nltpnft 13065	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → (𝐴 = +∞ ↔ ¬ 𝐴 < +∞))
5		ngtmnft 13067	. . . . . 6 ⊢ (𝐴 ∈ ℝ^* → (𝐴 = -∞ ↔ ¬ -∞ < 𝐴))
6	4, 5	orbi12d 918	. . . . 5 ⊢ (𝐴 ∈ ℝ^* → ((𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (¬ 𝐴 < +∞ ∨ ¬ -∞ < 𝐴)))
7		ianor 983	. . . . . 6 ⊢ (¬ (-∞ < 𝐴 ∧ 𝐴 < +∞) ↔ (¬ -∞ < 𝐴 ∨ ¬ 𝐴 < +∞))
8		orcom 870	. . . . . 6 ⊢ ((¬ -∞ < 𝐴 ∨ ¬ 𝐴 < +∞) ↔ (¬ 𝐴 < +∞ ∨ ¬ -∞ < 𝐴))
9	7, 8	bitr2i 276	. . . . 5 ⊢ ((¬ 𝐴 < +∞ ∨ ¬ -∞ < 𝐴) ↔ ¬ (-∞ < 𝐴 ∧ 𝐴 < +∞))
10	6, 9	bitrdi 287	. . . 4 ⊢ (𝐴 ∈ ℝ^* → ((𝐴 = +∞ ∨ 𝐴 = -∞) ↔ ¬ (-∞ < 𝐴 ∧ 𝐴 < +∞)))
11	10	con2bid 354	. . 3 ⊢ (𝐴 ∈ ℝ^* → ((-∞ < 𝐴 ∧ 𝐴 < +∞) ↔ ¬ (𝐴 = +∞ ∨ 𝐴 = -∞)))
12		elxr 13017	. . . . 5 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
13		3orass 1089	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
14		orcom 870	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)) ↔ ((𝐴 = +∞ ∨ 𝐴 = -∞) ∨ 𝐴 ∈ ℝ))
15	13, 14	bitri 275	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ ((𝐴 = +∞ ∨ 𝐴 = -∞) ∨ 𝐴 ∈ ℝ))
16	12, 15	sylbb 219	. . . 4 ⊢ (𝐴 ∈ ℝ^* → ((𝐴 = +∞ ∨ 𝐴 = -∞) ∨ 𝐴 ∈ ℝ))
17	16	ord 864	. . 3 ⊢ (𝐴 ∈ ℝ^* → (¬ (𝐴 = +∞ ∨ 𝐴 = -∞) → 𝐴 ∈ ℝ))
18	11, 17	sylbid 240	. 2 ⊢ (𝐴 ∈ ℝ^* → ((-∞ < 𝐴 ∧ 𝐴 < +∞) → 𝐴 ∈ ℝ))
19	3, 18	impbid2 226	1 ⊢ (𝐴 ∈ ℝ^* → (𝐴 ∈ ℝ ↔ (-∞ < 𝐴 ∧ 𝐴 < +∞)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∨ w3o 1085 = wceq 1541 ∈ wcel 2113 class class class wbr 5093 ℝcr 11012 +∞cpnf 11150 -∞cmnf 11151 ℝ^*cxr 11152 < clt 11153

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-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-cnex 11069 ax-resscn 11070 ax-pre-lttri 11087 ax-pre-lttrn 11088

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-br 5094 df-opab 5156 df-mpt 5175 df-id 5514 df-po 5527 df-so 5528 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-er 8628 df-en 8876 df-dom 8877 df-sdom 8878 df-pnf 11155 df-mnf 11156 df-xr 11157 df-ltxr 11158 df-le 11159

This theorem is referenced by: xrre 13070 xrre2 13071 xrre3 13072 supxrre1 13231 elioc2 13311 elico2 13312 elicc2 13313 xblpnfps 24311 xblpnf 24312 isnghm3 24641 ovoliun 25434 ovolicopnf 25453 voliunlem3 25481 volsup 25485 itg2seq 25671 nmblore 30768 nmopre 31852 supxrgere 45457 supxrgelem 45461 supxrge 45462 suplesup 45463 infrpge 45475 limsupre 45764

W3C validator