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 ⊢ 𝐼 = ( 0 ..^ 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 ⊢ 𝐴 = ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) )
itsclinecirc0b.b ⊢ 𝐵 = ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) )
itsclinecirc0b.c ⊢ 𝐶 = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) )
Assertion itsclinecirc0in ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) = { ⟨“ ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ”⟩ , ⟨“ ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ”⟩ } )

Proof

Step Hyp Ref Expression
1 itsclinecirc0b.i ⊢ 𝐼 = ( 0 ..^ 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 ⊢ 𝐴 = ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) )
10 itsclinecirc0b.b ⊢ 𝐵 = ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) )
11 itsclinecirc0b.c ⊢ 𝐶 = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) )
12 elin ⊢ ( 𝑧 ∈ ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ↔ ( 𝑧 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) )
13 1 2 3 4 5 6 7 8 9 10 11 itsclinecirc0b ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑧 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ↔ ( 𝑧 ∈ 𝑃 ∧ ( ( ( 𝑧 ‘ 0 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑧 ‘ 1 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑧 ‘ 0 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑧 ‘ 1 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )
14 12 13 bitrid ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑧 ∈ ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ↔ ( 𝑧 ∈ 𝑃 ∧ ( ( ( 𝑧 ‘ 0 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑧 ‘ 1 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑧 ‘ 0 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑧 ‘ 1 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ) )
15 1 3 rrx2pyel ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℝ )
16 15 adantr ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
17 1 3 rrx2pyel ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℝ )
18 17 adantl ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
19 16 18 resubcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ∈ ℝ )
20 9 19 eqeltrid ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝐴 ∈ ℝ )
21 20 3adant3 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝐴 ∈ ℝ )
22 21 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐴 ∈ ℝ )
23 1 3 rrx2pxel ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 0 ) ∈ ℝ )
24 23 adantl ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑌 ‘ 0 ) ∈ ℝ )
25 1 3 rrx2pxel ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 0 ) ∈ ℝ )
26 25 adantr ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ‘ 0 ) ∈ ℝ )
27 24 26 resubcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ∈ ℝ )
28 10 27 eqeltrid ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝐵 ∈ ℝ )
29 28 3adant3 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝐵 ∈ ℝ )
30 29 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → 𝐵 ∈ ℝ )
31 16 24 remulcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) ∈ ℝ )
32 26 18 remulcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ∈ ℝ )
33 31 32 resubcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ∈ ℝ )
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 6 resum2sqcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑄 ∈ ℝ )
46 20 28 45 syl2anc ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝑄 ∈ ℝ )
47 46 3adant3 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝑄 ∈ ℝ )
48 1 3 10 9 rrx2pnedifcoorneorr ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝐵 ≠ 0 ∨ 𝐴 ≠ 0 ) )
49 48 orcomd ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )
50 6 resum2sqorgt0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) → 0 < 𝑄 )
51 21 29 49 50 syl3anc ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 0 < 𝑄 )
52 51 gt0ne0d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → 𝑄 ≠ 0 )
53 47 52 jca ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑄 ∈ ℝ ∧ 𝑄 ≠ 0 ) )
54 53 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑄 ∈ ℝ ∧ 𝑄 ≠ 0 ) )
55 itsclc0lem1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑄 ∈ ℝ ∧ 𝑄 ≠ 0 ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ )
56 37 44 54 55 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ )
57 30 22 36 3jca ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) )
58 itsclc0lem2 ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑄 ∈ ℝ ∧ 𝑄 ≠ 0 ) ) → ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ )
59 57 44 54 58 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ )
60 itsclc0lem2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑄 ∈ ℝ ∧ 𝑄 ≠ 0 ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ )
61 37 44 54 60 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ )
62 itsclc0lem1 ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) ∧ ( 𝑄 ∈ ℝ ∧ 𝑄 ≠ 0 ) ) → ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ )
63 57 44 54 62 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ )
64 1 3 prelrrx2b ⊢ ( ( ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ ∧ ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ ) ∧ ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ ∧ ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∈ ℝ ) ) → ( ( 𝑧 ∈ 𝑃 ∧ ( ( ( 𝑧 ‘ 0 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑧 ‘ 1 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑧 ‘ 0 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑧 ‘ 1 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ↔ 𝑧 ∈ { ⟨“ ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ”⟩ , ⟨“ ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ”⟩ } ) )
65 56 59 61 63 64 syl22anc ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 𝑧 ∈ 𝑃 ∧ ( ( ( 𝑧 ‘ 0 ) = ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑧 ‘ 1 ) = ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ∨ ( ( 𝑧 ‘ 0 ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ∧ ( 𝑧 ‘ 1 ) = ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ) ) ) ↔ 𝑧 ∈ { ⟨“ ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ”⟩ , ⟨“ ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ”⟩ } ) )
66 14 65 bitrd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( 𝑧 ∈ ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ↔ 𝑧 ∈ { ⟨“ ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ”⟩ , ⟨“ ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ”⟩ } ) )
67 66 eqrdv ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 ≤ 𝐷 ) ) → ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) = { ⟨“ ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ( ( ( 𝐵 · 𝐶 ) − ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ”⟩ , ⟨“ ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ( ( ( 𝐵 · 𝐶 ) + ( 𝐴 · ( √ ‘ 𝐷 ) ) ) / 𝑄 ) ”⟩ } )