Theorem mnfltd 13167

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5114  ℝcr 11117  -∞cmnf 11259   < clt 11261

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-cnex 11174

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-xp 5672  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266

This theorem is used by:  qbtwnxr  13244  xltnegi  13260  supxrre  13371  infxrre  13381  caucvgrlem  15750  tgioo  24983  reconnlem1  25014  reconnlem2  25015  ovoliunlem1  25691  ovoliun  25694  ioombl1lem2  25748  ismbf3d  25843  dvferm1lem  26173  dvferm2lem  26175  degltlem1  26259  ply1divex  26324  dvdsq1p  26350  logdmnrp  26836  atans2  27126  ply1degltel  33908  ply1degleel  33909  ply1degltlss  33910  ply1degltdimlem  34036  areacirclem5  38396  aks6d1c5lem3  42937  infleinflem2  46119  xrralrecnnge  46138  icoopn  46274  icomnfinre  46301  ressiocsup  46303  ressioosup  46304  preimaiocmnf  46309  limciccioolb  46370  limsupre  46388  limcresioolb  46390  limcleqr  46391  xlimmnfvlem1  46579  fourierdlem32  46886  fourierdlem46  46899  fourierdlem48  46901  fourierdlem49  46902  fourierdlem74  46927  fourierdlem88  46941  fourierdlem95  46948  fourierdlem103  46956  fourierdlem104  46957  fouriersw  46978  ioorrnopnxrlem  47053  hspdifhsp  47363  hspmbllem2  47374  pimgtmnf2  47461  smfsuplem1  47558