Theorem ltpnf 13022

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 11161	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
6		pnfxr 11169	. . 3 ⊢ +∞ ∈ ℝ*
7		ltxr 13017	. . 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 5092  ℝcr 11008   <_ℝ cltrr 11013  +∞cpnf 11146  -∞cmnf 11147  ℝ^*cxr 11148   < clt 11149

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 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-xp 5625  df-pnf 11151  df-xr 11153  df-ltxr 11154

This theorem is referenced by:  ltpnfd  13023  0ltpnf  13024  xrlttri  13041  xrlttr  13042  xrrebnd  13070  xrre  13071  qbtwnxr  13102  xnn0lem1lt  13146  xrinfmsslem  13210  xrub  13214  supxrunb1  13221  supxrunb2  13222  dfrp2  13297  elioc2  13312  elicc2  13314  ioomax  13325  ioopos  13327  elioopnf  13346  elicopnf  13348  difreicc  13387  hashbnd  14243  hashv01gt1  14252  fprodge0  15900  fprodge1  15902  pcadd  16801  ramubcl  16930  rge0srg  21345  mnfnei  23106  icopnfcld  24653  iocmnfcld  24654  xrtgioo  24693  xrge0tsms  24721  ioombl1lem4  25460  icombl1  25462  mbfmax  25548  upgrfi  29036  topnfbey  30413  isblo3i  30745  htthlem  30861  xlt2addrd  32702  fsumrp0cl  32975  xrge0tsmsd  33015  pnfinf  33125  xrge0slmod  33285  xrge0iifcnv  33900  xrge0iifiso  33902  xrge0iifhom  33904  lmxrge0  33919  esumcst  34030  esumcvgre  34058  voliune  34196  volfiniune  34197  sxbrsigalem0  34239  orvcgteel  34436  dstfrvclim1  34446  itg2addnclem2  37652  asindmre  37683  dvasin  37684  dvacos  37685  rfcnpre3  45011  supxrgere  45313  supxrgelem  45317  xrlexaddrp  45332  infxr  45346  xrpnf  45464  limsupre  45622  limsuppnflem  45691  liminflelimsupuz  45766  limsupub2  45793  icccncfext  45868  fourierdlem111  46198  fourierdlem113  46200  fouriersw  46212  sge0iunmptlemre  46396  sge0rpcpnf  46402  sge0xaddlem1  46414  meaiuninclem  46461  hoidmvlelem5  46580  ovolval5lem1  46633  pimltpnff  46684  iccpartiltu  47406  itscnhlinecirc02p  48770