Theorem itsclc0b

Description: The intersection points of a (nondegenerate) line through two points and a circle around the origin. (Contributed by AV, 2-May-2023) (Revised by AV, 14-May-2023)

	Ref	Expression
Hypotheses	itsclc0.i	⊢ 𝐼 = { 1 , 2 }
	itsclc0.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
	itsclc0.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
	itsclc0.s	⊢ 𝑆 = ( Sphere ‘ 𝐸 )
	itsclc0.0	⊢ 0 = ( 𝐼 × { 0 } )
	itsclc0.q	⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
	itsclc0.d	⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
	itsclc0.l	⊢ 𝐿 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 }
Assertion	itsclc0b	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑋 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑋 ∈ 𝐿 ) ↔ ( 𝑋 ∈ 𝑃 ∧ ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		itsclc0.i	⊢ 𝐼 = { 1 , 2 }
2		itsclc0.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3		itsclc0.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4		itsclc0.s	⊢ 𝑆 = ( Sphere ‘ 𝐸 )
5		itsclc0.0	⊢ 0 = ( 𝐼 × { 0 } )
6		itsclc0.q	⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
7		itsclc0.d	⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
8		itsclc0.l	⊢ 𝐿 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 }
9		rprege0	⊢ ( 𝑅 ∈ ℝ+ → ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) )
10		elrege0	⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) ↔ ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) )
11	9 10	sylibr	⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ( 0 [,) +∞ ) )
12	11	adantr	⊢ ( ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) → 𝑅 ∈ ( 0 [,) +∞ ) )
13	12	3ad2ant3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝑅 ∈ ( 0 [,) +∞ ) )
14		eqid	⊢ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) }
15	1 2 3 4 5 14	2sphere0	⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
16	15	eleq2d	⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → ( 𝑋 ∈ ( 0 𝑆 𝑅 ) ↔ 𝑋 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } ) )
17	13 16	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑋 ∈ ( 0 𝑆 𝑅 ) ↔ 𝑋 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } ) )
18		fveq1	⊢ ( 𝑝 = 𝑋 → ( 𝑝 ‘ 1 ) = ( 𝑋 ‘ 1 ) )
19	18	oveq2d	⊢ ( 𝑝 = 𝑋 → ( 𝐴 · ( 𝑝 ‘ 1 ) ) = ( 𝐴 · ( 𝑋 ‘ 1 ) ) )
20		fveq1	⊢ ( 𝑝 = 𝑋 → ( 𝑝 ‘ 2 ) = ( 𝑋 ‘ 2 ) )
21	20	oveq2d	⊢ ( 𝑝 = 𝑋 → ( 𝐵 · ( 𝑝 ‘ 2 ) ) = ( 𝐵 · ( 𝑋 ‘ 2 ) ) )
22	19 21	oveq12d	⊢ ( 𝑝 = 𝑋 → ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) )
23	22	eqeq1d	⊢ ( 𝑝 = 𝑋 → ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) )
24	23 8	elrab2	⊢ ( 𝑋 ∈ 𝐿 ↔ ( 𝑋 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) )
25	24	a1i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑋 ∈ 𝐿 ↔ ( 𝑋 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) ) )
26	17 25	anbi12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑋 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑋 ∈ 𝐿 ) ↔ ( 𝑋 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } ∧ ( 𝑋 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) ) ) )
27	18	oveq1d	⊢ ( 𝑝 = 𝑋 → ( ( 𝑝 ‘ 1 ) ↑ 2 ) = ( ( 𝑋 ‘ 1 ) ↑ 2 ) )
28	20	oveq1d	⊢ ( 𝑝 = 𝑋 → ( ( 𝑝 ‘ 2 ) ↑ 2 ) = ( ( 𝑋 ‘ 2 ) ↑ 2 ) )
29	27 28	oveq12d	⊢ ( 𝑝 = 𝑋 → ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) )
30	29	eqeq1d	⊢ ( 𝑝 = 𝑋 → ( ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
31	30	elrab	⊢ ( 𝑋 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } ↔ ( 𝑋 ∈ 𝑃 ∧ ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
32	31	anbi1i	⊢ ( ( 𝑋 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } ∧ ( 𝑋 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) ) ↔ ( ( 𝑋 ∈ 𝑃 ∧ ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( 𝑋 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) ) )
33		anandi	⊢ ( ( 𝑋 ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) ) ↔ ( ( 𝑋 ∈ 𝑃 ∧ ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( 𝑋 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) ) )
34		simpl1	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑋 ∈ 𝑃 ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) )
35		simpl2	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑋 ∈ 𝑃 ) → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )
36		simpl3l	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑋 ∈ 𝑃 ) → 𝑅 ∈ ℝ+ )
37		simpl3r	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑋 ∈ 𝑃 ) → 0 ≤ 𝐷 )
38	1 3	rrx2pxel	⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℝ )
39	1 3	rrx2pyel	⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 2 ) ∈ ℝ )
40	38 39	jca	⊢ ( 𝑋 ∈ 𝑃 → ( ( 𝑋 ‘ 1 ) ∈ ℝ ∧ ( 𝑋 ‘ 2 ) ∈ ℝ ) )
41	40	adantl	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑋 ∈ 𝑃 ) → ( ( 𝑋 ‘ 1 ) ∈ ℝ ∧ ( 𝑋 ‘ 2 ) ∈ ℝ ) )
42	36 37 41	jca31	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑋 ∈ 𝑃 ) → ( ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( ( 𝑋 ‘ 1 ) ∈ ℝ ∧ ( 𝑋 ‘ 2 ) ∈ ℝ ) ) )
43	6 7	itsclc0xyqsolb	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ∧ ( ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ∧ ( ( 𝑋 ‘ 1 ) ∈ ℝ ∧ ( 𝑋 ‘ 2 ) ∈ ℝ ) ) ) → ( ( ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) ↔ ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )
44	34 35 42 43	syl21anc	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) ∧ 𝑋 ∈ 𝑃 ) → ( ( ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) ↔ ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) )
45	44	pm5.32da	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑋 ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) ) ↔ ( 𝑋 ∈ 𝑃 ∧ ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )
46	33 45	bitr3id	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝑋 ∈ 𝑃 ∧ ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( 𝑋 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) ) ↔ ( 𝑋 ∈ 𝑃 ∧ ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )
47	32 46	syl5bb	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑋 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } ∧ ( 𝑋 ∈ 𝑃 ∧ ( ( 𝐴 · ( 𝑋 ‘ 1 ) ) + ( 𝐵 · ( 𝑋 ‘ 2 ) ) ) = 𝐶 ) ) ↔ ( 𝑋 ∈ 𝑃 ∧ ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )
48	26 47	bitrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑋 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑋 ∈ 𝐿 ) ↔ ( 𝑋 ∈ 𝑃 ∧ ( ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑋 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑋 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )