itscnhlinecirc02plem3

Description: Lemma 3 for itscnhlinecirc02p . (Contributed by AV, 10-Mar-2023)

	Ref	Expression
Hypotheses	itscnhlinecirc02p.i	$⊢ I = \{1, 2\}$
	itscnhlinecirc02p.e	$⊢ E = msup$
	itscnhlinecirc02p.p	$⊢ P = ℝ^{I}$
	itscnhlinecirc02p.s	$⊢ S = Sphere (E)$
	itscnhlinecirc02p.0	$⊢ \underset{˙}{0} = I \times \{0\}$
	itscnhlinecirc02p.l	$⊢ L = {Line}_{M} (E)$
	itscnhlinecirc02p.d	$⊢ D = dist (E)$
Assertion	itscnhlinecirc02plem3	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to 0 < {(- 2 (Y (1) - X (1)) (X (2) Y (1) - X (1) Y (2)))}^{2} - 4 ({(X (2) - Y (2))}^{2} + {(Y (1) - X (1))}^{2}) ({(X (2) Y (1) - X (1) Y (2))}^{2} - {(X (2) - Y (2))}^{2} R^{2})$

Proof

Step	Hyp	Ref	Expression
1		itscnhlinecirc02p.i	$⊢ I = \{1, 2\}$
2		itscnhlinecirc02p.e	$⊢ E = msup$
3		itscnhlinecirc02p.p	$⊢ P = ℝ^{I}$
4		itscnhlinecirc02p.s	$⊢ S = Sphere (E)$
5		itscnhlinecirc02p.0	$⊢ \underset{˙}{0} = I \times \{0\}$
6		itscnhlinecirc02p.l	$⊢ L = {Line}_{M} (E)$
7		itscnhlinecirc02p.d	$⊢ D = dist (E)$
8	1 3	rrx2pxel	$⊢ X \in P \to X (1) \in ℝ$
9	1 3	rrx2pyel	$⊢ X \in P \to X (2) \in ℝ$
10	8 9	jca	$⊢ X \in P \to (X (1) \in ℝ \land X (2) \in ℝ)$
11	10	3ad2ant1	$⊢ (X \in P \land Y \in P \land X (2) \neq Y (2)) \to (X (1) \in ℝ \land X (2) \in ℝ)$
12	11	adantr	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to (X (1) \in ℝ \land X (2) \in ℝ)$
13	1 3	rrx2pxel	$⊢ Y \in P \to Y (1) \in ℝ$
14	1 3	rrx2pyel	$⊢ Y \in P \to Y (2) \in ℝ$
15	13 14	jca	$⊢ Y \in P \to (Y (1) \in ℝ \land Y (2) \in ℝ)$
16	15	3ad2ant2	$⊢ (X \in P \land Y \in P \land X (2) \neq Y (2)) \to (Y (1) \in ℝ \land Y (2) \in ℝ)$
17	16	adantr	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to (Y (1) \in ℝ \land Y (2) \in ℝ)$
18		simpl3	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to X (2) \neq Y (2)$
19		rpre	$⊢ R \in ℝ^{+} \to R \in ℝ$
20	19	adantr	$⊢ (R \in ℝ^{+} \land X D \underset{˙}{0} < R) \to R \in ℝ$
21	20	adantl	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to R \in ℝ$
22		simpl1	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \to X \in P$
23		2nn0	$⊢ 2 \in ℕ_{0}$
24		eqid	$⊢ 𝔼_{hil} (2) = 𝔼_{hil} (2)$
25	24	ehlval	$⊢ 2 \in ℕ_{0} \to 𝔼_{hil} (2) = msup$
26	23 25	ax-mp	$⊢ 𝔼_{hil} (2) = msup$
27		fz12pr	$⊢ (1 \dots 2) = \{1, 2\}$
28	27 1	eqtr4i	$⊢ (1 \dots 2) = I$
29	28	fveq2i	$⊢ msup = msup$
30	26 29	eqtri	$⊢ 𝔼_{hil} (2) = msup$
31	2 30	eqtr4i	$⊢ E = 𝔼_{hil} (2)$
32	1	oveq2i	$⊢ ℝ^{I} = ℝ^{\{1, 2\}}$
33	3 32	eqtri	$⊢ P = ℝ^{\{1, 2\}}$
34	1	xpeq1i	$⊢ I \times \{0\} = \{1, 2\} \times \{0\}$
35	5 34	eqtri	$⊢ \underset{˙}{0} = \{1, 2\} \times \{0\}$
36	31 33 7 35	ehl2eudisval0	$⊢ X \in P \to X D \underset{˙}{0} = \sqrt{{X (1)}^{2} + {X (2)}^{2}}$
37	22 36	syl	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \to X D \underset{˙}{0} = \sqrt{{X (1)}^{2} + {X (2)}^{2}}$
38	37	breq1d	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \to (X D \underset{˙}{0} < R \leftrightarrow \sqrt{{X (1)}^{2} + {X (2)}^{2}} < R)$
39		rpge0	$⊢ R \in ℝ^{+} \to 0 \leq R$
40	19 39	sqrtsqd	$⊢ R \in ℝ^{+} \to \sqrt{R^{2}} = R$
41	40	eqcomd	$⊢ R \in ℝ^{+} \to R = \sqrt{R^{2}}$
42	41	adantl	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \to R = \sqrt{R^{2}}$
43	42	breq2d	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \to (\sqrt{{X (1)}^{2} + {X (2)}^{2}} < R \leftrightarrow \sqrt{{X (1)}^{2} + {X (2)}^{2}} < \sqrt{R^{2}})$
44	43	biimpa	$⊢ (((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \land \sqrt{{X (1)}^{2} + {X (2)}^{2}} < R) \to \sqrt{{X (1)}^{2} + {X (2)}^{2}} < \sqrt{R^{2}}$
45	22 8	syl	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \to X (1) \in ℝ$
46	45	adantr	$⊢ (((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \land \sqrt{{X (1)}^{2} + {X (2)}^{2}} < R) \to X (1) \in ℝ$
47	46	resqcld	$⊢ (((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \land \sqrt{{X (1)}^{2} + {X (2)}^{2}} < R) \to {X (1)}^{2} \in ℝ$
48	22 9	syl	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \to X (2) \in ℝ$
49	48	adantr	$⊢ (((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \land \sqrt{{X (1)}^{2} + {X (2)}^{2}} < R) \to X (2) \in ℝ$
50	49	resqcld	$⊢ (((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \land \sqrt{{X (1)}^{2} + {X (2)}^{2}} < R) \to {X (2)}^{2} \in ℝ$
51	47 50	readdcld	$⊢ (((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \land \sqrt{{X (1)}^{2} + {X (2)}^{2}} < R) \to {X (1)}^{2} + {X (2)}^{2} \in ℝ$
52	46	sqge0d	$⊢ (((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \land \sqrt{{X (1)}^{2} + {X (2)}^{2}} < R) \to 0 \leq {X (1)}^{2}$
53	49	sqge0d	$⊢ (((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \land \sqrt{{X (1)}^{2} + {X (2)}^{2}} < R) \to 0 \leq {X (2)}^{2}$
54	47 50 52 53	addge0d	$⊢ (((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \land \sqrt{{X (1)}^{2} + {X (2)}^{2}} < R) \to 0 \leq {X (1)}^{2} + {X (2)}^{2}$
55	19	adantl	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \to R \in ℝ$
56	55	adantr	$⊢ (((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \land \sqrt{{X (1)}^{2} + {X (2)}^{2}} < R) \to R \in ℝ$
57	56	resqcld	$⊢ (((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \land \sqrt{{X (1)}^{2} + {X (2)}^{2}} < R) \to R^{2} \in ℝ$
58	56	sqge0d	$⊢ (((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \land \sqrt{{X (1)}^{2} + {X (2)}^{2}} < R) \to 0 \leq R^{2}$
59	51 54 57 58	sqrtltd	$⊢ (((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \land \sqrt{{X (1)}^{2} + {X (2)}^{2}} < R) \to ({X (1)}^{2} + {X (2)}^{2} < R^{2} \leftrightarrow \sqrt{{X (1)}^{2} + {X (2)}^{2}} < \sqrt{R^{2}})$
60	44 59	mpbird	$⊢ (((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \land \sqrt{{X (1)}^{2} + {X (2)}^{2}} < R) \to {X (1)}^{2} + {X (2)}^{2} < R^{2}$
61	60	ex	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \to (\sqrt{{X (1)}^{2} + {X (2)}^{2}} < R \to {X (1)}^{2} + {X (2)}^{2} < R^{2})$
62	38 61	sylbid	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land R \in ℝ^{+}) \to (X D \underset{˙}{0} < R \to {X (1)}^{2} + {X (2)}^{2} < R^{2})$
63	62	impr	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to {X (1)}^{2} + {X (2)}^{2} < R^{2}$
64		eqid	$⊢ Y (1) - X (1) = Y (1) - X (1)$
65		eqid	$⊢ X (2) - Y (2) = X (2) - Y (2)$
66		eqid	$⊢ X (2) Y (1) - X (1) Y (2) = X (2) Y (1) - X (1) Y (2)$
67	64 65 66	itscnhlinecirc02plem2	$⊢ (((X (1) \in ℝ \land X (2) \in ℝ) \land (Y (1) \in ℝ \land Y (2) \in ℝ) \land X (2) \neq Y (2)) \land (R \in ℝ \land {X (1)}^{2} + {X (2)}^{2} < R^{2})) \to 0 < {(- 2 (Y (1) - X (1)) (X (2) Y (1) - X (1) Y (2)))}^{2} - 4 ({(X (2) - Y (2))}^{2} + {(Y (1) - X (1))}^{2}) ({(X (2) Y (1) - X (1) Y (2))}^{2} - {(X (2) - Y (2))}^{2} R^{2})$
68	12 17 18 21 63 67	syl32anc	$⊢ ((X \in P \land Y \in P \land X (2) \neq Y (2)) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to 0 < {(- 2 (Y (1) - X (1)) (X (2) Y (1) - X (1) Y (2)))}^{2} - 4 ({(X (2) - Y (2))}^{2} + {(Y (1) - X (1))}^{2}) ({(X (2) Y (1) - X (1) Y (2))}^{2} - {(X (2) - Y (2))}^{2} R^{2})$

Metamath Proof Explorer

Theorem itscnhlinecirc02plem3

Proof