Theorem ltpnf 11992

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 2651	. . . 4 ⊢ +∞ = +∞
2		orc 399	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 707	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 407	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 10123	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 10130	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 11987	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 695	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 247	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   = wceq 1523   ∈ wcel 2030   class class class wbr 4685  ℝcr 9973   <_ℝ cltrr 9978  +∞cpnf 10109  -∞cmnf 10110  ℝ^*cxr 10111   < clt 10112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-xp 5149  df-pnf 10114  df-xr 10116  df-ltxr 10117

This theorem is referenced by:  ltpnfd  11993  0ltpnf  11994  xrlttri  12010  xrlttr  12011  xrrebnd  12037  xrre  12038  qbtwnxr  12069  xltnegi  12085  xrinfmsslem  12176  xrub  12180  supxrunb1  12187  supxrunb2  12188  elioc2  12274  elicc2  12276  ioomax  12286  ioopos  12288  elioopnf  12305  elicopnf  12307  difreicc  12342  hashbnd  13163  hashnnn0genn0  13171  hashv01gt1  13173  fprodge0  14768  fprodge1  14770  pcadd  15640  ramubcl  15769  rge0srg  19865  mnfnei  21073  xblss2ps  22253  icopnfcld  22618  iocmnfcld  22619  blcvx  22648  xrtgioo  22656  reconnlem1  22676  xrge0tsms  22684  iccpnfhmeo  22791  ioombl1lem4  23375  icombl1  23377  uniioombllem1  23395  mbfmax  23461  ismbf3d  23466  itg2seq  23554  lhop2  23823  dvfsumlem2  23835  logccv  24454  xrlimcnp  24740  pntleme  25342  upgrfi  26031  topnfbey  27455  isblo3i  27784  htthlem  27902  xlt2addrd  29651  dfrp2  29660  fsumrp0cl  29823  pnfinf  29865  xrge0tsmsd  29913  xrge0slmod  29972  xrge0iifcnv  30107  xrge0iifiso  30109  xrge0iifhom  30111  lmxrge0  30126  esumcst  30253  esumcvgre  30281  voliune  30420  volfiniune  30421  sxbrsigalem0  30461  orvcgteel  30657  dstfrvclim1  30667  itg2addnclem2  33592  asindmre  33625  dvasin  33626  dvacos  33627  rfcnpre3  39506  supxrgere  39862  supxrgelem  39866  xrlexaddrp  39881  infxr  39896  xrpnf  40029  limsupre  40191  limsuppnfdlem  40251  limsuppnflem  40260  liminflelimsupuz  40335  icccncfext  40418  fourierdlem111  40752  fourierdlem113  40754  fouriersw  40766  sge0iunmptlemre  40950  sge0rpcpnf  40956  sge0xaddlem1  40968  meaiuninclem  41015  hoidmvlelem5  41134  ovolval5lem1  41187  pimltpnf  41237  iccpartiltu  41683