Theorem ltpnf 13065

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 11185	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11193	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13060	. . 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 5086  ℝcr 11031   <_ℝ cltrr 11036  +∞cpnf 11170  -∞cmnf 11171  ℝ^*cxr 11172   < clt 11173

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 5232  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-cnex 11088

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5631  df-pnf 11175  df-xr 11177  df-ltxr 11178

This theorem is referenced by:  ltpnfd  13066  0ltpnf  13067  xrlttri  13084  xrlttr  13085  xrrebnd  13114  xrre  13115  qbtwnxr  13146  xnn0lem1lt  13190  xrinfmsslem  13254  xrub  13258  supxrunb1  13265  supxrunb2  13266  dfrp2  13341  elioc2  13356  elicc2  13358  ioomax  13369  ioopos  13371  elioopnf  13390  elicopnf  13392  difreicc  13431  hashbnd  14292  hashv01gt1  14301  fprodge0  15952  fprodge1  15954  pcadd  16854  ramubcl  16983  rge0srg  21431  mnfnei  23199  icopnfcld  24745  iocmnfcld  24746  xrtgioo  24785  xrge0tsms  24813  ioombl1lem4  25541  icombl1  25543  mbfmax  25629  upgrfi  29177  topnfbey  30557  isblo3i  30890  htthlem  31006  xlt2addrd  32850  fsumrp0cl  33099  xrge0tsmsd  33152  pnfinf  33262  xrge0slmod  33426  xrge0iifcnv  34096  xrge0iifiso  34098  xrge0iifhom  34100  lmxrge0  34115  esumcst  34226  esumcvgre  34254  voliune  34392  volfiniune  34393  sxbrsigalem0  34434  orvcgteel  34631  dstfrvclim1  34641  itg2addnclem2  38010  asindmre  38041  dvasin  38042  dvacos  38043  rfcnpre3  45485  supxrgere  45784  supxrgelem  45788  xrlexaddrp  45803  infxr  45817  xrpnf  45934  limsupre  46090  limsuppnflem  46159  liminflelimsupuz  46234  limsupub2  46261  icccncfext  46336  fourierdlem111  46666  fourierdlem113  46668  fouriersw  46680  sge0iunmptlemre  46864  sge0rpcpnf  46870  sge0xaddlem1  46882  meaiuninclem  46929  hoidmvlelem5  47048  ovolval5lem1  47101  pimltpnff  47152  iccpartiltu  47897  itscnhlinecirc02p  49276