inlinecirc02p

Description: Intersection of a line with a circle: A line passing through a point within a circle around the origin intersects the circle at exactly two different points. (Contributed by AV, 9-May-2023) (Revised by AV, 16-May-2023)

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

Proof

Step	Hyp	Ref	Expression
1		inlinecirc02p.i	$⊢ I = \{1, 2\}$
2		inlinecirc02p.e	$⊢ E = I$
3		inlinecirc02p.p	$⊢ P = ℝ^{I}$
4		inlinecirc02p.s	$⊢ S = Sphere (E)$
5		inlinecirc02p.0	$⊢ \underset{˙}{0} = I \times \{0\}$
6		inlinecirc02p.l	$⊢ L = {Line}_{M} (E)$
7		inlinecirc02p.d	$⊢ D = dist (E)$
8	3	ovexi	$⊢ P \in V$
9	8	a1i	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to P \in V$
10		simpl	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to (X \in P \land Y \in P \land X \neq Y)$
11		simpl	$⊢ (R \in ℝ^{+} \land X D \underset{˙}{0} < R) \to R \in ℝ^{+}$
12	11	adantl	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to R \in ℝ^{+}$
13	1 3	rrx2pxel	$⊢ X \in P \to X (1) \in ℝ$
14	13	3ad2ant1	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X (1) \in ℝ$
15	14	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to X (1) \in ℝ$
16	1 3	rrx2pyel	$⊢ X \in P \to X (2) \in ℝ$
17	16	3ad2ant1	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X (2) \in ℝ$
18	17	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to X (2) \in ℝ$
19	1 3	rrx2pxel	$⊢ Y \in P \to Y (1) \in ℝ$
20	19	3ad2ant2	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Y (1) \in ℝ$
21	20	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to Y (1) \in ℝ$
22	1 3	rrx2pyel	$⊢ Y \in P \to Y (2) \in ℝ$
23	22	3ad2ant2	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Y (2) \in ℝ$
24	23	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to Y (2) \in ℝ$
25		eqid	$⊢ Y (1) - X (1) = Y (1) - X (1)$
26		eqid	$⊢ X (2) - Y (2) = X (2) - Y (2)$
27		eqid	$⊢ (Y (1) - X (1)) X (2) + (X (2) - Y (2)) X (1) = (Y (1) - X (1)) X (2) + (X (2) - Y (2)) X (1)$
28		rpre	$⊢ R \in ℝ^{+} \to R \in ℝ$
29	28	adantr	$⊢ (R \in ℝ^{+} \land X D \underset{˙}{0} < R) \to R \in ℝ$
30	29	adantl	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to R \in ℝ$
31		2nn0	$⊢ 2 \in ℕ_{0}$
32		eqid	$⊢ 𝔼_{hil} (2) = 𝔼_{hil} (2)$
33	32	ehlval	$⊢ 2 \in ℕ_{0} \to 𝔼_{hil} (2) = (1 \dots 2)$
34	31 33	ax-mp	$⊢ 𝔼_{hil} (2) = (1 \dots 2)$
35		fz12pr	$⊢ (1 \dots 2) = \{1, 2\}$
36	35 1	eqtr4i	$⊢ (1 \dots 2) = I$
37	36	fveq2i	$⊢ (1 \dots 2) = I$
38	34 37	eqtri	$⊢ 𝔼_{hil} (2) = I$
39	2 38	eqtr4i	$⊢ E = 𝔼_{hil} (2)$
40	1	oveq2i	$⊢ ℝ^{I} = ℝ^{\{1, 2\}}$
41	3 40	eqtri	$⊢ P = ℝ^{\{1, 2\}}$
42	1	xpeq1i	$⊢ I \times \{0\} = \{1, 2\} \times \{0\}$
43	5 42	eqtri	$⊢ \underset{˙}{0} = \{1, 2\} \times \{0\}$
44	39 41 7 43	ehl2eudis0lt	$⊢ (X \in P \land R \in ℝ^{+}) \to (X D \underset{˙}{0} < R \leftrightarrow {X (1)}^{2} + {X (2)}^{2} < R^{2})$
45	44	3ad2antl1	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land R \in ℝ^{+}) \to (X D \underset{˙}{0} < R \leftrightarrow {X (1)}^{2} + {X (2)}^{2} < R^{2})$
46	45	biimpd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land R \in ℝ^{+}) \to (X D \underset{˙}{0} < R \to {X (1)}^{2} + {X (2)}^{2} < R^{2})$
47	46	impr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to {X (1)}^{2} + {X (2)}^{2} < R^{2}$
48	1 3	rrx2pnecoorneor	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (X (1) \neq Y (1) \lor X (2) \neq Y (2))$
49	48	orcomd	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (X (2) \neq Y (2) \lor X (1) \neq Y (1))$
50	49	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to (X (2) \neq Y (2) \lor X (1) \neq Y (1))$
51		eqid	$⊢ {(X (2) - Y (2))}^{2} + {(Y (1) - X (1))}^{2} = {(X (2) - Y (2))}^{2} + {(Y (1) - X (1))}^{2}$
52		eqid	$⊢ R^{2} ({(X (2) - Y (2))}^{2} + {(Y (1) - X (1))}^{2}) - {((Y (1) - X (1)) X (2) + (X (2) - Y (2)) X (1))}^{2} = R^{2} ({(X (2) - Y (2))}^{2} + {(Y (1) - X (1))}^{2}) - {((Y (1) - X (1)) X (2) + (X (2) - Y (2)) X (1))}^{2}$
53	15 18 21 24 25 26 27 30 47 50 51 52	2itscp	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to 0 < R^{2} ({(X (2) - Y (2))}^{2} + {(Y (1) - X (1))}^{2}) - {((Y (1) - X (1)) X (2) + (X (2) - Y (2)) X (1))}^{2}$
54	19	recnd	$⊢ Y \in P \to Y (1) \in ℂ$
55	54	adantl	$⊢ (X \in P \land Y \in P) \to Y (1) \in ℂ$
56	13	recnd	$⊢ X \in P \to X (1) \in ℂ$
57	56	adantr	$⊢ (X \in P \land Y \in P) \to X (1) \in ℂ$
58	16	recnd	$⊢ X \in P \to X (2) \in ℂ$
59	58	adantr	$⊢ (X \in P \land Y \in P) \to X (2) \in ℂ$
60	55 57 59	subdird	$⊢ (X \in P \land Y \in P) \to (Y (1) - X (1)) X (2) = Y (1) X (2) - X (1) X (2)$
61	22	recnd	$⊢ Y \in P \to Y (2) \in ℂ$
62	61	adantl	$⊢ (X \in P \land Y \in P) \to Y (2) \in ℂ$
63	59 62 57	subdird	$⊢ (X \in P \land Y \in P) \to (X (2) - Y (2)) X (1) = X (2) X (1) - Y (2) X (1)$
64	60 63	oveq12d	$⊢ (X \in P \land Y \in P) \to (Y (1) - X (1)) X (2) + (X (2) - Y (2)) X (1) = (Y (1) X (2) - X (1) X (2)) + X (2) X (1) - Y (2) X (1)$
65	55 59	mulcomd	$⊢ (X \in P \land Y \in P) \to Y (1) X (2) = X (2) Y (1)$
66	65	oveq1d	$⊢ (X \in P \land Y \in P) \to Y (1) X (2) - X (1) X (2) = X (2) Y (1) - X (1) X (2)$
67	59 57	mulcomd	$⊢ (X \in P \land Y \in P) \to X (2) X (1) = X (1) X (2)$
68	62 57	mulcomd	$⊢ (X \in P \land Y \in P) \to Y (2) X (1) = X (1) Y (2)$
69	67 68	oveq12d	$⊢ (X \in P \land Y \in P) \to X (2) X (1) - Y (2) X (1) = X (1) X (2) - X (1) Y (2)$
70	66 69	oveq12d	$⊢ (X \in P \land Y \in P) \to (Y (1) X (2) - X (1) X (2)) + X (2) X (1) - Y (2) X (1) = (X (2) Y (1) - X (1) X (2)) + X (1) X (2) - X (1) Y (2)$
71	59 55	mulcld	$⊢ (X \in P \land Y \in P) \to X (2) Y (1) \in ℂ$
72	57 59	mulcld	$⊢ (X \in P \land Y \in P) \to X (1) X (2) \in ℂ$
73	57 62	mulcld	$⊢ (X \in P \land Y \in P) \to X (1) Y (2) \in ℂ$
74	71 72 73	npncand	$⊢ (X \in P \land Y \in P) \to (X (2) Y (1) - X (1) X (2)) + X (1) X (2) - X (1) Y (2) = X (2) Y (1) - X (1) Y (2)$
75	64 70 74	3eqtrd	$⊢ (X \in P \land Y \in P) \to (Y (1) - X (1)) X (2) + (X (2) - Y (2)) X (1) = X (2) Y (1) - X (1) Y (2)$
76	75	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (Y (1) - X (1)) X (2) + (X (2) - Y (2)) X (1) = X (2) Y (1) - X (1) Y (2)$
77	76	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to (Y (1) - X (1)) X (2) + (X (2) - Y (2)) X (1) = X (2) Y (1) - X (1) Y (2)$
78	77	eqcomd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to X (2) Y (1) - X (1) Y (2) = (Y (1) - X (1)) X (2) + (X (2) - Y (2)) X (1)$
79	78	oveq1d	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to {(X (2) Y (1) - X (1) Y (2))}^{2} = {((Y (1) - X (1)) X (2) + (X (2) - Y (2)) X (1))}^{2}$
80	79	oveq2d	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to R^{2} ({(X (2) - Y (2))}^{2} + {(Y (1) - X (1))}^{2}) - {(X (2) Y (1) - X (1) Y (2))}^{2} = R^{2} ({(X (2) - Y (2))}^{2} + {(Y (1) - X (1))}^{2}) - {((Y (1) - X (1)) X (2) + (X (2) - Y (2)) X (1))}^{2}$
81	53 80	breqtrrd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to 0 < R^{2} ({(X (2) - Y (2))}^{2} + {(Y (1) - X (1))}^{2}) - {(X (2) Y (1) - X (1) Y (2))}^{2}$
82		eqid	$⊢ R^{2} ({(X (2) - Y (2))}^{2} + {(Y (1) - X (1))}^{2}) - {(X (2) Y (1) - X (1) Y (2))}^{2} = R^{2} ({(X (2) - Y (2))}^{2} + {(Y (1) - X (1))}^{2}) - {(X (2) Y (1) - X (1) Y (2))}^{2}$
83		eqid	$⊢ X (2) Y (1) - X (1) Y (2) = X (2) Y (1) - X (1) Y (2)$
84	1 2 3 4 5 6 51 82 26 25 83	inlinecirc02plem	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < R^{2} ({(X (2) - Y (2))}^{2} + {(Y (1) - X (1))}^{2}) - {(X (2) Y (1) - X (1) Y (2))}^{2})) \to \exists a \in P \exists b \in P ((\underset{˙}{0} S R) \cap (X L Y) = \{a, b\} \land a \neq b)$
85	10 12 81 84	syl12anc	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to \exists a \in P \exists b \in P ((\underset{˙}{0} S R) \cap (X L Y) = \{a, b\} \land a \neq b)$
86		prprelprb	$⊢ (\underset{˙}{0} S R) \cap (X L Y) \in PrPairs (P) \leftrightarrow (P \in V \land \exists a \in P \exists b \in P ((\underset{˙}{0} S R) \cap (X L Y) = \{a, b\} \land a \neq b))$
87	9 85 86	sylanbrc	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to (\underset{˙}{0} S R) \cap (X L Y) \in PrPairs (P)$

Metamath Proof Explorer

Theorem inlinecirc02p

Proof