itscnhlinecirc02plem3

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

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

Proof

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

Metamath Proof Explorer

Theorem itscnhlinecirc02plem3

Proof