Theorem pnfnlt 12511

Description: No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.)

Assertion

Ref	Expression
pnfnlt	⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)

Proof of Theorem pnfnlt

Step	Hyp	Ref	Expression
1		pnfnre 10671	. . . . . . 7 ⊢ +∞ ∉ ℝ
2	1	neli 3093	. . . . . 6 ⊢ ¬ +∞ ∈ ℝ
3	2	intnanr 491	. . . . 5 ⊢ ¬ (+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ)
4	3	intnanr 491	. . . 4 ⊢ ¬ ((+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ +∞ <ℝ 𝐴)
5		pnfnemnf 10685	. . . . . 6 ⊢ +∞ ≠ -∞
6	5	neii 2989	. . . . 5 ⊢ ¬ +∞ = -∞
7	6	intnanr 491	. . . 4 ⊢ ¬ (+∞ = -∞ ∧ 𝐴 = +∞)
8	4, 7	pm3.2ni 878	. . 3 ⊢ ¬ (((+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ +∞ <ℝ 𝐴) ∨ (+∞ = -∞ ∧ 𝐴 = +∞))
9	2	intnanr 491	. . . 4 ⊢ ¬ (+∞ ∈ ℝ ∧ 𝐴 = +∞)
10	6	intnanr 491	. . . 4 ⊢ ¬ (+∞ = -∞ ∧ 𝐴 ∈ ℝ)
11	9, 10	pm3.2ni 878	. . 3 ⊢ ¬ ((+∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (+∞ = -∞ ∧ 𝐴 ∈ ℝ))
12	8, 11	pm3.2ni 878	. 2 ⊢ ¬ ((((+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ +∞ <ℝ 𝐴) ∨ (+∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((+∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (+∞ = -∞ ∧ 𝐴 ∈ ℝ)))
13		pnfxr 10684	. . 3 ⊢ +∞ ∈ ℝ*
14		ltxr 12498	. . 3 ⊢ ((+∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (+∞ < 𝐴 ↔ ((((+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ +∞ <ℝ 𝐴) ∨ (+∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((+∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (+∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
15	13, 14	mpan 689	. 2 ⊢ (𝐴 ∈ ℝ* → (+∞ < 𝐴 ↔ ((((+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ +∞ <ℝ 𝐴) ∨ (+∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((+∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (+∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
16	12, 15	mtbiri 330	1 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111   class class class wbr 5030  ℝcr 10525   <_ℝ cltrr 10530  +∞cpnf 10661  -∞cmnf 10662  ℝ^*cxr 10663   < clt 10664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-xp 5525  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669

This theorem is referenced by:  pnfge  12513  xrltnsym  12518  xrlttr  12521  qbtwnxr  12581  xltnegi  12597  xmullem2  12646  xrinfmexpnf  12687  xrsupsslem  12688  xrinfmsslem  12689  xrub  12693  supxrpnf  12699  supxrunb1  12700  supxrunb2  12701  xrinf0  12719  lt6abl  19008  pnfnei  21825  metdstri  23456  esumpcvgval  31447  icorempo  34768  iooelexlt  34779  iccpartigtl  43940