Metamath Proof Explorer

Theorem ioo2bl

Description: An open interval of reals in terms of a ball. (Contributed by NM, 18-May-2007) (Revised by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypothesis remet.1 
|- D = ( ( abs o. - ) |` ( RR X. RR ) )
Assertion ioo2bl 
|- ( ( A e. RR /\ B e. RR ) -> ( A (,) B ) = ( ( ( A + B ) / 2 ) ( ball ` D ) ( ( B - A ) / 2 ) ) )

Proof

Step Hyp Ref Expression
1 remet.1 
 |-  D = ( ( abs o. - ) |` ( RR X. RR ) )
2 readdcl 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B + A ) e. RR )
3 2 ancoms 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B + A ) e. RR )
4 3 rehalfcld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( B + A ) / 2 ) e. RR )
5 resubcl 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B - A ) e. RR )
6 5 ancoms 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B - A ) e. RR )
7 6 rehalfcld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( B - A ) / 2 ) e. RR )
8 1 bl2ioo 
 |-  ( ( ( ( B + A ) / 2 ) e. RR /\ ( ( B - A ) / 2 ) e. RR ) -> ( ( ( B + A ) / 2 ) ( ball ` D ) ( ( B - A ) / 2 ) ) = ( ( ( ( B + A ) / 2 ) - ( ( B - A ) / 2 ) ) (,) ( ( ( B + A ) / 2 ) + ( ( B - A ) / 2 ) ) ) )
9 4 7 8 syl2anc 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( B + A ) / 2 ) ( ball ` D ) ( ( B - A ) / 2 ) ) = ( ( ( ( B + A ) / 2 ) - ( ( B - A ) / 2 ) ) (,) ( ( ( B + A ) / 2 ) + ( ( B - A ) / 2 ) ) ) )
10 recn 
 |-  ( B e. RR -> B e. CC )
11 recn 
 |-  ( A e. RR -> A e. CC )
12 addcom 
 |-  ( ( B e. CC /\ A e. CC ) -> ( B + A ) = ( A + B ) )
13 10 11 12 syl2anr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B + A ) = ( A + B ) )
14 13 oveq1d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( B + A ) / 2 ) = ( ( A + B ) / 2 ) )
15 14 oveq1d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( B + A ) / 2 ) ( ball ` D ) ( ( B - A ) / 2 ) ) = ( ( ( A + B ) / 2 ) ( ball ` D ) ( ( B - A ) / 2 ) ) )
16 halfaddsub 
 |-  ( ( B e. CC /\ A e. CC ) -> ( ( ( ( B + A ) / 2 ) + ( ( B - A ) / 2 ) ) = B /\ ( ( ( B + A ) / 2 ) - ( ( B - A ) / 2 ) ) = A ) )
17 10 11 16 syl2anr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( ( B + A ) / 2 ) + ( ( B - A ) / 2 ) ) = B /\ ( ( ( B + A ) / 2 ) - ( ( B - A ) / 2 ) ) = A ) )
18 17 simprd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( B + A ) / 2 ) - ( ( B - A ) / 2 ) ) = A )
19 17 simpld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( B + A ) / 2 ) + ( ( B - A ) / 2 ) ) = B )
20 18 19 oveq12d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( ( B + A ) / 2 ) - ( ( B - A ) / 2 ) ) (,) ( ( ( B + A ) / 2 ) + ( ( B - A ) / 2 ) ) ) = ( A (,) B ) )
21 9 15 20 3eqtr3rd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A (,) B ) = ( ( ( A + B ) / 2 ) ( ball ` D ) ( ( B - A ) / 2 ) ) )