Theorem mnfltd 13137

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

Syntax hints:   → wi 4   ∈ wcel 2145   class class class wbr 5104  ℝcr 11087  -∞cmnf 11229   < clt 11231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-pow 5326  ax-pr 5394  ax-un 7722  ax-cnex 11144

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-xp 5657  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236

This theorem is referenced by:  qbtwnxr  13214  xltnegi  13230  supxrre  13341  infxrre  13351  caucvgrlem  15712  tgioo  24910  reconnlem1  24941  reconnlem2  24942  ovoliunlem1  25618  ovoliun  25621  ioombl1lem2  25675  ismbf3d  25770  dvferm1lem  26100  dvferm2lem  26102  degltlem1  26186  ply1divex  26251  dvdsq1p  26277  logdmnrp  26760  atans2  27050  ply1degltel  33796  ply1degleel  33797  ply1degltlss  33798  ply1degltdimlem  33924  areacirclem5  38218  aks6d1c5lem3  42761  infleinflem2  45945  xrralrecnnge  45964  icoopn  46100  icomnfinre  46127  ressiocsup  46129  ressioosup  46130  preimaiocmnf  46135  limciccioolb  46196  limsupre  46214  limcresioolb  46216  limcleqr  46217  xlimmnfvlem1  46405  fourierdlem32  46712  fourierdlem46  46725  fourierdlem48  46727  fourierdlem49  46728  fourierdlem74  46753  fourierdlem88  46767  fourierdlem95  46774  fourierdlem103  46782  fourierdlem104  46783  fouriersw  46804  ioorrnopnxrlem  46879  hspdifhsp  47189  hspmbllem2  47200  pimgtmnf2  47287  smfsuplem1  47384