Database
REAL AND COMPLEX NUMBERS
Order sets
Infinity and the extended real number system (cont.)
xrre3
Next ⟩
ge0gtmnf
Metamath Proof Explorer
Ascii
Unicode
Theorem
xrre3
Description:
A way of proving that an extended real is real.
(Contributed by
FL
, 29-May-2014)
Ref
Expression
Assertion
xrre3
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
∧
B
≤
A
∧
A
<
+∞
→
A
∈
ℝ
Proof
Step
Hyp
Ref
Expression
1
mnflt
⊢
B
∈
ℝ
→
−∞
<
B
2
1
adantl
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
→
−∞
<
B
3
mnfxr
⊢
−∞
∈
ℝ
*
4
rexr
⊢
B
∈
ℝ
→
B
∈
ℝ
*
5
4
adantl
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
→
B
∈
ℝ
*
6
simpl
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
→
A
∈
ℝ
*
7
xrltletr
⊢
−∞
∈
ℝ
*
∧
B
∈
ℝ
*
∧
A
∈
ℝ
*
→
−∞
<
B
∧
B
≤
A
→
−∞
<
A
8
3
5
6
7
mp3an2i
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
→
−∞
<
B
∧
B
≤
A
→
−∞
<
A
9
2
8
mpand
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
→
B
≤
A
→
−∞
<
A
10
9
imp
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
∧
B
≤
A
→
−∞
<
A
11
10
adantrr
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
∧
B
≤
A
∧
A
<
+∞
→
−∞
<
A
12
simprr
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
∧
B
≤
A
∧
A
<
+∞
→
A
<
+∞
13
xrrebnd
⊢
A
∈
ℝ
*
→
A
∈
ℝ
↔
−∞
<
A
∧
A
<
+∞
14
13
ad2antrr
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
∧
B
≤
A
∧
A
<
+∞
→
A
∈
ℝ
↔
−∞
<
A
∧
A
<
+∞
15
11
12
14
mpbir2and
⊢
A
∈
ℝ
*
∧
B
∈
ℝ
∧
B
≤
A
∧
A
<
+∞
→
A
∈
ℝ