Theorem mnflt0 13281

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

This proof depends on syntax axioms:   ∈ wcel 2147   class class class wbr 5106  ℝcr 11226  0cc0 11227  -∞cmnf 11368   < clt 11370

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-cnex 11283  ax-1cn 11285  ax-addrcl 11288  ax-rnegex 11298  ax-cnre 11300

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-xp 5661  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375

This theorem is used by:  ge0gtmnf  13329  xsubge0  13418  sgnmnf  15277  leordtval2  23560  mnfnei  23569  ovolicopnf  25875  voliunlem3  25903  volsup  25907  volivth  25958  itg2seq  26093  itg2monolem2  26102  deg1lt0  26439  plypf1  26561  xrge00  33645  dvasin  38814  readvrec2  43605  readvrec  43606  hbtlem5  44322  xrge0nemnfd  46549  xrpnf  46700  fourierdlem87  47408  fouriersw  47446  gsumge0cl  47586  sge0pr  47609  sge0ssre  47612