Step |
Hyp |
Ref |
Expression |
1 |
|
elxnn0 |
|- ( A e. NN0* <-> ( A e. NN0 \/ A = +oo ) ) |
2 |
|
nn0re |
|- ( A e. NN0 -> A e. RR ) |
3 |
2
|
rexrd |
|- ( A e. NN0 -> A e. RR* ) |
4 |
|
nn0ge0 |
|- ( A e. NN0 -> 0 <_ A ) |
5 |
|
elxrge0 |
|- ( A e. ( 0 [,] +oo ) <-> ( A e. RR* /\ 0 <_ A ) ) |
6 |
3 4 5
|
sylanbrc |
|- ( A e. NN0 -> A e. ( 0 [,] +oo ) ) |
7 |
|
0xr |
|- 0 e. RR* |
8 |
|
pnfxr |
|- +oo e. RR* |
9 |
|
0lepnf |
|- 0 <_ +oo |
10 |
|
ubicc2 |
|- ( ( 0 e. RR* /\ +oo e. RR* /\ 0 <_ +oo ) -> +oo e. ( 0 [,] +oo ) ) |
11 |
7 8 9 10
|
mp3an |
|- +oo e. ( 0 [,] +oo ) |
12 |
|
eleq1 |
|- ( A = +oo -> ( A e. ( 0 [,] +oo ) <-> +oo e. ( 0 [,] +oo ) ) ) |
13 |
11 12
|
mpbiri |
|- ( A = +oo -> A e. ( 0 [,] +oo ) ) |
14 |
6 13
|
jaoi |
|- ( ( A e. NN0 \/ A = +oo ) -> A e. ( 0 [,] +oo ) ) |
15 |
1 14
|
sylbi |
|- ( A e. NN0* -> A e. ( 0 [,] +oo ) ) |