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 13077

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 13075	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴) → -∞ < 𝐴)
2	1	ad2ant2r 747	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → -∞ < 𝐴)
3		simprr 772	. . 3 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ≤ 𝐵)
4	2, 3	jca 511	. 2 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (-∞ < 𝐴 ∧ 𝐴 ≤ 𝐵))
5		xrre 13072	. 2 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (-∞ < 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ)
6	4, 5	syldan 591	1 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2113 class class class wbr 5095 ℝcr 11014 0cc0 11015 -∞cmnf 11153 ℝ^*cxr 11154 < clt 11155 ≤ cle 11156

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 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7676 ax-cnex 11071 ax-resscn 11072 ax-1cn 11073 ax-addrcl 11076 ax-rnegex 11086 ax-cnre 11088 ax-pre-lttri 11089 ax-pre-lttrn 11090

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 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5516 df-po 5529 df-so 5530 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-iota 6444 df-fun 6490 df-fn 6491 df-f 6492 df-f1 6493 df-fo 6494 df-f1o 6495 df-fv 6496 df-er 8630 df-en 8878 df-dom 8879 df-sdom 8880 df-pnf 11157 df-mnf 11158 df-xr 11159 df-ltxr 11160 df-le 11161

This theorem is referenced by: psmetlecl 24233 xmetlecl 24264 prdsxmetlem 24286 stdbdmet 24434 stdbdmopn 24436 bddnghm 24644 nmoid 24660 xrsmopn 24731 metdsre 24772 metnrmlem1a 24777 ovollecl 25414 itg2lecl 25669 probmeasb 34466 heicant 37718 mblfinlem3 37722 mblfinlem4 37723