Theorem ltpnf 13034

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 2736	. . . 4 ⊢ +∞ = +∞
2		orc 867	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
3	1, 2	mpan2 691	. . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))
4	3	olcd 874	. 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))
5		rexr 11178	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11186	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13029	. . 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 1541   ∈ wcel 2113   class class class wbr 5098  ℝcr 11025   <_ℝ cltrr 11030  +∞cpnf 11163  -∞cmnf 11164  ℝ^*cxr 11165   < clt 11166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-pnf 11168  df-xr 11170  df-ltxr 11171

This theorem is referenced by:  ltpnfd  13035  0ltpnf  13036  xrlttri  13053  xrlttr  13054  xrrebnd  13083  xrre  13084  qbtwnxr  13115  xnn0lem1lt  13159  xrinfmsslem  13223  xrub  13227  supxrunb1  13234  supxrunb2  13235  dfrp2  13310  elioc2  13325  elicc2  13327  ioomax  13338  ioopos  13340  elioopnf  13359  elicopnf  13361  difreicc  13400  hashbnd  14259  hashv01gt1  14268  fprodge0  15916  fprodge1  15918  pcadd  16817  ramubcl  16946  rge0srg  21393  mnfnei  23165  icopnfcld  24711  iocmnfcld  24712  xrtgioo  24751  xrge0tsms  24779  ioombl1lem4  25518  icombl1  25520  mbfmax  25606  upgrfi  29164  topnfbey  30544  isblo3i  30876  htthlem  30992  xlt2addrd  32839  fsumrp0cl  33103  xrge0tsmsd  33155  pnfinf  33265  xrge0slmod  33429  xrge0iifcnv  34090  xrge0iifiso  34092  xrge0iifhom  34094  lmxrge0  34109  esumcst  34220  esumcvgre  34248  voliune  34386  volfiniune  34387  sxbrsigalem0  34428  orvcgteel  34625  dstfrvclim1  34635  itg2addnclem2  37873  asindmre  37904  dvasin  37905  dvacos  37906  rfcnpre3  45278  supxrgere  45578  supxrgelem  45582  xrlexaddrp  45597  infxr  45611  xrpnf  45729  limsupre  45885  limsuppnflem  45954  liminflelimsupuz  46029  limsupub2  46056  icccncfext  46131  fourierdlem111  46461  fourierdlem113  46463  fouriersw  46475  sge0iunmptlemre  46659  sge0rpcpnf  46665  sge0xaddlem1  46677  meaiuninclem  46724  hoidmvlelem5  46843  ovolval5lem1  46896  pimltpnff  46947  iccpartiltu  47668  itscnhlinecirc02p  49031