Theorem blss2

Description: One ball is contained in another if the center-to-center distance is less than the difference of the radii. (Contributed by Mario Carneiro, 15-Jan-2014) (Revised by Mario Carneiro, 23-Aug-2015)

	Ref	Expression
Assertion	blss2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl1	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
2		simpl2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑃 ∈ 𝑋 )
3		simpl3	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑄 ∈ 𝑋 )
4		simpr1	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑅 ∈ ℝ )
5	4	rexrd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑅 ∈ ℝ* )
6		simpr2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑆 ∈ ℝ )
7	6	rexrd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → 𝑆 ∈ ℝ* )
8	6 4	resubcld	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑆 − 𝑅 ) ∈ ℝ )
9		simpr3	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) )
10		xmetlecl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( ( 𝑆 − 𝑅 ) ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ )
11	1 2 3 8 9 10	syl122anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ )
12		rexsub	⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 𝑆 +𝑒 -𝑒 𝑅 ) = ( 𝑆 − 𝑅 ) )
13	6 4 12	syl2anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑆 +𝑒 -𝑒 𝑅 ) = ( 𝑆 − 𝑅 ) )
14	9 13	breqtrrd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) )
15	1 2 3 5 7 11 14	xblss2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ≤ ( 𝑆 − 𝑅 ) ) ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) )