This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssblps

Description: The size of a ball increases monotonically with its radius. (Contributed by NM, 20-Sep-2007) (Revised by Mario Carneiro, 24-Aug-2015) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion ssblps ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ S ∈ ℝ * ∧ R ≤ S → P ball ⁡ D R ⊆ P ball ⁡ D S

Proof

Step Hyp Ref Expression
1 simp1l ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ S ∈ ℝ * ∧ R ≤ S → D ∈ PsMet ⁡ X
2 simp1r ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ S ∈ ℝ * ∧ R ≤ S → P ∈ X
3 simp2l ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ S ∈ ℝ * ∧ R ≤ S → R ∈ ℝ *
4 simp2r ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ S ∈ ℝ * ∧ R ≤ S → S ∈ ℝ *
5 psmet0 ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X → P D P = 0
6 5 3ad2ant1 ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ S ∈ ℝ * ∧ R ≤ S → P D P = 0
7 0re ⊢ 0 ∈ ℝ
8 6 7 eqeltrdi ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ S ∈ ℝ * ∧ R ≤ S → P D P ∈ ℝ
9 simp3 ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ S ∈ ℝ * ∧ R ≤ S → R ≤ S
10 xsubge0 ⊢ S ∈ ℝ * ∧ R ∈ ℝ * → 0 ≤ S + 𝑒 − R ↔ R ≤ S
11 4 3 10 syl2anc ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ S ∈ ℝ * ∧ R ≤ S → 0 ≤ S + 𝑒 − R ↔ R ≤ S
12 9 11 mpbird ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ S ∈ ℝ * ∧ R ≤ S → 0 ≤ S + 𝑒 − R
13 6 12 eqbrtrd ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ S ∈ ℝ * ∧ R ≤ S → P D P ≤ S + 𝑒 − R
14 1 2 2 3 4 8 13 xblss2ps ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ S ∈ ℝ * ∧ R ≤ S → P ball ⁡ D R ⊆ P ball ⁡ D S