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