Metamath Proof Explorer

Theorem inlinecirc02p

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

Ref Expression
Hypotheses inlinecirc02p.i ⊢ 𝐼 = { 1 , 2 }
inlinecirc02p.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
inlinecirc02p.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
inlinecirc02p.s ⊢ 𝑆 = ( Sphere ‘ 𝐸 )
inlinecirc02p.0 ⊢ 0 = ( 𝐼 × { 0 } )
inlinecirc02p.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
inlinecirc02p.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
Assertion inlinecirc02p ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ∈ ( Pairsproper ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 inlinecirc02p.i ⊢ 𝐼 = { 1 , 2 }
2 inlinecirc02p.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3 inlinecirc02p.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4 inlinecirc02p.s ⊢ 𝑆 = ( Sphere ‘ 𝐸 )
5 inlinecirc02p.0 ⊢ 0 = ( 𝐼 × { 0 } )
6 inlinecirc02p.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
7 inlinecirc02p.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
8 3 ovexi ⊢ 𝑃 ∈ V
9 8 a1i ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → 𝑃 ∈ V )
10 simpl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) )
11 simpl ⊢ ( ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) → 𝑅 ∈ ℝ+ )
12 11 adantl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → 𝑅 ∈ ℝ+ )
13 1 3 rrx2pxel ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℝ )
14 13 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
15 14 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
16 1 3 rrx2pyel ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 2 ) ∈ ℝ )
17 16 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
18 17 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 𝑋 ‘ 2 ) ∈ ℝ )
19 1 3 rrx2pxel ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℝ )
20 19 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
21 20 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 𝑌 ‘ 1 ) ∈ ℝ )
22 1 3 rrx2pyel ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 2 ) ∈ ℝ )
23 22 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
24 23 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 𝑌 ‘ 2 ) ∈ ℝ )
25 eqid ⊢ ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) )
26 eqid ⊢ ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) )
27 eqid ⊢ ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑋 ‘ 2 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑋 ‘ 1 ) ) ) = ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑋 ‘ 2 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑋 ‘ 1 ) ) )
28 rpre ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ )
29 28 adantr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) → 𝑅 ∈ ℝ )
30 29 adantl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → 𝑅 ∈ ℝ )
31 2nn0 ⊢ 2 ∈ ℕ0
32 eqid ⊢ ( 𝔼hil ‘ 2 ) = ( 𝔼hil ‘ 2 )
33 32 ehlval ⊢ ( 2 ∈ ℕ0 → ( 𝔼hil ‘ 2 ) = ( ℝ^ ‘ ( 1 ... 2 ) ) )
34 31 33 ax-mp ⊢ ( 𝔼hil ‘ 2 ) = ( ℝ^ ‘ ( 1 ... 2 ) )
35 fz12pr ⊢ ( 1 ... 2 ) = { 1 , 2 }
36 35 1 eqtr4i ⊢ ( 1 ... 2 ) = 𝐼
37 36 fveq2i ⊢ ( ℝ^ ‘ ( 1 ... 2 ) ) = ( ℝ^ ‘ 𝐼 )
38 34 37 eqtri ⊢ ( 𝔼hil ‘ 2 ) = ( ℝ^ ‘ 𝐼 )
39 2 38 eqtr4i ⊢ 𝐸 = ( 𝔼hil ‘ 2 )
40 1 oveq2i ⊢ ( ℝ ↑m 𝐼 ) = ( ℝ ↑m { 1 , 2 } )
41 3 40 eqtri ⊢ 𝑃 = ( ℝ ↑m { 1 , 2 } )
42 1 xpeq1i ⊢ ( 𝐼 × { 0 } ) = ( { 1 , 2 } × { 0 } )
43 5 42 eqtri ⊢ 0 = ( { 1 , 2 } × { 0 } )
44 39 41 7 43 ehl2eudis0lt ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑅 ∈ ℝ+ ) → ( ( 𝑋 𝐷 0 ) < 𝑅 ↔ ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) )
45 44 3ad2antl1 ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑅 ∈ ℝ+ ) → ( ( 𝑋 𝐷 0 ) < 𝑅 ↔ ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) )
46 45 biimpd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑅 ∈ ℝ+ ) → ( ( 𝑋 𝐷 0 ) < 𝑅 → ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) )
47 46 impr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( 𝑋 ‘ 1 ) ↑ 2 ) + ( ( 𝑋 ‘ 2 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) )
48 1 3 rrx2pnecoorneor ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ∨ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) )
49 48 orcomd ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ∨ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) )
50 49 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ∨ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) )
51 eqid ⊢ ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) = ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) )
52 eqid ⊢ ( ( ( 𝑅 ↑ 2 ) · ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) ) − ( ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑋 ‘ 2 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑋 ‘ 1 ) ) ) ↑ 2 ) ) = ( ( ( 𝑅 ↑ 2 ) · ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) ) − ( ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑋 ‘ 2 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑋 ‘ 1 ) ) ) ↑ 2 ) )
53 15 18 21 24 25 26 27 30 47 50 51 52 2itscp ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → 0 < ( ( ( 𝑅 ↑ 2 ) · ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) ) − ( ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑋 ‘ 2 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑋 ‘ 1 ) ) ) ↑ 2 ) ) )
54 19 recnd ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℂ )
55 54 adantl ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑌 ‘ 1 ) ∈ ℂ )
56 13 recnd ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℂ )
57 56 adantr ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ‘ 1 ) ∈ ℂ )
58 16 recnd ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 2 ) ∈ ℂ )
59 58 adantr ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ‘ 2 ) ∈ ℂ )
60 55 57 59 subdird ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑋 ‘ 2 ) ) = ( ( ( 𝑌 ‘ 1 ) · ( 𝑋 ‘ 2 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑋 ‘ 2 ) ) ) )
61 22 recnd ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 2 ) ∈ ℂ )
62 61 adantl ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑌 ‘ 2 ) ∈ ℂ )
63 59 62 57 subdird ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑋 ‘ 1 ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑋 ‘ 1 ) ) − ( ( 𝑌 ‘ 2 ) · ( 𝑋 ‘ 1 ) ) ) )
64 60 63 oveq12d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑋 ‘ 2 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑋 ‘ 1 ) ) ) = ( ( ( ( 𝑌 ‘ 1 ) · ( 𝑋 ‘ 2 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑋 ‘ 2 ) ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑋 ‘ 1 ) ) − ( ( 𝑌 ‘ 2 ) · ( 𝑋 ‘ 1 ) ) ) ) )
65 55 59 mulcomd ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑌 ‘ 1 ) · ( 𝑋 ‘ 2 ) ) = ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) )
66 65 oveq1d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( 𝑌 ‘ 1 ) · ( 𝑋 ‘ 2 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑋 ‘ 2 ) ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑋 ‘ 2 ) ) ) )
67 59 57 mulcomd ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ‘ 2 ) · ( 𝑋 ‘ 1 ) ) = ( ( 𝑋 ‘ 1 ) · ( 𝑋 ‘ 2 ) ) )
68 62 57 mulcomd ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑌 ‘ 2 ) · ( 𝑋 ‘ 1 ) ) = ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) )
69 67 68 oveq12d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( 𝑋 ‘ 2 ) · ( 𝑋 ‘ 1 ) ) − ( ( 𝑌 ‘ 2 ) · ( 𝑋 ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑋 ‘ 2 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) )
70 66 69 oveq12d ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( ( 𝑌 ‘ 1 ) · ( 𝑋 ‘ 2 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑋 ‘ 2 ) ) ) + ( ( ( 𝑋 ‘ 2 ) · ( 𝑋 ‘ 1 ) ) − ( ( 𝑌 ‘ 2 ) · ( 𝑋 ‘ 1 ) ) ) ) = ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑋 ‘ 2 ) ) ) + ( ( ( 𝑋 ‘ 1 ) · ( 𝑋 ‘ 2 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) )
71 59 55 mulcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) ∈ ℂ )
72 57 59 mulcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ‘ 1 ) · ( 𝑋 ‘ 2 ) ) ∈ ℂ )
73 57 62 mulcld ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ∈ ℂ )
74 71 72 73 npncand ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑋 ‘ 2 ) ) ) + ( ( ( 𝑋 ‘ 1 ) · ( 𝑋 ‘ 2 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) )
75 64 70 74 3eqtrd ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑋 ‘ 2 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑋 ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) )
76 75 3adant3 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑋 ‘ 2 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑋 ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) )
77 76 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑋 ‘ 2 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑋 ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) )
78 77 eqcomd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) = ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑋 ‘ 2 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑋 ‘ 1 ) ) ) )
79 78 oveq1d ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) = ( ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑋 ‘ 2 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑋 ‘ 1 ) ) ) ↑ 2 ) )
80 79 oveq2d ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( 𝑅 ↑ 2 ) · ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) ) − ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) ) = ( ( ( 𝑅 ↑ 2 ) · ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) ) − ( ( ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) · ( 𝑋 ‘ 2 ) ) + ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) · ( 𝑋 ‘ 1 ) ) ) ↑ 2 ) ) )
81 53 80 breqtrrd ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → 0 < ( ( ( 𝑅 ↑ 2 ) · ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) ) − ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) ) )
82 eqid ⊢ ( ( ( 𝑅 ↑ 2 ) · ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) ) − ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) ) = ( ( ( 𝑅 ↑ 2 ) · ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) ) − ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) )
83 eqid ⊢ ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) = ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) )
84 1 2 3 4 5 6 51 82 26 25 83 inlinecirc02plem ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ 0 < ( ( ( 𝑅 ↑ 2 ) · ( ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) ↑ 2 ) + ( ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) ↑ 2 ) ) ) − ( ( ( ( 𝑋 ‘ 2 ) · ( 𝑌 ‘ 1 ) ) − ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 2 ) ) ) ↑ 2 ) ) ) ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) )
85 10 12 81 84 syl12anc ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) )
86 prprelprb ⊢ ( ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ∈ ( Pairsproper ‘ 𝑃 ) ↔ ( 𝑃 ∈ V ∧ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) = { 𝑎 , 𝑏 } ∧ 𝑎 ≠ 𝑏 ) ) )
87 9 85 86 sylanbrc ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ∈ ( Pairsproper ‘ 𝑃 ) )