Theorem itsclquadeu

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

	Ref	Expression
Hypotheses	itsclquadb.q	⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
	itsclquadb.t	⊢ 𝑇 = - ( 2 · ( 𝐵 · 𝐶 ) )
	itsclquadb.u	⊢ 𝑈 = ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) )
Assertion	itsclquadeu	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ↔ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		itsclquadb.q	⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
2		itsclquadb.t	⊢ 𝑇 = - ( 2 · ( 𝐵 · 𝐶 ) )
3		itsclquadb.u	⊢ 𝑈 = ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) )
4		oveq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ↑ 2 ) = ( 𝑧 ↑ 2 ) )
5	4	oveq1d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( ( 𝑧 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) )
6	5	eqeq1d	⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( ( 𝑧 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
7		oveq2	⊢ ( 𝑥 = 𝑧 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 𝑧 ) )
8	7	oveq1d	⊢ ( 𝑥 = 𝑧 → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) )
9	8	eqeq1d	⊢ ( 𝑥 = 𝑧 → ( ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ↔ ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) )
10	6 9	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ↔ ( ( ( 𝑧 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) )
11	10	reu8	⊢ ( ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ↔ ∃ 𝑥 ∈ ℝ ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ∧ ∀ 𝑧 ∈ ℝ ( ( ( ( 𝑧 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → 𝑥 = 𝑧 ) ) )
12	11	a1i	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ↔ ∃ 𝑥 ∈ ℝ ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ∧ ∀ 𝑧 ∈ ℝ ( ( ( ( 𝑧 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → 𝑥 = 𝑧 ) ) ) )
13		id	⊢ ( 𝐶 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) → 𝐶 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) )
14	13	eqcoms	⊢ ( ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 → 𝐶 = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) )
15	14	eqeq2d	⊢ ( ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 → ( ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ↔ ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) ) )
16	15	adantl	⊢ ( ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ↔ ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) ) )
17		simp11l	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → 𝐴 ∈ ℝ )
18	17	ad2antrr	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → 𝐴 ∈ ℝ )
19		simpr	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → 𝑧 ∈ ℝ )
20	18 19	remulcld	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( 𝐴 · 𝑧 ) ∈ ℝ )
21	20	recnd	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( 𝐴 · 𝑧 ) ∈ ℂ )
22	17	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ )
23		simpr	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
24	22 23	remulcld	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐴 · 𝑥 ) ∈ ℝ )
25	24	adantr	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( 𝐴 · 𝑥 ) ∈ ℝ )
26	25	recnd	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( 𝐴 · 𝑥 ) ∈ ℂ )
27		simp12	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → 𝐵 ∈ ℝ )
28		simp3	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → 𝑌 ∈ ℝ )
29	27 28	remulcld	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐵 · 𝑌 ) ∈ ℝ )
30	29	ad2antrr	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( 𝐵 · 𝑌 ) ∈ ℝ )
31	30	recnd	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( 𝐵 · 𝑌 ) ∈ ℂ )
32	21 26 31	addcan2d	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) ↔ ( 𝐴 · 𝑧 ) = ( 𝐴 · 𝑥 ) ) )
33	19	recnd	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → 𝑧 ∈ ℂ )
34		simplr	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → 𝑥 ∈ ℝ )
35	34	recnd	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → 𝑥 ∈ ℂ )
36	18	recnd	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → 𝐴 ∈ ℂ )
37		simp11r	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → 𝐴 ≠ 0 )
38	37	ad2antrr	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → 𝐴 ≠ 0 )
39	33 35 36 38	mulcand	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝐴 · 𝑧 ) = ( 𝐴 · 𝑥 ) ↔ 𝑧 = 𝑥 ) )
40		equcom	⊢ ( 𝑧 = 𝑥 ↔ 𝑥 = 𝑧 )
41	40	a1i	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( 𝑧 = 𝑥 ↔ 𝑥 = 𝑧 ) )
42	32 39 41	3bitrd	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) ↔ 𝑥 = 𝑧 ) )
43	42	biimpd	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) → 𝑥 = 𝑧 ) )
44	43	adantr	⊢ ( ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) → 𝑥 = 𝑧 ) )
45	16 44	sylbid	⊢ ( ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 → 𝑥 = 𝑧 ) )
46	45	an32s	⊢ ( ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ∧ 𝑧 ∈ ℝ ) → ( ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 → 𝑥 = 𝑧 ) )
47	46	adantld	⊢ ( ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ∧ 𝑧 ∈ ℝ ) → ( ( ( ( 𝑧 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → 𝑥 = 𝑧 ) )
48	47	ralrimiva	⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ∀ 𝑧 ∈ ℝ ( ( ( ( 𝑧 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → 𝑥 = 𝑧 ) )
49	48	ex	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 → ∀ 𝑧 ∈ ℝ ( ( ( ( 𝑧 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → 𝑥 = 𝑧 ) ) )
50	49	adantld	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ∀ 𝑧 ∈ ℝ ( ( ( ( 𝑧 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → 𝑥 = 𝑧 ) ) )
51	50	pm4.71d	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ↔ ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ∧ ∀ 𝑧 ∈ ℝ ( ( ( ( 𝑧 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → 𝑥 = 𝑧 ) ) ) )
52	51	bicomd	⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ∧ ∀ 𝑧 ∈ ℝ ( ( ( ( 𝑧 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → 𝑥 = 𝑧 ) ) ↔ ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) )
53	52	rexbidva	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ∃ 𝑥 ∈ ℝ ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ∧ ∀ 𝑧 ∈ ℝ ( ( ( ( 𝑧 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑧 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → 𝑥 = 𝑧 ) ) ↔ ∃ 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) )
54	1 2 3	itsclquadb	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ∃ 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ↔ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) )
55	12 53 54	3bitrd	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ↔ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) )