Theorem 0ltpnf 12356

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

Syntax hints:   ∈ wcel 2079   class class class wbr 4956  ℝcr 10371  0cc0 10372  +∞cpnf 10507   < clt 10510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310  ax-cnex 10428  ax-1cn 10430  ax-addrcl 10433  ax-rnegex 10443  ax-cnre 10445

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-opab 5019  df-xp 5441  df-pnf 10512  df-xr 10514  df-ltxr 10515

This theorem is referenced by:  xmulgt0  12515  reltxrnmnf  12574  hashneq0  13563  hashge2el2dif  13672  sgnpnf  14274  pnfnei  21500  0bdop  29449  xlt2addrd  30143  xnn0gt0  30155  xrge0mulc1cn  30757  pnfneige0  30767  lmxrge0  30768  mbfposadd  34416  ftc1anclem5  34448  fourierdlem111  41998  fouriersw  42012