Theorem mnfltd 13256

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   class class class wbr 5102  ℝcr 11202  -∞cmnf 11344   < clt 11346

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-pnf 11348  df-mnf 11349  df-xr 11350  df-ltxr 11351

This theorem is used by:  qbtwnxr  13333  xltnegi  13349  supxrre  13460  infxrre  13470  caucvgrlem  15845  tgioo  25120  reconnlem1  25151  reconnlem2  25152  ovoliunlem1  25828  ovoliun  25831  ioombl1lem2  25885  ismbf3d  25980  dvferm1lem  26309  dvferm2lem  26311  degltlem1  26395  ply1divex  26460  dvdsq1p  26486  logdmnrp  26974  atans2  27264  ply1degltel  34172  ply1degleel  34173  ply1degltlss  34174  ply1degltdimlem  34300  areacirclem5  38723  aks6d1c5lem3  43280  infleinflem2  46475  xrralrecnnge  46494  icoopn  46630  icomnfinre  46657  ressiocsup  46659  ressioosup  46660  preimaiocmnf  46665  limciccioolb  46726  limsupre  46744  limcresioolb  46746  limcleqr  46747  xlimmnfvlem1  46935  fourierdlem32  47242  fourierdlem46  47255  fourierdlem48  47257  fourierdlem49  47258  fourierdlem74  47283  fourierdlem88  47297  fourierdlem95  47304  fourierdlem103  47312  fourierdlem104  47313  fouriersw  47334  ioorrnopnxrlem  47409  hspdifhsp  47719  hspmbllem2  47730  pimgtmnf2  47817  smfsuplem1  47914