Theorem mnflt0 13026

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

Syntax hints:   ∈ wcel 2113   class class class wbr 5093  ℝcr 11012  0cc0 11013  -∞cmnf 11151   < clt 11153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-cnex 11069  ax-1cn 11071  ax-addrcl 11074  ax-rnegex 11084  ax-cnre 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-xp 5625  df-pnf 11155  df-mnf 11156  df-xr 11157  df-ltxr 11158

This theorem is referenced by:  ge0gtmnf  13073  xsubge0  13162  sgnmnf  15004  leordtval2  23128  mnfnei  23137  ovolicopnf  25453  voliunlem3  25481  volsup  25485  volivth  25536  itg2seq  25671  itg2monolem2  25680  deg1lt0  26024  plypf1  26145  xrge00  33002  dvasin  37764  readvrec2  42479  readvrec  42480  hbtlem5  43245  xrge0nemnfd  45455  xrpnf  45607  fourierdlem87  46315  fouriersw  46353  gsumge0cl  46493  sge0pr  46516  sge0ssre  46519