Theorem mnfltd 13023

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

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5091  ℝcr 11005  -∞cmnf 11144   < clt 11146

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-cnex 11062

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 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-xp 5622  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151

This theorem is referenced by:  qbtwnxr  13099  xltnegi  13115  supxrre  13226  infxrre  13236  caucvgrlem  15580  tgioo  24712  reconnlem1  24743  reconnlem2  24744  ovoliunlem1  25431  ovoliun  25434  ioombl1lem2  25488  ismbf3d  25583  dvferm1lem  25916  dvferm2lem  25918  degltlem1  26005  ply1divex  26070  dvdsq1p  26096  logdmnrp  26578  atans2  26869  ply1degltel  33553  ply1degleel  33554  ply1degltlss  33555  ply1degltdimlem  33633  areacirclem5  37758  aks6d1c5lem3  42176  infleinflem2  45415  xrralrecnnge  45434  icoopn  45571  icomnfinre  45598  ressiocsup  45600  ressioosup  45601  preimaiocmnf  45606  limciccioolb  45667  limsupre  45685  limcresioolb  45687  limcleqr  45688  xlimmnfvlem1  45876  fourierdlem32  46183  fourierdlem46  46196  fourierdlem48  46198  fourierdlem49  46199  fourierdlem74  46224  fourierdlem88  46238  fourierdlem95  46245  fourierdlem103  46253  fourierdlem104  46254  fouriersw  46275  ioorrnopnxrlem  46350  hspdifhsp  46660  hspmbllem2  46671  pimgtmnf2  46758  smfsuplem1  46855