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