Theorem blcntr 24337

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 13010	. . 3 ⊢ (𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ*)
2		rpgt0 13013	. . 3 ⊢ (𝑅 ∈ ℝ+ → 0 < 𝑅)
3	1, 2	jca 511	. 2 ⊢ (𝑅 ∈ ℝ+ → (𝑅 ∈ ℝ* ∧ 0 < 𝑅))
4		xblcntr 24335	. 2 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ (𝑅 ∈ ℝ* ∧ 0 < 𝑅)) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅))
5	3, 4	syl3an3 1165	1 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2107   class class class wbr 5116  ‘cfv 6527  (class class class)co 7399  0cc0 11121  ℝ^*cxr 11260   < clt 11261  ℝ⁺crp 13000  ∞Metcxmet 21285  ballcbl 21287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5263  ax-nul 5273  ax-pow 5332  ax-pr 5399  ax-un 7723  ax-cnex 11177  ax-resscn 11178

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-iun 4966  df-br 5117  df-opab 5179  df-mpt 5199  df-id 5545  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6480  df-fun 6529  df-fn 6530  df-f 6531  df-fv 6535  df-ov 7402  df-oprab 7403  df-mpo 7404  df-1st 7982  df-2nd 7983  df-map 8836  df-xr 11265  df-rp 13001  df-psmet 21292  df-xmet 21293  df-bl 21295

This theorem is referenced by:  bln0  24339  unirnbl  24344  blssex  24351  neibl  24425  blnei  24426  metss  24432  methaus  24444  met1stc  24445  met2ndci  24446  metrest  24448  prdsxmslem2  24453  metcnp3  24464  tgioo  24720  zdis  24741  metnrmlem2  24785  cnllycmp  24891  nmhmcn  25056  lmmbr  25195  cfilfcls  25211  iscmet3lem2  25229  caubl  25245  caublcls  25246  flimcfil  25251  ellimc3  25817  ulmdvlem1  26346  efopn  26603  logtayl  26605  xrlimcnp  26914  efrlim  26915  efrlimOLD  26916  lgamucov  26984  cnllysconn  35188  poimirlem30  37595  blbnd  37732  heibor1lem  37754  heibor1  37755  binomcxplemnotnn0  44306  hoiqssbl  46584