Theorem ltpnf 11954

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 2622	. . . 4 ⊢ +∞ = +∞
2		orc 400	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 707	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 408	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 10085	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 10092	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 11949	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 694	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 247	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   = wceq 1483   ∈ wcel 1990   class class class wbr 4653  ℝcr 9935   <_ℝ cltrr 9940  +∞cpnf 10071  -∞cmnf 10072  ℝ^*cxr 10073   < clt 10074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-xp 5120  df-pnf 10076  df-xr 10078  df-ltxr 10079

This theorem is referenced by:  ltpnfd  11955  0ltpnf  11956  xrlttri  11972  xrlttr  11973  xrrebnd  11999  xrre  12000  qbtwnxr  12031  xltnegi  12047  xrinfmsslem  12138  xrub  12142  supxrunb1  12149  supxrunb2  12150  elioc2  12236  elicc2  12238  ioomax  12248  ioopos  12250  elioopnf  12267  elicopnf  12269  difreicc  12304  hashbnd  13123  hashnnn0genn0  13131  hashv01gt1  13133  fprodge0  14724  fprodge1  14726  pcadd  15593  ramubcl  15722  rge0srg  19817  mnfnei  21025  xblss2ps  22206  icopnfcld  22571  iocmnfcld  22572  blcvx  22601  xrtgioo  22609  reconnlem1  22629  xrge0tsms  22637  iccpnfhmeo  22744  ioombl1lem4  23329  icombl1  23331  uniioombllem1  23349  mbfmax  23416  ismbf3d  23421  itg2seq  23509  lhop2  23778  dvfsumlem2  23790  logccv  24409  xrlimcnp  24695  pntleme  25297  upgrfi  25986  topnfbey  27325  isblo3i  27656  htthlem  27774  xlt2addrd  29523  dfrp2  29532  fsumrp0cl  29695  pnfinf  29737  xrge0tsmsd  29785  xrge0slmod  29844  xrge0iifcnv  29979  xrge0iifiso  29981  xrge0iifhom  29983  lmxrge0  29998  esumcst  30125  esumcvgre  30153  voliune  30292  volfiniune  30293  sxbrsigalem0  30333  orvcgteel  30529  dstfrvclim1  30539  itg2addnclem2  33462  asindmre  33495  dvasin  33496  dvacos  33497  rfcnpre3  39192  supxrgere  39549  supxrgelem  39553  xrlexaddrp  39568  infxr  39583  limsupre  39873  limsuppnfdlem  39933  limsuppnflem  39942  liminflelimsupuz  40017  icccncfext  40100  fourierdlem111  40434  fourierdlem113  40436  fouriersw  40448  sge0iunmptlemre  40632  sge0rpcpnf  40638  sge0xaddlem1  40650  meaiuninclem  40697  hoidmvlelem5  40813  ovolval5lem1  40866  pimltpnf  40916  iccpartiltu  41358