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 ⊢ 𝐼 = ( 0 ..^ 2 )
inlinecirc02p.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
inlinecirc02p.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
inlinecirc02p.s ⊢ 𝑆 = ( Sphere ‘ 𝐸 )
inlinecirc02p.0 ⊢ 0 = ⟨“ 0 0 ”⟩
inlinecirc02p.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
inlinecirc02p.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
Assertion inlinecirc02p ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( 0 𝑆 𝑅 ) ∩ ( 𝑋 𝐿 𝑌 ) ) ∈ ( Pairsproper ‘ 𝑃 ) )

Proof

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