Theorem mnflt0 13124

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

Syntax hints:   ∈ wcel 2141   class class class wbr 5099  ℝcr 11069  0cc0 11070  -∞cmnf 11211   < clt 11213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pow 5321  ax-pr 5389  ax-un 7714  ax-cnex 11126  ax-1cn 11128  ax-addrcl 11131  ax-rnegex 11141  ax-cnre 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-xp 5651  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218

This theorem is referenced by:  ge0gtmnf  13172  xsubge0  13261  sgnmnf  15105  leordtval2  23252  mnfnei  23261  ovolicopnf  25566  voliunlem3  25594  volsup  25598  volivth  25649  itg2seq  25784  itg2monolem2  25793  deg1lt0  26131  plypf1  26252  xrge00  33153  dvasin  38167  readvrec2  42934  readvrec  42935  hbtlem5  43669  xrge0nemnfd  45872  xrpnf  46023  fourierdlem87  46731  fouriersw  46769  gsumge0cl  46909  sge0pr  46932  sge0ssre  46935