Theorem mnfltd 13138

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5119  ℝcr 11126  -∞cmnf 11265   < clt 11267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-xp 5660  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272

This theorem is referenced by:  qbtwnxr  13214  xltnegi  13230  supxrre  13341  infxrre  13351  caucvgrlem  15687  tgioo  24733  reconnlem1  24764  reconnlem2  24765  ovoliunlem1  25453  ovoliun  25456  ioombl1lem2  25510  ismbf3d  25605  dvferm1lem  25938  dvferm2lem  25940  degltlem1  26027  ply1divex  26092  dvdsq1p  26118  logdmnrp  26600  atans2  26891  ply1degltel  33550  ply1degleel  33551  ply1degltlss  33552  ply1degltdimlem  33608  areacirclem5  37682  aks6d1c5lem3  42096  infleinflem2  45346  xrralrecnnge  45365  icoopn  45502  icomnfinre  45529  ressiocsup  45531  ressioosup  45532  preimaiocmnf  45537  limciccioolb  45598  limsupre  45618  limcresioolb  45620  limcleqr  45621  xlimmnfvlem1  45809  fourierdlem32  46116  fourierdlem46  46129  fourierdlem48  46131  fourierdlem49  46132  fourierdlem74  46157  fourierdlem88  46171  fourierdlem95  46178  fourierdlem103  46186  fourierdlem104  46187  fouriersw  46208  ioorrnopnxrlem  46283  hspdifhsp  46593  hspmbllem2  46604  pimgtmnf2  46691  smfsuplem1  46788