Theorem mnfltd 13283

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   class class class wbr 5106  ℝcr 11229  -∞cmnf 11371   < clt 11373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pow 5332  ax-pr 5396  ax-un 7778  ax-cnex 11286

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-xp 5662  df-pnf 11375  df-mnf 11376  df-xr 11377  df-ltxr 11378

This theorem is used by:  qbtwnxr  13360  xltnegi  13376  supxrre  13487  infxrre  13497  caucvgrlem  15872  tgioo  25148  reconnlem1  25179  reconnlem2  25180  ovoliunlem1  25856  ovoliun  25859  ioombl1lem2  25913  ismbf3d  26008  dvferm1lem  26337  dvferm2lem  26339  degltlem1  26423  ply1divex  26488  dvdsq1p  26514  logdmnrp  27002  atans2  27292  ply1degltel  34209  ply1degleel  34210  ply1degltlss  34211  ply1degltdimlem  34337  areacirclem5  38835  aks6d1c5lem3  43390  infleinflem2  46597  xrralrecnnge  46616  icoopn  46752  icomnfinre  46779  ressiocsup  46781  ressioosup  46782  preimaiocmnf  46787  limciccioolb  46848  limsupre  46866  limcresioolb  46868  limcleqr  46869  xlimmnfvlem1  47057  fourierdlem32  47364  fourierdlem46  47377  fourierdlem48  47379  fourierdlem49  47380  fourierdlem74  47405  fourierdlem88  47419  fourierdlem95  47426  fourierdlem103  47434  fourierdlem104  47435  fouriersw  47456  ioorrnopnxrlem  47531  hspdifhsp  47841  hspmbllem2  47852  pimgtmnf2  47939  smfsuplem1  48036