Theorem mnflt 12938

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 2736	. . . 4 ⊢ -∞ = -∞
2		olc 865	. . . 4 ⊢ ((-∞ = -∞ ∧ 𝐴 ∈ ℝ) → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
3	1, 2	mpan 687	. . 3 ⊢ (𝐴 ∈ ℝ → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
4	3	olcd 871	. 2 ⊢ (𝐴 ∈ ℝ → ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ))))
5		mnfxr 11111	. . 3 ⊢ -∞ ∈ ℝ*
6		rexr 11100	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
7		ltxr 12930	. . 3 ⊢ ((-∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
8	5, 6, 7	sylancr 587	. 2 ⊢ (𝐴 ∈ ℝ → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
9	4, 8	mpbird 256	1 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   = wceq 1540   ∈ wcel 2105   class class class wbr 5086  ℝcr 10949   <_ℝ cltrr 10954  +∞cpnf 11085  -∞cmnf 11086  ℝ^*cxr 11087   < clt 11088

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pow 5302  ax-pr 5366  ax-un 7629  ax-cnex 11006

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3442  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-br 5087  df-opab 5149  df-xp 5613  df-pnf 11090  df-mnf 11091  df-xr 11092  df-ltxr 11093

This theorem is referenced by:  mnfltd  12939  mnflt0  12940  mnfltxr  12942  xrlttri  12952  xrlttr  12953  xrrebnd  12981  xrre3  12984  qbtwnxr  13013  xrsupsslem  13120  xrub  13125  elico2  13222  elicc2  13223  ioomax  13233  elioomnf  13255  difreicc  13295  icopnfcld  24011  iocmnfcld  24012  xrtgioo  24049  bndth  24201  mbfmax  24893  itg2seq  24987  ellogdm  25874  esumcvgsum  32192  dya2iocbrsiga  32378  dya2icobrsiga  32379  orvclteel  32575  iooelexlt  35610  itg2addnclem  35905  asindmre  35937  dvasin  35938  dvacos  35939  rfcnpre4  42816  infrpge  43144  infxr  43160  infxrunb2  43161  infleinflem2  43164  icccncfext  43683  fourierdlem113  44015  fouriersw  44027  pimgtmnff  44516  iccpartigtl  45145