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 \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \to ((X < \frac{D}{2} \land Y < \frac{D}{2}) \to \sqrt{X^{2} + Y^{2}} < D)$

Proof

Step	Hyp	Ref	Expression
1		simp-4l	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to X \in ℝ$
2	1	resqcld	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to X^{2} \in ℝ$
3		simpllr	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to (Y \in ℝ \land 0 \leq Y)$
4	3	simpld	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to Y \in ℝ$
5	4	resqcld	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to Y^{2} \in ℝ$
6	2 5	readdcld	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to X^{2} + Y^{2} \in ℝ$
7	1	sqge0d	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to 0 \leq X^{2}$
8	4	sqge0d	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to 0 \leq Y^{2}$
9	2 5 7 8	addge0d	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to 0 \leq X^{2} + Y^{2}$
10	6 9	resqrtcld	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to \sqrt{X^{2} + Y^{2}} \in ℝ$
11		simplr	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to D \in ℝ^{+}$
12	11	rpred	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to D \in ℝ$
13	12	rehalfcld	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to \frac{D}{2} \in ℝ$
14	13	resqcld	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to {(\frac{D}{2})}^{2} \in ℝ$
15	14 14	readdcld	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to {(\frac{D}{2})}^{2} + {(\frac{D}{2})}^{2} \in ℝ$
16	13	sqge0d	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to 0 \leq {(\frac{D}{2})}^{2}$
17	14 14 16 16	addge0d	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to 0 \leq {(\frac{D}{2})}^{2} + {(\frac{D}{2})}^{2}$
18	15 17	resqrtcld	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to \sqrt{{(\frac{D}{2})}^{2} + {(\frac{D}{2})}^{2}} \in ℝ$
19		simprl	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to X < \frac{D}{2}$
20		simp-4r	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to 0 \leq X$
21		2rp	$⊢ 2 \in ℝ^{+}$
22	21	a1i	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to 2 \in ℝ^{+}$
23	11	rpge0d	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to 0 \leq D$
24	12 22 23	divge0d	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to 0 \leq \frac{D}{2}$
25	1 13 20 24	lt2sqd	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to (X < \frac{D}{2} \leftrightarrow X^{2} < {(\frac{D}{2})}^{2})$
26	19 25	mpbid	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to X^{2} < {(\frac{D}{2})}^{2}$
27		simprr	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to Y < \frac{D}{2}$
28	3	simprd	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to 0 \leq Y$
29	4 13 28 24	lt2sqd	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to (Y < \frac{D}{2} \leftrightarrow Y^{2} < {(\frac{D}{2})}^{2})$
30	27 29	mpbid	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to Y^{2} < {(\frac{D}{2})}^{2}$
31	2 5 14 14 26 30	lt2addd	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to X^{2} + Y^{2} < {(\frac{D}{2})}^{2} + {(\frac{D}{2})}^{2}$
32	6 9 15 17	sqrtltd	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to (X^{2} + Y^{2} < {(\frac{D}{2})}^{2} + {(\frac{D}{2})}^{2} \leftrightarrow \sqrt{X^{2} + Y^{2}} < \sqrt{{(\frac{D}{2})}^{2} + {(\frac{D}{2})}^{2}})$
33	31 32	mpbid	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to \sqrt{X^{2} + Y^{2}} < \sqrt{{(\frac{D}{2})}^{2} + {(\frac{D}{2})}^{2}}$
34		rpre	$⊢ D \in ℝ^{+} \to D \in ℝ$
35	34	rehalfcld	$⊢ D \in ℝ^{+} \to \frac{D}{2} \in ℝ$
36	35	resqcld	$⊢ D \in ℝ^{+} \to {(\frac{D}{2})}^{2} \in ℝ$
37	36	recnd	$⊢ D \in ℝ^{+} \to {(\frac{D}{2})}^{2} \in ℂ$
38	37	2timesd	$⊢ D \in ℝ^{+} \to 2 {(\frac{D}{2})}^{2} = {(\frac{D}{2})}^{2} + {(\frac{D}{2})}^{2}$
39	38	fveq2d	$⊢ D \in ℝ^{+} \to \sqrt{2 {(\frac{D}{2})}^{2}} = \sqrt{{(\frac{D}{2})}^{2} + {(\frac{D}{2})}^{2}}$
40	21	a1i	$⊢ D \in ℝ^{+} \to 2 \in ℝ^{+}$
41		rpge0	$⊢ D \in ℝ^{+} \to 0 \leq D$
42	34 40 41	divge0d	$⊢ D \in ℝ^{+} \to 0 \leq \frac{D}{2}$
43	35 42	sqrtsqd	$⊢ D \in ℝ^{+} \to \sqrt{{(\frac{D}{2})}^{2}} = \frac{D}{2}$
44	43	oveq2d	$⊢ D \in ℝ^{+} \to \sqrt{2} \sqrt{{(\frac{D}{2})}^{2}} = \sqrt{2} (\frac{D}{2})$
45		2re	$⊢ 2 \in ℝ$
46	45	a1i	$⊢ D \in ℝ^{+} \to 2 \in ℝ$
47		0le2	$⊢ 0 \leq 2$
48	47	a1i	$⊢ D \in ℝ^{+} \to 0 \leq 2$
49	35	sqge0d	$⊢ D \in ℝ^{+} \to 0 \leq {(\frac{D}{2})}^{2}$
50	46 48 36 49	sqrtmuld	$⊢ D \in ℝ^{+} \to \sqrt{2 {(\frac{D}{2})}^{2}} = \sqrt{2} \sqrt{{(\frac{D}{2})}^{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 \neq 0$
55	54	a1i	$⊢ D \in ℝ^{+} \to 2 \neq 0$
56	52 51 53 55	div32d	$⊢ D \in ℝ^{+} \to (\frac{\sqrt{2}}{2}) D = \sqrt{2} (\frac{D}{2})$
57	44 50 56	3eqtr4d	$⊢ D \in ℝ^{+} \to \sqrt{2 {(\frac{D}{2})}^{2}} = (\frac{\sqrt{2}}{2}) D$
58	39 57	eqtr3d	$⊢ D \in ℝ^{+} \to \sqrt{{(\frac{D}{2})}^{2} + {(\frac{D}{2})}^{2}} = (\frac{\sqrt{2}}{2}) D$
59		2lt4	$⊢ 2 < 4$
60		4re	$⊢ 4 \in ℝ$
61		0re	$⊢ 0 \in ℝ$
62		4pos	$⊢ 0 < 4$
63	61 60 62	ltleii	$⊢ 0 \leq 4$
64		sqrtlt	$⊢ ((2 \in ℝ \land 0 \leq 2) \land (4 \in ℝ \land 0 \leq 4)) \to (2 < 4 \leftrightarrow \sqrt{2} < \sqrt{4})$
65	45 47 60 63 64	mp4an	$⊢ 2 < 4 \leftrightarrow \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} \leftrightarrow \frac{\sqrt{2}}{2} < \frac{\sqrt{4}}{2}$
71	66 70	mpbi	$⊢ \frac{\sqrt{2}}{2} < \frac{\sqrt{4}}{2}$
72		sqrtsq	$⊢ (2 \in ℝ \land 0 \leq 2) \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 (\frac{\sqrt{2}}{2} < 1 \leftrightarrow (\frac{\sqrt{2}}{2}) D < 1 D)$
86	80 85	mpbii	$⊢ D \in ℝ^{+} \to (\frac{\sqrt{2}}{2}) D < 1 D$
87	53	mulid2d	$⊢ D \in ℝ^{+} \to 1 D = D$
88	86 87	breqtrd	$⊢ D \in ℝ^{+} \to (\frac{\sqrt{2}}{2}) D < D$
89	58 88	eqbrtrd	$⊢ D \in ℝ^{+} \to \sqrt{{(\frac{D}{2})}^{2} + {(\frac{D}{2})}^{2}} < D$
90	11 89	syl	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to \sqrt{{(\frac{D}{2})}^{2} + {(\frac{D}{2})}^{2}} < D$
91	10 18 12 33 90	lttrd	$⊢ ((((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \land (X < \frac{D}{2} \land Y < \frac{D}{2})) \to \sqrt{X^{2} + Y^{2}} < D$
92	91	ex	$⊢ (((X \in ℝ \land 0 \leq X) \land (Y \in ℝ \land 0 \leq Y)) \land D \in ℝ^{+}) \to ((X < \frac{D}{2} \land Y < \frac{D}{2}) \to \sqrt{X^{2} + Y^{2}} < D)$

Metamath Proof Explorer

Theorem sqsscirc1

Proof