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  21331  mnfnei  23084  icopnfcld  24631  iocmnfcld  24632  xrtgioo  24671  xrge0tsms  24699  ioombl1lem4  25438  icombl1  25440  mbfmax  25526  upgrfi  28994  topnfbey  30371  isblo3i  30703  htthlem  30819  xlt2addrd  32655  fsumrp0cl  32935  xrge0tsmsd  32975  pnfinf  33110  xrge0slmod  33292  xrge0iifcnv  33896  xrge0iifiso  33898  xrge0iifhom  33900  lmxrge0  33915  esumcst  34026  esumcvgre  34054  voliune  34192  volfiniune  34193  sxbrsigalem0  34235  orvcgteel  34432  dstfrvclim1  34442  itg2addnclem2  37639  asindmre  37670  dvasin  37671  dvacos  37672  rfcnpre3  45000  supxrgere  45302  supxrgelem  45306  xrlexaddrp  45321  infxr  45336  xrpnf  45454  limsupre  45612  limsuppnflem  45681  liminflelimsupuz  45756  limsupub2  45783  icccncfext  45858  fourierdlem111  46188  fourierdlem113  46190  fouriersw  46202  sge0iunmptlemre  46386  sge0rpcpnf  46392  sge0xaddlem1  46404  meaiuninclem  46451  hoidmvlelem5  46570  ovolval5lem1  46623  pimltpnff  46674  iccpartiltu  47396  itscnhlinecirc02p  48747