MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pnfnlt Structured version   Visualization version   GIF version

Theorem pnfnlt 12248
Description: No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.)
Assertion
Ref Expression
pnfnlt (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)

Proof of Theorem pnfnlt
StepHypRef Expression
1 pnfnre 10398 . . . . . . 7 +∞ ∉ ℝ
21neli 3104 . . . . . 6 ¬ +∞ ∈ ℝ
32intnanr 483 . . . . 5 ¬ (+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ)
43intnanr 483 . . . 4 ¬ ((+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ +∞ < 𝐴)
5 pnfnemnf 10412 . . . . . 6 +∞ ≠ -∞
65neii 3001 . . . . 5 ¬ +∞ = -∞
76intnanr 483 . . . 4 ¬ (+∞ = -∞ ∧ 𝐴 = +∞)
84, 7pm3.2ni 909 . . 3 ¬ (((+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ +∞ < 𝐴) ∨ (+∞ = -∞ ∧ 𝐴 = +∞))
92intnanr 483 . . . 4 ¬ (+∞ ∈ ℝ ∧ 𝐴 = +∞)
106intnanr 483 . . . 4 ¬ (+∞ = -∞ ∧ 𝐴 ∈ ℝ)
119, 10pm3.2ni 909 . . 3 ¬ ((+∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (+∞ = -∞ ∧ 𝐴 ∈ ℝ))
128, 11pm3.2ni 909 . 2 ¬ ((((+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ +∞ < 𝐴) ∨ (+∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((+∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (+∞ = -∞ ∧ 𝐴 ∈ ℝ)))
13 pnfxr 10410 . . 3 +∞ ∈ ℝ*
14 ltxr 12235 . . 3 ((+∞ ∈ ℝ*𝐴 ∈ ℝ*) → (+∞ < 𝐴 ↔ ((((+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ +∞ < 𝐴) ∨ (+∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((+∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (+∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
1513, 14mpan 681 . 2 (𝐴 ∈ ℝ* → (+∞ < 𝐴 ↔ ((((+∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ +∞ < 𝐴) ∨ (+∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((+∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (+∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
1612, 15mtbiri 319 1 (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wo 878   = wceq 1656  wcel 2164   class class class wbr 4873  cr 10251   < cltrr 10256  +∞cpnf 10388  -∞cmnf 10389  *cxr 10390   < clt 10391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-cnex 10308  ax-resscn 10309
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-xp 5348  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396
This theorem is referenced by:  pnfge  12250  xrltnsym  12256  xrlttr  12259  qbtwnxr  12319  xltnegi  12335  xmullem2  12383  xrinfmexpnf  12424  xrsupsslem  12425  xrinfmsslem  12426  xrub  12430  supxrpnf  12436  supxrunb1  12437  supxrunb2  12438  xrinf0  12456  lt6abl  18649  pnfnei  21395  metdstri  23024  esumpcvgval  30674  icorempt2  33737  iooelexlt  33748  iccpartigtl  42240
  Copyright terms: Public domain W3C validator