Theorem mnflt0 13117

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

Syntax hints:   ∈ wcel 2136   class class class wbr 5094  ℝcr 11062  0cc0 11063  -∞cmnf 11204   < clt 11206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-sep 5240  ax-pow 5316  ax-pr 5384  ax-un 7707  ax-cnex 11119  ax-1cn 11121  ax-addrcl 11124  ax-rnegex 11134  ax-cnre 11136

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-pw 4551  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-opab 5157  df-xp 5646  df-pnf 11208  df-mnf 11209  df-xr 11210  df-ltxr 11211

This theorem is referenced by:  ge0gtmnf  13165  xsubge0  13254  sgnmnf  15098  leordtval2  23245  mnfnei  23254  ovolicopnf  25559  voliunlem3  25587  volsup  25591  volivth  25642  itg2seq  25777  itg2monolem2  25786  deg1lt0  26124  plypf1  26245  xrge00  33146  dvasin  38151  readvrec2  42918  readvrec  42919  hbtlem5  43653  xrge0nemnfd  45856  xrpnf  46007  fourierdlem87  46715  fouriersw  46753  gsumge0cl  46893  sge0pr  46916  sge0ssre  46919