Theorem ltpnf 13141

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 2736	. . . 4 ⊢ +∞ = +∞
2		orc 867	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 691	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 874	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11286	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11294	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13136	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 586	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 257	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   class class class wbr 5124  ℝcr 11133   <_ℝ cltrr 11138  +∞cpnf 11271  -∞cmnf 11272  ℝ^*cxr 11273   < clt 11274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-cnex 11190

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-xp 5665  df-pnf 11276  df-xr 11278  df-ltxr 11279

This theorem is referenced by:  ltpnfd  13142  0ltpnf  13143  xrlttri  13160  xrlttr  13161  xrrebnd  13189  xrre  13190  qbtwnxr  13221  xnn0lem1lt  13265  xrinfmsslem  13329  xrub  13333  supxrunb1  13340  supxrunb2  13341  dfrp2  13416  elioc2  13431  elicc2  13433  ioomax  13444  ioopos  13446  elioopnf  13465  elicopnf  13467  difreicc  13506  hashbnd  14359  hashv01gt1  14368  fprodge0  16014  fprodge1  16016  pcadd  16914  ramubcl  17043  rge0srg  21411  mnfnei  23164  icopnfcld  24711  iocmnfcld  24712  xrtgioo  24751  xrge0tsms  24779  ioombl1lem4  25519  icombl1  25521  mbfmax  25607  upgrfi  29075  topnfbey  30455  isblo3i  30787  htthlem  30903  xlt2addrd  32741  fsumrp0cl  33021  xrge0tsmsd  33061  pnfinf  33186  xrge0slmod  33368  xrge0iifcnv  33969  xrge0iifiso  33971  xrge0iifhom  33973  lmxrge0  33988  esumcst  34099  esumcvgre  34127  voliune  34265  volfiniune  34266  sxbrsigalem0  34308  orvcgteel  34505  dstfrvclim1  34515  itg2addnclem2  37701  asindmre  37732  dvasin  37733  dvacos  37734  rfcnpre3  45037  supxrgere  45340  supxrgelem  45344  xrlexaddrp  45359  infxr  45374  xrpnf  45492  limsupre  45650  limsuppnflem  45719  liminflelimsupuz  45794  limsupub2  45821  icccncfext  45896  fourierdlem111  46226  fourierdlem113  46228  fouriersw  46240  sge0iunmptlemre  46424  sge0rpcpnf  46430  sge0xaddlem1  46442  meaiuninclem  46489  hoidmvlelem5  46608  ovolval5lem1  46661  pimltpnff  46712  iccpartiltu  47416  itscnhlinecirc02p  48745