Metamath Proof Explorer


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 syl5bb ( ( ( 𝑋𝑃𝑌𝑃𝑋𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 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 , ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ⟩ } } )