Theorem mnflt0 13067

Description: Minus infinity is less than 0. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
mnflt0	⊢ -∞ < 0

Proof of Theorem mnflt0

Step	Hyp	Ref	Expression
1		0re 11137	. 2 ⊢ 0 ∈ ℝ
2		mnflt 13065	. 2 ⊢ (0 ∈ ℝ → -∞ < 0)
3	1, 2	ax-mp 5	1 ⊢ -∞ < 0

Syntax hints:   ∈ wcel 2114   class class class wbr 5086  ℝcr 11028  0cc0 11029  -∞cmnf 11168   < clt 11170

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-1cn 11087  ax-addrcl 11090  ax-rnegex 11100  ax-cnre 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5630  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175

This theorem is referenced by:  ge0gtmnf  13115  xsubge0  13204  sgnmnf  15048  leordtval2  23187  mnfnei  23196  ovolicopnf  25501  voliunlem3  25529  volsup  25533  volivth  25584  itg2seq  25719  itg2monolem2  25728  deg1lt0  26066  plypf1  26187  xrge00  33089  dvasin  38039  readvrec2  42807  readvrec  42808  hbtlem5  43574  xrge0nemnfd  45780  xrpnf  45931  fourierdlem87  46639  fouriersw  46677  gsumge0cl  46817  sge0pr  46840  sge0ssre  46843