Theorem mnflt 13157

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 2726	. . . 4 ⊢ -∞ = -∞
2		olc 866	. . . 4 ⊢ ((-∞ = -∞ ∧ 𝐴 ∈ ℝ) → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
3	1, 2	mpan 688	. . 3 ⊢ (𝐴 ∈ ℝ → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
4	3	olcd 872	. 2 ⊢ (𝐴 ∈ ℝ → ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ))))
5		mnfxr 11321	. . 3 ⊢ -∞ ∈ ℝ*
6		rexr 11310	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
7		ltxr 13149	. . 3 ⊢ ((-∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
8	5, 6, 7	sylancr 585	. 2 ⊢ (𝐴 ∈ ℝ → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
9	4, 8	mpbird 256	1 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   = wceq 1534   ∈ wcel 2099   class class class wbr 5153  ℝcr 11157   <_ℝ cltrr 11162  +∞cpnf 11295  -∞cmnf 11296  ℝ^*cxr 11297   < clt 11298

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 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11214

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-xp 5688  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303

This theorem is referenced by:  mnfltd  13158  mnflt0  13159  mnfltxr  13161  xrlttri  13172  xrlttr  13173  xrrebnd  13201  xrre3  13204  qbtwnxr  13233  xrsupsslem  13340  xrub  13345  elico2  13442  elicc2  13443  ioomax  13453  elioomnf  13475  difreicc  13515  icopnfcld  24775  iocmnfcld  24776  xrtgioo  24813  bndth  24975  mbfmax  25669  itg2seq  25763  ellogdm  26666  esumcvgsum  33921  dya2iocbrsiga  34109  dya2icobrsiga  34110  orvclteel  34306  iooelexlt  37069  itg2addnclem  37372  asindmre  37404  dvasin  37405  dvacos  37406  rfcnpre4  44633  infrpge  44966  infxr  44982  infxrunb2  44983  infleinflem2  44986  icccncfext  45508  fourierdlem113  45840  fouriersw  45852  pimgtmnff  46343  iccpartigtl  46995