Description: An extended real that is neither minus infinity, nor plus infinity, is real. (Contributed by Glauco Siliprandi, 3-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | xrred.1 | |- ( ph -> A e. RR* ) |
|
xrred.2 | |- ( ph -> A =/= -oo ) |
||
xrred.3 | |- ( ph -> A =/= +oo ) |
||
Assertion | xrred | |- ( ph -> A e. RR ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xrred.1 | |- ( ph -> A e. RR* ) |
|
2 | xrred.2 | |- ( ph -> A =/= -oo ) |
|
3 | xrred.3 | |- ( ph -> A =/= +oo ) |
|
4 | 1 2 | jca | |- ( ph -> ( A e. RR* /\ A =/= -oo ) ) |
5 | xrnemnf | |- ( ( A e. RR* /\ A =/= -oo ) <-> ( A e. RR \/ A = +oo ) ) |
|
6 | 4 5 | sylib | |- ( ph -> ( A e. RR \/ A = +oo ) ) |
7 | 3 | neneqd | |- ( ph -> -. A = +oo ) |
8 | pm2.53 | |- ( ( A e. RR \/ A = +oo ) -> ( -. A e. RR -> A = +oo ) ) |
|
9 | 8 | con1d | |- ( ( A e. RR \/ A = +oo ) -> ( -. A = +oo -> A e. RR ) ) |
10 | 6 7 9 | sylc | |- ( ph -> A e. RR ) |