Metamath Proof Explorer


Theorem blhalf

Description: A ball of radius R / 2 is contained in a ball of radius R centered at any point inside the smaller ball. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 14-Jan-2014)

Ref Expression
Assertion blhalf ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ⊆ ( 𝑍 ( ball ‘ 𝑀 ) 𝑅 ) )

Proof

Step Hyp Ref Expression
1 simpll ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
2 simplr ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → 𝑌𝑋 )
3 simprr ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) )
4 simprl ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → 𝑅 ∈ ℝ )
5 4 rehalfcld ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → ( 𝑅 / 2 ) ∈ ℝ )
6 5 rexrd ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → ( 𝑅 / 2 ) ∈ ℝ* )
7 elbl ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ∧ ( 𝑅 / 2 ) ∈ ℝ* ) → ( 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ↔ ( 𝑍𝑋 ∧ ( 𝑌 𝑀 𝑍 ) < ( 𝑅 / 2 ) ) ) )
8 1 2 6 7 syl3anc ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → ( 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ↔ ( 𝑍𝑋 ∧ ( 𝑌 𝑀 𝑍 ) < ( 𝑅 / 2 ) ) ) )
9 3 8 mpbid ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → ( 𝑍𝑋 ∧ ( 𝑌 𝑀 𝑍 ) < ( 𝑅 / 2 ) ) )
10 9 simpld ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → 𝑍𝑋 )
11 xmetcl ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋𝑍𝑋 ) → ( 𝑌 𝑀 𝑍 ) ∈ ℝ* )
12 1 2 10 11 syl3anc ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → ( 𝑌 𝑀 𝑍 ) ∈ ℝ* )
13 9 simprd ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → ( 𝑌 𝑀 𝑍 ) < ( 𝑅 / 2 ) )
14 12 6 13 xrltled ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → ( 𝑌 𝑀 𝑍 ) ≤ ( 𝑅 / 2 ) )
15 5 recnd ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → ( 𝑅 / 2 ) ∈ ℂ )
16 4 recnd ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → 𝑅 ∈ ℂ )
17 16 2halvesd ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → ( ( 𝑅 / 2 ) + ( 𝑅 / 2 ) ) = 𝑅 )
18 15 15 17 mvlraddd ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → ( 𝑅 / 2 ) = ( 𝑅 − ( 𝑅 / 2 ) ) )
19 14 18 breqtrd ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → ( 𝑌 𝑀 𝑍 ) ≤ ( 𝑅 − ( 𝑅 / 2 ) ) )
20 blss2 ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋𝑍𝑋 ) ∧ ( ( 𝑅 / 2 ) ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ( 𝑌 𝑀 𝑍 ) ≤ ( 𝑅 − ( 𝑅 / 2 ) ) ) ) → ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ⊆ ( 𝑍 ( ball ‘ 𝑀 ) 𝑅 ) )
21 1 2 10 5 4 19 20 syl33anc ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑍 ∈ ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ) ) → ( 𝑌 ( ball ‘ 𝑀 ) ( 𝑅 / 2 ) ) ⊆ ( 𝑍 ( ball ‘ 𝑀 ) 𝑅 ) )