ehl2eudis0lt

Description: An upper bound of the Euclidean distance of a point to the origin in a real Euclidean space of dimension 2. (Contributed by AV, 9-May-2023)

	Ref	Expression
Hypotheses	ehl2eudisval0.e	$⊢ E = 𝔼_{hil} (2)$
	ehl2eudisval0.x	$⊢ X = ℝ^{\{1, 2\}}$
	ehl2eudisval0.d	$⊢ D = dist (E)$
	ehl2eudisval0.0	$⊢ \underset{˙}{0} = \{1, 2\} \times \{0\}$
Assertion	ehl2eudis0lt	$⊢ (F \in X \land R \in ℝ^{+}) \to (F D \underset{˙}{0} < R \leftrightarrow {F (1)}^{2} + {F (2)}^{2} < R^{2})$

Proof

Step	Hyp	Ref	Expression
1		ehl2eudisval0.e	$⊢ E = 𝔼_{hil} (2)$
2		ehl2eudisval0.x	$⊢ X = ℝ^{\{1, 2\}}$
3		ehl2eudisval0.d	$⊢ D = dist (E)$
4		ehl2eudisval0.0	$⊢ \underset{˙}{0} = \{1, 2\} \times \{0\}$
5	1 2 3 4	ehl2eudisval0	$⊢ F \in X \to F D \underset{˙}{0} = \sqrt{{F (1)}^{2} + {F (2)}^{2}}$
6	5	adantr	$⊢ (F \in X \land R \in ℝ^{+}) \to F D \underset{˙}{0} = \sqrt{{F (1)}^{2} + {F (2)}^{2}}$
7	6	breq1d	$⊢ (F \in X \land R \in ℝ^{+}) \to (F D \underset{˙}{0} < R \leftrightarrow \sqrt{{F (1)}^{2} + {F (2)}^{2}} < R)$
8		eqid	$⊢ \{1, 2\} = \{1, 2\}$
9	8 2	rrx2pxel	$⊢ F \in X \to F (1) \in ℝ$
10	8 2	rrx2pyel	$⊢ F \in X \to F (2) \in ℝ$
11		eqid	$⊢ {F (1)}^{2} + {F (2)}^{2} = {F (1)}^{2} + {F (2)}^{2}$
12	11	resum2sqcl	$⊢ (F (1) \in ℝ \land F (2) \in ℝ) \to {F (1)}^{2} + {F (2)}^{2} \in ℝ$
13	9 10 12	syl2anc	$⊢ F \in X \to {F (1)}^{2} + {F (2)}^{2} \in ℝ$
14		resqcl	$⊢ F (1) \in ℝ \to {F (1)}^{2} \in ℝ$
15		resqcl	$⊢ F (2) \in ℝ \to {F (2)}^{2} \in ℝ$
16	14 15	anim12i	$⊢ (F (1) \in ℝ \land F (2) \in ℝ) \to ({F (1)}^{2} \in ℝ \land {F (2)}^{2} \in ℝ)$
17		sqge0	$⊢ F (1) \in ℝ \to 0 \leq {F (1)}^{2}$
18		sqge0	$⊢ F (2) \in ℝ \to 0 \leq {F (2)}^{2}$
19	17 18	anim12i	$⊢ (F (1) \in ℝ \land F (2) \in ℝ) \to (0 \leq {F (1)}^{2} \land 0 \leq {F (2)}^{2})$
20		addge0	$⊢ (({F (1)}^{2} \in ℝ \land {F (2)}^{2} \in ℝ) \land (0 \leq {F (1)}^{2} \land 0 \leq {F (2)}^{2})) \to 0 \leq {F (1)}^{2} + {F (2)}^{2}$
21	16 19 20	syl2anc	$⊢ (F (1) \in ℝ \land F (2) \in ℝ) \to 0 \leq {F (1)}^{2} + {F (2)}^{2}$
22	9 10 21	syl2anc	$⊢ F \in X \to 0 \leq {F (1)}^{2} + {F (2)}^{2}$
23	13 22	resqrtcld	$⊢ F \in X \to \sqrt{{F (1)}^{2} + {F (2)}^{2}} \in ℝ$
24	13 22	sqrtge0d	$⊢ F \in X \to 0 \leq \sqrt{{F (1)}^{2} + {F (2)}^{2}}$
25	23 24	jca	$⊢ F \in X \to (\sqrt{{F (1)}^{2} + {F (2)}^{2}} \in ℝ \land 0 \leq \sqrt{{F (1)}^{2} + {F (2)}^{2}})$
26		rprege0	$⊢ R \in ℝ^{+} \to (R \in ℝ \land 0 \leq R)$
27		lt2sq	$⊢ ((\sqrt{{F (1)}^{2} + {F (2)}^{2}} \in ℝ \land 0 \leq \sqrt{{F (1)}^{2} + {F (2)}^{2}}) \land (R \in ℝ \land 0 \leq R)) \to (\sqrt{{F (1)}^{2} + {F (2)}^{2}} < R \leftrightarrow {\sqrt{{F (1)}^{2} + {F (2)}^{2}}}^{2} < R^{2})$
28	25 26 27	syl2an	$⊢ (F \in X \land R \in ℝ^{+}) \to (\sqrt{{F (1)}^{2} + {F (2)}^{2}} < R \leftrightarrow {\sqrt{{F (1)}^{2} + {F (2)}^{2}}}^{2} < R^{2})$
29	13 22	jca	$⊢ F \in X \to ({F (1)}^{2} + {F (2)}^{2} \in ℝ \land 0 \leq {F (1)}^{2} + {F (2)}^{2})$
30	29	adantr	$⊢ (F \in X \land R \in ℝ^{+}) \to ({F (1)}^{2} + {F (2)}^{2} \in ℝ \land 0 \leq {F (1)}^{2} + {F (2)}^{2})$
31		resqrtth	$⊢ ({F (1)}^{2} + {F (2)}^{2} \in ℝ \land 0 \leq {F (1)}^{2} + {F (2)}^{2}) \to {\sqrt{{F (1)}^{2} + {F (2)}^{2}}}^{2} = {F (1)}^{2} + {F (2)}^{2}$
32	30 31	syl	$⊢ (F \in X \land R \in ℝ^{+}) \to {\sqrt{{F (1)}^{2} + {F (2)}^{2}}}^{2} = {F (1)}^{2} + {F (2)}^{2}$
33	32	breq1d	$⊢ (F \in X \land R \in ℝ^{+}) \to ({\sqrt{{F (1)}^{2} + {F (2)}^{2}}}^{2} < R^{2} \leftrightarrow {F (1)}^{2} + {F (2)}^{2} < R^{2})$
34	7 28 33	3bitrd	$⊢ (F \in X \land R \in ℝ^{+}) \to (F D \underset{˙}{0} < R \leftrightarrow {F (1)}^{2} + {F (2)}^{2} < R^{2})$

Metamath Proof Explorer

Theorem ehl2eudis0lt

Proof