xrrege0 - Metamath Proof Explorer

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

Theorem xrrege0 13094

Description: A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.)

**Assertion**
Ref	Expression
xrrege0	⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ)

**Proof of Theorem xrrege0**
Step	Hyp	Ref	Expression
1		ge0gtmnf 13092	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴) → -∞ < 𝐴)
2	1	ad2ant2r 747	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → -∞ < 𝐴)
3		simprr 772	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ≤ 𝐵)
4	2, 3	jca 511	. 2 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (-∞ < 𝐴 ∧ 𝐴 ≤ 𝐵))
5		xrre 13089	. 2 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (-∞ < 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ)
6	4, 5	syldan 591	1 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2109 class class class wbr 5095 ℝcr 11027 0cc0 11028 -∞cmnf 11166 ℝ^*cxr 11167 < clt 11168 ≤ cle 11169

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-addrcl 11089 ax-rnegex 11099 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5518 df-po 5531 df-so 5532 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 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 8632 df-en 8880 df-dom 8881 df-sdom 8882 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174

This theorem is referenced by: psmetlecl 24219 xmetlecl 24250 prdsxmetlem 24272 stdbdmet 24420 stdbdmopn 24422 bddnghm 24630 nmoid 24646 xrsmopn 24717 metdsre 24758 metnrmlem1a 24763 ovollecl 25400 itg2lecl 25655 probmeasb 34400 heicant 37637 mblfinlem3 37641 mblfinlem4 37642