Theorem ltpnf 13140

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 2725	. . . 4 ⊢ +∞ = +∞
2		orc 865	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 689	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 872	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11297	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11305	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13135	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 584	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 256	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   = wceq 1533   ∈ wcel 2098   class class class wbr 5149  ℝcr 11144   <_ℝ cltrr 11149  +∞cpnf 11282  -∞cmnf 11283  ℝ^*cxr 11284   < clt 11285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11201

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-xp 5684  df-pnf 11287  df-xr 11289  df-ltxr 11290

This theorem is referenced by:  ltpnfd  13141  0ltpnf  13142  xrlttri  13158  xrlttr  13159  xrrebnd  13187  xrre  13188  qbtwnxr  13219  xnn0lem1lt  13263  xrinfmsslem  13327  xrub  13331  supxrunb1  13338  supxrunb2  13339  dfrp2  13413  elioc2  13427  elicc2  13429  ioomax  13439  ioopos  13441  elioopnf  13460  elicopnf  13462  difreicc  13501  hashbnd  14336  hashv01gt1  14345  fprodge0  15978  fprodge1  15980  pcadd  16866  ramubcl  16995  rge0srg  21393  mnfnei  23174  icopnfcld  24733  iocmnfcld  24734  xrtgioo  24771  xrge0tsms  24799  ioombl1lem4  25539  icombl1  25541  mbfmax  25627  upgrfi  28981  topnfbey  30356  isblo3i  30688  htthlem  30804  xlt2addrd  32615  fsumrp0cl  32845  xrge0tsmsd  32866  pnfinf  32988  xrge0slmod  33164  xrge0iifcnv  33667  xrge0iifiso  33669  xrge0iifhom  33671  lmxrge0  33686  esumcst  33815  esumcvgre  33843  voliune  33981  volfiniune  33982  sxbrsigalem0  34024  orvcgteel  34220  dstfrvclim1  34230  itg2addnclem2  37278  asindmre  37309  dvasin  37310  dvacos  37311  rfcnpre3  44539  supxrgere  44855  supxrgelem  44859  xrlexaddrp  44874  infxr  44889  xrpnf  45008  limsupre  45169  limsuppnflem  45238  liminflelimsupuz  45313  limsupub2  45340  icccncfext  45415  fourierdlem111  45745  fourierdlem113  45747  fouriersw  45759  sge0iunmptlemre  45943  sge0rpcpnf  45949  sge0xaddlem1  45961  meaiuninclem  46008  hoidmvlelem5  46127  ovolval5lem1  46180  pimltpnff  46231  iccpartiltu  46901  itscnhlinecirc02p  48046