Theorem mnfltd 13150

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

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5110  ℝcr 11100  -∞cmnf 11242   < clt 11244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-cnex 11157

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-xp 5669  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249

This theorem is referenced by:  qbtwnxr  13227  xltnegi  13243  supxrre  13354  infxrre  13364  caucvgrlem  15726  tgioo  24934  reconnlem1  24965  reconnlem2  24966  ovoliunlem1  25642  ovoliun  25645  ioombl1lem2  25699  ismbf3d  25794  dvferm1lem  26124  dvferm2lem  26126  degltlem1  26210  ply1divex  26275  dvdsq1p  26301  logdmnrp  26787  atans2  27077  ply1degltel  33865  ply1degleel  33866  ply1degltlss  33867  ply1degltdimlem  33993  areacirclem5  38344  aks6d1c5lem3  42885  infleinflem2  46069  xrralrecnnge  46088  icoopn  46224  icomnfinre  46251  ressiocsup  46253  ressioosup  46254  preimaiocmnf  46259  limciccioolb  46320  limsupre  46338  limcresioolb  46340  limcleqr  46341  xlimmnfvlem1  46529  fourierdlem32  46836  fourierdlem46  46849  fourierdlem48  46851  fourierdlem49  46852  fourierdlem74  46877  fourierdlem88  46891  fourierdlem95  46898  fourierdlem103  46906  fourierdlem104  46907  fouriersw  46928  ioorrnopnxrlem  47003  hspdifhsp  47313  hspmbllem2  47324  pimgtmnf2  47411  smfsuplem1  47508