Theorem mnfltd 13066

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  ℝcr 11028  -∞cmnf 11168   < clt 11170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5630  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175

This theorem is referenced by:  qbtwnxr  13143  xltnegi  13159  supxrre  13270  infxrre  13280  caucvgrlem  15626  tgioo  24771  reconnlem1  24802  reconnlem2  24803  ovoliunlem1  25479  ovoliun  25482  ioombl1lem2  25536  ismbf3d  25631  dvferm1lem  25961  dvferm2lem  25963  degltlem1  26047  ply1divex  26112  dvdsq1p  26138  logdmnrp  26618  atans2  26908  ply1degltel  33669  ply1degleel  33670  ply1degltlss  33671  ply1degltdimlem  33782  areacirclem5  38047  aks6d1c5lem3  42590  infleinflem2  45818  xrralrecnnge  45837  icoopn  45973  icomnfinre  46000  ressiocsup  46002  ressioosup  46003  preimaiocmnf  46008  limciccioolb  46069  limsupre  46087  limcresioolb  46089  limcleqr  46090  xlimmnfvlem1  46278  fourierdlem32  46585  fourierdlem46  46598  fourierdlem48  46600  fourierdlem49  46601  fourierdlem74  46626  fourierdlem88  46640  fourierdlem95  46647  fourierdlem103  46655  fourierdlem104  46656  fouriersw  46677  ioorrnopnxrlem  46752  hspdifhsp  47062  hspmbllem2  47073  pimgtmnf2  47160  smfsuplem1  47257