Metamath Proof Explorer

Theorem sqsscirc2

Description: The complex square of side D is a subset of the complex disc of radius D . (Contributed by Thierry Arnoux, 25-Sep-2017)

Ref Expression
Assertion sqsscirc2 
|- ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( ( ( abs ` ( Re ` ( B - A ) ) ) < ( D / 2 ) /\ ( abs ` ( Im ` ( B - A ) ) ) < ( D / 2 ) ) -> ( abs ` ( B - A ) ) < D ) )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> B e. CC )
2 simpll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> A e. CC )
3 1 2 subcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( B - A ) e. CC )
4 3 recld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( Re ` ( B - A ) ) e. RR )
5 4 recnd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( Re ` ( B - A ) ) e. CC )
6 5 abscld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( abs ` ( Re ` ( B - A ) ) ) e. RR )
7 5 absge0d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> 0 <_ ( abs ` ( Re ` ( B - A ) ) ) )
8 6 7 jca 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( ( abs ` ( Re ` ( B - A ) ) ) e. RR /\ 0 <_ ( abs ` ( Re ` ( B - A ) ) ) ) )
9 3 imcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( Im ` ( B - A ) ) e. RR )
10 9 recnd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( Im ` ( B - A ) ) e. CC )
11 10 abscld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( abs ` ( Im ` ( B - A ) ) ) e. RR )
12 10 absge0d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> 0 <_ ( abs ` ( Im ` ( B - A ) ) ) )
13 11 12 jca 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( ( abs ` ( Im ` ( B - A ) ) ) e. RR /\ 0 <_ ( abs ` ( Im ` ( B - A ) ) ) ) )
14 simpr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> D e. RR+ )
15 sqsscirc1 
 |-  ( ( ( ( ( abs ` ( Re ` ( B - A ) ) ) e. RR /\ 0 <_ ( abs ` ( Re ` ( B - A ) ) ) ) /\ ( ( abs ` ( Im ` ( B - A ) ) ) e. RR /\ 0 <_ ( abs ` ( Im ` ( B - A ) ) ) ) ) /\ D e. RR+ ) -> ( ( ( abs ` ( Re ` ( B - A ) ) ) < ( D / 2 ) /\ ( abs ` ( Im ` ( B - A ) ) ) < ( D / 2 ) ) -> ( sqrt ` ( ( ( abs ` ( Re ` ( B - A ) ) ) ^ 2 ) + ( ( abs ` ( Im ` ( B - A ) ) ) ^ 2 ) ) ) < D ) )
16 8 13 14 15 syl21anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( ( ( abs ` ( Re ` ( B - A ) ) ) < ( D / 2 ) /\ ( abs ` ( Im ` ( B - A ) ) ) < ( D / 2 ) ) -> ( sqrt ` ( ( ( abs ` ( Re ` ( B - A ) ) ) ^ 2 ) + ( ( abs ` ( Im ` ( B - A ) ) ) ^ 2 ) ) ) < D ) )
17 3 absval2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( abs ` ( B - A ) ) = ( sqrt ` ( ( ( Re ` ( B - A ) ) ^ 2 ) + ( ( Im ` ( B - A ) ) ^ 2 ) ) ) )
18 17 breq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( ( abs ` ( B - A ) ) < D <-> ( sqrt ` ( ( ( Re ` ( B - A ) ) ^ 2 ) + ( ( Im ` ( B - A ) ) ^ 2 ) ) ) < D ) )
19 absresq 
 |-  ( ( Re ` ( B - A ) ) e. RR -> ( ( abs ` ( Re ` ( B - A ) ) ) ^ 2 ) = ( ( Re ` ( B - A ) ) ^ 2 ) )
20 4 19 syl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( ( abs ` ( Re ` ( B - A ) ) ) ^ 2 ) = ( ( Re ` ( B - A ) ) ^ 2 ) )
21 absresq 
 |-  ( ( Im ` ( B - A ) ) e. RR -> ( ( abs ` ( Im ` ( B - A ) ) ) ^ 2 ) = ( ( Im ` ( B - A ) ) ^ 2 ) )
22 9 21 syl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( ( abs ` ( Im ` ( B - A ) ) ) ^ 2 ) = ( ( Im ` ( B - A ) ) ^ 2 ) )
23 20 22 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( ( ( abs ` ( Re ` ( B - A ) ) ) ^ 2 ) + ( ( abs ` ( Im ` ( B - A ) ) ) ^ 2 ) ) = ( ( ( Re ` ( B - A ) ) ^ 2 ) + ( ( Im ` ( B - A ) ) ^ 2 ) ) )
24 23 fveq2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( sqrt ` ( ( ( abs ` ( Re ` ( B - A ) ) ) ^ 2 ) + ( ( abs ` ( Im ` ( B - A ) ) ) ^ 2 ) ) ) = ( sqrt ` ( ( ( Re ` ( B - A ) ) ^ 2 ) + ( ( Im ` ( B - A ) ) ^ 2 ) ) ) )
25 24 breq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( ( sqrt ` ( ( ( abs ` ( Re ` ( B - A ) ) ) ^ 2 ) + ( ( abs ` ( Im ` ( B - A ) ) ) ^ 2 ) ) ) < D <-> ( sqrt ` ( ( ( Re ` ( B - A ) ) ^ 2 ) + ( ( Im ` ( B - A ) ) ^ 2 ) ) ) < D ) )
26 18 25 bitr4d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( ( abs ` ( B - A ) ) < D <-> ( sqrt ` ( ( ( abs ` ( Re ` ( B - A ) ) ) ^ 2 ) + ( ( abs ` ( Im ` ( B - A ) ) ) ^ 2 ) ) ) < D ) )
27 16 26 sylibrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ D e. RR+ ) -> ( ( ( abs ` ( Re ` ( B - A ) ) ) < ( D / 2 ) /\ ( abs ` ( Im ` ( B - A ) ) ) < ( D / 2 ) ) -> ( abs ` ( B - A ) ) < D ) )