Theorem itsclinecirc0in

Description: The intersection points of a line through two different points and a circle around the origin, using the definition of a line in a two dimensional Euclidean space, expressed as intersection. (Contributed by AV, 7-May-2023) (Revised by AV, 14-May-2023)

	Ref	Expression
Hypotheses	itsclinecirc0b.i	⊢ 𝐼 = { 1 , 2 }
	itsclinecirc0b.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
	itsclinecirc0b.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
	itsclinecirc0b.s	⊢ 𝑆 = ( Sphere ‘ 𝐸 )
	itsclinecirc0b.0	⊢ 0 = ( 𝐼 × { 0 } )
	itsclinecirc0b.q	⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
	itsclinecirc0b.d	⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
	itsclinecirc0b.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
	itsclinecirc0b.a	⊢ 𝐴 = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) )
	itsclinecirc0b.b	⊢ 𝐵 = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
	itsclinecirc0b.c	⊢ 𝐶 = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) )
Assertion	itsclinecirc0in	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) = { { ⟨ 1 , ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ , ⟨ 2 , ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ } , { ⟨ 1 , ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ , ⟨ 2 , ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ } } )

Proof

Step	Hyp	Ref	Expression
1		itsclinecirc0b.i	⊢ 𝐼 = { 1 , 2 }
2		itsclinecirc0b.e	⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3		itsclinecirc0b.p	⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4		itsclinecirc0b.s	⊢ 𝑆 = ( Sphere ‘ 𝐸 )
5		itsclinecirc0b.0	⊢ 0 = ( 𝐼 × { 0 } )
6		itsclinecirc0b.q	⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
7		itsclinecirc0b.d	⊢ 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
8		itsclinecirc0b.l	⊢ 𝐿 = ( LineM ‘ 𝐸 )
9		itsclinecirc0b.a	⊢ 𝐴 = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) )
10		itsclinecirc0b.b	⊢ 𝐵 = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
11		itsclinecirc0b.c	⊢ 𝐶 = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) )
12		elin	⊢ ( 𝑧 ∈ ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ↔ ( 𝑧 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) )
13	1 2 3 4 5 6 7 8 9 10 11	itsclinecirc0b	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑧 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ↔ ( 𝑧 ∈ 𝑃 ∧ ( ( ( 𝑧 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑧 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑧 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑧 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )
14	12 13	bitrid	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑧 ∈ ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ↔ ( 𝑧 ∈ 𝑃 ∧ ( ( ( 𝑧 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑧 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑧 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑧 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )
15	1 3	rrx2pyel	⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 2 ) ∈ ℝ )
16	15	adantr	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
17	1 3	rrx2pyel	⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 2 ) ∈ ℝ )
18	17	adantl	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
19	16 18	resubcld	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ∈ ℝ )
20	9 19	eqeltrid	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝐴 ∈ ℝ )
21	20	3adant3	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝐴 ∈ ℝ )
22	21	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐴 ∈ ℝ )
23	1 3	rrx2pxel	⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℝ )
24	23	adantl	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
25	1 3	rrx2pxel	⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℝ )
26	25	adantr	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
27	24 26	resubcld	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ∈ ℝ )
28	10 27	eqeltrid	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝐵 ∈ ℝ )
29	28	3adant3	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝐵 ∈ ℝ )
30	29	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐵 ∈ ℝ )
31	16 24	remulcld	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) ∈ ℝ )
32	26 18	remulcld	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ∈ ℝ )
33	31 32	resubcld	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ∈ ℝ )
34	11 33	eqeltrid	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝐶 ∈ ℝ )
35	34	3adant3	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝐶 ∈ ℝ )
36	35	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐶 ∈ ℝ )
37	22 30 36	3jca	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) )
38	21 29 35	3jca	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) )
39		rpre	⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ )
40	39	adantr	⊢ ( ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) → 𝑅 ∈ ℝ )
41	6 7	itsclc0lem3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ) → 𝐷 ∈ ℝ )
42	38 40 41	syl2an	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐷 ∈ ℝ )
43		simprr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 0 ≤ 𝐷 )
44	42 43	jca	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) )
45	20 28	jca	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
46	6	resum2sqcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑄 ∈ ℝ )
47	45 46	syl	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝑄 ∈ ℝ )
48	47	3adant3	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝑄 ∈ ℝ )
49	1 3 10 9	rrx2pnedifcoorneorr	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝐵 ≠ 0 ∨ 𝐴 ≠ 0 ) )
50	49	orcomd	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )
51	6	resum2sqorgt0	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) → 0 < 𝑄 )
52	21 29 50 51	syl3anc	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 0 < 𝑄 )
53	52	gt0ne0d	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝑄 ≠ 0 )
54	48 53	jca	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑄 ∈ ℝ ∧ 𝑄 ≠ 0 ) )
55	54	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑄 ∈ ℝ ∧ 𝑄 ≠ 0 ) )
56		itsclc0lem1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑄 ∈ ℝ ∧ 𝑄 ≠ 0 ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ )
57	37 44 55 56	syl3anc	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ )
58	30 22 36	3jca	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) )
59	48	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝑄 ∈ ℝ )
60	53	adantr	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝑄 ≠ 0 )
61	59 60	jca	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑄 ∈ ℝ ∧ 𝑄 ≠ 0 ) )
62		itsclc0lem2	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑄 ∈ ℝ ∧ 𝑄 ≠ 0 ) ) → ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ )
63	58 44 61 62	syl3anc	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ )
64		itsclc0lem2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑄 ∈ ℝ ∧ 𝑄 ≠ 0 ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ )
65	37 44 61 64	syl3anc	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ )
66		itsclc0lem1	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑄 ∈ ℝ ∧ 𝑄 ≠ 0 ) ) → ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ )
67	58 44 61 66	syl3anc	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ )
68	1 3	prelrrx2b	⊢ ( ( ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ ∧ ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ ) ∧ ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ ∧ ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ ) ) → ( ( 𝑧 ∈ 𝑃 ∧ ( ( ( 𝑧 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑧 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑧 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑧 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ↔ 𝑧 ∈ { { ⟨ 1 , ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ , ⟨ 2 , ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ } , { ⟨ 1 , ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ , ⟨ 2 , ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ } } ) )
69	57 63 65 67 68	syl22anc	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑧 ∈ 𝑃 ∧ ( ( ( 𝑧 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑧 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑧 ‘ 1 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑧 ‘ 2 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ↔ 𝑧 ∈ { { ⟨ 1 , ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ , ⟨ 2 , ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ } , { ⟨ 1 , ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ , ⟨ 2 , ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ } } ) )
70	14 69	bitrd	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑧 ∈ ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ↔ 𝑧 ∈ { { ⟨ 1 , ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ , ⟨ 2 , ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ } , { ⟨ 1 , ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ , ⟨ 2 , ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ } } ) )
71	70	eqrdv	⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) = { { ⟨ 1 , ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ , ⟨ 2 , ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ } , { ⟨ 1 , ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ , ⟨ 2 , ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ } } )