Theorem ltpnf 13056

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 2729	. . . 4 ⊢ +∞ = +∞
2		orc 867	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 691	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 874	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11196	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11204	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13051	. . 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 5102  ℝcr 11043   <_ℝ cltrr 11048  +∞cpnf 11181  -∞cmnf 11182  ℝ^*cxr 11183   < clt 11184

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 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-xp 5637  df-pnf 11186  df-xr 11188  df-ltxr 11189

This theorem is referenced by:  ltpnfd  13057  0ltpnf  13058  xrlttri  13075  xrlttr  13076  xrrebnd  13104  xrre  13105  qbtwnxr  13136  xnn0lem1lt  13180  xrinfmsslem  13244  xrub  13248  supxrunb1  13255  supxrunb2  13256  dfrp2  13331  elioc2  13346  elicc2  13348  ioomax  13359  ioopos  13361  elioopnf  13380  elicopnf  13382  difreicc  13421  hashbnd  14277  hashv01gt1  14286  fprodge0  15935  fprodge1  15937  pcadd  16836  ramubcl  16965  rge0srg  21380  mnfnei  23141  icopnfcld  24688  iocmnfcld  24689  xrtgioo  24728  xrge0tsms  24756  ioombl1lem4  25495  icombl1  25497  mbfmax  25583  upgrfi  29071  topnfbey  30448  isblo3i  30780  htthlem  30896  xlt2addrd  32732  fsumrp0cl  33005  xrge0tsmsd  33045  pnfinf  33152  xrge0slmod  33312  xrge0iifcnv  33916  xrge0iifiso  33918  xrge0iifhom  33920  lmxrge0  33935  esumcst  34046  esumcvgre  34074  voliune  34212  volfiniune  34213  sxbrsigalem0  34255  orvcgteel  34452  dstfrvclim1  34462  itg2addnclem2  37659  asindmre  37690  dvasin  37691  dvacos  37692  rfcnpre3  45020  supxrgere  45322  supxrgelem  45326  xrlexaddrp  45341  infxr  45356  xrpnf  45474  limsupre  45632  limsuppnflem  45701  liminflelimsupuz  45776  limsupub2  45803  icccncfext  45878  fourierdlem111  46208  fourierdlem113  46210  fouriersw  46222  sge0iunmptlemre  46406  sge0rpcpnf  46412  sge0xaddlem1  46424  meaiuninclem  46471  hoidmvlelem5  46590  ovolval5lem1  46643  pimltpnff  46694  iccpartiltu  47416  itscnhlinecirc02p  48767