Theorem mnfltd 13027

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5095  ℝcr 11014  -∞cmnf 11153   < clt 11155

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7676  ax-cnex 11071

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-xp 5627  df-pnf 11157  df-mnf 11158  df-xr 11159  df-ltxr 11160

This theorem is referenced by:  qbtwnxr  13103  xltnegi  13119  supxrre  13230  infxrre  13240  caucvgrlem  15584  tgioo  24714  reconnlem1  24745  reconnlem2  24746  ovoliunlem1  25433  ovoliun  25436  ioombl1lem2  25490  ismbf3d  25585  dvferm1lem  25918  dvferm2lem  25920  degltlem1  26007  ply1divex  26072  dvdsq1p  26098  logdmnrp  26580  atans2  26871  ply1degltel  33564  ply1degleel  33565  ply1degltlss  33566  ply1degltdimlem  33658  areacirclem5  37775  aks6d1c5lem3  42253  infleinflem2  45496  xrralrecnnge  45515  icoopn  45652  icomnfinre  45679  ressiocsup  45681  ressioosup  45682  preimaiocmnf  45687  limciccioolb  45748  limsupre  45766  limcresioolb  45768  limcleqr  45769  xlimmnfvlem1  45957  fourierdlem32  46264  fourierdlem46  46277  fourierdlem48  46279  fourierdlem49  46280  fourierdlem74  46305  fourierdlem88  46319  fourierdlem95  46326  fourierdlem103  46334  fourierdlem104  46335  fouriersw  46356  ioorrnopnxrlem  46431  hspdifhsp  46741  hspmbllem2  46752  pimgtmnf2  46839  smfsuplem1  46936