Theorem mnfltd 12511

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5057  ℝcr 10528  -∞cmnf 10665   < clt 10667

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 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-xp 5554  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672

This theorem is referenced by:  qbtwnxr  12585  xltnegi  12601  supxrre  12712  infxrre  12721  caucvgrlem  15021  tgioo  23396  reconnlem1  23426  reconnlem2  23427  ovoliunlem1  24095  ovoliun  24098  ioombl1lem2  24152  ismbf3d  24247  dvferm1lem  24573  dvferm2lem  24575  degltlem1  24658  ply1divex  24722  dvdsq1p  24746  logdmnrp  25216  atans2  25501  areacirclem5  34978  infleinflem2  41628  xrralrecnnge  41651  icoopn  41790  icomnfinre  41817  ressiocsup  41819  ressioosup  41820  preimaiocmnf  41826  limciccioolb  41891  limsupre  41911  limcresioolb  41913  limcleqr  41914  xlimmnfvlem1  42102  fourierdlem32  42414  fourierdlem46  42427  fourierdlem48  42429  fourierdlem49  42430  fourierdlem74  42455  fourierdlem88  42469  fourierdlem95  42476  fourierdlem103  42484  fourierdlem104  42485  fouriersw  42506  ioorrnopnxrlem  42581  hspdifhsp  42888  hspmbllem2  42899  pimltmnf2  42969  pimgtmnf2  42982  smfsuplem1  43075