itsclinecirc0b

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. (Contributed by AV, 2-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	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}))))$

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		eqid	$⊢ Y (2) - X (2) = Y (2) - X (2)$
13	1 2 3 8 10 12 11	rrx2linest	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X L Y = \{p \in P \| B p (2) = (Y (2) - X (2)) p (1) + C\}$
14	13	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to X L Y = \{p \in P \| B p (2) = (Y (2) - X (2)) p (1) + C\}$
15	1 3	rrx2pxel	$⊢ Y \in P \to Y (1) \in ℝ$
16	15	adantl	$⊢ (X \in P \land Y \in P) \to Y (1) \in ℝ$
17	1 3	rrx2pxel	$⊢ X \in P \to X (1) \in ℝ$
18	17	adantr	$⊢ (X \in P \land Y \in P) \to X (1) \in ℝ$
19	16 18	resubcld	$⊢ (X \in P \land Y \in P) \to Y (1) - X (1) \in ℝ$
20	10 19	eqeltrid	$⊢ (X \in P \land Y \in P) \to B \in ℝ$
21	20	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to B \in ℝ$
22	21	ad2antrr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to B \in ℝ$
23	1 3	rrx2pyel	$⊢ p \in P \to p (2) \in ℝ$
24	23	adantl	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to p (2) \in ℝ$
25	22 24	remulcld	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to B p (2) \in ℝ$
26	25	recnd	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to B p (2) \in ℂ$
27	1 3	rrx2pyel	$⊢ Y \in P \to Y (2) \in ℝ$
28	27	adantl	$⊢ (X \in P \land Y \in P) \to Y (2) \in ℝ$
29	1 3	rrx2pyel	$⊢ X \in P \to X (2) \in ℝ$
30	29	adantr	$⊢ (X \in P \land Y \in P) \to X (2) \in ℝ$
31	28 30	resubcld	$⊢ (X \in P \land Y \in P) \to Y (2) - X (2) \in ℝ$
32	31	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Y (2) - X (2) \in ℝ$
33	32	ad2antrr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to Y (2) - X (2) \in ℝ$
34	1 3	rrx2pxel	$⊢ p \in P \to p (1) \in ℝ$
35	34	adantl	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to p (1) \in ℝ$
36	33 35	remulcld	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to (Y (2) - X (2)) p (1) \in ℝ$
37	36	recnd	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to (Y (2) - X (2)) p (1) \in ℂ$
38	30 16	remulcld	$⊢ (X \in P \land Y \in P) \to X (2) Y (1) \in ℝ$
39	18 28	remulcld	$⊢ (X \in P \land Y \in P) \to X (1) Y (2) \in ℝ$
40	38 39	resubcld	$⊢ (X \in P \land Y \in P) \to X (2) Y (1) - X (1) Y (2) \in ℝ$
41	11 40	eqeltrid	$⊢ (X \in P \land Y \in P) \to C \in ℝ$
42	41	recnd	$⊢ (X \in P \land Y \in P) \to C \in ℂ$
43	42	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to C \in ℂ$
44	43	ad2antrr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to C \in ℂ$
45	26 37 44	subaddd	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to (B p (2) - (Y (2) - X (2)) p (1) = C \leftrightarrow (Y (2) - X (2)) p (1) + C = B p (2))$
46		eqcom	$⊢ B p (2) = (Y (2) - X (2)) p (1) + C \leftrightarrow (Y (2) - X (2)) p (1) + C = B p (2)$
47	45 46	syl6rbbr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to (B p (2) = (Y (2) - X (2)) p (1) + C \leftrightarrow B p (2) - (Y (2) - X (2)) p (1) = C)$
48	30 28	resubcld	$⊢ (X \in P \land Y \in P) \to X (2) - Y (2) \in ℝ$
49	9 48	eqeltrid	$⊢ (X \in P \land Y \in P) \to A \in ℝ$
50	49	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to A \in ℝ$
51	50	ad2antrr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to A \in ℝ$
52	51 35	remulcld	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to A p (1) \in ℝ$
53	52	recnd	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to A p (1) \in ℂ$
54	53 26	addcomd	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to A p (1) + B p (2) = B p (2) + A p (1)$
55	28	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Y (2) \in ℝ$
56	55	ad2antrr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to Y (2) \in ℝ$
57	56	recnd	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to Y (2) \in ℂ$
58	30	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to X (2) \in ℝ$
59	58	ad2antrr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to X (2) \in ℝ$
60	59	recnd	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to X (2) \in ℂ$
61	57 60	negsubdi2d	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to - (Y (2) - X (2)) = X (2) - Y (2)$
62	61 9	syl6reqr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to A = - (Y (2) - X (2))$
63	62	oveq1d	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to A p (1) = (- (Y (2) - X (2))) p (1)$
64	31	recnd	$⊢ (X \in P \land Y \in P) \to Y (2) - X (2) \in ℂ$
65	64	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to Y (2) - X (2) \in ℂ$
66	65	ad2antrr	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to Y (2) - X (2) \in ℂ$
67	35	recnd	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to p (1) \in ℂ$
68	66 67	mulneg1d	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to (- (Y (2) - X (2))) p (1) = - (Y (2) - X (2)) p (1)$
69	63 68	eqtr2d	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to - (Y (2) - X (2)) p (1) = A p (1)$
70	69	oveq2d	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to B p (2) + (- (Y (2) - X (2)) p (1)) = B p (2) + A p (1)$
71	26 37	negsubd	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to B p (2) + (- (Y (2) - X (2)) p (1)) = B p (2) - (Y (2) - X (2)) p (1)$
72	54 70 71	3eqtr2rd	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to B p (2) - (Y (2) - X (2)) p (1) = A p (1) + B p (2)$
73	72	eqeq1d	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to (B p (2) - (Y (2) - X (2)) p (1) = C \leftrightarrow A p (1) + B p (2) = C)$
74	47 73	bitrd	$⊢ (((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \land p \in P) \to (B p (2) = (Y (2) - X (2)) p (1) + C \leftrightarrow A p (1) + B p (2) = C)$
75	74	rabbidva	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to \{p \in P \| B p (2) = (Y (2) - X (2)) p (1) + C\} = \{p \in P \| A p (1) + B p (2) = C\}$
76	14 75	eqtrd	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to X L Y = \{p \in P \| A p (1) + B p (2) = C\}$
77	76	eleq2d	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to (Z \in (X L Y) \leftrightarrow Z \in \{p \in P \| A p (1) + B p (2) = C\})$
78	77	anbi2d	$⊢ ((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 (\underset{˙}{0} S R) \land Z \in \{p \in P \| A p (1) + B p (2) = C\}))$
79	50	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to A \in ℝ$
80	21	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to B \in ℝ$
81	41	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to C \in ℝ$
82	81	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to C \in ℝ$
83	1 3 10 9	rrx2pnedifcoorneorr	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (B \neq 0 \lor A \neq 0)$
84	83	orcomd	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (A \neq 0 \lor B \neq 0)$
85	84	adantr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to (A \neq 0 \lor B \neq 0)$
86		simpr	$⊢ ((X \in P \land Y \in P \land X \neq Y) \land (R \in ℝ^{+} \land 0 \leq D)) \to (R \in ℝ^{+} \land 0 \leq D)$
87		eqid	$⊢ \{p \in P \| A p (1) + B p (2) = C\} = \{p \in P \| A p (1) + B p (2) = C\}$
88	1 2 3 4 5 6 7 87	itsclc0b	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0) \land (R \in ℝ^{+} \land 0 \leq D)) \to ((Z \in (\underset{˙}{0} S R) \land Z \in \{p \in P \| A p (1) + B p (2) = C\}) \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}))))$
89	79 80 82 85 86 88	syl311anc	$⊢ ((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 \{p \in P \| A p (1) + B p (2) = C\}) \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}))))$
90	78 89	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) \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}))))$

Metamath Proof Explorer

Theorem itsclinecirc0b

Proof