# Metamath Proof Explorer

## Theorem xmetlecl

Description: Real closure of an extended metric value that is upper bounded by a real. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmetlecl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in ℝ\wedge {A}{D}{B}\le {C}\right)\right)\to {A}{D}{B}\in ℝ$

### Proof

Step Hyp Ref Expression
1 xmetcl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{B}\in {ℝ}^{*}$
2 1 3expb ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to {A}{D}{B}\in {ℝ}^{*}$
3 2 3adant3 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in ℝ\wedge {A}{D}{B}\le {C}\right)\right)\to {A}{D}{B}\in {ℝ}^{*}$
4 simp3l ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in ℝ\wedge {A}{D}{B}\le {C}\right)\right)\to {C}\in ℝ$
5 xmetge0 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to 0\le {A}{D}{B}$
6 5 3expb ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to 0\le {A}{D}{B}$
7 6 3adant3 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in ℝ\wedge {A}{D}{B}\le {C}\right)\right)\to 0\le {A}{D}{B}$
8 simp3r ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in ℝ\wedge {A}{D}{B}\le {C}\right)\right)\to {A}{D}{B}\le {C}$
9 xrrege0 ${⊢}\left(\left({A}{D}{B}\in {ℝ}^{*}\wedge {C}\in ℝ\right)\wedge \left(0\le {A}{D}{B}\wedge {A}{D}{B}\le {C}\right)\right)\to {A}{D}{B}\in ℝ$
10 3 4 7 8 9 syl22anc ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in ℝ\wedge {A}{D}{B}\le {C}\right)\right)\to {A}{D}{B}\in ℝ$