Theorem mnfltd 13073

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

Syntax hints:   → wi 4   ∈ wcel 2119   class class class wbr 5079  ℝcr 11035  -∞cmnf 11175   < clt 11177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-cnex 11092

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-xp 5631  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182

This theorem is referenced by:  qbtwnxr  13150  xltnegi  13166  supxrre  13277  infxrre  13287  caucvgrlem  15633  tgioo  24786  reconnlem1  24817  reconnlem2  24818  ovoliunlem1  25494  ovoliun  25497  ioombl1lem2  25551  ismbf3d  25646  dvferm1lem  25976  dvferm2lem  25978  degltlem1  26062  ply1divex  26127  dvdsq1p  26153  logdmnrp  26630  atans2  26920  ply1degltel  33684  ply1degleel  33685  ply1degltlss  33686  ply1degltdimlem  33813  areacirclem5  38086  aks6d1c5lem3  42629  infleinflem2  45822  xrralrecnnge  45841  icoopn  45977  icomnfinre  46004  ressiocsup  46006  ressioosup  46007  preimaiocmnf  46012  limciccioolb  46073  limsupre  46091  limcresioolb  46093  limcleqr  46094  xlimmnfvlem1  46282  fourierdlem32  46589  fourierdlem46  46602  fourierdlem48  46604  fourierdlem49  46605  fourierdlem74  46630  fourierdlem88  46644  fourierdlem95  46651  fourierdlem103  46659  fourierdlem104  46660  fouriersw  46681  ioorrnopnxrlem  46756  hspdifhsp  47066  hspmbllem2  47077  pimgtmnf2  47164  smfsuplem1  47261