Theorem mnfltd 13187

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5166  ℝcr 11183  -∞cmnf 11322   < clt 11324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329

This theorem is referenced by:  qbtwnxr  13262  xltnegi  13278  supxrre  13389  infxrre  13398  caucvgrlem  15721  tgioo  24837  reconnlem1  24867  reconnlem2  24868  ovoliunlem1  25556  ovoliun  25559  ioombl1lem2  25613  ismbf3d  25708  dvferm1lem  26042  dvferm2lem  26044  degltlem1  26131  ply1divex  26196  dvdsq1p  26222  logdmnrp  26701  atans2  26992  ply1degltel  33580  ply1degleel  33581  ply1degltlss  33582  ply1degltdimlem  33635  areacirclem5  37672  aks6d1c5lem3  42094  infleinflem2  45286  xrralrecnnge  45305  icoopn  45443  icomnfinre  45470  ressiocsup  45472  ressioosup  45473  preimaiocmnf  45479  limciccioolb  45542  limsupre  45562  limcresioolb  45564  limcleqr  45565  xlimmnfvlem1  45753  fourierdlem32  46060  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem74  46101  fourierdlem88  46115  fourierdlem95  46122  fourierdlem103  46130  fourierdlem104  46131  fouriersw  46152  ioorrnopnxrlem  46227  hspdifhsp  46537  hspmbllem2  46548  pimgtmnf2  46635  smfsuplem1  46732