Description: Plus infinity is an infinite for the completed real line, as any real number is infinitesimal compared to it. (Contributed by Thierry Arnoux, 1-Feb-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | pnfinf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpgt0 | |
|
2 | nnz | |
|
3 | 2 | adantl | |
4 | rpxr | |
|
5 | 4 | adantr | |
6 | xrsmulgzz | |
|
7 | 3 5 6 | syl2anc | |
8 | 3 | zred | |
9 | rpre | |
|
10 | 9 | adantr | |
11 | rexmul | |
|
12 | remulcl | |
|
13 | 11 12 | eqeltrd | |
14 | 8 10 13 | syl2anc | |
15 | 7 14 | eqeltrd | |
16 | ltpnf | |
|
17 | 15 16 | syl | |
18 | 17 | ralrimiva | |
19 | xrsex | |
|
20 | pnfxr | |
|
21 | xrsbas | |
|
22 | xrs0 | |
|
23 | eqid | |
|
24 | xrslt | |
|
25 | 21 22 23 24 | isinftm | |
26 | 19 20 25 | mp3an13 | |
27 | 4 26 | syl | |
28 | 1 18 27 | mpbir2and | |