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

Theorem ltpnf 13042
Description: Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
ltpnf (𝐴 ∈ ℝ → 𝐴 < +∞)

Proof of Theorem ltpnf
StepHypRef Expression
1 eqid 2737 . . . 4 +∞ = +∞
2 orc 866 . . . 4 ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
31, 2mpan2 690 . . 3 (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
43olcd 873 . 2 (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 < +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5 rexr 11202 . . 3 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6 pnfxr 11210 . . 3 +∞ ∈ ℝ*
7 ltxr 13037 . . 3 ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 < +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
85, 6, 7sylancl 587 . 2 (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 < +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
94, 8mpbird 257 1 (𝐴 ∈ ℝ → 𝐴 < +∞)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wo 846   = wceq 1542  wcel 2107   class class class wbr 5106  cr 11051   < cltrr 11056  +∞cpnf 11187  -∞cmnf 11188  *cxr 11189   < clt 11190
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11108
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-xp 5640  df-pnf 11192  df-xr 11194  df-ltxr 11195
This theorem is referenced by:  ltpnfd  13043  0ltpnf  13044  xrlttri  13059  xrlttr  13060  xrrebnd  13088  xrre  13089  qbtwnxr  13120  xnn0lem1lt  13164  xrinfmsslem  13228  xrub  13232  supxrunb1  13239  supxrunb2  13240  dfrp2  13314  elioc2  13328  elicc2  13330  ioomax  13340  ioopos  13342  elioopnf  13361  elicopnf  13363  difreicc  13402  hashbnd  14237  hashv01gt1  14246  fprodge0  15877  fprodge1  15879  pcadd  16762  ramubcl  16891  rge0srg  20871  mnfnei  22575  icopnfcld  24134  iocmnfcld  24135  xrtgioo  24172  xrge0tsms  24200  ioombl1lem4  24928  icombl1  24930  mbfmax  25016  upgrfi  28045  topnfbey  29416  isblo3i  29746  htthlem  29862  xlt2addrd  31666  fsumrp0cl  31889  xrge0tsmsd  31902  pnfinf  32022  xrge0slmod  32143  xrge0iifcnv  32517  xrge0iifiso  32519  xrge0iifhom  32521  lmxrge0  32536  esumcst  32665  esumcvgre  32693  voliune  32831  volfiniune  32832  sxbrsigalem0  32874  orvcgteel  33070  dstfrvclim1  33080  itg2addnclem2  36133  asindmre  36164  dvasin  36165  dvacos  36166  rfcnpre3  43245  supxrgere  43574  supxrgelem  43578  xrlexaddrp  43593  infxr  43608  xrpnf  43728  limsupre  43889  limsuppnflem  43958  liminflelimsupuz  44033  limsupub2  44060  icccncfext  44135  fourierdlem111  44465  fourierdlem113  44467  fouriersw  44479  sge0iunmptlemre  44663  sge0rpcpnf  44669  sge0xaddlem1  44681  meaiuninclem  44728  hoidmvlelem5  44847  ovolval5lem1  44900  pimltpnff  44951  iccpartiltu  45621  itscnhlinecirc02p  46878
  Copyright terms: Public domain W3C validator