Metamath Proof Explorer


Theorem blgt0

Description: A nonempty ball implies that the radius is positive. (Contributed by NM, 11-Mar-2007) (Revised by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion blgt0 ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 < 𝑅 )

Proof

Step Hyp Ref Expression
1 0xr 0 ∈ ℝ*
2 1 a1i ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ∈ ℝ* )
3 simpl1 ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
4 simpl2 ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑃𝑋 )
5 elbl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → ( 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝐴𝑋 ∧ ( 𝑃 𝐷 𝐴 ) < 𝑅 ) ) )
6 5 simprbda ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝐴𝑋 )
7 xmetcl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝐴𝑋 ) → ( 𝑃 𝐷 𝐴 ) ∈ ℝ* )
8 3 4 6 7 syl3anc ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑃 𝐷 𝐴 ) ∈ ℝ* )
9 simpl3 ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 𝑅 ∈ ℝ* )
10 xmetge0 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝐴𝑋 ) → 0 ≤ ( 𝑃 𝐷 𝐴 ) )
11 3 4 6 10 syl3anc ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 ≤ ( 𝑃 𝐷 𝐴 ) )
12 5 simplbda ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑃 𝐷 𝐴 ) < 𝑅 )
13 2 8 9 11 12 xrlelttrd ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → 0 < 𝑅 )