Theorem mnflt0 13092

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

Syntax hints:   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074  0cc0 11075  -∞cmnf 11213   < clt 11215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-1cn 11133  ax-addrcl 11136  ax-rnegex 11146  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220

This theorem is referenced by:  ge0gtmnf  13139  xsubge0  13228  sgnmnf  15068  leordtval2  23106  mnfnei  23115  ovolicopnf  25432  voliunlem3  25460  volsup  25464  volivth  25515  itg2seq  25650  itg2monolem2  25659  deg1lt0  26003  plypf1  26124  xrge00  32960  dvasin  37705  readvrec2  42356  readvrec  42357  hbtlem5  43124  xrge0nemnfd  45335  xrpnf  45488  fourierdlem87  46198  fouriersw  46236  gsumge0cl  46376  sge0pr  46399  sge0ssre  46402