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 } )
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 } )
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 1 xpeq1i ⊢ ( 𝐼 × { 0 } ) = ( ( 0 ..^ 2 ) × { 0 } )
33 5 32 eqtri ⊢ 0 = ( ( 0 ..^ 2 ) × { 0 } )
34 29 31 7 33 ehl2eudisval0 ⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 𝐷 0 ) = ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) )
35 22 34 syl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( 𝑋 𝐷 0 ) = ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) )
36 35 breq1d ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( ( 𝑋 𝐷 0 ) < 𝑅 ↔ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) )
37 rpge0 ⊢ ( 𝑅 ∈ ℝ+ → 0 ≤ 𝑅 )
38 19 37 sqrtsqd ⊢ ( 𝑅 ∈ ℝ+ → ( √ ‘ ( 𝑅 ↑ 2 ) ) = 𝑅 )
39 38 eqcomd ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 = ( √ ‘ ( 𝑅 ↑ 2 ) ) )
40 39 adantl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → 𝑅 = ( √ ‘ ( 𝑅 ↑ 2 ) ) )
41 40 breq2d ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ↔ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < ( √ ‘ ( 𝑅 ↑ 2 ) ) ) )
42 41 biimpa ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < ( √ ‘ ( 𝑅 ↑ 2 ) ) )
43 22 8 syl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( 𝑋 ‘ 0 ) ∈ ℝ )
44 43 adantr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( 𝑋 ‘ 0 ) ∈ ℝ )
45 44 resqcld ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( ( 𝑋 ‘ 0 ) ↑ 2 ) ∈ ℝ )
46 22 9 syl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
47 46 adantr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( 𝑋 ‘ 1 ) ∈ ℝ )
48 47 resqcld ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( ( 𝑋 ‘ 1 ) ↑ 2 ) ∈ ℝ )
49 45 48 readdcld ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ∈ ℝ )
50 44 sqge0d ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → 0 ≤ ( ( 𝑋 ‘ 0 ) ↑ 2 ) )
51 47 sqge0d ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → 0 ≤ ( ( 𝑋 ‘ 1 ) ↑ 2 ) )
52 45 48 50 51 addge0d ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → 0 ≤ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) )
53 19 adantl ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → 𝑅 ∈ ℝ )
54 53 adantr ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → 𝑅 ∈ ℝ )
55 54 resqcld ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
56 54 sqge0d ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → 0 ≤ ( 𝑅 ↑ 2 ) )
57 49 52 55 56 sqrtltd ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ↔ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < ( √ ‘ ( 𝑅 ↑ 2 ) ) ) )
58 42 57 mpbird ⊢ ( ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 ) → ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) )
59 58 ex ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( ( √ ‘ ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) ) < 𝑅 → ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) )
60 36 59 sylbid ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ 𝑅 ∈ ℝ+ ) → ( ( 𝑋 𝐷 0 ) < 𝑅 → ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) )
61 60 impr ⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ) ∧ ( 𝑅 ∈ ℝ+ ∧ ( 𝑋 𝐷 0 ) < 𝑅 ) ) → ( ( ( 𝑋 ‘ 0 ) ↑ 2 ) + ( ( 𝑋 ‘ 1 ) ↑ 2 ) ) < ( 𝑅 ↑ 2 ) )
62 eqid ⊢ ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) ) = ( ( 𝑌 ‘ 0 ) − ( 𝑋 ‘ 0 ) )
63 eqid ⊢ ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) ) = ( ( 𝑋 ‘ 1 ) − ( 𝑌 ‘ 1 ) )
64 eqid ⊢ ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) ) = ( ( ( 𝑋 ‘ 1 ) · ( 𝑌 ‘ 0 ) ) − ( ( 𝑋 ‘ 0 ) · ( 𝑌 ‘ 1 ) ) )
65 62 63 64 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 ) ) ) ) ) ) )
66 12 17 18 21 61 65 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 ) ) ) ) ) ) )