Theorem 0ltpnf 12968

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 11087	. 2 ⊢ 0 ∈ ℝ
2		ltpnf 12966	. 2 ⊢ (0 ∈ ℝ → 0 < +∞)
3	1, 2	ax-mp 5	1 ⊢ 0 < +∞

Syntax hints:   ∈ wcel 2106   class class class wbr 5100  ℝcr 10980  0cc0 10981  +∞cpnf 11116   < clt 11119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-sep 5251  ax-nul 5258  ax-pow 5315  ax-pr 5379  ax-un 7659  ax-cnex 11037  ax-1cn 11039  ax-addrcl 11042  ax-rnegex 11052  ax-cnre 11054

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4278  df-if 4482  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4861  df-br 5101  df-opab 5163  df-xp 5633  df-pnf 11121  df-xr 11123  df-ltxr 11124

This theorem is referenced by:  xmulgt0  13127  reltxrnmnf  13186  hashneq0  14188  hashge2el2dif  14303  sgnpnf  14908  pnfnei  22481  0bdop  30709  xlt2addrd  31432  xnn0gt0  31443  xrge0mulc1cn  32253  pnfneige0  32263  lmxrge0  32264  mbfposadd  35980  ftc1anclem5  36010  fourierdlem111  44146  fouriersw  44160