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 
|- ( ph -> A e. RR )
iooabslt.2 
|- ( ph -> B e. RR )
iooabslt.3 
|- ( ph -> C e. ( ( A - B ) (,) ( A + B ) ) )
Assertion iooabslt 
|- ( ph -> ( abs ` ( A - C ) ) < B )

Proof

Step Hyp Ref Expression
1 iooabslt.1 
 |-  ( ph -> A e. RR )
2 iooabslt.2 
 |-  ( ph -> B e. RR )
3 iooabslt.3 
 |-  ( ph -> C e. ( ( A - B ) (,) ( A + B ) ) )
4 1 recnd 
 |-  ( ph -> A e. CC )
5 elioore 
 |-  ( C e. ( ( A - B ) (,) ( A + B ) ) -> C e. RR )
6 3 5 syl 
 |-  ( ph -> C e. RR )
7 6 recnd 
 |-  ( ph -> C e. CC )
8 eqid 
 |-  ( abs o. - ) = ( abs o. - )
9 8 cnmetdval 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A ( abs o. - ) C ) = ( abs ` ( A - C ) ) )
10 4 7 9 syl2anc 
 |-  ( ph -> ( A ( abs o. - ) C ) = ( abs ` ( A - C ) ) )
11 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
12 11 bl2ioo 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) B ) = ( ( A - B ) (,) ( A + B ) ) )
13 1 2 12 syl2anc 
 |-  ( ph -> ( A ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) B ) = ( ( A - B ) (,) ( A + B ) ) )
14 3 13 eleqtrrd 
 |-  ( ph -> C e. ( A ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) B ) )
15 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
16 15 a1i 
 |-  ( ph -> ( abs o. - ) e. ( *Met ` CC ) )
17 4 1 elind 
 |-  ( ph -> A e. ( CC i^i RR ) )
18 2 rexrd 
 |-  ( ph -> B e. RR* )
19 11 blres 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ A e. ( CC i^i RR ) /\ B e. RR* ) -> ( A ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) B ) = ( ( A ( ball ` ( abs o. - ) ) B ) i^i RR ) )
20 16 17 18 19 syl3anc 
 |-  ( ph -> ( A ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) B ) = ( ( A ( ball ` ( abs o. - ) ) B ) i^i RR ) )
21 14 20 eleqtrd 
 |-  ( ph -> C e. ( ( A ( ball ` ( abs o. - ) ) B ) i^i RR ) )
22 elin 
 |-  ( C e. ( ( A ( ball ` ( abs o. - ) ) B ) i^i RR ) <-> ( C e. ( A ( ball ` ( abs o. - ) ) B ) /\ C e. RR ) )
23 21 22 sylib 
 |-  ( ph -> ( C e. ( A ( ball ` ( abs o. - ) ) B ) /\ C e. RR ) )
24 23 simpld 
 |-  ( ph -> C e. ( A ( ball ` ( abs o. - ) ) B ) )
25 elbl 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ A e. CC /\ B e. RR* ) -> ( C e. ( A ( ball ` ( abs o. - ) ) B ) <-> ( C e. CC /\ ( A ( abs o. - ) C ) < B ) ) )
26 16 4 18 25 syl3anc 
 |-  ( ph -> ( C e. ( A ( ball ` ( abs o. - ) ) B ) <-> ( C e. CC /\ ( A ( abs o. - ) C ) < B ) ) )
27 24 26 mpbid 
 |-  ( ph -> ( C e. CC /\ ( A ( abs o. - ) C ) < B ) )
28 27 simprd 
 |-  ( ph -> ( A ( abs o. - ) C ) < B )
29 10 28 eqbrtrrd 
 |-  ( ph -> ( abs ` ( A - C ) ) < B )