Theorem mnfltd 13163

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

Syntax hints:   → wi 4   ∈ wcel 2105   class class class wbr 5147  ℝcr 11151  -∞cmnf 11290   < clt 11292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-xp 5694  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297

This theorem is referenced by:  qbtwnxr  13238  xltnegi  13254  supxrre  13365  infxrre  13374  caucvgrlem  15705  tgioo  24831  reconnlem1  24861  reconnlem2  24862  ovoliunlem1  25550  ovoliun  25553  ioombl1lem2  25607  ismbf3d  25702  dvferm1lem  26036  dvferm2lem  26038  degltlem1  26125  ply1divex  26190  dvdsq1p  26216  logdmnrp  26697  atans2  26988  ply1degltel  33594  ply1degleel  33595  ply1degltlss  33596  ply1degltdimlem  33649  areacirclem5  37698  aks6d1c5lem3  42118  infleinflem2  45320  xrralrecnnge  45339  icoopn  45477  icomnfinre  45504  ressiocsup  45506  ressioosup  45507  preimaiocmnf  45513  limciccioolb  45576  limsupre  45596  limcresioolb  45598  limcleqr  45599  xlimmnfvlem1  45787  fourierdlem32  46094  fourierdlem46  46107  fourierdlem48  46109  fourierdlem49  46110  fourierdlem74  46135  fourierdlem88  46149  fourierdlem95  46156  fourierdlem103  46164  fourierdlem104  46165  fouriersw  46186  ioorrnopnxrlem  46261  hspdifhsp  46571  hspmbllem2  46582  pimgtmnf2  46669  smfsuplem1  46766