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 = (0 ..^2)$
	inlinecirc02p.e	$⊢ E = I$
	inlinecirc02p.p	$⊢ P = ℝ^{I}$
	inlinecirc02p.s	$⊢ S = Sphere (E)$
	inlinecirc02p.0	$⊢ \underset{˙}{0} = ⟨“ 00 ”⟩$
	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 = (0 ..^2)$
2		inlinecirc02p.e	$⊢ E = I$
3		inlinecirc02p.p	$⊢ P = ℝ^{I}$
4		inlinecirc02p.s	$⊢ S = Sphere (E)$
5		inlinecirc02p.0	$⊢ \underset{˙}{0} = ⟨“ 00 ”⟩$
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 (0) \in ℝ$
14	13	3ad2ant1	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X (0) \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 (0) \in ℝ$
16	1 3	rrx2pyel	$⊢ X \in P \to X (1) \in ℝ$
17	16	3ad2ant1	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X (1) \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 (1) \in ℝ$
19	1 3	rrx2pxel	$⊢ Y \in P \to Y (0) \in ℝ$
20	19	3ad2ant2	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Y (0) \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 (0) \in ℝ$
22	1 3	rrx2pyel	$⊢ Y \in P \to Y (1) \in ℝ$
23	22	3ad2ant2	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Y (1) \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 (1) \in ℝ$
25		eqid	$⊢ Y (0) - X (0) = Y (0) - X (0)$
26		eqid	$⊢ X (1) - Y (1) = X (1) - Y (1)$
27		eqid	$⊢ (Y (0) - X (0)) X (1) + (X (1) - Y (1)) X (0) = (Y (0) - X (0)) X (1) + (X (1) - Y (1)) X (0)$
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	1	eqcomi	$⊢ (0 ..^2) = I$
32	31	fveq2i	$⊢ (0 ..^2) = I$
33		2nn0	$⊢ 2 \in ℕ_{0}$
34		eqid	$⊢ 𝔼_{hil} (2) = 𝔼_{hil} (2)$
35	34	ehlval	$⊢ 2 \in ℕ_{0} \to 𝔼_{hil} (2) = (0 ..^2)$
36	33 35	ax-mp	$⊢ 𝔼_{hil} (2) = (0 ..^2)$
37	32 36 2	3eqtr4ri	$⊢ E = 𝔼_{hil} (2)$
38	1	oveq2i	$⊢ ℝ^{I} = ℝ^{(0 ..^2)}$
39	3 38	eqtri	$⊢ P = ℝ^{(0 ..^2)}$
40	37 39 7 5	ehl2eudis0lt	$⊢ (X \in P \land R \in ℝ^{+}) \to (X D \underset{˙}{0} < R \leftrightarrow {X (0)}^{2} + {X (1)}^{2} < R^{2})$
41	40	3ad2antl1	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land R \in ℝ^{+}) \to (X D \underset{˙}{0} < R \leftrightarrow {X (0)}^{2} + {X (1)}^{2} < R^{2})$
42	41	biimpd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land R \in ℝ^{+}) \to (X D \underset{˙}{0} < R \to {X (0)}^{2} + {X (1)}^{2} < R^{2})$
43	42	impr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to {X (0)}^{2} + {X (1)}^{2} < R^{2}$
44	1 3	rrx2pnecoorneor	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (X (0) \neq Y (0) \lor X (1) \neq Y (1))$
45	44	orcomd	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (X (1) \neq Y (1) \lor X (0) \neq Y (0))$
46	45	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to (X (1) \neq Y (1) \lor X (0) \neq Y (0))$
47		eqid	$⊢ {(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2} = {(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}$
48		eqid	$⊢ R^{2} ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) - {((Y (0) - X (0)) X (1) + (X (1) - Y (1)) X (0))}^{2} = R^{2} ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) - {((Y (0) - X (0)) X (1) + (X (1) - Y (1)) X (0))}^{2}$
49	15 18 21 24 25 26 27 30 43 46 47 48	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 (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) - {((Y (0) - X (0)) X (1) + (X (1) - Y (1)) X (0))}^{2}$
50	19	recnd	$⊢ Y \in P \to Y (0) \in ℂ$
51	50	adantl	$⊢ (X \in P \land Y \in P) \to Y (0) \in ℂ$
52	13	recnd	$⊢ X \in P \to X (0) \in ℂ$
53	52	adantr	$⊢ (X \in P \land Y \in P) \to X (0) \in ℂ$
54	16	recnd	$⊢ X \in P \to X (1) \in ℂ$
55	54	adantr	$⊢ (X \in P \land Y \in P) \to X (1) \in ℂ$
56	51 53 55	subdird	$⊢ (X \in P \land Y \in P) \to (Y (0) - X (0)) X (1) = Y (0) X (1) - X (0) X (1)$
57	22	recnd	$⊢ Y \in P \to Y (1) \in ℂ$
58	57	adantl	$⊢ (X \in P \land Y \in P) \to Y (1) \in ℂ$
59	55 58 53	subdird	$⊢ (X \in P \land Y \in P) \to (X (1) - Y (1)) X (0) = X (1) X (0) - Y (1) X (0)$
60	56 59	oveq12d	$⊢ (X \in P \land Y \in P) \to (Y (0) - X (0)) X (1) + (X (1) - Y (1)) X (0) = (Y (0) X (1) - X (0) X (1)) + X (1) X (0) - Y (1) X (0)$
61	51 55	mulcomd	$⊢ (X \in P \land Y \in P) \to Y (0) X (1) = X (1) Y (0)$
62	61	oveq1d	$⊢ (X \in P \land Y \in P) \to Y (0) X (1) - X (0) X (1) = X (1) Y (0) - X (0) X (1)$
63	55 53	mulcomd	$⊢ (X \in P \land Y \in P) \to X (1) X (0) = X (0) X (1)$
64	58 53	mulcomd	$⊢ (X \in P \land Y \in P) \to Y (1) X (0) = X (0) Y (1)$
65	63 64	oveq12d	$⊢ (X \in P \land Y \in P) \to X (1) X (0) - Y (1) X (0) = X (0) X (1) - X (0) Y (1)$
66	62 65	oveq12d	$⊢ (X \in P \land Y \in P) \to (Y (0) X (1) - X (0) X (1)) + X (1) X (0) - Y (1) X (0) = (X (1) Y (0) - X (0) X (1)) + X (0) X (1) - X (0) Y (1)$
67	55 51	mulcld	$⊢ (X \in P \land Y \in P) \to X (1) Y (0) \in ℂ$
68	53 55	mulcld	$⊢ (X \in P \land Y \in P) \to X (0) X (1) \in ℂ$
69	53 58	mulcld	$⊢ (X \in P \land Y \in P) \to X (0) Y (1) \in ℂ$
70	67 68 69	npncand	$⊢ (X \in P \land Y \in P) \to (X (1) Y (0) - X (0) X (1)) + X (0) X (1) - X (0) Y (1) = X (1) Y (0) - X (0) Y (1)$
71	60 66 70	3eqtrd	$⊢ (X \in P \land Y \in P) \to (Y (0) - X (0)) X (1) + (X (1) - Y (1)) X (0) = X (1) Y (0) - X (0) Y (1)$
72	71	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (Y (0) - X (0)) X (1) + (X (1) - Y (1)) X (0) = X (1) Y (0) - X (0) Y (1)$
73	72	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to (Y (0) - X (0)) X (1) + (X (1) - Y (1)) X (0) = X (1) Y (0) - X (0) Y (1)$
74	73	eqcomd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to X (1) Y (0) - X (0) Y (1) = (Y (0) - X (0)) X (1) + (X (1) - Y (1)) X (0)$
75	74	oveq1d	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land X D \underset{˙}{0} < R)) \to {(X (1) Y (0) - X (0) Y (1))}^{2} = {((Y (0) - X (0)) X (1) + (X (1) - Y (1)) X (0))}^{2}$
76	75	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 (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) - {(X (1) Y (0) - X (0) Y (1))}^{2} = R^{2} ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) - {((Y (0) - X (0)) X (1) + (X (1) - Y (1)) X (0))}^{2}$
77	49 76	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 (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) - {(X (1) Y (0) - X (0) Y (1))}^{2}$
78		eqid	$⊢ R^{2} ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) - {(X (1) Y (0) - X (0) Y (1))}^{2} = R^{2} ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) - {(X (1) Y (0) - X (0) Y (1))}^{2}$
79		eqid	$⊢ X (1) Y (0) - X (0) Y (1) = X (1) Y (0) - X (0) Y (1)$
80	1 2 3 4 5 6 47 78 26 25 79	inlinecirc02plem	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 < R^{2} ({(X (1) - Y (1))}^{2} + {(Y (0) - X (0))}^{2}) - {(X (1) Y (0) - X (0) Y (1))}^{2})) \to \exists a \in P \exists b \in P ((\underset{˙}{0} S R) \cap (X L Y) = \{a, b\} \land a \neq b)$
81	10 12 77 80	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)$
82		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))$
83	9 81 82	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