itsclinecirc0in

Description: The intersection points of a line through two different points and a circle around the origin, using the definition of a line in a two dimensional Euclidean space, expressed as intersection. (Contributed by AV, 7-May-2023) (Revised by AV, 14-May-2023)

	Ref	Expression
Hypotheses	itsclinecirc0b.i	$⊢ I = \{1, 2\}$
	itsclinecirc0b.e	$⊢ E = I$
	itsclinecirc0b.p	$⊢ P = ℝ^{I}$
	itsclinecirc0b.s	$⊢ S = Sphere (E)$
	itsclinecirc0b.0	$⊢ \underset{˙}{0} = I \times \{0\}$
	itsclinecirc0b.q	$⊢ Q = A^{2} + B^{2}$
	itsclinecirc0b.d	$⊢ D = R^{2} Q - C^{2}$
	itsclinecirc0b.l	$⊢ L = {Line}_{M} (E)$
	itsclinecirc0b.a	$⊢ A = X (2) - Y (2)$
	itsclinecirc0b.b	$⊢ B = Y (1) - X (1)$
	itsclinecirc0b.c	$⊢ C = X (2) Y (1) - X (1) Y (2)$
Assertion	itsclinecirc0in	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to (\underset{˙}{0} S R) \cap (X L Y) = \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}\}$

Proof

