Theorem blcntr 23562

Description: A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)

Assertion

Ref	Expression
blcntr	⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅))

Proof of Theorem blcntr

Step	Hyp	Ref	Expression
1		rpxr 12736	. . 3 ⊢ (𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ*)
2		rpgt0 12739	. . 3 ⊢ (𝑅 ∈ ℝ+ → 0 < 𝑅)
3	1, 2	jca 512	. 2 ⊢ (𝑅 ∈ ℝ+ → (𝑅 ∈ ℝ* ∧ 0 < 𝑅))
4		xblcntr 23560	. 2 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ (𝑅 ∈ ℝ* ∧ 0 < 𝑅)) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅))
5	3, 4	syl3an3 1164	1 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅))

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086   ∈ wcel 2110   class class class wbr 5079  ‘cfv 6431  (class class class)co 7269  0cc0 10870  ℝ^*cxr 11007   < clt 11008  ℝ⁺crp 12727  ∞Metcxmet 20578  ballcbl 20580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7580  ax-cnex 10926  ax-resscn 10927

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-fv 6439  df-ov 7272  df-oprab 7273  df-mpo 7274  df-1st 7822  df-2nd 7823  df-map 8598  df-xr 11012  df-rp 12728  df-psmet 20585  df-xmet 20586  df-bl 20588

This theorem is referenced by:  bln0  23564  unirnbl  23569  blssex  23576  neibl  23653  blnei  23654  metss  23660  methaus  23672  met1stc  23673  met2ndci  23674  metrest  23676  prdsxmslem2  23681  metcnp3  23692  tgioo  23955  zdis  23975  metnrmlem2  24019  cnllycmp  24115  nmhmcn  24279  lmmbr  24418  cfilfcls  24434  iscmet3lem2  24452  caubl  24468  caublcls  24469  flimcfil  24474  ellimc3  25039  ulmdvlem1  25555  efopn  25809  logtayl  25811  xrlimcnp  26114  efrlim  26115  lgamucov  26183  cnllysconn  33201  poimirlem30  35801  blbnd  35939  heibor1lem  35961  heibor1  35962  binomcxplemnotnn0  41942  hoiqssbl  44132