Theorem ltpnf 11830

Description: Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)

Assertion

Ref	Expression
ltpnf	⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Proof of Theorem ltpnf

Step	Hyp	Ref	Expression
1		eqid 2610	. . . 4 ⊢ +∞ = +∞
2		orc 399	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 703	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 407	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 9964	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 9971	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 11825	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 693	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 246	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977   class class class wbr 4583  ℝcr 9814   <_ℝ cltrr 9819  +∞cpnf 9950  -∞cmnf 9951  ℝ^*cxr 9952   < clt 9953

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-xp 5044  df-pnf 9955  df-xr 9957  df-ltxr 9958

This theorem is referenced by:  ltpnfd  11831  0ltpnf  11832  xrlttri  11848  xrlttr  11849  xrrebnd  11873  xrre  11874  qbtwnxr  11905  xltnegi  11921  xrinfmsslem  12010  xrub  12014  supxrunb1  12021  supxrunb2  12022  elioc2  12107  elicc2  12109  ioomax  12119  ioopos  12121  elioopnf  12138  elicopnf  12140  difreicc  12175  hashbnd  12985  hashnnn0genn0  12993  hashv01gt1  12995  fprodge0  14563  fprodge1  14565  pcadd  15431  ramubcl  15560  rge0srg  19636  mnfnei  20835  xblss2ps  22016  icopnfcld  22381  iocmnfcld  22382  blcvx  22409  xrtgioo  22417  reconnlem1  22437  xrge0tsms  22445  iccpnfhmeo  22552  ioombl1lem4  23136  icombl1  23138  uniioombllem1  23155  mbfmax  23222  ismbf3d  23227  itg2seq  23315  lhop2  23582  dvfsumlem2  23594  logccv  24209  xrlimcnp  24495  pntleme  25097  upgrfi  25758  umgrafi  25851  frgrawopreglem2  26572  topnfbey  26717  isblo3i  27040  htthlem  27158  xlt2addrd  28913  dfrp2  28922  fsumrp0cl  29026  pnfinf  29068  xrge0tsmsd  29116  xrge0slmod  29175  xrge0iifcnv  29307  xrge0iifiso  29309  xrge0iifhom  29311  lmxrge0  29326  esumcst  29452  esumcvgre  29480  voliune  29619  volfiniune  29620  sxbrsigalem0  29660  orvcgteel  29856  dstfrvclim1  29866  itg2addnclem2  32632  asindmre  32665  dvasin  32666  dvacos  32667  rfcnpre3  38215  supxrgere  38490  supxrgelem  38494  xrlexaddrp  38509  infxr  38524  limsupre  38708  icccncfext  38773  fourierdlem111  39110  fourierdlem113  39112  fouriersw  39124  sge0iunmptlemre  39308  sge0rpcpnf  39314  sge0xaddlem1  39326  meaiuninclem  39373  hoidmvlelem5  39489  ovolval5lem1  39542  pimltpnf  39593  iccpartiltu  39960