Theorem mnfltd 13123

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

Step	Hyp	Ref	Expression
1		mnfltd.a	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		mnflt 13122	. 2 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → -∞ < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2141   class class class wbr 5099  ℝcr 11069  -∞cmnf 11211   < clt 11213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pow 5321  ax-pr 5389  ax-un 7714  ax-cnex 11126

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-xp 5651  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218

This theorem is referenced by:  qbtwnxr  13200  xltnegi  13216  supxrre  13327  infxrre  13337  caucvgrlem  15683  tgioo  24836  reconnlem1  24867  reconnlem2  24868  ovoliunlem1  25544  ovoliun  25547  ioombl1lem2  25601  ismbf3d  25696  dvferm1lem  26026  dvferm2lem  26028  degltlem1  26112  ply1divex  26177  dvdsq1p  26203  logdmnrp  26683  atans2  26973  ply1degltel  33751  ply1degleel  33752  ply1degltlss  33753  ply1degltdimlem  33880  areacirclem5  38175  aks6d1c5lem3  42718  infleinflem2  45910  xrralrecnnge  45929  icoopn  46065  icomnfinre  46092  ressiocsup  46094  ressioosup  46095  preimaiocmnf  46100  limciccioolb  46161  limsupre  46179  limcresioolb  46181  limcleqr  46182  xlimmnfvlem1  46370  fourierdlem32  46677  fourierdlem46  46690  fourierdlem48  46692  fourierdlem49  46693  fourierdlem74  46718  fourierdlem88  46732  fourierdlem95  46739  fourierdlem103  46747  fourierdlem104  46748  fouriersw  46769  ioorrnopnxrlem  46844  hspdifhsp  47154  hspmbllem2  47165  pimgtmnf2  47252  smfsuplem1  47349