Theorem 0ltpnf 13251

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

This proof depends on syntax axioms:   ∈ wcel 2144   class class class wbr 5102  ℝcr 11199  0cc0 11200  +∞cpnf 11340   < clt 11343

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11256  ax-1cn 11258  ax-addrcl 11261  ax-rnegex 11271  ax-cnre 11273

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-pnf 11345  df-xr 11347  df-ltxr 11348

This theorem is used by:  xmulgt0  13413  reltxrnmnf  13473  hashneq0  14508  hashge2el2dif  14625  sgnpnf  15246  pnfnei  23538  0bdop  32595  xlt2addrd  33351  xnn0gt0  33361  xrge0mulc1cn  34573  pnfneige0  34583  lmxrge0  34584  mbfposadd  38586  ftc1anclem5  38616  fourierdlem111  47227  fouriersw  47241