Metamath Proof Explorer

Theorem psmetlecl

Description: Real closure of an extended metric value that is upper bounded by a real. (Contributed by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion psmetlecl ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℝ ∧ A D B ≤ C → A D B ∈ ℝ

Proof

Step Hyp Ref Expression
1 psmetcl ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B ∈ ℝ *
2 1 3expb ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → A D B ∈ ℝ *
3 2 3adant3 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℝ ∧ A D B ≤ C → A D B ∈ ℝ *
4 simp3l ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℝ ∧ A D B ≤ C → C ∈ ℝ
5 psmetge0 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → 0 ≤ A D B
6 5 3expb ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X → 0 ≤ A D B
7 6 3adant3 ⊢ D ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℝ ∧ A D B ≤ C → 0 ≤ A D B
8 simp3r ⊢ D ∈ PsMet ⁡ 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 ∈ PsMet ⁡ X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ ℝ ∧ A D B ≤ C → A D B ∈ ℝ