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 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℝ ∧ A D B ≤ C → A D B ∈ ℝ

Proof

Step Hyp Ref Expression
1 xmetcl ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B ∈ ℝ *
2 1 3expb ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B ∈ ℝ *
3 2 3adant3 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℝ ∧ A D B ≤ C → A D B ∈ ℝ *
4 simp3l ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℝ ∧ A D B ≤ C → C ∈ ℝ
5 xmetge0 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → 0 ≤ A D B
6 5 3expb ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X → 0 ≤ A D B
7 6 3adant3 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℝ ∧ A D B ≤ C → 0 ≤ A D B
8 simp3r ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℝ ∧ A D B ≤ C → A D B ≤ C
9 xrrege0 ⊢ A D B ∈ ℝ * ∧ C ∈ ℝ ∧ 0 ≤ A D B ∧ A D B ≤ C → A D B ∈ ℝ
10 3 4 7 8 9 syl22anc ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℝ ∧ A D B ≤ C → A D B ∈ ℝ