# 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 ${⊢}\left(\left(\left({X}\in ℝ\wedge 0\le {X}\right)\wedge \left({Y}\in ℝ\wedge 0\le {Y}\right)\right)\wedge {D}\in {ℝ}^{+}\right)\to \left(\left({X}<\frac{{D}}{2}\wedge {Y}<\frac{{D}}{2}\right)\to \sqrt{{{X}}^{2}+{{Y}}^{2}}<{D}\right)$

### Proof

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