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	⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
	itsclc0yqsol.d	⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
Assertion	itschlc0xyqsol1	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 = 0 ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑅 ∈ ℝ⁺ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( 𝑌 = ( 𝐶 / 𝐵 ) ∧ ( 𝑋 = - ( ( √ ‘ 𝐷 ) / 𝐵 ) ∨ 𝑋 = ( ( √ ‘ 𝐷 ) / 𝐵 ) ) ) ) )

Proof

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

Metamath Proof Explorer

Theorem itschlc0xyqsol1

Proof