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 = (0 ..^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 (1) - Y (1)$
	itsclinecirc0b.b	$⊢ B = Y (0) - X (0)$
	itsclinecirc0b.c	$⊢ C = X (1) Y (0) - X (0) Y (1)$
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) = \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩\}$

Proof

Step	Hyp	Ref	Expression
1		itsclinecirc0b.i	$⊢ I = (0 ..^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 (1) - Y (1)$
10		itsclinecirc0b.b	$⊢ B = Y (0) - X (0)$
11		itsclinecirc0b.c	$⊢ C = X (1) Y (0) - X (0) Y (1)$
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 (0) = \frac{A C + B \sqrt{D}}{Q} \land z (1) = \frac{B C - A \sqrt{D}}{Q}) \lor (z (0) = \frac{A C - B \sqrt{D}}{Q} \land z (1) = \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 (0) = \frac{A C + B \sqrt{D}}{Q} \land z (1) = \frac{B C - A \sqrt{D}}{Q}) \lor (z (0) = \frac{A C - B \sqrt{D}}{Q} \land z (1) = \frac{B C + A \sqrt{D}}{Q}))))$
15	1 3	rrx2pyel	$⊢ X \in P \to X (1) \in ℝ$
16	15	adantr	$⊢ (X \in P \land Y \in P) \to X (1) \in ℝ$
17	1 3	rrx2pyel	$⊢ Y \in P \to Y (1) \in ℝ$
18	17	adantl	$⊢ (X \in P \land Y \in P) \to Y (1) \in ℝ$
19	16 18	resubcld	$⊢ (X \in P \land Y \in P) \to X (1) - Y (1) \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 (0) \in ℝ$
24	23	adantl	$⊢ (X \in P \land Y \in P) \to Y (0) \in ℝ$
25	1 3	rrx2pxel	$⊢ X \in P \to X (0) \in ℝ$
26	25	adantr	$⊢ (X \in P \land Y \in P) \to X (0) \in ℝ$
27	24 26	resubcld	$⊢ (X \in P \land Y \in P) \to Y (0) - X (0) \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 (1) Y (0) \in ℝ$
32	26 18	remulcld	$⊢ (X \in P \land Y \in P) \to X (0) Y (1) \in ℝ$
33	31 32	resubcld	$⊢ (X \in P \land Y \in P) \to X (1) Y (0) - X (0) Y (1) \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	6	resum2sqcl	$⊢ (A \in ℝ \land B \in ℝ) \to Q \in ℝ$
46	20 28 45	syl2anc	$⊢ (X \in P \land Y \in P) \to Q \in ℝ$
47	46	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Q \in ℝ$
48	1 3 10 9	rrx2pnedifcoorneorr	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (B \neq 0 \lor A \neq 0)$
49	48	orcomd	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (A \neq 0 \lor B \neq 0)$
50	6	resum2sqorgt0	$⊢ (A \in ℝ \land B \in ℝ \land (A \neq 0 \lor B \neq 0)) \to 0 < Q$
51	21 29 49 50	syl3anc	$⊢ (X \in P \land Y \in P \land X \neq Y) \to 0 < Q$
52	51	gt0ne0d	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Q \neq 0$
53	47 52	jca	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (Q \in ℝ \land Q \neq 0)$
54	53	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)$
55		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 ℝ$
56	37 44 54 55	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 ℝ$
57	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 ℝ)$
58		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 ℝ$
59	57 44 54 58	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 ℝ$
60		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 ℝ$
61	37 44 54 60	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 ℝ$
62		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 ℝ$
63	57 44 54 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	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 (0) = \frac{A C + B \sqrt{D}}{Q} \land z (1) = \frac{B C - A \sqrt{D}}{Q}) \lor (z (0) = \frac{A C - B \sqrt{D}}{Q} \land z (1) = \frac{B C + A \sqrt{D}}{Q}))) \leftrightarrow z \in \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩\})$
65	56 59 61 63 64	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 (0) = \frac{A C + B \sqrt{D}}{Q} \land z (1) = \frac{B C - A \sqrt{D}}{Q}) \lor (z (0) = \frac{A C - B \sqrt{D}}{Q} \land z (1) = \frac{B C + A \sqrt{D}}{Q}))) \leftrightarrow z \in \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩\})$
66	14 65	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 \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩\})$
67	66	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) = \{⟨“ (\frac{A C + B \sqrt{D}}{Q}) (\frac{B C - A \sqrt{D}}{Q}) ”⟩, ⟨“ (\frac{A C - B \sqrt{D}}{Q}) (\frac{B C + A \sqrt{D}}{Q}) ”⟩\}$

Metamath Proof Explorer

Theorem itsclinecirc0in

Proof