Metamath Proof Explorer

Theorem sqsscirc1

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

Ref Expression
Assertion sqsscirc1 
|- ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) -> ( ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) -> ( sqrt ` ( ( X ^ 2 ) + ( Y ^ 2 ) ) ) < D ) )

Proof

Step Hyp Ref Expression
1 simp-4l 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> X e. RR )
2 1 resqcld 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( X ^ 2 ) e. RR )
3 simpllr 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( Y e. RR /\ 0 <_ Y ) )
4 3 simpld 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> Y e. RR )
5 4 resqcld 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( Y ^ 2 ) e. RR )
6 2 5 readdcld 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( ( X ^ 2 ) + ( Y ^ 2 ) ) e. RR )
7 1 sqge0d 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> 0 <_ ( X ^ 2 ) )
8 4 sqge0d 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> 0 <_ ( Y ^ 2 ) )
9 2 5 7 8 addge0d 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> 0 <_ ( ( X ^ 2 ) + ( Y ^ 2 ) ) )
10 6 9 resqrtcld 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( sqrt ` ( ( X ^ 2 ) + ( Y ^ 2 ) ) ) e. RR )
11 simplr 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> D e. RR+ )
12 11 rpred 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> D e. RR )
13 12 rehalfcld 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( D / 2 ) e. RR )
14 13 resqcld 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( ( D / 2 ) ^ 2 ) e. RR )
15 14 14 readdcld 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( ( ( D / 2 ) ^ 2 ) + ( ( D / 2 ) ^ 2 ) ) e. RR )
16 13 sqge0d 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> 0 <_ ( ( D / 2 ) ^ 2 ) )
17 14 14 16 16 addge0d 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> 0 <_ ( ( ( D / 2 ) ^ 2 ) + ( ( D / 2 ) ^ 2 ) ) )
18 15 17 resqrtcld 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( sqrt ` ( ( ( D / 2 ) ^ 2 ) + ( ( D / 2 ) ^ 2 ) ) ) e. RR )
19 simprl 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> X < ( D / 2 ) )
20 simp-4r 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> 0 <_ X )
21 2rp 
 |-  2 e. RR+
22 21 a1i 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> 2 e. RR+ )
23 11 rpge0d 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> 0 <_ D )
24 12 22 23 divge0d 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> 0 <_ ( D / 2 ) )
25 1 13 20 24 lt2sqd 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( X < ( D / 2 ) <-> ( X ^ 2 ) < ( ( D / 2 ) ^ 2 ) ) )
26 19 25 mpbid 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( X ^ 2 ) < ( ( D / 2 ) ^ 2 ) )
27 simprr 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> Y < ( D / 2 ) )
28 3 simprd 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> 0 <_ Y )
29 4 13 28 24 lt2sqd 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( Y < ( D / 2 ) <-> ( Y ^ 2 ) < ( ( D / 2 ) ^ 2 ) ) )
30 27 29 mpbid 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( Y ^ 2 ) < ( ( D / 2 ) ^ 2 ) )
31 2 5 14 14 26 30 lt2addd 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( ( X ^ 2 ) + ( Y ^ 2 ) ) < ( ( ( D / 2 ) ^ 2 ) + ( ( D / 2 ) ^ 2 ) ) )
32 6 9 15 17 sqrtltd 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) < ( ( ( D / 2 ) ^ 2 ) + ( ( D / 2 ) ^ 2 ) ) <-> ( sqrt ` ( ( X ^ 2 ) + ( Y ^ 2 ) ) ) < ( sqrt ` ( ( ( D / 2 ) ^ 2 ) + ( ( D / 2 ) ^ 2 ) ) ) ) )
33 31 32 mpbid 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( sqrt ` ( ( X ^ 2 ) + ( Y ^ 2 ) ) ) < ( sqrt ` ( ( ( D / 2 ) ^ 2 ) + ( ( D / 2 ) ^ 2 ) ) ) )
34 rpre 
 |-  ( D e. RR+ -> D e. RR )
35 34 rehalfcld 
 |-  ( D e. RR+ -> ( D / 2 ) e. RR )
36 35 resqcld 
 |-  ( D e. RR+ -> ( ( D / 2 ) ^ 2 ) e. RR )
37 36 recnd 
 |-  ( D e. RR+ -> ( ( D / 2 ) ^ 2 ) e. CC )
38 37 2timesd 
 |-  ( D e. RR+ -> ( 2 x. ( ( D / 2 ) ^ 2 ) ) = ( ( ( D / 2 ) ^ 2 ) + ( ( D / 2 ) ^ 2 ) ) )
39 38 fveq2d 
 |-  ( D e. RR+ -> ( sqrt ` ( 2 x. ( ( D / 2 ) ^ 2 ) ) ) = ( sqrt ` ( ( ( D / 2 ) ^ 2 ) + ( ( D / 2 ) ^ 2 ) ) ) )
40 21 a1i 
 |-  ( D e. RR+ -> 2 e. RR+ )
41 rpge0 
 |-  ( D e. RR+ -> 0 <_ D )
42 34 40 41 divge0d 
 |-  ( D e. RR+ -> 0 <_ ( D / 2 ) )
43 35 42 sqrtsqd 
 |-  ( D e. RR+ -> ( sqrt ` ( ( D / 2 ) ^ 2 ) ) = ( D / 2 ) )
