Theorem mnflt0 13235

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

This proof depends on syntax axioms:   ∈ wcel 2145   class class class wbr 5103  ℝcr 11180  0cc0 11181  -∞cmnf 11322   < clt 11324

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-cnex 11237  ax-1cn 11239  ax-addrcl 11242  ax-rnegex 11252  ax-cnre 11254

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329

This theorem is used by:  ge0gtmnf  13283  xsubge0  13372  sgnmnf  15228  leordtval2  23510  mnfnei  23519  ovolicopnf  25825  voliunlem3  25853  volsup  25857  volivth  25908  itg2seq  26043  itg2monolem2  26052  deg1lt0  26389  plypf1  26511  xrge00  33557  dvasin  38590  readvrec2  43380  readvrec  43381  hbtlem5  44088  xrge0nemnfd  46288  xrpnf  46439  fourierdlem87  47147  fouriersw  47185  gsumge0cl  47325  sge0pr  47348  sge0ssre  47351