Theorem mnflt0 13257

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

This proof depends on syntax axioms:   ∈ wcel 2144   class class class wbr 5102  ℝcr 11202  0cc0 11203  -∞cmnf 11344   < clt 11346

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11259  ax-1cn 11261  ax-addrcl 11264  ax-rnegex 11274  ax-cnre 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-pnf 11348  df-mnf 11349  df-xr 11350  df-ltxr 11351

This theorem is used by:  ge0gtmnf  13305  xsubge0  13394  sgnmnf  15253  leordtval2  23535  mnfnei  23544  ovolicopnf  25850  voliunlem3  25878  volsup  25882  volivth  25933  itg2seq  26068  itg2monolem2  26077  deg1lt0  26414  plypf1  26536  xrge00  33621  dvasin  38715  readvrec2  43505  readvrec  43506  hbtlem5  44223  xrge0nemnfd  46437  xrpnf  46588  fourierdlem87  47296  fouriersw  47334  gsumge0cl  47474  sge0pr  47497  sge0ssre  47500