Theorem mnflt0 12245

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

Syntax hints:   ∈ wcel 2166   class class class wbr 4873  ℝcr 10251  0cc0 10252  -∞cmnf 10389   < clt 10391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-cnex 10308  ax-1cn 10310  ax-addrcl 10313  ax-rnegex 10323  ax-cnre 10325

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-xp 5348  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396

This theorem is referenced by:  ge0gtmnf  12291  xsubge0  12379  xrge0neqmnfOLD  12566  sgnmnf  14212  leordtval2  21387  mnfnei  21396  ovolicopnf  23690  voliunlem3  23718  volsup  23722  volivth  23773  itg2seq  23908  itg2monolem2  23917  deg1lt0  24250  plypf1  24367  xrge00  30231  dvasin  34039  hbtlem5  38541  xrge0nemnfd  40345  xrpnf  40510  fourierdlem87  41204  fouriersw  41242  gsumge0cl  41379  sge0pr  41402  sge0ssre  41405