Theorem mnflt0 13188

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 11292	. 2 ⊢ 0 ∈ ℝ
2		mnflt 13186	. 2 ⊢ (0 ∈ ℝ → -∞ < 0)
3	1, 2	ax-mp 5	1 ⊢ -∞ < 0

Syntax hints:   ∈ wcel 2108   class class class wbr 5166  ℝcr 11183  0cc0 11184  -∞cmnf 11322   < clt 11324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-1cn 11242  ax-addrcl 11245  ax-rnegex 11255  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329

This theorem is referenced by:  ge0gtmnf  13234  xsubge0  13323  sgnmnf  15144  leordtval2  23241  mnfnei  23250  ovolicopnf  25578  voliunlem3  25606  volsup  25610  volivth  25661  itg2seq  25797  itg2monolem2  25806  deg1lt0  26150  plypf1  26271  xrge00  32998  dvasin  37664  hbtlem5  43085  xrge0nemnfd  45247  xrpnf  45401  fourierdlem87  46114  fouriersw  46152  gsumge0cl  46292  sge0pr  46315  sge0ssre  46318