Theorem mnfltd 13234

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  ℝcr 11180  -∞cmnf 11322   < clt 11324

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-cnex 11237

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329

This theorem is used by:  qbtwnxr  13311  xltnegi  13327  supxrre  13438  infxrre  13448  caucvgrlem  15820  tgioo  25095  reconnlem1  25126  reconnlem2  25127  ovoliunlem1  25803  ovoliun  25806  ioombl1lem2  25860  ismbf3d  25955  dvferm1lem  26284  dvferm2lem  26286  degltlem1  26370  ply1divex  26435  dvdsq1p  26461  logdmnrp  26951  atans2  27241  ply1degltel  34108  ply1degleel  34109  ply1degltlss  34110  ply1degltdimlem  34236  areacirclem5  38598  aks6d1c5lem3  43155  infleinflem2  46326  xrralrecnnge  46345  icoopn  46481  icomnfinre  46508  ressiocsup  46510  ressioosup  46511  preimaiocmnf  46516  limciccioolb  46577  limsupre  46595  limcresioolb  46597  limcleqr  46598  xlimmnfvlem1  46786  fourierdlem32  47093  fourierdlem46  47106  fourierdlem48  47108  fourierdlem49  47109  fourierdlem74  47134  fourierdlem88  47148  fourierdlem95  47155  fourierdlem103  47163  fourierdlem104  47164  fouriersw  47185  ioorrnopnxrlem  47260  hspdifhsp  47570  hspmbllem2  47581  pimgtmnf2  47668  smfsuplem1  47765