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 ⊢ 𝐼 = ( 0 ..^ 2 )
itscnhlinecirc02p.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
itscnhlinecirc02p.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
itscnhlinecirc02p.s ⊢ 𝑆 = ( Sphere ‘ 𝐸 )
itscnhlinecirc02p.0 ⊢ 0 = ( 𝐼 × { 0 } )
itscnhlinecirc02p.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
itscnhlinecirc02p.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
Assertion itscnhlinecirc02p ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ∃! 𝑠 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑠 ) = 2 ∧ ∀ 𝑦 ∈ 𝑠 ∃! 𝑥 ∈ ℝ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 0 𝑆 𝑅 ) ∧ ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 𝑋 𝐿 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 itscnhlinecirc02p.i ⊢ 𝐼 = ( 0 ..^ 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 1 2 3 4 5 6 7 itscnhlinecirc02plem3 ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → 0 < ( ( - ( 2 · ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ↑ 2 ) − ( 4 · ( ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ) · ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) )
9 1 3 rrx2pyel ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℝ )
10 9 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
11 10 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
12 1 3 rrx2pyel ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℝ )
13 12 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
14 13 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
15 11 14 resubcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ∈ ℝ )
16 15 resqcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) ∈ ℝ )
17 1 3 rrx2pxel ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 0 ) ∈ ℝ )
18 17 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑌 ‘ 0 ) ∈ ℝ )
19 18 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 𝑌 ‘ 0 ) ∈ ℝ )
20 1 3 rrx2pxel ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 0 ) ∈ ℝ )
21 20 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 0 ) ∈ ℝ )
22 21 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 𝑋 ‘ 0 ) ∈ ℝ )
23 19 22 resubcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ∈ ℝ )
24 23 resqcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ∈ ℝ )
25 16 24 readdcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ) ∈ ℝ )
26 10 13 resubcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ∈ ℝ )
27 26 resqcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) ∈ ℝ )
28 18 21 resubcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ∈ ℝ )
29 28 resqcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ∈ ℝ )
30 10 recnd ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 1 ) ∈ ℂ )
31 13 recnd ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑌 ‘ 1 ) ∈ ℂ )
32 simp3 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) )
33 30 31 32 subne0d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ≠ 0 )
34 26 33 sqgt0d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → 0 < ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) )
35 28 sqge0d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → 0 ≤ ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) )
36 27 29 34 35 addgtge0d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → 0 < ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ) )
37 36 gt0ne0d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ) ≠ 0 )
38 37 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ) ≠ 0 )
39 2re ⊢ 2 ∈ ℝ
40 39 a1i ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → 2 ∈ ℝ )
41 11 19 remulcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) ∈ ℝ )
42 22 14 remulcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ∈ ℝ )
43 41 42 resubcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ∈ ℝ )
44 23 43 remulcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ∈ ℝ )
45 40 44 remulcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 2 · ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ∈ ℝ )
46 45 renegcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → - ( 2 · ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ∈ ℝ )
47 43 resqcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↑ 2 ) ∈ ℝ )
48 rpre ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ )
49 48 ad2antrl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → 𝑅 ∈ ℝ )
50 49 resqcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
51 16 50 remulcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℝ )
52 47 51 resubcld ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ∈ ℝ )
53 eqidd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( - ( 2 · ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ↑ 2 ) − ( 4 · ( ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ) · ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) = ( ( - ( 2 · ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ↑ 2 ) − ( 4 · ( ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ) · ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) )
54 25 38 46 52 53 requad2 ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ∃! 𝑠 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑠 ) = 2 ∧ ∀ 𝑦 ∈ 𝑠 ( ( ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ) · ( 𝑦 ↑ 2 ) ) + ( ( - ( 2 · ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) · 𝑦 ) + ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) ↔ 0 < ( ( - ( 2 · ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ↑ 2 ) − ( 4 · ( ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ) · ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) )
55 8 54 mpbird ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ∃! 𝑠 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑠 ) = 2 ∧ ∀ 𝑦 ∈ 𝑠 ( ( ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ) · ( 𝑦 ↑ 2 ) ) + ( ( - ( 2 · ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) · 𝑦 ) + ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
56 0xr ⊢ 0 ∈ ℝ*
57 56 a1i ⊢ ( 𝑅 ∈ ℝ+ → 0 ∈ ℝ* )
58 pnfxr ⊢ +∞ ∈ ℝ*
59 58 a1i ⊢ ( 𝑅 ∈ ℝ+ → +∞ ∈ ℝ* )
60 rpxr ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ* )
61 rpge0 ⊢ ( 𝑅 ∈ ℝ+ → 0 ≤ 𝑅 )
62 48 ltpnfd ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 < +∞ )
63 57 59 60 61 62 elicod ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ( 0 [,) +∞ ) )
64 eqid ⊢ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) }
65 1 2 3 4 5 64 2sphere0 ⊢ ( 𝑅 ∈ ( 0 [,) +∞ ) → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
66 63 65 syl ⊢ ( 𝑅 ∈ ℝ+ → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
67 66 ad2antrl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
68 67 ad2antrr ⊢ ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
69 68 ad2antrr ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( 0 𝑆 𝑅 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } )
70 69 eleq2d ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 0 𝑆 𝑅 ) ↔ ⟨“ 𝑥 𝑦 ”⟩ ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } ) )
71 fveq1 ⊢ ( 𝑝 = ⟨“ 𝑥 𝑦 ”⟩ → ( 𝑝 ‘ 0 ) = ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) )
72 71 oveq1d ⊢ ( 𝑝 = ⟨“ 𝑥 𝑦 ”⟩ → ( ( 𝑝 ‘ 0 ) ↑ 2 ) = ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ↑ 2 ) )
73 fveq1 ⊢ ( 𝑝 = ⟨“ 𝑥 𝑦 ”⟩ → ( 𝑝 ‘ 1 ) = ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) )
74 73 oveq1d ⊢ ( 𝑝 = ⟨“ 𝑥 𝑦 ”⟩ → ( ( 𝑝 ‘ 1 ) ↑ 2 ) = ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ↑ 2 ) )
75 72 74 oveq12d ⊢ ( 𝑝 = ⟨“ 𝑥 𝑦 ”⟩ → ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ↑ 2 ) + ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ↑ 2 ) ) )
76 75 eqeq1d ⊢ ( 𝑝 = ⟨“ 𝑥 𝑦 ”⟩ → ( ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ↑ 2 ) + ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
77 76 elrab ⊢ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } ↔ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ↑ 2 ) + ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
78 77 a1i ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( ⟨“ 𝑥 𝑦 ”⟩ ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( 𝑝 ‘ 0 ) ↑ 2 ) + ( ( 𝑝 ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) } ↔ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ↑ 2 ) + ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ) )
79 simpr ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
80 elpwi ⊢ ( 𝑠 ∈ 𝒫 ℝ → 𝑠 ⊆ ℝ )
81 80 ad4antlr ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → 𝑠 ⊆ ℝ )
82 simplr ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → 𝑦 ∈ 𝑠 )
83 81 82 sseldd ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → 𝑦 ∈ ℝ )
84 s2fv0 ⊢ ( 𝑥 ∈ ℝ → ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) = 𝑥 )
85 84 oveq1d ⊢ ( 𝑥 ∈ ℝ → ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ↑ 2 ) = ( 𝑥 ↑ 2 ) )
86 s2fv1 ⊢ ( 𝑦 ∈ ℝ → ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) = 𝑦 )
87 86 oveq1d ⊢ ( 𝑦 ∈ ℝ → ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ↑ 2 ) = ( 𝑦 ↑ 2 ) )
88 85 87 oveqan12d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ↑ 2 ) + ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ↑ 2 ) ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
89 88 eqeq1d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ↑ 2 ) + ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
90 89 anbi2d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ↑ 2 ) + ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ↔ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ) )
91 79 83 90 syl2anc ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ↑ 2 ) + ( ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ↔ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ) )
92 70 78 91 3bitrd ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 0 𝑆 𝑅 ) ↔ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ) )
93 simp1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → 𝑋 ∈ 𝑃 )
94 simp2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → 𝑌 ∈ 𝑃 )
95 fveq1 ⊢ ( 𝑋 = 𝑌 → ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) )
96 95 a1i ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 = 𝑌 → ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) )
97 96 necon3d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) → 𝑋 ≠ 𝑌 ) )
98 97 3impia ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → 𝑋 ≠ 𝑌 )
99 93 94 98 3jca ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) )
100 99 ad3antrrr ⊢ ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) )
101 100 ad2antrr ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) )
102 eqid ⊢ ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) = ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) )
103 eqid ⊢ ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) = ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) )
104 eqid ⊢ ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) )
105 1 2 3 6 102 103 104 rrx2linest2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) } )
106 101 105 syl ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑋 𝐿 𝑌 ) = { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) } )
107 106 eleq2d ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 𝑋 𝐿 𝑌 ) ↔ ⟨“ 𝑥 𝑦 ”⟩ ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) } ) )
108 71 oveq2d ⊢ ( 𝑝 = ⟨“ 𝑥 𝑦 ”⟩ → ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) = ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ) )
109 73 oveq2d ⊢ ( 𝑝 = ⟨“ 𝑥 𝑦 ”⟩ → ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) = ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ) )
110 108 109 oveq12d ⊢ ( 𝑝 = ⟨“ 𝑥 𝑦 ”⟩ → ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) ) = ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ) ) )
111 110 eqeq1d ⊢ ( 𝑝 = ⟨“ 𝑥 𝑦 ”⟩ → ( ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↔ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) )
112 111 elrab ⊢ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) } ↔ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) )
113 84 oveq2d ⊢ ( 𝑥 ∈ ℝ → ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ) = ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) )
114 86 oveq2d ⊢ ( 𝑦 ∈ ℝ → ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ) = ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) )
115 113 114 oveqan12d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ) ) = ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) )
116 115 eqeq1d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↔ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) )
117 116 anbi2d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 0 ) ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ⟨“ 𝑥 𝑦 ”⟩ ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ↔ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) )
118 112 117 bitrid ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ⟨“ 𝑥 𝑦 ”⟩ ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) } ↔ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) )
119 79 83 118 syl2anc ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( ⟨“ 𝑥 𝑦 ”⟩ ∈ { 𝑝 ∈ 𝑃 ∣ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · ( 𝑝 ‘ 0 ) ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( 𝑝 ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) } ↔ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) )
120 107 119 bitrd ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 𝑋 𝐿 𝑌 ) ↔ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) )
121 92 120 anbi12d ⊢ ( ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( ( ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 0 𝑆 𝑅 ) ∧ ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 𝑋 𝐿 𝑌 ) ) ↔ ( ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ) )
122 121 reubidva ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ∃! 𝑥 ∈ ℝ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 0 𝑆 𝑅 ) ∧ ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 𝑋 𝐿 𝑌 ) ) ↔ ∃! 𝑥 ∈ ℝ ( ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ) )
123 elelpwi ⊢ ( ( 𝑦 ∈ 𝑠 ∧ 𝑠 ∈ 𝒫 ℝ ) → 𝑦 ∈ ℝ )
124 1 3 prelrrx2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 )
125 124 ancoms ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 )
126 125 biantrurd ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ) )
127 126 bicomd ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ↔ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) )
128 125 biantrurd ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↔ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) )
129 128 bicomd ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ↔ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) )
130 127 129 anbi12d ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ↔ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) )
131 130 reubidva ⊢ ( 𝑦 ∈ ℝ → ( ∃! 𝑥 ∈ ℝ ( ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ↔ ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) )
132 123 131 syl ⊢ ( ( 𝑦 ∈ 𝑠 ∧ 𝑠 ∈ 𝒫 ℝ ) → ( ∃! 𝑥 ∈ ℝ ( ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ↔ ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) )
133 132 expcom ⊢ ( 𝑠 ∈ 𝒫 ℝ → ( 𝑦 ∈ 𝑠 → ( ∃! 𝑥 ∈ ℝ ( ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ↔ ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ) )
134 133 ad2antlr ⊢ ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) → ( 𝑦 ∈ 𝑠 → ( ∃! 𝑥 ∈ ℝ ( ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ↔ ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ) )
135 134 imp ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ∃! 𝑥 ∈ ℝ ( ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ∧ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ 𝑃 ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) ↔ ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) )
136 26 33 jca ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ∈ ℝ ∧ ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ≠ 0 ) )
137 136 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ∈ ℝ ∧ ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ≠ 0 ) )
138 137 ad3antrrr ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ∈ ℝ ∧ ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ≠ 0 ) )
139 19 ad3antrrr ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( 𝑌 ‘ 0 ) ∈ ℝ )
140 22 ad3antrrr ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( 𝑋 ‘ 0 ) ∈ ℝ )
141 139 140 resubcld ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ∈ ℝ )
142 11 ad3antrrr ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
143 142 139 remulcld ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) ∈ ℝ )
144 14 ad3antrrr ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
145 140 144 remulcld ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ∈ ℝ )
146 143 145 resubcld ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ∈ ℝ )
147 simplrl ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) → 𝑅 ∈ ℝ+ )
148 147 ad2antrr ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → 𝑅 ∈ ℝ+ )
149 123 expcom ⊢ ( 𝑠 ∈ 𝒫 ℝ → ( 𝑦 ∈ 𝑠 → 𝑦 ∈ ℝ ) )
150 149 ad2antlr ⊢ ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) → ( 𝑦 ∈ 𝑠 → 𝑦 ∈ ℝ ) )
151 150 imp ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → 𝑦 ∈ ℝ )
152 eqid ⊢ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ) = ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) )
153 eqid ⊢ - ( 2 · ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) = - ( 2 · ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) )
154 eqid ⊢ ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) = ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) )
155 152 153 154 itsclquadeu ⊢ ( ( ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ∈ ℝ ∧ ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ≠ 0 ) ∧ ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ∈ ℝ ∧ ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑦 ∈ ℝ ) → ( ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ↔ ( ( ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ) · ( 𝑦 ↑ 2 ) ) + ( ( - ( 2 · ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) · 𝑦 ) + ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
156 138 141 146 148 151 155 syl311anc ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ∃! 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) · 𝑥 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · 𝑦 ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ↔ ( ( ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ) · ( 𝑦 ↑ 2 ) ) + ( ( - ( 2 · ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) · 𝑦 ) + ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
157 122 135 156 3bitrd ⊢ ( ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) ∧ 𝑦 ∈ 𝑠 ) → ( ∃! 𝑥 ∈ ℝ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 0 𝑆 𝑅 ) ∧ ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 𝑋 𝐿 𝑌 ) ) ↔ ( ( ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ) · ( 𝑦 ↑ 2 ) ) + ( ( - ( 2 · ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) · 𝑦 ) + ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
158 157 ralbidva ⊢ ( ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) ∧ ( ♯ ‘ 𝑠 ) = 2 ) → ( ∀ 𝑦 ∈ 𝑠 ∃! 𝑥 ∈ ℝ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 0 𝑆 𝑅 ) ∧ ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 𝑋 𝐿 𝑌 ) ) ↔ ∀ 𝑦 ∈ 𝑠 ( ( ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ) · ( 𝑦 ↑ 2 ) ) + ( ( - ( 2 · ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) · 𝑦 ) + ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
159 158 pm5.32da ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) ∧ 𝑠 ∈ 𝒫 ℝ ) → ( ( ( ♯ ‘ 𝑠 ) = 2 ∧ ∀ 𝑦 ∈ 𝑠 ∃! 𝑥 ∈ ℝ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 0 𝑆 𝑅 ) ∧ ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 𝑋 𝐿 𝑌 ) ) ) ↔ ( ( ♯ ‘ 𝑠 ) = 2 ∧ ∀ 𝑦 ∈ 𝑠 ( ( ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ) · ( 𝑦 ↑ 2 ) ) + ( ( - ( 2 · ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) · 𝑦 ) + ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) ) )
160 159 reubidva ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ∃! 𝑠 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑠 ) = 2 ∧ ∀ 𝑦 ∈ 𝑠 ∃! 𝑥 ∈ ℝ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 0 𝑆 𝑅 ) ∧ ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 𝑋 𝐿 𝑌 ) ) ) ↔ ∃! 𝑠 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑠 ) = 2 ∧ ∀ 𝑦 ∈ 𝑠 ( ( ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) ↑ 2 ) ) · ( 𝑦 ↑ 2 ) ) + ( ( - ( 2 · ( ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) · ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ) ) · 𝑦 ) + ( ( ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) ↑ 2 ) − ( ( ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) ) )
161 55 160 mpbird ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ∃! 𝑠 ∈ 𝒫 ℝ ( ( ♯ ‘ 𝑠 ) = 2 ∧ ∀ 𝑦 ∈ 𝑠 ∃! 𝑥 ∈ ℝ ( ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 0 𝑆 𝑅 ) ∧ ⟨“ 𝑥 𝑦 ”⟩ ∈ ( 𝑋 𝐿 𝑌 ) ) ) )