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 ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {A}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to 0<{R}$

Proof

Step Hyp Ref Expression
1 0xr ${⊢}0\in {ℝ}^{*}$
2 1 a1i ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {A}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to 0\in {ℝ}^{*}$
3 simpl1 ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {A}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {D}\in \mathrm{\infty Met}\left({X}\right)$
4 simpl2 ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {A}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {P}\in {X}$
5 elbl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\to \left({A}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)↔\left({A}\in {X}\wedge {P}{D}{A}<{R}\right)\right)$
6 5 simprbda ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {A}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {A}\in {X}$
7 xmetcl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {A}\in {X}\right)\to {P}{D}{A}\in {ℝ}^{*}$
8 3 4 6 7 syl3anc ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {A}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {P}{D}{A}\in {ℝ}^{*}$
9 simpl3 ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {A}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {R}\in {ℝ}^{*}$
10 xmetge0 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {A}\in {X}\right)\to 0\le {P}{D}{A}$
11 3 4 6 10 syl3anc ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {A}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to 0\le {P}{D}{A}$
12 5 simplbda ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {A}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to {P}{D}{A}<{R}$
13 2 8 9 11 12 xrlelttrd ${⊢}\left(\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {P}\in {X}\wedge {R}\in {ℝ}^{*}\right)\wedge {A}\in \left({P}\mathrm{ball}\left({D}\right){R}\right)\right)\to 0<{R}$