Metamath Proof Explorer

Theorem itscnhlinecirc02p

Description: Intersection of a nonhorizontal line with a circle: A nonhorizontal line passing through a point within a circle around the origin intersects the circle at exactly two different points. (Contributed by AV, 28-Jan-2023)

Ref Expression
Hypotheses itscnhlinecirc02p.i ⊢ 𝐼 = { 1 , 2 }
itscnhlinecirc02p.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
itscnhlinecirc02p.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
itscnhlinecirc02p.s ⊢ 𝑆 = ( Sphere ‘ 𝐸 )
itscnhlinecirc02p.0 ⊢ 0 = ( 𝐼 × { 0 } )
itscnhlinecirc02p.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
itscnhlinecirc02p.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
itscnhlinecirc02p.z ⊢ 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ }
Assertion itscnhlinecirc02p ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ∃! 𝑠 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑠 ) = 2 ∧ ∀ 𝑦 ∈ 𝑠 ∃! 𝑥 ∈ ℝ ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 itscnhlinecirc02p.i ⊢ 𝐼 = { 1 , 2 }
2 itscnhlinecirc02p.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3 itscnhlinecirc02p.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4 itscnhlinecirc02p.s ⊢ 𝑆 = ( Sphere ‘ 𝐸 )
5 itscnhlinecirc02p.0 ⊢ 0 = ( 𝐼 × { 0 } )
6 itscnhlinecirc02p.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
7 itscnhlinecirc02p.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
8 itscnhlinecirc02p.z ⊢ 𝑍 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ }
9 1 2 3 4 5 6 7 itscnhlinecirc02plem3 ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → 0 < ( ( - ( 2 · ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↑ 2 ) − ( 4 · ( ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) · ( ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) )
10 1 3 rrx2pyel ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 2 ) ∈ ℝ )
11 10 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
12 11 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
13 1 3 rrx2pyel ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 2 ) ∈ ℝ )
14 13 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
15 14 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
16 12 15 resubcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ∈ ℝ )
17 16 resqcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) ∈ ℝ )
18 1 3 rrx2pxel ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℝ )
19 18 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
20 19 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
21 1 3 rrx2pxel ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℝ )
22 21 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
23 22 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
24 20 23 resubcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ∈ ℝ )
25 24 resqcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ∈ ℝ )
26 17 25 readdcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) ∈ ℝ )
27 11 14 resubcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ∈ ℝ )
28 27 resqcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) ∈ ℝ )
29 19 22 resubcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ∈ ℝ )
30 29 resqcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ∈ ℝ )
31 11 recnd ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → ( 𝑋 ‘ 2 ) ∈ ℂ )
32 14 recnd ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → ( 𝑌 ‘ 2 ) ∈ ℂ )
33 simp3 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) )
34 31 32 33 subne0d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ≠ 0 )
35 27 34 sqgt0d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → 0 < ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) )
36 29 sqge0d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → 0 ≤ ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) )
37 28 30 35 36 addgtge0d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → 0 < ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) )
38 37 gt0ne0d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) ≠ 0 )
39 38 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) ≠ 0 )
40 2re ⊢ 2 ∈ ℝ
41 40 a1i ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → 2 ∈ ℝ )
42 12 20 remulcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) ∈ ℝ )
43 23 15 remulcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ∈ ℝ )
44 42 43 resubcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ∈ ℝ )
45 24 44 remulcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ∈ ℝ )
46 41 45 remulcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 2 · ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ∈ ℝ )
47 46 renegcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → - ( 2 · ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ∈ ℝ )
48 44 resqcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) ∈ ℝ )
49 rpre ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ )
50 49 adantr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) → 𝑅 ∈ ℝ )
51 50 adantl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → 𝑅 ∈ ℝ )
52 51 resqcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
53 17 52 remulcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℝ )
54 48 53 resubcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ∈ ℝ )
55 eqidd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( - ( 2 · ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↑ 2 ) − ( 4 · ( ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) · ( ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) = ( ( - ( 2 · ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↑ 2 ) − ( 4 · ( ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) · ( ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) )
56 26 39 47 54 55 requad2 ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ∃! 𝑠 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑠 ) = 2 ∧ ∀ 𝑦 ∈ 𝑠 ( ( ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) · ( 𝑦 ↑ 2 ) ) + ( ( - ( 2 · ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) · 𝑦 ) + ( ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) ↔ 0 < ( ( - ( 2 · ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↑ 2 ) − ( 4 · ( ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) · ( ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) )
57 9 56 mpbird ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ∃! 𝑠 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑠 ) = 2 ∧ ∀ 𝑦 ∈ 𝑠 ( ( ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) · ( 𝑦 ↑ 2 ) ) + ( ( - ( 2 · ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) · 𝑦 ) + ( ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
58 0xr ⊢ 0 ∈ ℝ*
59 58 a1i ⊢ ( 𝑅 ∈ ℝ+ → 0 ∈ ℝ* )
60 pnfxr ⊢ +∞ ∈ ℝ*
61 60 a1i ⊢ ( 𝑅 ∈ ℝ+ → +∞ ∈ ℝ* )
62 rpxr ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ* )
63 rpge0 ⊢ ( 𝑅 ∈ ℝ+ → 0 ≤ 𝑅 )
64 ltpnf ⊢ ( 𝑅 ∈ ℝ → 𝑅 < +∞ )
65 49 64 syl ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 < +∞ )
66 59 61 62 63 65 elicod ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ( 0 [,) +∞ ) )
67 eqid ⊢ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) }
68 1 2 3 4 5 67 2sphere0 ⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
69 66 68 syl ⊢ ( 𝑅 ∈ ℝ+ → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
70 69 adantr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
71 70 adantl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
72 71 adantr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
73 72 adantr ⊢ ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
74 73 adantr ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
75 74 adantr ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
76 75 eleq2d ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ↔ 𝑍 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } ) )
77 fveq1 ⊢ ( 𝑝 = 𝑍 → ( 𝑝 ‘ 1 ) = ( 𝑍 ‘ 1 ) )
78 8 fveq1i ⊢ ( 𝑍 ‘ 1 ) = ( { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ‘ 1 )
79 1ne2 ⊢ 1 ≠ 2
80 1ex ⊢ 1 ∈ V
81 vex ⊢ 𝑥 ∈ V
82 80 81 fvpr1 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ‘ 1 ) = 𝑥 )
83 79 82 ax-mp ⊢ ( { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ‘ 1 ) = 𝑥
84 78 83 eqtri ⊢ ( 𝑍 ‘ 1 ) = 𝑥
85 84 a1i ⊢ ( 𝑝 = 𝑍 → ( 𝑍 ‘ 1 ) = 𝑥 )
86 77 85 eqtrd ⊢ ( 𝑝 = 𝑍 → ( 𝑝 ‘ 1 ) = 𝑥 )
87 86 oveq1d ⊢ ( 𝑝 = 𝑍 → ( ( 𝑝 ‘ 1 ) ↑ 2 ) = ( 𝑥 ↑ 2 ) )
88 fveq1 ⊢ ( 𝑝 = 𝑍 → ( 𝑝 ‘ 2 ) = ( 𝑍 ‘ 2 ) )
89 8 fveq1i ⊢ ( 𝑍 ‘ 2 ) = ( { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ‘ 2 )
90 2ex ⊢ 2 ∈ V
91 vex ⊢ 𝑦 ∈ V
92 90 91 fvpr2 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ‘ 2 ) = 𝑦 )
93 79 92 ax-mp ⊢ ( { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ‘ 2 ) = 𝑦
94 89 93 eqtri ⊢ ( 𝑍 ‘ 2 ) = 𝑦
95 94 a1i ⊢ ( 𝑝 = 𝑍 → ( 𝑍 ‘ 2 ) = 𝑦 )
96 88 95 eqtrd ⊢ ( 𝑝 = 𝑍 → ( 𝑝 ‘ 2 ) = 𝑦 )
97 96 oveq1d ⊢ ( 𝑝 = 𝑍 → ( ( 𝑝 ‘ 2 ) ↑ 2 ) = ( 𝑦 ↑ 2 ) )
98 87 97 oveq12d ⊢ ( 𝑝 = 𝑍 → ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
99 98 eqeq1d ⊢ ( 𝑝 = 𝑍 → ( ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
100 99 elrab ⊢ ( 𝑍 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } ↔ ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
101 100 a1i ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑍 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 1 ) ↑ 2 ) + ( ( 𝑝 ‘ 2 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } ↔ ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ) )
102 76 101 bitrd ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ↔ ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ) )
103 simp1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → 𝑋 ∈ 𝑃 )
104 simp2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → 𝑌 ∈ 𝑃 )
105 fveq1 ⊢ ( 𝑋 = 𝑌 → ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) )
106 105 a1i ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 = 𝑌 → ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) )
107 106 necon3d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) → 𝑋 ≠ 𝑌 ) )
108 107 ex ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑌 ∈ 𝑃 → ( ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) → 𝑋 ≠ 𝑌 ) ) )
109 108 3imp ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → 𝑋 ≠ 𝑌 )
110 103 104 109 3jca ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) )
111 110 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) )
112 111 adantr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) )
113 112 adantr ⊢ ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) )
114 113 adantr ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) )
115 114 adantr ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) )
116 eqid ⊢ ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) )
117 eqid ⊢ ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
118 eqid ⊢ ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) )
119 1 2 3 6 116 117 118 rrx2linest2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) } )
120 115 119 syl ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) } )
121 120 eleq2d ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ↔ 𝑍 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) } ) )
122 86 oveq2d ⊢ ( 𝑝 = 𝑍 → ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) = ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) )
123 96 oveq2d ⊢ ( 𝑝 = 𝑍 → ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) = ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) )
124 122 123 oveq12d ⊢ ( 𝑝 = 𝑍 → ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) ) = ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) )
125 124 eqeq1d ⊢ ( 𝑝 = 𝑍 → ( ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↔ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) )
126 125 elrab ⊢ ( 𝑍 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) } ↔ ( 𝑍 ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) )
127 126 a1i ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑍 ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑝 ‘ 1 ) ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑝 ‘ 2 ) ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) } ↔ ( 𝑍 ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) )
128 121 127 bitrd ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ↔ ( 𝑍 ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) )
129 102 128 anbi12d ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) ↔ ( ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( 𝑍 ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ) )
130 129 reubidva ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ∃! 𝑥 ∈ ℝ ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) ↔ ∃! 𝑥 ∈ ℝ ( ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( 𝑍 ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ) )
131 elelpwi ⊢ ( ( 𝑦 ∈ 𝑠 ∧ 𝑠 ∈ 𝒫 ℝ ) → 𝑦 ∈ ℝ )
132 1 3 prelrrx2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ∈ 𝑃 )
133 132 ancoms ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ∈ 𝑃 )
134 8 eleq1i ⊢ ( 𝑍 ∈ 𝑃 ↔ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ∈ 𝑃 )
135 133 134 sylibr ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → 𝑍 ∈ 𝑃 )
136 135 biantrurd ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ) )
137 136 bicomd ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ↔ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
138 135 biantrurd ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↔ ( 𝑍 ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) )
139 138 bicomd ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝑍 ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) )
140 137 139 anbi12d ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( 𝑍 ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↔ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) )
141 140 reubidva ⊢ ( 𝑦 ∈ ℝ → ( ∃! 𝑥 ∈ ℝ ( ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( 𝑍 ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↔ ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) )
142 131 141 syl ⊢ ( ( 𝑦 ∈ 𝑠 ∧ 𝑠 ∈ 𝒫 ℝ ) → ( ∃! 𝑥 ∈ ℝ ( ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( 𝑍 ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↔ ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) )
143 142 expcom ⊢ ( 𝑠 ∈ 𝒫 ℝ → ( 𝑦 ∈ 𝑠 → ( ∃! 𝑥 ∈ ℝ ( ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( 𝑍 ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↔ ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ) )
144 143 adantl ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) → ( 𝑦 ∈ 𝑠 → ( ∃! 𝑥 ∈ ℝ ( ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( 𝑍 ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↔ ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ) )
145 144 adantr ⊢ ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) → ( 𝑦 ∈ 𝑠 → ( ∃! 𝑥 ∈ ℝ ( ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( 𝑍 ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↔ ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ) )
146 145 imp ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ∃! 𝑥 ∈ ℝ ( ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( 𝑍 ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↔ ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) )
147 27 34 jca ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) → ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ∈ ℝ ∧ ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ≠ 0 ) )
148 147 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ∈ ℝ ∧ ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ≠ 0 ) )
149 148 ad3antrrr ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ∈ ℝ ∧ ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ≠ 0 ) )
150 20 ad3antrrr ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
151 23 ad3antrrr ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
152 150 151 resubcld ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ∈ ℝ )
153 12 ad3antrrr ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
154 153 150 remulcld ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) ∈ ℝ )
155 15 ad3antrrr ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
156 151 155 remulcld ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ∈ ℝ )
157 154 156 resubcld ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ∈ ℝ )
158 149 152 157 3jca ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ∈ ℝ ∧ ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ≠ 0 ) ∧ ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ∈ ℝ ∧ ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ∈ ℝ ) )
159 simplrl ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) → 𝑅 ∈ ℝ+ )
160 159 adantr ⊢ ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) → 𝑅 ∈ ℝ+ )
161 160 adantr ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → 𝑅 ∈ ℝ+ )
162 131 expcom ⊢ ( 𝑠 ∈ 𝒫 ℝ → ( 𝑦 ∈ 𝑠 → 𝑦 ∈ ℝ ) )
163 162 adantl ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) → ( 𝑦 ∈ 𝑠 → 𝑦 ∈ ℝ ) )
164 163 adantr ⊢ ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) → ( 𝑦 ∈ 𝑠 → 𝑦 ∈ ℝ ) )
165 164 imp ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → 𝑦 ∈ ℝ )
166 158 161 165 3jca ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ∈ ℝ ∧ ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ≠ 0 ) ∧ ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ∈ ℝ ∧ ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑦 ∈ ℝ ) )
167 eqid ⊢ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) = ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) )
168 eqid ⊢ - ( 2 · ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) = - ( 2 · ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) )
169 eqid ⊢ ( ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) = ( ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) )
170 167 168 169 itsclquadeu ⊢ ( ( ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ∈ ℝ ∧ ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ≠ 0 ) ∧ ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ∈ ℝ ∧ ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑦 ∈ ℝ ) → ( ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( ( ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) · ( 𝑦 ↑ 2 ) ) + ( ( - ( 2 · ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) · 𝑦 ) + ( ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
171 166 170 syl ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ↔ ( ( ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) · ( 𝑦 ↑ 2 ) ) + ( ( - ( 2 · ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) · 𝑦 ) + ( ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
172 146 171 bitrd ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ∃! 𝑥 ∈ ℝ ( ( 𝑍 ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( 𝑍 ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) ↔ ( ( ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) · ( 𝑦 ↑ 2 ) ) + ( ( - ( 2 · ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) · 𝑦 ) + ( ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
173 130 172 bitrd ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ∃! 𝑥 ∈ ℝ ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) ↔ ( ( ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) · ( 𝑦 ↑ 2 ) ) + ( ( - ( 2 · ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) · 𝑦 ) + ( ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
174 173 ralbidva ⊢ ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) → ( ∀ 𝑦 ∈ 𝑠 ∃! 𝑥 ∈ ℝ ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) ↔ ∀ 𝑦 ∈ 𝑠 ( ( ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) · ( 𝑦 ↑ 2 ) ) + ( ( - ( 2 · ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) · 𝑦 ) + ( ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
175 174 pm5.32da ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) → ( ( ( ♯ ‘ 𝑠 ) = 2 ∧ ∀ 𝑦 ∈ 𝑠 ∃! 𝑥 ∈ ℝ ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) ) ↔ ( ( ♯ ‘ 𝑠 ) = 2 ∧ ∀ 𝑦 ∈ 𝑠 ( ( ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) · ( 𝑦 ↑ 2 ) ) + ( ( - ( 2 · ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) · 𝑦 ) + ( ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) ) )
176 175 reubidva ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ∃! 𝑠 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑠 ) = 2 ∧ ∀ 𝑦 ∈ 𝑠 ∃! 𝑥 ∈ ℝ ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) ) ↔ ∃! 𝑠 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑠 ) = 2 ∧ ∀ 𝑦 ∈ 𝑠 ( ( ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) · ( 𝑦 ↑ 2 ) ) + ( ( - ( 2 · ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) ) · 𝑦 ) + ( ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) ) )
177 57 176 mpbird ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ∃! 𝑠 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑠 ) = 2 ∧ ∀ 𝑦 ∈ 𝑠 ∃! 𝑥 ∈ ℝ ( 𝑍 ∈ ( 0 𝑆 𝑅 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑌 ) ) ) )