Theorem mnfltd 13025

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5093  ℝcr 11012  -∞cmnf 11151   < clt 11153

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 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-cnex 11069

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 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-xp 5625  df-pnf 11155  df-mnf 11156  df-xr 11157  df-ltxr 11158

This theorem is referenced by:  qbtwnxr  13101  xltnegi  13117  supxrre  13228  infxrre  13238  caucvgrlem  15582  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  33562  ply1degleel  33563  ply1degltlss  33564  ply1degltdimlem  33656  areacirclem5  37772  aks6d1c5lem3  42250  infleinflem2  45493  xrralrecnnge  45512  icoopn  45649  icomnfinre  45676  ressiocsup  45678  ressioosup  45679  preimaiocmnf  45684  limciccioolb  45745  limsupre  45763  limcresioolb  45765  limcleqr  45766  xlimmnfvlem1  45954  fourierdlem32  46261  fourierdlem46  46274  fourierdlem48  46276  fourierdlem49  46277  fourierdlem74  46302  fourierdlem88  46316  fourierdlem95  46323  fourierdlem103  46331  fourierdlem104  46332  fouriersw  46353  ioorrnopnxrlem  46428  hspdifhsp  46738  hspmbllem2  46749  pimgtmnf2  46836  smfsuplem1  46933