Theorem ltpnf 13289

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 2763	. . . 4 ⊢ +∞ = +∞
2		orc 881	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 704	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 888	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11394	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11402	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13284	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 598	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 260	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2147   class class class wbr 5108  ℝcr 11238   <_ℝ cltrr 11243  +∞cpnf 11379  -∞cmnf 11380  ℝ^*cxr 11381   < clt 11382

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-cnex 11295

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-xp 5664  df-pnf 11384  df-xr 11386  df-ltxr 11387

This theorem is used by:  ltpnfd  13290  0ltpnf  13291  xrlttri  13308  xrlttr  13309  xrrebnd  13338  xrre  13339  qbtwnxr  13370  xnn0lem1lt  13414  xrinfmsslem  13478  xrub  13482  supxrunb1  13489  supxrunb2  13490  dfrp2  13565  elioc2  13580  elicc2  13582  ioomax  13593  ioopos  13595  elioopnf  13614  elicopnf  13616  difreicc  13655  hashbnd  14521  hashv01gt1  14530  fprodge0  16204  fprodge1  16206  pcadd  17111  ramubcl  17240  rge0srg  21798  mnfnei  23594  icopnfcld  25141  iocmnfcld  25142  xrtgioo  25181  xrge0tsms  25209  ioombl1lem4  25937  icombl1  25939  mbfmax  26025  upgrfi  29726  topnfbey  31127  isblo3i  31460  htthlem  31576  xlt2addrd  33447  fsumrp0cl  33681  xrge0tsmsd  33733  pnfinf  33843  xrge0slmod  34013  xrge0iifcnv  34676  xrge0iifiso  34678  xrge0iifhom  34680  lmxrge0  34695  esumcst  34806  esumcvgre  34834  voliune  34973  volfiniune  34974  sxbrsigalem0  35014  orvcgteel  35211  dstfrvclim1  35221  itg2addnclem2  38858  asindmre  38889  dvasin  38890  dvacos  38891  rfcnpre3  46324  supxrgere  46618  supxrgelem  46622  xrlexaddrp  46637  infxr  46651  xrpnf  46768  limsupre  46924  limsuppnflem  46993  liminflelimsupuz  47068  limsupub2  47095  icccncfext  47170  fourierdlem111  47500  fouriersw  47514  sge0iunmptlemre  47698  sge0rpcpnf  47704  sge0xaddlem1  47716  meaiuninclem  47763  hoidmvlelem5  47882  ovolval5lem1  47935  pimltpnff  47986  iccpartiltu  48777