44 43 oveq2d 
 |-  ( D e. RR+ -> ( ( sqrt ` 2 ) x. ( sqrt ` ( ( D / 2 ) ^ 2 ) ) ) = ( ( sqrt ` 2 ) x. ( D / 2 ) ) )
45 2re 
 |-  2 e. RR
46 45 a1i 
 |-  ( D e. RR+ -> 2 e. RR )
47 0le2 
 |-  0 <_ 2
48 47 a1i 
 |-  ( D e. RR+ -> 0 <_ 2 )
49 35 sqge0d 
 |-  ( D e. RR+ -> 0 <_ ( ( D / 2 ) ^ 2 ) )
50 46 48 36 49 sqrtmuld 
 |-  ( D e. RR+ -> ( sqrt ` ( 2 x. ( ( D / 2 ) ^ 2 ) ) ) = ( ( sqrt ` 2 ) x. ( sqrt ` ( ( D / 2 ) ^ 2 ) ) ) )
51 2cnd 
 |-  ( D e. RR+ -> 2 e. CC )
52 51 sqrtcld 
 |-  ( D e. RR+ -> ( sqrt ` 2 ) e. CC )
53 rpcn 
 |-  ( D e. RR+ -> D e. CC )
54 2ne0 
 |-  2 =/= 0
55 54 a1i 
 |-  ( D e. RR+ -> 2 =/= 0 )
56 52 51 53 55 div32d 
 |-  ( D e. RR+ -> ( ( ( sqrt ` 2 ) / 2 ) x. D ) = ( ( sqrt ` 2 ) x. ( D / 2 ) ) )
57 44 50 56 3eqtr4d 
 |-  ( D e. RR+ -> ( sqrt ` ( 2 x. ( ( D / 2 ) ^ 2 ) ) ) = ( ( ( sqrt ` 2 ) / 2 ) x. D ) )
58 39 57 eqtr3d 
 |-  ( D e. RR+ -> ( sqrt ` ( ( ( D / 2 ) ^ 2 ) + ( ( D / 2 ) ^ 2 ) ) ) = ( ( ( sqrt ` 2 ) / 2 ) x. D ) )
59 2lt4 
 |-  2 < 4
60 4re 
 |-  4 e. RR
61 0re 
 |-  0 e. RR
62 4pos 
 |-  0 < 4
63 61 60 62 ltleii 
 |-  0 <_ 4
64 sqrtlt 
 |-  ( ( ( 2 e. RR /\ 0 <_ 2 ) /\ ( 4 e. RR /\ 0 <_ 4 ) ) -> ( 2 < 4 <-> ( sqrt ` 2 ) < ( sqrt ` 4 ) ) )
65 45 47 60 63 64 mp4an 
 |-  ( 2 < 4 <-> ( sqrt ` 2 ) < ( sqrt ` 4 ) )
66 59 65 mpbi 
 |-  ( sqrt ` 2 ) < ( sqrt ` 4 )
67 2pos 
 |-  0 < 2
68 45 67 sqrtpclii 
 |-  ( sqrt ` 2 ) e. RR
69 60 62 sqrtpclii 
 |-  ( sqrt ` 4 ) e. RR
70 68 69 45 67 ltdiv1ii 
 |-  ( ( sqrt ` 2 ) < ( sqrt ` 4 ) <-> ( ( sqrt ` 2 ) / 2 ) < ( ( sqrt ` 4 ) / 2 ) )
71 66 70 mpbi 
 |-  ( ( sqrt ` 2 ) / 2 ) < ( ( sqrt ` 4 ) / 2 )
72 sqrtsq 
 |-  ( ( 2 e. RR /\ 0 <_ 2 ) -> ( sqrt ` ( 2 ^ 2 ) ) = 2 )
73 45 47 72 mp2an 
 |-  ( sqrt ` ( 2 ^ 2 ) ) = 2
74 73 oveq1i 
 |-  ( ( sqrt ` ( 2 ^ 2 ) ) / 2 ) = ( 2 / 2 )
75 sq2 
 |-  ( 2 ^ 2 ) = 4
76 75 fveq2i 
 |-  ( sqrt ` ( 2 ^ 2 ) ) = ( sqrt ` 4 )
77 76 oveq1i 
 |-  ( ( sqrt ` ( 2 ^ 2 ) ) / 2 ) = ( ( sqrt ` 4 ) / 2 )
78 2div2e1 
 |-  ( 2 / 2 ) = 1
79 74 77 78 3eqtr3i 
 |-  ( ( sqrt ` 4 ) / 2 ) = 1
80 71 79 breqtri 
 |-  ( ( sqrt ` 2 ) / 2 ) < 1
81 46 48 resqrtcld 
 |-  ( D e. RR+ -> ( sqrt ` 2 ) e. RR )
82 81 rehalfcld 
 |-  ( D e. RR+ -> ( ( sqrt ` 2 ) / 2 ) e. RR )
83 1red 
 |-  ( D e. RR+ -> 1 e. RR )
84 id 
 |-  ( D e. RR+ -> D e. RR+ )
85 82 83 84 ltmul1d 
 |-  ( D e. RR+ -> ( ( ( sqrt ` 2 ) / 2 ) < 1 <-> ( ( ( sqrt ` 2 ) / 2 ) x. D ) < ( 1 x. D ) ) )
86 80 85 mpbii 
 |-  ( D e. RR+ -> ( ( ( sqrt ` 2 ) / 2 ) x. D ) < ( 1 x. D ) )
87 53 mulid2d 
 |-  ( D e. RR+ -> ( 1 x. D ) = D )
88 86 87 breqtrd 
 |-  ( D e. RR+ -> ( ( ( sqrt ` 2 ) / 2 ) x. D ) < D )
89 58 88 eqbrtrd 
 |-  ( D e. RR+ -> ( sqrt ` ( ( ( D / 2 ) ^ 2 ) + ( ( D / 2 ) ^ 2 ) ) ) < D )
90 11 89 syl 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( sqrt ` ( ( ( D / 2 ) ^ 2 ) + ( ( D / 2 ) ^ 2 ) ) ) < D )
91 10 18 12 33 90 lttrd 
 |-  ( ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) /\ ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) ) -> ( sqrt ` ( ( X ^ 2 ) + ( Y ^ 2 ) ) ) < D )
92 91 ex 
 |-  ( ( ( ( X e. RR /\ 0 <_ X ) /\ ( Y e. RR /\ 0 <_ Y ) ) /\ D e. RR+ ) -> ( ( X < ( D / 2 ) /\ Y < ( D / 2 ) ) -> ( sqrt ` ( ( X ^ 2 ) + ( Y ^ 2 ) ) ) < D ) )