Theorem ltpnf 11898

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 2621	. . . 4 ⊢ +∞ = +∞
2		orc 400	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 706	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 408	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 10029	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 10036	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 11893	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 693	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 247	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   = wceq 1480   ∈ wcel 1987   class class class wbr 4613  ℝcr 9879   <_ℝ cltrr 9884  +∞cpnf 10015  -∞cmnf 10016  ℝ^*cxr 10017   < clt 10018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-xp 5080  df-pnf 10020  df-xr 10022  df-ltxr 10023

This theorem is referenced by:  ltpnfd  11899  0ltpnf  11900  xrlttri  11916  xrlttr  11917  xrrebnd  11942  xrre  11943  qbtwnxr  11974  xltnegi  11990  xrinfmsslem  12081  xrub  12085  supxrunb1  12092  supxrunb2  12093  elioc2  12178  elicc2  12180  ioomax  12190  ioopos  12192  elioopnf  12209  elicopnf  12211  difreicc  12246  hashbnd  13063  hashnnn0genn0  13071  hashv01gt1  13073  fprodge0  14649  fprodge1  14651  pcadd  15517  ramubcl  15646  rge0srg  19736  mnfnei  20935  xblss2ps  22116  icopnfcld  22481  iocmnfcld  22482  blcvx  22509  xrtgioo  22517  reconnlem1  22537  xrge0tsms  22545  iccpnfhmeo  22652  ioombl1lem4  23236  icombl1  23238  uniioombllem1  23255  mbfmax  23322  ismbf3d  23327  itg2seq  23415  lhop2  23682  dvfsumlem2  23694  logccv  24309  xrlimcnp  24595  pntleme  25197  upgrfi  25882  topnfbey  27179  isblo3i  27502  htthlem  27620  xlt2addrd  29364  dfrp2  29373  fsumrp0cl  29477  pnfinf  29519  xrge0tsmsd  29567  xrge0slmod  29626  xrge0iifcnv  29758  xrge0iifiso  29760  xrge0iifhom  29762  lmxrge0  29777  esumcst  29903  esumcvgre  29931  voliune  30070  volfiniune  30071  sxbrsigalem0  30111  orvcgteel  30307  dstfrvclim1  30317  itg2addnclem2  33091  asindmre  33124  dvasin  33125  dvacos  33126  rfcnpre3  38672  supxrgere  39010  supxrgelem  39014  xrlexaddrp  39029  infxr  39044  limsupre  39274  limsuppnfdlem  39334  limsuppnflem  39343  icccncfext  39401  fourierdlem111  39738  fourierdlem113  39740  fouriersw  39752  sge0iunmptlemre  39936  sge0rpcpnf  39942  sge0xaddlem1  39954  meaiuninclem  40001  hoidmvlelem5  40117  ovolval5lem1  40170  pimltpnf  40220  iccpartiltu  40653