itschlc0xyqsol1

Description: Lemma for itsclc0 . Solutions of the quadratic equations for the coordinates of the intersection points of a horizontal line and a circle. (Contributed by AV, 25-Feb-2023)

	Ref	Expression
Hypotheses	itscnhlc0yqe.q	$⊢ Q = A^{2} + B^{2}$
	itsclc0yqsol.d	$⊢ D = R^{2} Q - C^{2}$
Assertion	itschlc0xyqsol1	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to (Y = \frac{C}{B} \land (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B})))$

Proof

Step	Hyp	Ref	Expression
1		itscnhlc0yqe.q	$⊢ Q = A^{2} + B^{2}$
2		itsclc0yqsol.d	$⊢ D = R^{2} Q - C^{2}$
3		animorr	$⊢ (A = 0 \land B \neq 0) \to (A \neq 0 \lor B \neq 0)$
4	3	anim2i	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0))$
5	1 2	itsclc0yqsol	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A \neq 0 \lor B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to (Y = \frac{B C - A \sqrt{D}}{Q} \lor Y = \frac{B C + A \sqrt{D}}{Q}))$
6	4 5	syl3an1	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to (Y = \frac{B C - A \sqrt{D}}{Q} \lor Y = \frac{B C + A \sqrt{D}}{Q}))$
7	6	imp	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land (X^{2} + Y^{2} = R^{2} \land A X + B Y = C)) \to (Y = \frac{B C - A \sqrt{D}}{Q} \lor Y = \frac{B C + A \sqrt{D}}{Q})$
8		oveq1	$⊢ A = 0 \to A \sqrt{D} = 0 \cdot \sqrt{D}$
9	8	adantr	$⊢ (A = 0 \land B \neq 0) \to A \sqrt{D} = 0 \cdot \sqrt{D}$
10	9	adantl	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to A \sqrt{D} = 0 \cdot \sqrt{D}$
11	10	adantr	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to A \sqrt{D} = 0 \cdot \sqrt{D}$
12		rpcn	$⊢ R \in ℝ^{+} \to R \in ℂ$
13	12	adantr	$⊢ (R \in ℝ^{+} \land 0 \leq D) \to R \in ℂ$
14	13	adantl	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to R \in ℂ$
15	14	sqcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to R^{2} \in ℂ$
16	1	resum2sqcl	$⊢ (A \in ℝ \land B \in ℝ) \to Q \in ℝ$
17	16	recnd	$⊢ (A \in ℝ \land B \in ℝ) \to Q \in ℂ$
18	17	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to Q \in ℂ$
19	18	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to Q \in ℂ$
20	19	adantr	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q \in ℂ$
21	15 20	mulcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to R^{2} Q \in ℂ$
22		simpll3	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to C \in ℝ$
23	22	recnd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to C \in ℂ$
24	23	sqcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to C^{2} \in ℂ$
25	21 24	subcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to R^{2} Q - C^{2} \in ℂ$
26	2 25	eqeltrid	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to D \in ℂ$
27	26	sqrtcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \sqrt{D} \in ℂ$
28	27	mul02d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to 0 \cdot \sqrt{D} = 0$
29	11 28	eqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to A \sqrt{D} = 0$
30	29	oveq2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C - A \sqrt{D} = B C - 0$
31		simpll2	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B \in ℝ$
32	31	recnd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B \in ℂ$
33	32 23	mulcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C \in ℂ$
34	33	subid1d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C - 0 = B C$
35	30 34	eqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C - A \sqrt{D} = B C$
36		sq0i	$⊢ A = 0 \to A^{2} = 0$
37	36	adantr	$⊢ (A = 0 \land B \neq 0) \to A^{2} = 0$
38	37	adantl	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to A^{2} = 0$
39	38	adantr	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} = 0$
40	39	oveq1d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} + B^{2} = 0 + B^{2}$
41	32	sqcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} \in ℂ$
42	41	addid2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to 0 + B^{2} = B^{2}$
43	40 42	eqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to A^{2} + B^{2} = B^{2}$
44	1 43	syl5eq	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q = B^{2}$
45		recn	$⊢ B \in ℝ \to B \in ℂ$
46	45	sqvald	$⊢ B \in ℝ \to B^{2} = B B$
47	46	3ad2ant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B^{2} = B B$
48	47	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to B^{2} = B B$
49	48	adantr	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} = B B$
50	44 49	eqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to Q = B B$
51	35 50	oveq12d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B C - A \sqrt{D}}{Q} = \frac{B C}{B B}$
52		simplrr	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B \neq 0$
53	23 32 32 52 52	divcan5d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B C}{B B} = \frac{C}{B}$
54	51 53	eqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B C - A \sqrt{D}}{Q} = \frac{C}{B}$
55	54	eqeq2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to (Y = \frac{B C - A \sqrt{D}}{Q} \leftrightarrow Y = \frac{C}{B})$
56	55	biimpd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to (Y = \frac{B C - A \sqrt{D}}{Q} \to Y = \frac{C}{B})$
57	29	oveq2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C + A \sqrt{D} = B C + 0$
58	33	addid1d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C + 0 = B C$
59	57 58	eqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B C + A \sqrt{D} = B C$
60	59 44	oveq12d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B C + A \sqrt{D}}{Q} = \frac{B C}{B^{2}}$
61		simp2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B \in ℝ$
62	61	recnd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B \in ℂ$
63	62	sqvald	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B^{2} = B B$
64	63	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to B^{2} = B B$
65	64	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to \frac{B C}{B^{2}} = \frac{B C}{B B}$
66		simpl3	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to C \in ℝ$
67	66	recnd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to C \in ℂ$
68	62	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to B \in ℂ$
69		simpr	$⊢ (A = 0 \land B \neq 0) \to B \neq 0$
70	69	adantl	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to B \neq 0$
71	67 68 68 70 70	divcan5d	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to \frac{B C}{B B} = \frac{C}{B}$
72	65 71	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \to \frac{B C}{B^{2}} = \frac{C}{B}$
73	72	adantr	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B C}{B^{2}} = \frac{C}{B}$
74	60 73	eqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B C + A \sqrt{D}}{Q} = \frac{C}{B}$
75	74	eqeq2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to (Y = \frac{B C + A \sqrt{D}}{Q} \leftrightarrow Y = \frac{C}{B})$
76	75	biimpd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to (Y = \frac{B C + A \sqrt{D}}{Q} \to Y = \frac{C}{B})$
77	56 76	jaod	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to ((Y = \frac{B C - A \sqrt{D}}{Q} \lor Y = \frac{B C + A \sqrt{D}}{Q}) \to Y = \frac{C}{B})$
78	77	3adant3	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to ((Y = \frac{B C - A \sqrt{D}}{Q} \lor Y = \frac{B C + A \sqrt{D}}{Q}) \to Y = \frac{C}{B})$
79	78	adantr	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land (X^{2} + Y^{2} = R^{2} \land A X + B Y = C)) \to ((Y = \frac{B C - A \sqrt{D}}{Q} \lor Y = \frac{B C + A \sqrt{D}}{Q}) \to Y = \frac{C}{B})$
80		oveq1	$⊢ Y = \frac{C}{B} \to Y^{2} = {(\frac{C}{B})}^{2}$
81	80	oveq2d	$⊢ Y = \frac{C}{B} \to X^{2} + Y^{2} = X^{2} + {(\frac{C}{B})}^{2}$
82	81	eqeq1d	$⊢ Y = \frac{C}{B} \to (X^{2} + Y^{2} = R^{2} \leftrightarrow X^{2} + {(\frac{C}{B})}^{2} = R^{2})$
83	15	3adant3	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to R^{2} \in ℂ$
84	23	3adant3	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to C \in ℂ$
85	32	3adant3	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B \in ℂ$
86		simp1rr	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B \neq 0$
87	84 85 86	divcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{C}{B} \in ℂ$
88	87	sqcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to {(\frac{C}{B})}^{2} \in ℂ$
89		simp3l	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to X \in ℝ$
90	89	recnd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to X \in ℂ$
91	90	sqcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to X^{2} \in ℂ$
92	83 88 91	subadd2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (R^{2} - {(\frac{C}{B})}^{2} = X^{2} \leftrightarrow X^{2} + {(\frac{C}{B})}^{2} = R^{2})$
93	23 32 52	sqdivd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to {(\frac{C}{B})}^{2} = \frac{C^{2}}{B^{2}}$
94	93	oveq2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to R^{2} - {(\frac{C}{B})}^{2} = R^{2} - (\frac{C^{2}}{B^{2}})$
95	31	resqcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} \in ℝ$
96	31 52	sqgt0d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to 0 < B^{2}$
97	95 96	elrpd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to B^{2} \in ℝ^{+}$
98	97	rpcnne0d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to (B^{2} \in ℂ \land B^{2} \neq 0)$
99		subdivcomb1	$⊢ (R^{2} \in ℂ \land C^{2} \in ℂ \land (B^{2} \in ℂ \land B^{2} \neq 0)) \to \frac{B^{2} R^{2} - C^{2}}{B^{2}} = R^{2} - (\frac{C^{2}}{B^{2}})$
100	15 24 98 99	syl3anc	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to \frac{B^{2} R^{2} - C^{2}}{B^{2}} = R^{2} - (\frac{C^{2}}{B^{2}})$
101	94 100	eqtr4d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to R^{2} - {(\frac{C}{B})}^{2} = \frac{B^{2} R^{2} - C^{2}}{B^{2}}$
102	101	eqeq1d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D)) \to (R^{2} - {(\frac{C}{B})}^{2} = X^{2} \leftrightarrow \frac{B^{2} R^{2} - C^{2}}{B^{2}} = X^{2})$
103	102	3adant3	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (R^{2} - {(\frac{C}{B})}^{2} = X^{2} \leftrightarrow \frac{B^{2} R^{2} - C^{2}}{B^{2}} = X^{2})$
104	41	3adant3	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B^{2} \in ℂ$
105	104 83	mulcomd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B^{2} R^{2} = R^{2} B^{2}$
106	44	3adant3	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to Q = B^{2}$
107	106	eqcomd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B^{2} = Q$
108	107	oveq2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to R^{2} B^{2} = R^{2} Q$
109	105 108	eqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B^{2} R^{2} = R^{2} Q$
110	109	oveq1d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to B^{2} R^{2} - C^{2} = R^{2} Q - C^{2}$
111	110	oveq1d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{B^{2} R^{2} - C^{2}}{B^{2}} = \frac{R^{2} Q - C^{2}}{B^{2}}$
112	111	eqeq1d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (\frac{B^{2} R^{2} - C^{2}}{B^{2}} = X^{2} \leftrightarrow \frac{R^{2} Q - C^{2}}{B^{2}} = X^{2})$
113	2	oveq1i	$⊢ \frac{D}{B^{2}} = \frac{R^{2} Q - C^{2}}{B^{2}}$
114	113	eqeq1i	$⊢ \frac{D}{B^{2}} = X^{2} \leftrightarrow \frac{R^{2} Q - C^{2}}{B^{2}} = X^{2}$
115		eqcom	$⊢ \frac{D}{B^{2}} = X^{2} \leftrightarrow X^{2} = \frac{D}{B^{2}}$
116	26	3adant3	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to D \in ℂ$
117		sqrtth	$⊢ D \in ℂ \to {\sqrt{D}}^{2} = D$
118	117	eqcomd	$⊢ D \in ℂ \to D = {\sqrt{D}}^{2}$
119	116 118	syl	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to D = {\sqrt{D}}^{2}$
120	119	oveq1d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{D}{B^{2}} = \frac{{\sqrt{D}}^{2}}{B^{2}}$
121	27	3adant3	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \sqrt{D} \in ℂ$
122	121 85 86	sqdivd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to {(\frac{\sqrt{D}}{B})}^{2} = \frac{{\sqrt{D}}^{2}}{B^{2}}$
123	120 122	eqtr4d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{D}{B^{2}} = {(\frac{\sqrt{D}}{B})}^{2}$
124	123	eqeq2d	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (X^{2} = \frac{D}{B^{2}} \leftrightarrow X^{2} = {(\frac{\sqrt{D}}{B})}^{2})$
125	121 85 86	divcld	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to \frac{\sqrt{D}}{B} \in ℂ$
126	90 125	jca	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (X \in ℂ \land \frac{\sqrt{D}}{B} \in ℂ)$
127		sqeqor	$⊢ (X \in ℂ \land \frac{\sqrt{D}}{B} \in ℂ) \to (X^{2} = {(\frac{\sqrt{D}}{B})}^{2} \leftrightarrow (X = \frac{\sqrt{D}}{B} \lor X = - \frac{\sqrt{D}}{B}))$
128	126 127	syl	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (X^{2} = {(\frac{\sqrt{D}}{B})}^{2} \leftrightarrow (X = \frac{\sqrt{D}}{B} \lor X = - \frac{\sqrt{D}}{B}))$
129		orcom	$⊢ (X = \frac{\sqrt{D}}{B} \lor X = - \frac{\sqrt{D}}{B}) \leftrightarrow (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B})$
130	129	a1i	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to ((X = \frac{\sqrt{D}}{B} \lor X = - \frac{\sqrt{D}}{B}) \leftrightarrow (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B}))$
131	124 128 130	3bitrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (X^{2} = \frac{D}{B^{2}} \leftrightarrow (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B}))$
132	131	biimpd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (X^{2} = \frac{D}{B^{2}} \to (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B}))$
133	115 132	syl5bi	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (\frac{D}{B^{2}} = X^{2} \to (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B}))$
134	114 133	syl5bir	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (\frac{R^{2} Q - C^{2}}{B^{2}} = X^{2} \to (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B}))$
135	112 134	sylbid	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (\frac{B^{2} R^{2} - C^{2}}{B^{2}} = X^{2} \to (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B}))$
136	103 135	sylbid	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (R^{2} - {(\frac{C}{B})}^{2} = X^{2} \to (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B}))$
137	92 136	sylbird	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (X^{2} + {(\frac{C}{B})}^{2} = R^{2} \to (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B}))$
138	137	com12	$⊢ X^{2} + {(\frac{C}{B})}^{2} = R^{2} \to ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B}))$
139	82 138	syl6bi	$⊢ Y = \frac{C}{B} \to (X^{2} + Y^{2} = R^{2} \to ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B})))$
140	139	com13	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to (X^{2} + Y^{2} = R^{2} \to (Y = \frac{C}{B} \to (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B})))$
141	140	adantrd	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to (Y = \frac{C}{B} \to (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B})))$
142	141	imp	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land (X^{2} + Y^{2} = R^{2} \land A X + B Y = C)) \to (Y = \frac{C}{B} \to (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B}))$
143	142	ancld	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land (X^{2} + Y^{2} = R^{2} \land A X + B Y = C)) \to (Y = \frac{C}{B} \to (Y = \frac{C}{B} \land (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B})))$
144	79 143	syld	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land (X^{2} + Y^{2} = R^{2} \land A X + B Y = C)) \to ((Y = \frac{B C - A \sqrt{D}}{Q} \lor Y = \frac{B C + A \sqrt{D}}{Q}) \to (Y = \frac{C}{B} \land (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B})))$
145	7 144	mpd	$⊢ ((((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \land (X^{2} + Y^{2} = R^{2} \land A X + B Y = C)) \to (Y = \frac{C}{B} \land (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B}))$
146	145	ex	$⊢ (((A \in ℝ \land B \in ℝ \land C \in ℝ) \land (A = 0 \land B \neq 0)) \land (R \in ℝ^{+} \land 0 \leq D) \land (X \in ℝ \land Y \in ℝ)) \to ((X^{2} + Y^{2} = R^{2} \land A X + B Y = C) \to (Y = \frac{C}{B} \land (X = - \frac{\sqrt{D}}{B} \lor X = \frac{\sqrt{D}}{B})))$

Metamath Proof Explorer

Theorem itschlc0xyqsol1

Proof