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 \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to ((\|ℜ (B - A)\| < \frac{D}{2} \land \|ℑ (B - A)\| < \frac{D}{2}) \to \|B - A\| < D)$

Proof

Step	Hyp	Ref	Expression
1		simplr	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to B \in ℂ$
2		simpll	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to A \in ℂ$
3	1 2	subcld	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to B - A \in ℂ$
4	3	recld	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to ℜ (B - A) \in ℝ$
5	4	recnd	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to ℜ (B - A) \in ℂ$
6	5	abscld	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to \|ℜ (B - A)\| \in ℝ$
7	5	absge0d	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to 0 \leq \|ℜ (B - A)\|$
8	6 7	jca	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to (\|ℜ (B - A)\| \in ℝ \land 0 \leq \|ℜ (B - A)\|)$
9	3	imcld	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to ℑ (B - A) \in ℝ$
10	9	recnd	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to ℑ (B - A) \in ℂ$
11	10	abscld	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to \|ℑ (B - A)\| \in ℝ$
12	10	absge0d	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to 0 \leq \|ℑ (B - A)\|$
13	11 12	jca	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to (\|ℑ (B - A)\| \in ℝ \land 0 \leq \|ℑ (B - A)\|)$
14		simpr	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to D \in ℝ^{+}$
15		sqsscirc1	$⊢ (((\|ℜ (B - A)\| \in ℝ \land 0 \leq \|ℜ (B - A)\|) \land (\|ℑ (B - A)\| \in ℝ \land 0 \leq \|ℑ (B - A)\|)) \land D \in ℝ^{+}) \to ((\|ℜ (B - A)\| < \frac{D}{2} \land \|ℑ (B - A)\| < \frac{D}{2}) \to \sqrt{{\|ℜ (B - A)\|}^{2} + {\|ℑ (B - A)\|}^{2}} < D)$
16	8 13 14 15	syl21anc	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to ((\|ℜ (B - A)\| < \frac{D}{2} \land \|ℑ (B - A)\| < \frac{D}{2}) \to \sqrt{{\|ℜ (B - A)\|}^{2} + {\|ℑ (B - A)\|}^{2}} < D)$
17	3	absval2d	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to \|B - A\| = \sqrt{{ℜ (B - A)}^{2} + {ℑ (B - A)}^{2}}$
18	17	breq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to (\|B - A\| < D \leftrightarrow \sqrt{{ℜ (B - A)}^{2} + {ℑ (B - A)}^{2}} < D)$
19		absresq	$⊢ ℜ (B - A) \in ℝ \to {\|ℜ (B - A)\|}^{2} = {ℜ (B - A)}^{2}$
20	4 19	syl	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to {\|ℜ (B - A)\|}^{2} = {ℜ (B - A)}^{2}$
21		absresq	$⊢ ℑ (B - A) \in ℝ \to {\|ℑ (B - A)\|}^{2} = {ℑ (B - A)}^{2}$
22	9 21	syl	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to {\|ℑ (B - A)\|}^{2} = {ℑ (B - A)}^{2}$
23	20 22	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to {\|ℜ (B - A)\|}^{2} + {\|ℑ (B - A)\|}^{2} = {ℜ (B - A)}^{2} + {ℑ (B - A)}^{2}$
24	23	fveq2d	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to \sqrt{{\|ℜ (B - A)\|}^{2} + {\|ℑ (B - A)\|}^{2}} = \sqrt{{ℜ (B - A)}^{2} + {ℑ (B - A)}^{2}}$
25	24	breq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to (\sqrt{{\|ℜ (B - A)\|}^{2} + {\|ℑ (B - A)\|}^{2}} < D \leftrightarrow \sqrt{{ℜ (B - A)}^{2} + {ℑ (B - A)}^{2}} < D)$
26	18 25	bitr4d	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to (\|B - A\| < D \leftrightarrow \sqrt{{\|ℜ (B - A)\|}^{2} + {\|ℑ (B - A)\|}^{2}} < D)$
27	16 26	sylibrd	$⊢ ((A \in ℂ \land B \in ℂ) \land D \in ℝ^{+}) \to ((\|ℜ (B - A)\| < \frac{D}{2} \land \|ℑ (B - A)\| < \frac{D}{2}) \to \|B - A\| < D)$

Metamath Proof Explorer

Theorem sqsscirc2

Proof