Metamath Proof Explorer

Theorem itscnhlinecirc02plem3

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

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

Proof

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