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} = 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 (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} = 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 (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	1	xpeq1i	$⊢ I \times \{0\} = (0 ..^2) \times \{0\}$
33	5 32	eqtri	$⊢ \underset{˙}{0} = (0 ..^2) \times \{0\}$
34	29 31 7 33	ehl2eudisval0	$⊢ X \in P \to X D \underset{˙}{0} = \sqrt{{X (0)}^{2} + {X (1)}^{2}}$
35	22 34	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}}$
36	35	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)$
37		rpge0	$⊢ R \in ℝ^{+} \to 0 \leq R$
38	19 37	sqrtsqd	$⊢ R \in ℝ^{+} \to \sqrt{R^{2}} = R$
39	38	eqcomd	$⊢ R \in ℝ^{+} \to R = \sqrt{R^{2}}$
40	39	adantl	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land R \in ℝ^{+}) \to R = \sqrt{R^{2}}$
41	40	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}})$
42	41	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}}$
43	22 8	syl	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land R \in ℝ^{+}) \to X (0) \in ℝ$
44	43	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 ℝ$
45	44	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 ℝ$
46	22 9	syl	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land R \in ℝ^{+}) \to X (1) \in ℝ$
47	46	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 ℝ$
48	47	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 ℝ$
49	45 48	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 ℝ$
50	44	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}$
51	47	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}$
52	45 48 50 51	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}$
53	19	adantl	$⊢ ((X \in P \land Y \in P \land X (1) \neq Y (1)) \land R \in ℝ^{+}) \to R \in ℝ$
54	53	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 ℝ$
55	54	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 ℝ$
56	54	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}$
57	49 52 55 56	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}})$
58	42 57	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}$
59	58	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})$
60	36 59	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})$
61	60	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}$
62		eqid	$⊢ Y (0) - X (0) = Y (0) - X (0)$
63		eqid	$⊢ X (1) - Y (1) = X (1) - Y (1)$
64		eqid	$⊢ X (1) Y (0) - X (0) Y (1) = X (1) Y (0) - X (0) Y (1)$
65	62 63 64	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})$
66	12 17 18 21 61 65	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