Metamath Proof Explorer

Theorem itscnhlinecirc02plem3

Description: Lemma 3 for itscnhlinecirc02p . (Contributed by AV, 10-Mar-2023)

Ref Expression
Hypotheses itscnhlinecirc02p.i ⊢ 𝐼 = ( 0 ..^ 2 )
itscnhlinecirc02p.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
itscnhlinecirc02p.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
itscnhlinecirc02p.s ⊢ 𝑆 = ( Sphere ‘ 𝐸 )
itscnhlinecirc02p.0 ⊢ 0 = ⟨“ 0 0 ”⟩
itscnhlinecirc02p.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
itscnhlinecirc02p.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
Assertion 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 ) ) ) ) ) ) )

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 0 ”⟩
6 itscnhlinecirc02p.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
7 itscnhlinecirc02p.d ⊢ 𝐷 = ( dist ‘ 𝐸 )
8 1 3 rrx2pxel ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 0 ) ∈ ℝ )
9 1 3 rrx2pyel ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 1 ) ∈ ℝ )
10 8 9 jca ⊢ ( 𝑋 ∈ 𝑃 → ( ( 𝑋 ‘ 0 ) ∈ ℝ ∧ ( 𝑋 ‘ 1 ) ∈ ℝ ) )
11 10 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( ( 𝑋 ‘ 0 ) ∈ ℝ ∧ ( 𝑋 ‘ 1 ) ∈ ℝ ) )
12 11 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( 𝑋 ‘ 0 ) ∈ ℝ ∧ ( 𝑋 ‘ 1 ) ∈ ℝ ) )
13 1 3 rrx2pxel ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 0 ) ∈ ℝ )
14 1 3 rrx2pyel ⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 1 ) ∈ ℝ )
15 13 14 jca ⊢ ( 𝑌 ∈ 𝑃 → ( ( 𝑌 ‘ 0 ) ∈ ℝ ∧ ( 𝑌 ‘ 1 ) ∈ ℝ ) )
16 15 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) → ( ( 𝑌 ‘ 0 ) ∈ ℝ ∧ ( 𝑌 ‘ 1 ) ∈ ℝ ) )
17 16 adantr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( 𝑌 ‘ 0 ) ∈ ℝ ∧ ( 𝑌 ‘ 1 ) ∈ ℝ ) )
18 simpl3 ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) )
19 rpre ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ )
20 19 adantr ⊢ ( ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) → 𝑅 ∈ ℝ )
21 20 adantl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → 𝑅 ∈ ℝ )
22 simpl1 ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → 𝑋 ∈ 𝑃 )
23 1 eqcomi ⊢ ( 0 ..^ 2 ) = 𝐼
24 23 fveq2i ⊢ ( ℝ^ ‘ ( 0 ..^ 2 ) ) = ( ℝ^ ‘ 𝐼 )
25 2nn0 ⊢ 2 ∈ ℕ0
26 eqid ⊢ ( 𝔼hil ‘ 2 ) = ( 𝔼hil ‘ 2 )
27 26 ehlval ⊢ ( 2 ∈ ℕ0 → ( 𝔼hil ‘ 2 ) = ( ℝ^ ‘ ( 0 ..^ 2 ) ) )
28 25 27 ax-mp ⊢ ( 𝔼hil ‘ 2 ) = ( ℝ^ ‘ ( 0 ..^ 2 ) )
29 24 28 2 3eqtr4ri ⊢ 𝐸 = ( 𝔼hil ‘ 2 )
30 1 oveq2i ⊢ ( ℝ ↑m 𝐼 ) = ( ℝ ↑m ( 0 ..^ 2 ) )
31 3 30 eqtri ⊢ 𝑃 = ( ℝ ↑m ( 0 ..^ 2 ) )
32 29 31 7 5 ehl2eudisval0 ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 𝐷 0 ) = ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) )
33 22 32 syl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( 𝑋 𝐷 0 ) = ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) )
34 33 breq1d ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( ( 𝑋 𝐷 0 ) < 𝑅 ↔ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) )
35 rpge0 ⊢ ( 𝑅 ∈ ℝ+ → 0 ≤ 𝑅 )
36 19 35 sqrtsqd ⊢ ( 𝑅 ∈ ℝ+ → ( √ ‘ ( 𝑅 ↑ 2 ) ) = 𝑅 )
37 36 eqcomd ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 = ( √ ‘ ( 𝑅 ↑ 2 ) ) )
38 37 adantl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → 𝑅 = ( √ ‘ ( 𝑅 ↑ 2 ) ) )
39 38 breq2d ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ↔ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < ( √ ‘ ( 𝑅 ↑ 2 ) ) ) )
40 39 biimpa ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < ( √ ‘ ( 𝑅 ↑ 2 ) ) )
41 22 8 syl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( 𝑋 ‘ 0 ) ∈ ℝ )
42 41 adantr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( 𝑋 ‘ 0 ) ∈ ℝ )
43 42 resqcld ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( ( 𝑋 ‘ 0 ) ↑ 2 ) ∈ ℝ )
44 22 9 syl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
45 44 adantr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
46 45 resqcld ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( ( 𝑋 ‘ 1 ) ↑ 2 ) ∈ ℝ )
47 43 46 readdcld ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ∈ ℝ )
48 42 sqge0d ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → 0 ≤ ( ( 𝑋 ‘ 0 ) ↑ 2 ) )
49 45 sqge0d ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → 0 ≤ ( ( 𝑋 ‘ 1 ) ↑ 2 ) )
50 43 46 48 49 addge0d ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → 0 ≤ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) )
51 19 adantl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → 𝑅 ∈ ℝ )
52 51 adantr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → 𝑅 ∈ ℝ )
53 52 resqcld ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
54 52 sqge0d ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → 0 ≤ ( 𝑅 ↑ 2 ) )
55 47 50 53 54 sqrtltd ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ↔ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < ( √ ‘ ( 𝑅 ↑ 2 ) ) ) )
56 40 55 mpbird ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) )
57 56 ex ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 → ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) )
58 34 57 sylbid ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( ( 𝑋 𝐷 0 ) < 𝑅 → ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) )
59 58 impr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) )
60 eqid ⊢ ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) = ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) )
61 eqid ⊢ ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) = ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) )
62 eqid ⊢ ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) )
63 60 61 62 itscnhlinecirc02plem2 ⊢ ( ( ( ( ( 𝑋 ‘ 0 ) ∈ ℝ ∧ ( 𝑋 ‘ 1 ) ∈ ℝ ) ∧ ( ( 𝑌 ‘ 0 ) ∈ ℝ ∧ ( 𝑌 ‘ 1 ) ∈ ℝ ) ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ ∧ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) ) → 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 ) ) ) ) ) ) )
64 12 17 18 21 59 63 syl32anc ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 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 ) ) ) ) ) ) )