Theorem ltpnf 13046

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 2737	. . . 4 ⊢ +∞ = +∞
2		orc 868	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 692	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 875	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11190	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11198	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13041	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
8	5, 6, 7	sylancl 587	. 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))))
9	4, 8	mpbird 257	1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114   class class class wbr 5100  ℝcr 11037   <_ℝ cltrr 11042  +∞cpnf 11175  -∞cmnf 11176  ℝ^*cxr 11177   < clt 11178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-pnf 11180  df-xr 11182  df-ltxr 11183

This theorem is referenced by:  ltpnfd  13047  0ltpnf  13048  xrlttri  13065  xrlttr  13066  xrrebnd  13095  xrre  13096  qbtwnxr  13127  xnn0lem1lt  13171  xrinfmsslem  13235  xrub  13239  supxrunb1  13246  supxrunb2  13247  dfrp2  13322  elioc2  13337  elicc2  13339  ioomax  13350  ioopos  13352  elioopnf  13371  elicopnf  13373  difreicc  13412  hashbnd  14271  hashv01gt1  14280  fprodge0  15928  fprodge1  15930  pcadd  16829  ramubcl  16958  rge0srg  21405  mnfnei  23177  icopnfcld  24723  iocmnfcld  24724  xrtgioo  24763  xrge0tsms  24791  ioombl1lem4  25530  icombl1  25532  mbfmax  25618  upgrfi  29176  topnfbey  30556  isblo3i  30889  htthlem  31005  xlt2addrd  32850  fsumrp0cl  33114  xrge0tsmsd  33167  pnfinf  33277  xrge0slmod  33441  xrge0iifcnv  34111  xrge0iifiso  34113  xrge0iifhom  34115  lmxrge0  34130  esumcst  34241  esumcvgre  34269  voliune  34407  volfiniune  34408  sxbrsigalem0  34449  orvcgteel  34646  dstfrvclim1  34656  itg2addnclem2  37923  asindmre  37954  dvasin  37955  dvacos  37956  rfcnpre3  45393  supxrgere  45692  supxrgelem  45696  xrlexaddrp  45711  infxr  45725  xrpnf  45843  limsupre  45999  limsuppnflem  46068  liminflelimsupuz  46143  limsupub2  46170  icccncfext  46245  fourierdlem111  46575  fourierdlem113  46577  fouriersw  46589  sge0iunmptlemre  46773  sge0rpcpnf  46779  sge0xaddlem1  46791  meaiuninclem  46838  hoidmvlelem5  46957  ovolval5lem1  47010  pimltpnff  47061  iccpartiltu  47782  itscnhlinecirc02p  49145