Theorem 0ltpnf 13244

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

This proof depends on syntax axioms:   ∈ wcel 2145   class class class wbr 5103  ℝcr 11192  0cc0 11193  +∞cpnf 11333   < clt 11336

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-1cn 11251  ax-addrcl 11254  ax-rnegex 11264  ax-cnre 11266

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-pnf 11338  df-xr 11340  df-ltxr 11341

This theorem is used by:  xmulgt0  13406  reltxrnmnf  13466  hashneq0  14501  hashge2el2dif  14618  sgnpnf  15239  pnfnei  23531  0bdop  32588  xlt2addrd  33344  xnn0gt0  33354  xrge0mulc1cn  34566  pnfneige0  34576  lmxrge0  34577  mbfposadd  38565  ftc1anclem5  38595  fourierdlem111  47196  fouriersw  47210