Theorem mnflt 13022

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 2731	. . . 4 ⊢ -∞ = -∞
2		olc 868	. . . 4 ⊢ ((-∞ = -∞ ∧ 𝐴 ∈ ℝ) → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
3	1, 2	mpan 690	. . 3 ⊢ (𝐴 ∈ ℝ → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
4	3	olcd 874	. 2 ⊢ (𝐴 ∈ ℝ → ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ))))
5		mnfxr 11169	. . 3 ⊢ -∞ ∈ ℝ*
6		rexr 11158	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
7		ltxr 13014	. . 3 ⊢ ((-∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
8	5, 6, 7	sylancr 587	. 2 ⊢ (𝐴 ∈ ℝ → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
9	4, 8	mpbird 257	1 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2111   class class class wbr 5091  ℝcr 11005   <_ℝ cltrr 11010  +∞cpnf 11143  -∞cmnf 11144  ℝ^*cxr 11145   < clt 11146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-cnex 11062

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-xp 5622  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151

This theorem is referenced by:  mnfltd  13023  mnflt0  13024  mnfltxr  13026  xrlttri  13038  xrlttr  13039  xrrebnd  13067  xrre3  13070  qbtwnxr  13099  xrsupsslem  13206  xrub  13211  elico2  13310  elicc2  13311  ioomax  13322  elioomnf  13344  difreicc  13384  icopnfcld  24683  iocmnfcld  24684  xrtgioo  24723  bndth  24885  mbfmax  25578  itg2seq  25671  ellogdm  26576  esumcvgsum  34099  dya2iocbrsiga  34286  dya2icobrsiga  34287  orvclteel  34484  iooelexlt  37402  itg2addnclem  37717  asindmre  37749  dvasin  37750  dvacos  37751  rfcnpre4  45077  infrpge  45396  infxr  45411  infxrunb2  45412  infleinflem2  45415  icccncfext  45931  fourierdlem113  46263  fouriersw  46275  pimgtmnff  46766  iccpartigtl  47460