Metamath Proof Explorer


Theorem iooabslt

Description: An upper bound for the distance from the center of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses iooabslt.1 φ A
iooabslt.2 φ B
iooabslt.3 φ C A B A + B
Assertion iooabslt φ A C < B

Proof

Step Hyp Ref Expression
1 iooabslt.1 φ A
2 iooabslt.2 φ B
3 iooabslt.3 φ C A B A + B
4 1 recnd φ A
5 elioore C A B A + B C
6 3 5 syl φ C
7 6 recnd φ C
8 eqid abs = abs
9 8 cnmetdval A C A abs C = A C
10 4 7 9 syl2anc φ A abs C = A C
11 eqid abs 2 = abs 2
12 11 bl2ioo A B A ball abs 2 B = A B A + B
13 1 2 12 syl2anc φ A ball abs 2 B = A B A + B
14 3 13 eleqtrrd φ C A ball abs 2 B
15 cnxmet abs ∞Met
16 15 a1i φ abs ∞Met
17 4 1 elind φ A
18 2 rexrd φ B *
19 11 blres abs ∞Met A B * A ball abs 2 B = A ball abs B
20 16 17 18 19 syl3anc φ A ball abs 2 B = A ball abs B
21 14 20 eleqtrd φ C A ball abs B
22 elin C A ball abs B C A ball abs B C
23 21 22 sylib φ C A ball abs B C
24 23 simpld φ C A ball abs B
25 elbl abs ∞Met A B * C A ball abs B C A abs C < B
26 16 4 18 25 syl3anc φ C A ball abs B C A abs C < B
27 24 26 mpbid φ C A abs C < B
28 27 simprd φ A abs C < B
29 10 28 eqbrtrrd φ A C < B