Theorem mnfltd 13137

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

Syntax hints:   → wi 4   ∈ wcel 2099   class class class wbr 5148  ℝcr 11138  -∞cmnf 11277   < clt 11279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-cnex 11195

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-xp 5684  df-pnf 11281  df-mnf 11282  df-xr 11283  df-ltxr 11284

This theorem is referenced by:  qbtwnxr  13212  xltnegi  13228  supxrre  13339  infxrre  13348  caucvgrlem  15652  tgioo  24725  reconnlem1  24755  reconnlem2  24756  ovoliunlem1  25444  ovoliun  25447  ioombl1lem2  25501  ismbf3d  25596  dvferm1lem  25929  dvferm2lem  25931  degltlem1  26021  ply1divex  26085  dvdsq1p  26110  logdmnrp  26588  atans2  26876  ply1degltel  33265  ply1degleel  33266  ply1degltlss  33267  ply1degltdimlem  33320  areacirclem5  37185  aks6d1c5lem3  41608  infleinflem2  44753  xrralrecnnge  44772  icoopn  44910  icomnfinre  44937  ressiocsup  44939  ressioosup  44940  preimaiocmnf  44946  limciccioolb  45009  limsupre  45029  limcresioolb  45031  limcleqr  45032  xlimmnfvlem1  45220  fourierdlem32  45527  fourierdlem46  45540  fourierdlem48  45542  fourierdlem49  45543  fourierdlem74  45568  fourierdlem88  45582  fourierdlem95  45589  fourierdlem103  45597  fourierdlem104  45598  fouriersw  45619  ioorrnopnxrlem  45694  hspdifhsp  46004  hspmbllem2  46015  pimgtmnf2  46102  smfsuplem1  46199