Theorem mnflt 13245

Description: Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)

Assertion

Ref	Expression
mnflt	⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)

Proof of Theorem mnflt

Step	Hyp	Ref	Expression
1		eqid 2761	. . . 4 ⊢ -∞ = -∞
2		olc 882	. . . 4 ⊢ ((-∞ = -∞ ∧ 𝐴 ∈ ℝ) → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
3	1, 2	mpan 703	. . 3 ⊢ (𝐴 ∈ ℝ → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
4	3	olcd 888	. 2 ⊢ (𝐴 ∈ ℝ → ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ))))
5		mnfxr 11359	. . 3 ⊢ -∞ ∈ ℝ*
6		rexr 11348	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
7		ltxr 13237	. . 3 ⊢ ((-∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
8	5, 6, 7	sylancr 599	. 2 ⊢ (𝐴 ∈ ℝ → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
9	4, 8	mpbird 260	1 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145   class class class wbr 5103  ℝcr 11192   <_ℝ cltrr 11197  +∞cpnf 11333  -∞cmnf 11334  ℝ^*cxr 11335   < clt 11336

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-cnex 11249

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341

This theorem is used by:  mnfltd  13246  mnflt0  13247  mnfltxr  13249  xrlttri  13261  xrlttr  13262  xrrebnd  13291  xrre3  13294  qbtwnxr  13323  xrsupsslem  13430  xrub  13435  elico2  13534  elicc2  13535  ioomax  13546  elioomnf  13568  difreicc  13608  icopnfcld  25079  iocmnfcld  25080  xrtgioo  25119  bndth  25272  mbfmax  25963  itg2seq  26056  ellogdm  26960  esumcvgsum  34713  dya2iocbrsiga  34900  dya2icobrsiga  34901  orvclteel  35098  iooelexlt  38265  itg2addnclem  38569  asindmre  38601  dvasin  38602  dvacos  38603  rfcnpre4  46020  infrpge  46332  infxr  46347  infxrunb2  46348  infleinflem2  46351  icccncfext  46866  fouriersw  47210  pimgtmnff  47701  iccpartigtl  48474