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	$⊢ (D \in ∞Met (X) \land (A \in X \land B \in X) \land (C \in ℝ \land A D B \leq C)) \to A D B \in ℝ$

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

Metamath Proof Explorer