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

Theorem mnfltd 12740
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 12739 . 2 (𝐴 ∈ ℝ → -∞ < 𝐴)
31, 2syl 17 1 (𝜑 → -∞ < 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111   class class class wbr 5067  cr 10752  -∞cmnf 10889   < clt 10891
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541  ax-cnex 10809
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3422  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4834  df-br 5068  df-opab 5130  df-xp 5571  df-pnf 10893  df-mnf 10894  df-xr 10895  df-ltxr 10896
This theorem is referenced by:  qbtwnxr  12814  xltnegi  12830  supxrre  12941  infxrre  12950  caucvgrlem  15260  tgioo  23717  reconnlem1  23747  reconnlem2  23748  ovoliunlem1  24423  ovoliun  24426  ioombl1lem2  24480  ismbf3d  24575  dvferm1lem  24905  dvferm2lem  24907  degltlem1  24994  ply1divex  25058  dvdsq1p  25082  logdmnrp  25553  atans2  25838  areacirclem5  35632  infleinflem2  42611  xrralrecnnge  42631  icoopn  42766  icomnfinre  42793  ressiocsup  42795  ressioosup  42796  preimaiocmnf  42802  limciccioolb  42865  limsupre  42885  limcresioolb  42887  limcleqr  42888  xlimmnfvlem1  43076  fourierdlem32  43383  fourierdlem46  43396  fourierdlem48  43398  fourierdlem49  43399  fourierdlem74  43424  fourierdlem88  43438  fourierdlem95  43445  fourierdlem103  43453  fourierdlem104  43454  fouriersw  43475  ioorrnopnxrlem  43550  hspdifhsp  43857  hspmbllem2  43868  pimltmnf2  43938  pimgtmnf2  43951  smfsuplem1  44044
  Copyright terms: Public domain W3C validator