Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 0ltpnf | Structured version Visualization version GIF version |
Description: Zero is less than plus infinity. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
0ltpnf | ⊢ 0 < +∞ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0re 10832 | . 2 ⊢ 0 ∈ ℝ | |
2 | ltpnf 12709 | . 2 ⊢ (0 ∈ ℝ → 0 < +∞) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 0 < +∞ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 class class class wbr 5050 ℝcr 10725 0cc0 10726 +∞cpnf 10861 < clt 10864 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 ax-sep 5189 ax-nul 5196 ax-pow 5255 ax-pr 5319 ax-un 7520 ax-cnex 10782 ax-1cn 10784 ax-addrcl 10787 ax-rnegex 10797 ax-cnre 10799 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3063 df-rex 3064 df-rab 3067 df-v 3407 df-dif 3866 df-un 3868 df-in 3870 df-ss 3880 df-nul 4235 df-if 4437 df-pw 4512 df-sn 4539 df-pr 4541 df-op 4545 df-uni 4817 df-br 5051 df-opab 5113 df-xp 5554 df-pnf 10866 df-xr 10868 df-ltxr 10869 |
This theorem is referenced by: xmulgt0 12870 reltxrnmnf 12929 hashneq0 13928 hashge2el2dif 14043 sgnpnf 14653 pnfnei 22114 0bdop 30071 xlt2addrd 30798 xnn0gt0 30809 xrge0mulc1cn 31602 pnfneige0 31612 lmxrge0 31613 mbfposadd 35559 ftc1anclem5 35589 fourierdlem111 43431 fouriersw 43445 |
Copyright terms: Public domain | W3C validator |