Theorem mnflt0 13168

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

This proof depends on syntax axioms:   ∈ wcel 2146   class class class wbr 5114  ℝcr 11117  0cc0 11118  -∞cmnf 11259   < clt 11261

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-1cn 11176  ax-addrcl 11179  ax-rnegex 11189  ax-cnre 11191

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-xp 5672  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266

This theorem is used by:  ge0gtmnf  13216  xsubge0  13305  sgnmnf  15158  leordtval2  23406  mnfnei  23415  ovolicopnf  25720  voliunlem3  25748  volsup  25752  volivth  25803  itg2seq  25938  itg2monolem2  25947  deg1lt0  26285  plypf1  26406  xrge00  33365  dvasin  38396  readvrec2  43163  readvrec  43164  hbtlem5  43896  xrge0nemnfd  46089  xrpnf  46240  fourierdlem87  46948  fouriersw  46986  gsumge0cl  47126  sge0pr  47149  sge0ssre  47152