Theorem pnfnlt 13040

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 11171	. . . . . . 7 ⊢ +∞ ∉ ℝ
2	1	neli 3036	. . . . . 6 ⊢ ¬ +∞ ∈ ℝ
3	2	intnanr 487	. . . . 5 ⊢ ¬ (+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ)
4	3	intnanr 487	. . . 4 ⊢ ¬ ((+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ +∞ <ℝ 𝐴)
5		pnfnemnf 11185	. . . . . 6 ⊢ +∞ ≠ -∞
6	5	neii 2932	. . . . 5 ⊢ ¬ +∞ = -∞
7	6	intnanr 487	. . . 4 ⊢ ¬ (+∞ = -∞ ∧ 𝐴 = +∞)
8	4, 7	pm3.2ni 880	. . 3 ⊢ ¬ (((+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ +∞ <ℝ 𝐴) ∨ (+∞ = -∞ ∧ 𝐴 = +∞))
9	2	intnanr 487	. . . 4 ⊢ ¬ (+∞ ∈ ℝ ∧ 𝐴 = +∞)
10	6	intnanr 487	. . . 4 ⊢ ¬ (+∞ = -∞ ∧ 𝐴 ∈ ℝ)
11	9, 10	pm3.2ni 880	. . 3 ⊢ ¬ ((+∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (+∞ = -∞ ∧ 𝐴 ∈ ℝ))
12	8, 11	pm3.2ni 880	. 2 ⊢ ¬ ((((+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ +∞ <ℝ 𝐴) ∨ (+∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((+∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (+∞ = -∞ ∧ 𝐴 ∈ ℝ)))
13		pnfxr 11184	. . 3 ⊢ +∞ ∈ ℝ*
14		ltxr 13027	. . 3 ⊢ ((+∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (+∞ < 𝐴 ↔ ((((+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ +∞ <ℝ 𝐴) ∨ (+∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((+∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (+∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
15	13, 14	mpan 690	. 2 ⊢ (𝐴 ∈ ℝ* → (+∞ < 𝐴 ↔ ((((+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ +∞ <ℝ 𝐴) ∨ (+∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((+∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (+∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
16	12, 15	mtbiri 327	1 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2113   class class class wbr 5096  ℝcr 11023   <_ℝ cltrr 11028  +∞cpnf 11161  -∞cmnf 11162  ℝ^*cxr 11163   < clt 11164

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-resscn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-xp 5628  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169

This theorem is referenced by:  pnfge  13042  xrltnsym  13049  xrlttr  13052  qbtwnxr  13113  xltnegi  13129  xmullem2  13178  xrinfmexpnf  13219  xrsupsslem  13220  xrinfmsslem  13221  xrub  13225  supxrpnf  13231  supxrunb1  13232  supxrunb2  13233  xrinf0  13252  lt6abl  19822  pnfnei  23162  metdstri  24794  esumpcvgval  34184  icorempo  37495  iooelexlt  37506  iccpartigtl  47611