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 ‘ 𝑀 ) 𝑅 ) )