Theorem mnflt0 12523

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

Syntax hints:   ∈ wcel 2114   class class class wbr 5068  ℝcr 10538  0cc0 10539  -∞cmnf 10675   < clt 10677

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-1cn 10597  ax-addrcl 10600  ax-rnegex 10610  ax-cnre 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-xp 5563  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682

This theorem is referenced by:  ge0gtmnf  12568  xsubge0  12657  sgnmnf  14456  leordtval2  21822  mnfnei  21831  ovolicopnf  24127  voliunlem3  24155  volsup  24159  volivth  24210  itg2seq  24345  itg2monolem2  24354  deg1lt0  24687  plypf1  24804  xrge00  30675  dvasin  34980  hbtlem5  39735  xrge0nemnfd  41607  xrpnf  41769  fourierdlem87  42485  fouriersw  42523  gsumge0cl  42660  sge0pr  42683  sge0ssre  42686