Theorem mnfltd 13050

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  ℝcr 11037  -∞cmnf 11176   < clt 11178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183

This theorem is referenced by:  qbtwnxr  13127  xltnegi  13143  supxrre  13254  infxrre  13264  caucvgrlem  15608  tgioo  24752  reconnlem1  24783  reconnlem2  24784  ovoliunlem1  25471  ovoliun  25474  ioombl1lem2  25528  ismbf3d  25623  dvferm1lem  25956  dvferm2lem  25958  degltlem1  26045  ply1divex  26110  dvdsq1p  26136  logdmnrp  26618  atans2  26909  ply1degltel  33686  ply1degleel  33687  ply1degltlss  33688  ply1degltdimlem  33799  areacirclem5  37960  aks6d1c5lem3  42504  infleinflem2  45726  xrralrecnnge  45745  icoopn  45882  icomnfinre  45909  ressiocsup  45911  ressioosup  45912  preimaiocmnf  45917  limciccioolb  45978  limsupre  45996  limcresioolb  45998  limcleqr  45999  xlimmnfvlem1  46187  fourierdlem32  46494  fourierdlem46  46507  fourierdlem48  46509  fourierdlem49  46510  fourierdlem74  46535  fourierdlem88  46549  fourierdlem95  46556  fourierdlem103  46564  fourierdlem104  46565  fouriersw  46586  ioorrnopnxrlem  46661  hspdifhsp  46971  hspmbllem2  46982  pimgtmnf2  47069  smfsuplem1  47166