Theorem mnfltd 13044

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 13043	. 2 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → -∞ < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5095  ℝcr 11027  -∞cmnf 11166   < clt 11168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-cnex 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-xp 5629  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173

This theorem is referenced by:  qbtwnxr  13120  xltnegi  13136  supxrre  13247  infxrre  13257  caucvgrlem  15598  tgioo  24700  reconnlem1  24731  reconnlem2  24732  ovoliunlem1  25419  ovoliun  25422  ioombl1lem2  25476  ismbf3d  25571  dvferm1lem  25904  dvferm2lem  25906  degltlem1  25993  ply1divex  26058  dvdsq1p  26084  logdmnrp  26566  atans2  26857  ply1degltel  33539  ply1degleel  33540  ply1degltlss  33541  ply1degltdimlem  33597  areacirclem5  37694  aks6d1c5lem3  42113  infleinflem2  45354  xrralrecnnge  45373  icoopn  45510  icomnfinre  45537  ressiocsup  45539  ressioosup  45540  preimaiocmnf  45545  limciccioolb  45606  limsupre  45626  limcresioolb  45628  limcleqr  45629  xlimmnfvlem1  45817  fourierdlem32  46124  fourierdlem46  46137  fourierdlem48  46139  fourierdlem49  46140  fourierdlem74  46165  fourierdlem88  46179  fourierdlem95  46186  fourierdlem103  46194  fourierdlem104  46195  fouriersw  46216  ioorrnopnxrlem  46291  hspdifhsp  46601  hspmbllem2  46612  pimgtmnf2  46699  smfsuplem1  46796