Step	Hyp	Ref	Expression
1		itsclinecirc0b.i	$⊢ I = \{1, 2\}$
2		itsclinecirc0b.e	$⊢ E = I$
3		itsclinecirc0b.p	$⊢ P = ℝ^{I}$
4		itsclinecirc0b.s	$⊢ S = Sphere (E)$
5		itsclinecirc0b.0	$⊢ \underset{˙}{0} = I \times \{0\}$
6		itsclinecirc0b.q	$⊢ Q = A^{2} + B^{2}$
7		itsclinecirc0b.d	$⊢ D = R^{2} Q - C^{2}$
8		itsclinecirc0b.l	$⊢ L = {Line}_{M} (E)$
9		itsclinecirc0b.a	$⊢ A = X (2) - Y (2)$
10		itsclinecirc0b.b	$⊢ B = Y (1) - X (1)$
11		itsclinecirc0b.c	$⊢ C = X (2) Y (1) - X (1) Y (2)$
12		elin	$⊢ z \in ((\underset{˙}{0} S R) \cap (X L Y)) \leftrightarrow (z \in (\underset{˙}{0} S R) \land z \in (X L Y))$
13	1 2 3 4 5 6 7 8 9 10 11	itsclinecirc0b	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to ((z \in (\underset{˙}{0} S R) \land z \in (X L Y)) \leftrightarrow (z \in P \land ((z (1) = \frac{A C + B \sqrt{D}}{Q} \land z (2) = \frac{B C - A \sqrt{D}}{Q}) \lor (z (1) = \frac{A C - B \sqrt{D}}{Q} \land z (2) = \frac{B C + A \sqrt{D}}{Q}))))$
14	12 13	bitrid	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to (z \in ((\underset{˙}{0} S R) \cap (X L Y)) \leftrightarrow (z \in P \land ((z (1) = \frac{A C + B \sqrt{D}}{Q} \land z (2) = \frac{B C - A \sqrt{D}}{Q}) \lor (z (1) = \frac{A C - B \sqrt{D}}{Q} \land z (2) = \frac{B C + A \sqrt{D}}{Q}))))$
15	1 3	rrx2pyel	$⊢ X \in P \to X (2) \in ℝ$
16	15	adantr	$⊢ (X \in P \land Y \in P) \to X (2) \in ℝ$
17	1 3	rrx2pyel	$⊢ Y \in P \to Y (2) \in ℝ$
18	17	adantl	$⊢ (X \in P \land Y \in P) \to Y (2) \in ℝ$
19	16 18	resubcld	$⊢ (X \in P \land Y \in P) \to X (2) - Y (2) \in ℝ$
20	9 19	eqeltrid	$⊢ (X \in P \land Y \in P) \to A \in ℝ$
21	20	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to A \in ℝ$
22	21	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to A \in ℝ$
23	1 3	rrx2pxel	$⊢ Y \in P \to Y (1) \in ℝ$
24	23	adantl	$⊢ (X \in P \land Y \in P) \to Y (1) \in ℝ$
25	1 3	rrx2pxel	$⊢ X \in P \to X (1) \in ℝ$
26	25	adantr	$⊢ (X \in P \land Y \in P) \to X (1) \in ℝ$
27	24 26	resubcld	$⊢ (X \in P \land Y \in P) \to Y (1) - X (1) \in ℝ$
28	10 27	eqeltrid	$⊢ (X \in P \land Y \in P) \to B \in ℝ$
29	28	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to B \in ℝ$
30	29	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to B \in ℝ$
31	16 24	remulcld	$⊢ (X \in P \land Y \in P) \to X (2) Y (1) \in ℝ$
32	26 18	remulcld	$⊢ (X \in P \land Y \in P) \to X (1) Y (2) \in ℝ$
33	31 32	resubcld	$⊢ (X \in P \land Y \in P) \to X (2) Y (1) - X (1) Y (2) \in ℝ$
34	11 33	eqeltrid	$⊢ (X \in P \land Y \in P) \to C \in ℝ$
35	34	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to C \in ℝ$
36	35	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to C \in ℝ$
37	22 30 36	3jca	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A \in ℝ \land B \in ℝ \land C \in ℝ)$
38	21 29 35	3jca	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (A \in ℝ \land B \in ℝ \land C \in ℝ)$
39		rpre	$⊢ R \in ℝ^{+} \to R \in ℝ$
40	39	adantr	$⊢ (R \in ℝ^{+} \land 0 \leq D) \to R \in ℝ$
41	6 7	itsclc0lem3	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ) \to D \in ℝ$
42	38 40 41	syl2an	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to D \in ℝ$
43		simprr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to 0 \leq D$
44	42 43	jca	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to (D \in ℝ \land 0 \leq D)$
45	20 28	jca	$⊢ (X \in P \land Y \in P) \to (A \in ℝ \land B \in ℝ)$
46	6	resum2sqcl	$⊢ (A \in ℝ \land B \in ℝ) \to Q \in ℝ$
47	45 46	syl	$⊢ (X \in P \land Y \in P) \to Q \in ℝ$
48	47	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Q \in ℝ$
49	1 3 10 9	rrx2pnedifcoorneorr	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (B \neq 0 \lor A \neq 0)$
50	49	orcomd	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (A \neq 0 \lor B \neq 0)$
51	6	resum2sqorgt0	$⊢ (A \in ℝ \land B \in ℝ \land (A \neq 0 \lor B \neq 0)) \to 0 < Q$
52	21 29 50 51	syl3anc	$⊢ (X \in P \land Y \in P \land X \neq Y) \to 0 < Q$
53	52	gt0ne0d	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Q \neq 0$
54	48 53	jca	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (Q \in ℝ \land Q \neq 0)$
55	54	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to (Q \in ℝ \land Q \neq 0)$
56		itsclc0lem1	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (D \in ℝ \land 0 \leq D) \land (Q \in ℝ \land Q \neq 0)) \to \frac{A C + B \sqrt{D}}{Q} \in ℝ$
57	37 44 55 56	syl3anc	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A C + B \sqrt{D}}{Q} \in ℝ$
58	30 22 36	3jca	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to (B \in ℝ \land A \in ℝ \land C \in ℝ)$
59	48	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q \in ℝ$
60	53	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q \neq 0$
61	59 60	jca	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to (Q \in ℝ \land Q \neq 0)$
62		itsclc0lem2	$⊢ ((B \in ℝ \land A \in ℝ \land C \in ℝ) \land (D \in ℝ \land 0 \leq D) \land (Q \in ℝ \land Q \neq 0)) \to \frac{B C - A \sqrt{D}}{Q} \in ℝ$
63	58 44 61 62	syl3anc	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B C - A \sqrt{D}}{Q} \in ℝ$
64		itsclc0lem2	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (D \in ℝ \land 0 \leq D) \land (Q \in ℝ \land Q \neq 0)) \to \frac{A C - B \sqrt{D}}{Q} \in ℝ$
65	37 44 61 64	syl3anc	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{A C - B \sqrt{D}}{Q} \in ℝ$
66		itsclc0lem1	$⊢ ((B \in ℝ \land A \in ℝ \land C \in ℝ) \land (D \in ℝ \land 0 \leq D) \land (Q \in ℝ \land Q \neq 0)) \to \frac{B C + A \sqrt{D}}{Q} \in ℝ$
67	58 44 61 66	syl3anc	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B C + A \sqrt{D}}{Q} \in ℝ$
68	1 3	prelrrx2b	$⊢ ((\frac{A C + B \sqrt{D}}{Q} \in ℝ \land \frac{B C - A \sqrt{D}}{Q} \in ℝ) \land (\frac{A C - B \sqrt{D}}{Q} \in ℝ \land \frac{B C + A \sqrt{D}}{Q} \in ℝ)) \to ((z \in P \land ((z (1) = \frac{A C + B \sqrt{D}}{Q} \land z (2) = \frac{B C - A \sqrt{D}}{Q}) \lor (z (1) = \frac{A C - B \sqrt{D}}{Q} \land z (2) = \frac{B C + A \sqrt{D}}{Q}))) \leftrightarrow z \in \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}\})$
69	57 63 65 67 68	syl22anc	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to ((z \in P \land ((z (1) = \frac{A C + B \sqrt{D}}{Q} \land z (2) = \frac{B C - A \sqrt{D}}{Q}) \lor (z (1) = \frac{A C - B \sqrt{D}}{Q} \land z (2) = \frac{B C + A \sqrt{D}}{Q}))) \leftrightarrow z \in \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}\})$
70	14 69	bitrd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to (z \in ((\underset{˙}{0} S R) \cap (X L Y)) \leftrightarrow z \in \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}\})$
71	70	eqrdv	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to (\underset{˙}{0} S R) \cap (X L Y) = \{\{⟨1, \frac{A C + B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C - A \sqrt{D}}{Q}⟩\}, \{⟨1, \frac{A C - B \sqrt{D}}{Q}⟩, ⟨2, \frac{B C + A \sqrt{D}}{Q}⟩\}\}$

Metamath Proof Explorer

Theorem itsclinecirc0in

Proof