Theorem mnfltd 13110

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

Syntax hints:   → wi 4   ∈ wcel 2104   class class class wbr 5149  ℝcr 11113  -∞cmnf 11252   < clt 11254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7729  ax-cnex 11170

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-xp 5683  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259

This theorem is referenced by:  qbtwnxr  13185  xltnegi  13201  supxrre  13312  infxrre  13321  caucvgrlem  15625  tgioo  24534  reconnlem1  24564  reconnlem2  24565  ovoliunlem1  25253  ovoliun  25256  ioombl1lem2  25310  ismbf3d  25405  dvferm1lem  25735  dvferm2lem  25737  degltlem1  25824  ply1divex  25888  dvdsq1p  25912  logdmnrp  26383  atans2  26670  ply1degltel  32938  ply1degleel  32939  ply1degltlss  32940  ply1degltdimlem  32993  areacirclem5  36885  infleinflem2  44381  xrralrecnnge  44400  icoopn  44538  icomnfinre  44565  ressiocsup  44567  ressioosup  44568  preimaiocmnf  44574  limciccioolb  44637  limsupre  44657  limcresioolb  44659  limcleqr  44660  xlimmnfvlem1  44848  fourierdlem32  45155  fourierdlem46  45168  fourierdlem48  45170  fourierdlem49  45171  fourierdlem74  45196  fourierdlem88  45210  fourierdlem95  45217  fourierdlem103  45225  fourierdlem104  45226  fouriersw  45247  ioorrnopnxrlem  45322  hspdifhsp  45632  hspmbllem2  45643  pimgtmnf2  45730  smfsuplem1  45827