Theorem 0ltpnf 13101

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

Syntax hints:   ∈ wcel 2106   class class class wbr 5148  ℝcr 11108  0cc0 11109  +∞cpnf 11244   < clt 11247

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 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-1cn 11167  ax-addrcl 11170  ax-rnegex 11180  ax-cnre 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-xp 5682  df-pnf 11249  df-xr 11251  df-ltxr 11252

This theorem is referenced by:  xmulgt0  13261  reltxrnmnf  13320  hashneq0  14323  hashge2el2dif  14440  sgnpnf  15039  pnfnei  22723  0bdop  31241  xlt2addrd  31966  xnn0gt0  31977  xrge0mulc1cn  32916  pnfneige0  32926  lmxrge0  32927  mbfposadd  36530  ftc1anclem5  36560  fourierdlem111  44923  fouriersw  44937