Theorem mnfltd 13054

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5110  ℝcr 11059  -∞cmnf 11196   < clt 11198

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11116

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-xp 5644  df-pnf 11200  df-mnf 11201  df-xr 11202  df-ltxr 11203

This theorem is referenced by:  qbtwnxr  13129  xltnegi  13145  supxrre  13256  infxrre  13265  caucvgrlem  15569  tgioo  24196  reconnlem1  24226  reconnlem2  24227  ovoliunlem1  24903  ovoliun  24906  ioombl1lem2  24960  ismbf3d  25055  dvferm1lem  25385  dvferm2lem  25387  degltlem1  25474  ply1divex  25538  dvdsq1p  25562  logdmnrp  26033  atans2  26318  ply1degltel  32365  ply1degltlss  32366  ply1degltdimlem  32404  areacirclem5  36243  infleinflem2  43726  xrralrecnnge  43745  icoopn  43883  icomnfinre  43910  ressiocsup  43912  ressioosup  43913  preimaiocmnf  43919  limciccioolb  43982  limsupre  44002  limcresioolb  44004  limcleqr  44005  xlimmnfvlem1  44193  fourierdlem32  44500  fourierdlem46  44513  fourierdlem48  44515  fourierdlem49  44516  fourierdlem74  44541  fourierdlem88  44555  fourierdlem95  44562  fourierdlem103  44570  fourierdlem104  44571  fouriersw  44592  ioorrnopnxrlem  44667  hspdifhsp  44977  hspmbllem2  44988  pimgtmnf2  45075  smfsuplem1  45172