Theorem mnflt 13154

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 2762	. . . 4 ⊢ -∞ = -∞
2		olc 881	. . . 4 ⊢ ((-∞ = -∞ ∧ 𝐴 ∈ ℝ) → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
3	1, 2	mpan 702	. . 3 ⊢ (𝐴 ∈ ℝ → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
4	3	olcd 887	. 2 ⊢ (𝐴 ∈ ℝ → ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ))))
5		mnfxr 11272	. . 3 ⊢ -∞ ∈ ℝ*
6		rexr 11261	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
7		ltxr 13146	. . 3 ⊢ ((-∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
8	5, 6, 7	sylancr 598	. 2 ⊢ (𝐴 ∈ ℝ → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
9	4, 8	mpbird 260	1 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1569   ∈ wcel 2142   class class class wbr 5108  ℝcr 11105   <_ℝ cltrr 11110  +∞cpnf 11246  -∞cmnf 11247  ℝ^*cxr 11248   < clt 11249

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-cnex 11162

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-xp 5666  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254

This theorem is used by:  mnfltd  13155  mnflt0  13156  mnfltxr  13158  xrlttri  13170  xrlttr  13171  xrrebnd  13200  xrre3  13203  qbtwnxr  13232  xrsupsslem  13339  xrub  13344  elico2  13443  elicc2  13444  ioomax  13455  elioomnf  13477  difreicc  13517  icopnfcld  24935  iocmnfcld  24936  xrtgioo  24975  bndth  25128  mbfmax  25819  itg2seq  25912  ellogdm  26815  esumcvgsum  34487  dya2iocbrsiga  34674  dya2icobrsiga  34675  orvclteel  34872  iooelexlt  38036  itg2addnclem  38350  asindmre  38382  dvasin  38383  dvacos  38384  rfcnpre4  45782  infrpge  46095  infxr  46110  infxrunb2  46111  infleinflem2  46114  icccncfext  46629  fouriersw  46973  pimgtmnff  47464  iccpartigtl  48200