Theorem mnflt 12715

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 2737	. . . 4 ⊢ -∞ = -∞
2		olc 868	. . . 4 ⊢ ((-∞ = -∞ ∧ 𝐴 ∈ ℝ) → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
3	1, 2	mpan 690	. . 3 ⊢ (𝐴 ∈ ℝ → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
4	3	olcd 874	. 2 ⊢ (𝐴 ∈ ℝ → ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ))))
5		mnfxr 10890	. . 3 ⊢ -∞ ∈ ℝ*
6		rexr 10879	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
7		ltxr 12707	. . 3 ⊢ ((-∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
8	5, 6, 7	sylancr 590	. 2 ⊢ (𝐴 ∈ ℝ → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
9	4, 8	mpbird 260	1 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 847   = wceq 1543   ∈ wcel 2110   class class class wbr 5053  ℝcr 10728   <_ℝ cltrr 10733  +∞cpnf 10864  -∞cmnf 10865  ℝ^*cxr 10866   < clt 10867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-xp 5557  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872

This theorem is referenced by:  mnfltd  12716  mnflt0  12717  mnfltxr  12719  xrlttri  12729  xrlttr  12730  xrrebnd  12758  xrre3  12761  qbtwnxr  12790  xrsupsslem  12897  xrub  12902  elico2  12999  elicc2  13000  ioomax  13010  elioomnf  13032  difreicc  13072  icopnfcld  23665  iocmnfcld  23666  xrtgioo  23703  bndth  23855  mbfmax  24546  itg2seq  24640  ellogdm  25527  esumcvgsum  31768  dya2iocbrsiga  31954  dya2icobrsiga  31955  orvclteel  32151  iooelexlt  35270  itg2addnclem  35565  asindmre  35597  dvasin  35598  dvacos  35599  rfcnpre4  42250  infrpge  42563  infxr  42579  infxrunb2  42580  infleinflem2  42583  icccncfext  43103  fourierdlem113  43435  fouriersw  43447  iccpartigtl  44548