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 DPsMetXAXBXCADBCADB

Proof

Step Hyp Ref Expression
1 psmetcl DPsMetXAXBXADB*
2 1 3expb DPsMetXAXBXADB*
3 2 3adant3 DPsMetXAXBXCADBCADB*
4 simp3l DPsMetXAXBXCADBCC
5 psmetge0 DPsMetXAXBX0ADB
6 5 3expb DPsMetXAXBX0ADB
7 6 3adant3 DPsMetXAXBXCADBC0ADB
8 simp3r DPsMetXAXBXCADBCADBC
9 xrrege0 ADB*C0ADBADBCADB
10 3 4 7 8 9 syl22anc DPsMetXAXBXCADBCADB