Theorem 0ltpnf 13089

Description: Zero is less than plus infinity. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
0ltpnf	⊢ 0 < +∞

Proof of Theorem 0ltpnf

Step	Hyp	Ref	Expression
1		0re 11183	. 2 ⊢ 0 ∈ ℝ
2		ltpnf 13087	. 2 ⊢ (0 ∈ ℝ → 0 < +∞)
3	1, 2	ax-mp 5	1 ⊢ 0 < +∞

Syntax hints:   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074  0cc0 11075  +∞cpnf 11212   < clt 11215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-1cn 11133  ax-addrcl 11136  ax-rnegex 11146  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-pnf 11217  df-xr 11219  df-ltxr 11220

This theorem is referenced by:  xmulgt0  13250  reltxrnmnf  13310  hashneq0  14336  hashge2el2dif  14452  sgnpnf  15066  pnfnei  23114  0bdop  31929  xlt2addrd  32689  xnn0gt0  32699  xrge0mulc1cn  33938  pnfneige0  33948  lmxrge0  33949  mbfposadd  37668  ftc1anclem5  37698  fourierdlem111  46222  fouriersw  46236