Theorem mnflt 12357

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 2793	. . . 4 ⊢ -∞ = -∞
2		olc 863	. . . 4 ⊢ ((-∞ = -∞ ∧ 𝐴 ∈ ℝ) → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
3	1, 2	mpan 686	. . 3 ⊢ (𝐴 ∈ ℝ → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
4	3	olcd 869	. 2 ⊢ (𝐴 ∈ ℝ → ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ))))
5		mnfxr 10534	. . 3 ⊢ -∞ ∈ ℝ*
6		rexr 10522	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
7		ltxr 12349	. . 3 ⊢ ((-∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
8	5, 6, 7	sylancr 587	. 2 ⊢ (𝐴 ∈ ℝ → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
9	4, 8	mpbird 258	1 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 842   = wceq 1520   ∈ wcel 2079   class class class wbr 4956  ℝcr 10371   <_ℝ cltrr 10376  +∞cpnf 10507  -∞cmnf 10508  ℝ^*cxr 10509   < clt 10510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310  ax-cnex 10428

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-opab 5019  df-xp 5441  df-pnf 10512  df-mnf 10513  df-xr 10514  df-ltxr 10515

This theorem is referenced by:  mnfltd  12358  mnflt0  12359  mnfltxr  12361  xrlttri  12371  xrlttr  12372  xrrebnd  12400  xrre3  12403  qbtwnxr  12432  xrsupsslem  12539  xrub  12544  elico2  12639  elicc2  12640  ioomax  12650  elioomnf  12671  difreicc  12709  icopnfcld  23047  iocmnfcld  23048  xrtgioo  23085  bndth  23233  mbfmax  23921  itg2seq  24014  ellogdm  24891  esumcvgsum  30920  dya2iocbrsiga  31106  dya2icobrsiga  31107  orvclteel  31303  iooelexlt  34120  itg2addnclem  34420  asindmre  34454  dvasin  34455  dvacos  34456  rfcnpre4  40782  infrpge  41113  infxr  41129  infxrunb2  41130  infleinflem2  41133  icccncfext  41665  fourierdlem113  42000  fouriersw  42012  iccpartigtl  43019