MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mnfltd Structured version   Visualization version   GIF version

Theorem mnfltd 13046
Description: Minus infinity is less than any (finite) real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
mnfltd.a (𝜑𝐴 ∈ ℝ)
Assertion
Ref Expression
mnfltd (𝜑 → -∞ < 𝐴)

Proof of Theorem mnfltd
StepHypRef Expression
1 mnfltd.a . 2 (𝜑𝐴 ∈ ℝ)
2 mnflt 13045 . 2 (𝐴 ∈ ℝ → -∞ < 𝐴)
31, 2syl 17 1 (𝜑 → -∞ < 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107   class class class wbr 5106  cr 11051  -∞cmnf 11188   < clt 11190
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11108
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-xp 5640  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195
This theorem is referenced by:  qbtwnxr  13120  xltnegi  13136  supxrre  13247  infxrre  13256  caucvgrlem  15558  tgioo  24162  reconnlem1  24192  reconnlem2  24193  ovoliunlem1  24869  ovoliun  24872  ioombl1lem2  24926  ismbf3d  25021  dvferm1lem  25351  dvferm2lem  25353  degltlem1  25440  ply1divex  25504  dvdsq1p  25528  logdmnrp  25999  atans2  26284  areacirclem5  36173  infleinflem2  43612  xrralrecnnge  43632  icoopn  43770  icomnfinre  43797  ressiocsup  43799  ressioosup  43800  preimaiocmnf  43806  limciccioolb  43869  limsupre  43889  limcresioolb  43891  limcleqr  43892  xlimmnfvlem1  44080  fourierdlem32  44387  fourierdlem46  44400  fourierdlem48  44402  fourierdlem49  44403  fourierdlem74  44428  fourierdlem88  44442  fourierdlem95  44449  fourierdlem103  44457  fourierdlem104  44458  fouriersw  44479  ioorrnopnxrlem  44554  hspdifhsp  44864  hspmbllem2  44875  pimgtmnf2  44962  smfsuplem1  45059
  Copyright terms: Public domain W3C validator