Theorem 0ltpnf 13258

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 11317	. 2 ⊢ 0 ∈ ℝ
2		ltpnf 13256	. 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 11206  0cc0 11207  +∞cpnf 11347   < clt 11350

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 5327  ax-pr 5391  ax-un 7755  ax-cnex 11263  ax-1cn 11265  ax-addrcl 11268  ax-rnegex 11278  ax-cnre 11280

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 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5657  df-pnf 11352  df-xr 11354  df-ltxr 11355

This theorem is used by:  xmulgt0  13420  reltxrnmnf  13480  hashneq0  14515  hashge2el2dif  14632  sgnpnf  15255  pnfnei  23547  0bdop  32604  xlt2addrd  33401  xnn0gt0  33411  xrge0mulc1cn  34623  pnfneige0  34633  lmxrge0  34634  mbfposadd  38694  ftc1anclem5  38724  fourierdlem111  47335  fouriersw  47349