itsclquadb

Description: Quadratic equation for the y-coordinate of the intersection points of a line and a circle. (Contributed by AV, 22-Feb-2023)

	Ref	Expression
Hypotheses	itsclquadb.q	$⊢ Q = A^{2} + B^{2}$
	itsclquadb.t	$⊢ T = - 2 B C$
	itsclquadb.u	$⊢ U = C^{2} - A^{2} R^{2}$
Assertion	itsclquadb	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (\exists x \in ℝ (x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \leftrightarrow Q Y^{2} + T Y + U = 0)$

Proof

Step	Hyp	Ref	Expression
1		itsclquadb.q	$⊢ Q = A^{2} + B^{2}$
2		itsclquadb.t	$⊢ T = - 2 B C$
3		itsclquadb.u	$⊢ U = C^{2} - A^{2} R^{2}$
4		simpl1	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \to ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ)$
5		simp2	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to R \in ℝ^{+}$
6	5	adantr	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \to R \in ℝ^{+}$
7		simp3	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to Y \in ℝ$
8	7	anim1ci	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \to (x \in ℝ \land Y \in ℝ)$
9	1 2 3	itscnhlc0yqe	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land (x \in ℝ \land Y \in ℝ)) \to ((x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \to Q Y^{2} + T Y + U = 0)$
10	4 6 8 9	syl3anc	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land x \in ℝ) \to ((x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \to Q Y^{2} + T Y + U = 0)$
11	10	rexlimdva	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (\exists x \in ℝ (x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \to Q Y^{2} + T Y + U = 0)$
12		simp3	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to C \in ℝ$
13	12	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C \in ℝ$
14		simp2	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to B \in ℝ$
15	14	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to B \in ℝ$
16	15 7	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to B Y \in ℝ$
17	13 16	resubcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C - B Y \in ℝ$
18		simp11l	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A \in ℝ$
19		simp11r	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A \neq 0$
20	17 18 19	redivcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to \frac{C - B Y}{A} \in ℝ$
21	20	adantr	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land Q Y^{2} + T Y + U = 0) \to \frac{C - B Y}{A} \in ℝ$
22		oveq1	$⊢ x = \frac{C - B Y}{A} \to x^{2} = {(\frac{C - B Y}{A})}^{2}$
23	22	oveq1d	$⊢ x = \frac{C - B Y}{A} \to x^{2} + Y^{2} = {(\frac{C - B Y}{A})}^{2} + Y^{2}$
24	23	eqeq1d	$⊢ x = \frac{C - B Y}{A} \to (x^{2} + Y^{2} = R^{2} \leftrightarrow {(\frac{C - B Y}{A})}^{2} + Y^{2} = R^{2})$
25		oveq2	$⊢ x = \frac{C - B Y}{A} \to A x = A (\frac{C - B Y}{A})$
26	25	oveq1d	$⊢ x = \frac{C - B Y}{A} \to A x + B Y = A (\frac{C - B Y}{A}) + B Y$
27	26	eqeq1d	$⊢ x = \frac{C - B Y}{A} \to (A x + B Y = C \leftrightarrow A (\frac{C - B Y}{A}) + B Y = C)$
28	24 27	anbi12d	$⊢ x = \frac{C - B Y}{A} \to ((x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \leftrightarrow ({(\frac{C - B Y}{A})}^{2} + Y^{2} = R^{2} \land A (\frac{C - B Y}{A}) + B Y = C))$
29	28	adantl	$⊢ (((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land Q Y^{2} + T Y + U = 0) \land x = \frac{C - B Y}{A}) \to ((x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \leftrightarrow ({(\frac{C - B Y}{A})}^{2} + Y^{2} = R^{2} \land A (\frac{C - B Y}{A}) + B Y = C))$
30	17	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C - B Y \in ℂ$
31	18	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A \in ℂ$
32	30 31 19	sqdivd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to {(\frac{C - B Y}{A})}^{2} = \frac{{(C - B Y)}^{2}}{A^{2}}$
33	13	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C \in ℂ$
34	16	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to B Y \in ℂ$
35		binom2sub	$⊢ (C \in ℂ \land B Y \in ℂ) \to {(C - B Y)}^{2} = C^{2} - 2 C B Y + {B Y}^{2}$
36	33 34 35	syl2anc	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to {(C - B Y)}^{2} = C^{2} - 2 C B Y + {B Y}^{2}$
37	13	resqcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} \in ℝ$
38	37	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} \in ℂ$
39		2re	$⊢ 2 \in ℝ$
40	39	a1i	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to 2 \in ℝ$
41	13 16	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C B Y \in ℝ$
42	40 41	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to 2 C B Y \in ℝ$
43	42	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to 2 C B Y \in ℂ$
44	38 43	negsubd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} + (- 2 C B Y) = C^{2} - 2 C B Y$
45	15	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to B \in ℂ$
46	7	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to Y \in ℂ$
47	33 45 46	mulassd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C B Y = C B Y$
48	47	eqcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C B Y = C B Y$
49	48	oveq2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to 2 C B Y = 2 C B Y$
50		2cnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to 2 \in ℂ$
51	13 15	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C B \in ℝ$
52	51	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C B \in ℂ$
53	50 52 46	mulassd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to 2 C B Y = 2 C B Y$
54	53	eqcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to 2 C B Y = 2 C B Y$
55	33 45	mulcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C B = B C$
56	55	oveq2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to 2 C B = 2 B C$
57	56	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to 2 C B Y = 2 B C Y$
58	49 54 57	3eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to 2 C B Y = 2 B C Y$
59	58	negeqd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to - 2 C B Y = - 2 B C Y$
60	59	oveq2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} + (- 2 C B Y) = C^{2} + (- 2 B C Y)$
61	44 60	eqtr3d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} - 2 C B Y = C^{2} + (- 2 B C Y)$
62	45 46	sqmuld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to {B Y}^{2} = B^{2} Y^{2}$
63	61 62	oveq12d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} - 2 C B Y + {B Y}^{2} = C^{2} + (- 2 B C Y) + B^{2} Y^{2}$
64	15 13	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to B C \in ℝ$
65	40 64	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to 2 B C \in ℝ$
66	65	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to 2 B C \in ℂ$
67	66 46	mulneg1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (- 2 B C) Y = - 2 B C Y$
68	2	eqcomi	$⊢ - 2 B C = T$
69	68	oveq1i	$⊢ (- 2 B C) Y = T Y$
70	69	a1i	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (- 2 B C) Y = T Y$
71	67 70	eqtr3d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to - 2 B C Y = T Y$
72	71	oveq2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} + (- 2 B C Y) = C^{2} + T Y$
73	72	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} + (- 2 B C Y) + B^{2} Y^{2} = C^{2} + T Y + B^{2} Y^{2}$
74	36 63 73	3eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to {(C - B Y)}^{2} = C^{2} + T Y + B^{2} Y^{2}$
75	74	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to \frac{{(C - B Y)}^{2}}{A^{2}} = \frac{C^{2} + T Y + B^{2} Y^{2}}{A^{2}}$
76	32 75	eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to {(\frac{C - B Y}{A})}^{2} = \frac{C^{2} + T Y + B^{2} Y^{2}}{A^{2}}$
77		resqcl	$⊢ Y \in ℝ \to Y^{2} \in ℝ$
78	77	recnd	$⊢ Y \in ℝ \to Y^{2} \in ℂ$
79	78	3ad2ant3	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to Y^{2} \in ℂ$
80	18	resqcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A^{2} \in ℝ$
81	80	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A^{2} \in ℂ$
82		recn	$⊢ A \in ℝ \to A \in ℂ$
83		sqne0	$⊢ A \in ℂ \to (A^{2} \neq 0 \leftrightarrow A \neq 0)$
84	82 83	syl	$⊢ A \in ℝ \to (A^{2} \neq 0 \leftrightarrow A \neq 0)$
85	84	biimpar	$⊢ (A \in ℝ \land A \neq 0) \to A^{2} \neq 0$
86	85	3ad2ant1	$⊢ ((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \to A^{2} \neq 0$
87	86	3ad2ant1	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A^{2} \neq 0$
88	79 81 87	divcan2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A^{2} (\frac{Y^{2}}{A^{2}}) = Y^{2}$
89	88	eqcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to Y^{2} = A^{2} (\frac{Y^{2}}{A^{2}})$
90	76 89	oveq12d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to {(\frac{C - B Y}{A})}^{2} + Y^{2} = (\frac{C^{2} + T Y + B^{2} Y^{2}}{A^{2}}) + A^{2} (\frac{Y^{2}}{A^{2}})$
91	81 79 81 87	divassd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to \frac{A^{2} Y^{2}}{A^{2}} = A^{2} (\frac{Y^{2}}{A^{2}})$
92	91	eqcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A^{2} (\frac{Y^{2}}{A^{2}}) = \frac{A^{2} Y^{2}}{A^{2}}$
93	92	oveq2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (\frac{C^{2} + T Y + B^{2} Y^{2}}{A^{2}}) + A^{2} (\frac{Y^{2}}{A^{2}}) = (\frac{C^{2} + T Y + B^{2} Y^{2}}{A^{2}}) + (\frac{A^{2} Y^{2}}{A^{2}})$
94	65	renegcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to - 2 B C \in ℝ$
95	2 94	eqeltrid	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to T \in ℝ$
96	95 7	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to T Y \in ℝ$
97	37 96	readdcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} + T Y \in ℝ$
98	15	resqcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to B^{2} \in ℝ$
99	7	resqcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to Y^{2} \in ℝ$
100	98 99	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to B^{2} Y^{2} \in ℝ$
101	97 100	readdcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} + T Y + B^{2} Y^{2} \in ℝ$
102	101	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} + T Y + B^{2} Y^{2} \in ℂ$
103	80 99	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A^{2} Y^{2} \in ℝ$
104	103	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A^{2} Y^{2} \in ℂ$
105	102 104 81 87	divdird	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to \frac{(C^{2} + T Y) + B^{2} Y^{2} + A^{2} Y^{2}}{A^{2}} = (\frac{C^{2} + T Y + B^{2} Y^{2}}{A^{2}}) + (\frac{A^{2} Y^{2}}{A^{2}})$
106	105	eqcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (\frac{C^{2} + T Y + B^{2} Y^{2}}{A^{2}}) + (\frac{A^{2} Y^{2}}{A^{2}}) = \frac{(C^{2} + T Y) + B^{2} Y^{2} + A^{2} Y^{2}}{A^{2}}$
107	90 93 106	3eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to {(\frac{C - B Y}{A})}^{2} + Y^{2} = \frac{(C^{2} + T Y) + B^{2} Y^{2} + A^{2} Y^{2}}{A^{2}}$
108	107	adantr	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land Q Y^{2} + T Y + U = 0) \to {(\frac{C - B Y}{A})}^{2} + Y^{2} = \frac{(C^{2} + T Y) + B^{2} Y^{2} + A^{2} Y^{2}}{A^{2}}$
109	97	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} + T Y \in ℂ$
110	100	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to B^{2} Y^{2} \in ℂ$
111	109 110 104	addassd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (C^{2} + T Y) + B^{2} Y^{2} + A^{2} Y^{2} = C^{2} + T Y + B^{2} Y^{2} + A^{2} Y^{2}$
112	98	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to B^{2} \in ℂ$
113	99	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to Y^{2} \in ℂ$
114	112 81 113	adddird	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (B^{2} + A^{2}) Y^{2} = B^{2} Y^{2} + A^{2} Y^{2}$
115	112 81	addcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to B^{2} + A^{2} = A^{2} + B^{2}$
116	115	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (B^{2} + A^{2}) Y^{2} = (A^{2} + B^{2}) Y^{2}$
117	114 116	eqtr3d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to B^{2} Y^{2} + A^{2} Y^{2} = (A^{2} + B^{2}) Y^{2}$
118	117	oveq2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} + T Y + B^{2} Y^{2} + A^{2} Y^{2} = C^{2} + T Y + (A^{2} + B^{2}) Y^{2}$
119	96	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to T Y \in ℂ$
120	80 98	readdcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A^{2} + B^{2} \in ℝ$
121	120 99	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (A^{2} + B^{2}) Y^{2} \in ℝ$
122	121	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (A^{2} + B^{2}) Y^{2} \in ℂ$
123	38 119 122	addassd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} + T Y + (A^{2} + B^{2}) Y^{2} = C^{2} + T Y + (A^{2} + B^{2}) Y^{2}$
124	119 122	addcomd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to T Y + (A^{2} + B^{2}) Y^{2} = (A^{2} + B^{2}) Y^{2} + T Y$
125	124	oveq2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} + T Y + (A^{2} + B^{2}) Y^{2} = C^{2} + (A^{2} + B^{2}) Y^{2} + T Y$
126	123 125	eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} + T Y + (A^{2} + B^{2}) Y^{2} = C^{2} + (A^{2} + B^{2}) Y^{2} + T Y$
127	111 118 126	3eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (C^{2} + T Y) + B^{2} Y^{2} + A^{2} Y^{2} = C^{2} + (A^{2} + B^{2}) Y^{2} + T Y$
128	127	adantr	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land Q Y^{2} + T Y + U = 0) \to (C^{2} + T Y) + B^{2} Y^{2} + A^{2} Y^{2} = C^{2} + (A^{2} + B^{2}) Y^{2} + T Y$
129	128	oveq1d	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land Q Y^{2} + T Y + U = 0) \to \frac{(C^{2} + T Y) + B^{2} Y^{2} + A^{2} Y^{2}}{A^{2}} = \frac{C^{2} + (A^{2} + B^{2}) Y^{2} + T Y}{A^{2}}$
130	1	oveq1i	$⊢ Q Y^{2} = (A^{2} + B^{2}) Y^{2}$
131	3	oveq2i	$⊢ T Y + U = T Y + C^{2} - A^{2} R^{2}$
132	130 131	oveq12i	$⊢ Q Y^{2} + T Y + U = (A^{2} + B^{2}) Y^{2} + T Y + (C^{2} - A^{2} R^{2})$
133		rpre	$⊢ R \in ℝ^{+} \to R \in ℝ$
134	133	resqcld	$⊢ R \in ℝ^{+} \to R^{2} \in ℝ$
135	134	3ad2ant2	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to R^{2} \in ℝ$
136	80 135	remulcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A^{2} R^{2} \in ℝ$
137	37 136	resubcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} - A^{2} R^{2} \in ℝ$
138	137	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} - A^{2} R^{2} \in ℂ$
139	122 119 138	addassd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (A^{2} + B^{2}) Y^{2} + T Y + (C^{2} - A^{2} R^{2}) = (A^{2} + B^{2}) Y^{2} + T Y + (C^{2} - A^{2} R^{2})$
140	132 139	eqtr4id	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to Q Y^{2} + T Y + U = (A^{2} + B^{2}) Y^{2} + T Y + (C^{2} - A^{2} R^{2})$
141	140	eqeq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (Q Y^{2} + T Y + U = 0 \leftrightarrow (A^{2} + B^{2}) Y^{2} + T Y + (C^{2} - A^{2} R^{2}) = 0)$
142	121 96	readdcld	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (A^{2} + B^{2}) Y^{2} + T Y \in ℝ$
143	142	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (A^{2} + B^{2}) Y^{2} + T Y \in ℂ$
144		addeq0	$⊢ ((A^{2} + B^{2}) Y^{2} + T Y \in ℂ \land C^{2} - A^{2} R^{2} \in ℂ) \to ((A^{2} + B^{2}) Y^{2} + T Y + (C^{2} - A^{2} R^{2}) = 0 \leftrightarrow (A^{2} + B^{2}) Y^{2} + T Y = - (C^{2} - A^{2} R^{2}))$
145	143 138 144	syl2anc	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to ((A^{2} + B^{2}) Y^{2} + T Y + (C^{2} - A^{2} R^{2}) = 0 \leftrightarrow (A^{2} + B^{2}) Y^{2} + T Y = - (C^{2} - A^{2} R^{2}))$
146	141 145	bitrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (Q Y^{2} + T Y + U = 0 \leftrightarrow (A^{2} + B^{2}) Y^{2} + T Y = - (C^{2} - A^{2} R^{2}))$
147		oveq2	$⊢ (A^{2} + B^{2}) Y^{2} + T Y = - (C^{2} - A^{2} R^{2}) \to C^{2} + (A^{2} + B^{2}) Y^{2} + T Y = C^{2} + (- (C^{2} - A^{2} R^{2}))$
148	147	oveq1d	$⊢ (A^{2} + B^{2}) Y^{2} + T Y = - (C^{2} - A^{2} R^{2}) \to \frac{C^{2} + (A^{2} + B^{2}) Y^{2} + T Y}{A^{2}} = \frac{C^{2} + (- (C^{2} - A^{2} R^{2}))}{A^{2}}$
149	38 138	negsubd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} + (- (C^{2} - A^{2} R^{2})) = C^{2} - (C^{2} - A^{2} R^{2})$
150	136	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A^{2} R^{2} \in ℂ$
151	38 150	nncand	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} - (C^{2} - A^{2} R^{2}) = A^{2} R^{2}$
152	149 151	eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C^{2} + (- (C^{2} - A^{2} R^{2})) = A^{2} R^{2}$
153	152	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to \frac{C^{2} + (- (C^{2} - A^{2} R^{2}))}{A^{2}} = \frac{A^{2} R^{2}}{A^{2}}$
154	135	recnd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to R^{2} \in ℂ$
155	154 81 87	divcan3d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to \frac{A^{2} R^{2}}{A^{2}} = R^{2}$
156	153 155	eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to \frac{C^{2} + (- (C^{2} - A^{2} R^{2}))}{A^{2}} = R^{2}$
157	148 156	sylan9eqr	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land (A^{2} + B^{2}) Y^{2} + T Y = - (C^{2} - A^{2} R^{2})) \to \frac{C^{2} + (A^{2} + B^{2}) Y^{2} + T Y}{A^{2}} = R^{2}$
158	157	ex	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to ((A^{2} + B^{2}) Y^{2} + T Y = - (C^{2} - A^{2} R^{2}) \to \frac{C^{2} + (A^{2} + B^{2}) Y^{2} + T Y}{A^{2}} = R^{2})$
159	146 158	sylbid	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (Q Y^{2} + T Y + U = 0 \to \frac{C^{2} + (A^{2} + B^{2}) Y^{2} + T Y}{A^{2}} = R^{2})$
160	159	imp	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land Q Y^{2} + T Y + U = 0) \to \frac{C^{2} + (A^{2} + B^{2}) Y^{2} + T Y}{A^{2}} = R^{2}$
161	108 129 160	3eqtrd	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land Q Y^{2} + T Y + U = 0) \to {(\frac{C - B Y}{A})}^{2} + Y^{2} = R^{2}$
162	30 31 19	divcan2d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A (\frac{C - B Y}{A}) = C - B Y$
163	162	oveq1d	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A (\frac{C - B Y}{A}) + B Y = C - B Y + B Y$
164	33 34	npcand	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to C - B Y + B Y = C$
165	163 164	eqtrd	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to A (\frac{C - B Y}{A}) + B Y = C$
166	165	adantr	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land Q Y^{2} + T Y + U = 0) \to A (\frac{C - B Y}{A}) + B Y = C$
167	161 166	jca	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land Q Y^{2} + T Y + U = 0) \to ({(\frac{C - B Y}{A})}^{2} + Y^{2} = R^{2} \land A (\frac{C - B Y}{A}) + B Y = C)$
168	21 29 167	rspcedvd	$⊢ ((((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \land Q Y^{2} + T Y + U = 0) \to \exists x \in ℝ (x^{2} + Y^{2} = R^{2} \land A x + B Y = C)$
169	168	ex	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (Q Y^{2} + T Y + U = 0 \to \exists x \in ℝ (x^{2} + Y^{2} = R^{2} \land A x + B Y = C))$
170	11 169	impbid	$⊢ (((A \in ℝ \land A \neq 0) \land B \in ℝ \land C \in ℝ) \land R \in ℝ^{+} \land Y \in ℝ) \to (\exists x \in ℝ (x^{2} + Y^{2} = R^{2} \land A x + B Y = C) \leftrightarrow Q Y^{2} + T Y + U = 0)$

Metamath Proof Explorer

Theorem itsclquadb

Proof