![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nltpnft | Structured version Visualization version Unicode version |
Description: An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.) |
Ref | Expression |
---|---|
nltpnft |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pnfxr 11412 |
. . . 4
![]() ![]() ![]() ![]() | |
2 | xrltnr 11421 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
. . 3
![]() ![]() ![]() ![]() ![]() |
4 | breq1 4405 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | mtbiri 305 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | pnfge 11432 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | xrleloe 11443 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 1, 7 | mpan2 677 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 6, 8 | mpbid 214 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 9 | ord 379 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 5, 10 | impbid2 208 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-pre-lttri 9613 ax-pre-lttrn 9614 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-op 3975 df-uni 4199 df-br 4403 df-opab 4462 df-mpt 4463 df-id 4749 df-po 4755 df-so 4756 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-er 7363 df-en 7570 df-dom 7571 df-sdom 7572 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 |
This theorem is referenced by: xrrebnd 11463 xlt2add 11546 supxrbnd1 11607 supxrbnd2 11608 supxrgtmnf 11615 supxrre2 11617 ioopnfsup 12091 icopnfsup 12092 xrsdsreclblem 19014 ovoliun 22458 ovolicopnf 22478 voliunlem3 22505 volsup 22509 itg2seq 22700 nmoreltpnf 26410 nmopreltpnf 27522 xgepnf 28327 ismblfin 31981 supxrgere 37556 supxrgelem 37560 supxrge 37561 suplesup 37562 nepnfltpnf 37565 sge0repnf 38228 sge0rpcpnf 38263 sge0rernmpt 38264 |
Copyright terms: Public domain | W3C validator |