| Step | Hyp | Ref
| Expression |
| 1 | | itscnhlinecirc02p.i |
. . . 4
⊢ 𝐼 = {1, 2} |
| 2 | | itscnhlinecirc02p.e |
. . . 4
⊢ 𝐸 = (ℝ^‘𝐼) |
| 3 | | itscnhlinecirc02p.p |
. . . 4
⊢ 𝑃 = (ℝ ↑m
𝐼) |
| 4 | | itscnhlinecirc02p.s |
. . . 4
⊢ 𝑆 = (Sphere‘𝐸) |
| 5 | | itscnhlinecirc02p.0 |
. . . 4
⊢ 0 = (𝐼 × {0}) |
| 6 | | itscnhlinecirc02p.l |
. . . 4
⊢ 𝐿 = (LineM‘𝐸) |
| 7 | | itscnhlinecirc02p.d |
. . . 4
⊢ 𝐷 = (dist‘𝐸) |
| 8 | 1, 2, 3, 4, 5, 6, 7 | itscnhlinecirc02plem3 48705 |
. . 3
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘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))))))) |
| 9 | 1, 3 | rrx2pyel 48633 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑃 → (𝑋‘2) ∈ ℝ) |
| 10 | 9 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → (𝑋‘2) ∈ ℝ) |
| 11 | 10 | adantr 480 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (𝑋‘2) ∈ ℝ) |
| 12 | 1, 3 | rrx2pyel 48633 |
. . . . . . . . 9
⊢ (𝑌 ∈ 𝑃 → (𝑌‘2) ∈ ℝ) |
| 13 | 12 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → (𝑌‘2) ∈ ℝ) |
| 14 | 13 | adantr 480 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (𝑌‘2) ∈ ℝ) |
| 15 | 11, 14 | resubcld 11691 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((𝑋‘2) − (𝑌‘2)) ∈ ℝ) |
| 16 | 15 | resqcld 14165 |
. . . . 5
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (((𝑋‘2) − (𝑌‘2))↑2) ∈
ℝ) |
| 17 | 1, 3 | rrx2pxel 48632 |
. . . . . . . . 9
⊢ (𝑌 ∈ 𝑃 → (𝑌‘1) ∈ ℝ) |
| 18 | 17 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → (𝑌‘1) ∈ ℝ) |
| 19 | 18 | adantr 480 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (𝑌‘1) ∈ ℝ) |
| 20 | 1, 3 | rrx2pxel 48632 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑃 → (𝑋‘1) ∈ ℝ) |
| 21 | 20 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → (𝑋‘1) ∈ ℝ) |
| 22 | 21 | adantr 480 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (𝑋‘1) ∈ ℝ) |
| 23 | 19, 22 | resubcld 11691 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((𝑌‘1) − (𝑋‘1)) ∈ ℝ) |
| 24 | 23 | resqcld 14165 |
. . . . 5
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (((𝑌‘1) − (𝑋‘1))↑2) ∈
ℝ) |
| 25 | 16, 24 | readdcld 11290 |
. . . 4
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) ∈
ℝ) |
| 26 | 10, 13 | resubcld 11691 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → ((𝑋‘2) − (𝑌‘2)) ∈ ℝ) |
| 27 | 26 | resqcld 14165 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → (((𝑋‘2) − (𝑌‘2))↑2) ∈
ℝ) |
| 28 | 18, 21 | resubcld 11691 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → ((𝑌‘1) − (𝑋‘1)) ∈ ℝ) |
| 29 | 28 | resqcld 14165 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → (((𝑌‘1) − (𝑋‘1))↑2) ∈
ℝ) |
| 30 | 10 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → (𝑋‘2) ∈ ℂ) |
| 31 | 13 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → (𝑌‘2) ∈ ℂ) |
| 32 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → (𝑋‘2) ≠ (𝑌‘2)) |
| 33 | 30, 31, 32 | subne0d 11629 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → ((𝑋‘2) − (𝑌‘2)) ≠ 0) |
| 34 | 26, 33 | sqgt0d 14289 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → 0 < (((𝑋‘2) − (𝑌‘2))↑2)) |
| 35 | 28 | sqge0d 14177 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → 0 ≤ (((𝑌‘1) − (𝑋‘1))↑2)) |
| 36 | 27, 29, 34, 35 | addgtge0d 11837 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → 0 < ((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2))) |
| 37 | 36 | gt0ne0d 11827 |
. . . . 5
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → ((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) ≠ 0) |
| 38 | 37 | adantr 480 |
. . . 4
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) ≠ 0) |
| 39 | | 2re 12340 |
. . . . . . 7
⊢ 2 ∈
ℝ |
| 40 | 39 | a1i 11 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → 2 ∈ ℝ) |
| 41 | 11, 19 | remulcld 11291 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((𝑋‘2) · (𝑌‘1)) ∈ ℝ) |
| 42 | 22, 14 | remulcld 11291 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((𝑋‘1) · (𝑌‘2)) ∈ ℝ) |
| 43 | 41, 42 | resubcld 11691 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ∈ ℝ) |
| 44 | 23, 43 | remulcld 11291 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (((𝑌‘1) − (𝑋‘1)) · (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) ∈
ℝ) |
| 45 | 40, 44 | remulcld 11291 |
. . . . 5
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (2 · (((𝑌‘1) − (𝑋‘1)) · (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ∈
ℝ) |
| 46 | 45 | renegcld 11690 |
. . . 4
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → -(2 · (((𝑌‘1) − (𝑋‘1)) · (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ∈
ℝ) |
| 47 | 43 | resqcld 14165 |
. . . . 5
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))↑2) ∈
ℝ) |
| 48 | | rpre 13043 |
. . . . . . . . 9
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ) |
| 49 | 48 | adantr 480 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ+
∧ (𝑋𝐷 0 ) < 𝑅) → 𝑅 ∈ ℝ) |
| 50 | 49 | adantl 481 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → 𝑅 ∈ ℝ) |
| 51 | 50 | resqcld 14165 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (𝑅↑2) ∈ ℝ) |
| 52 | 16, 51 | remulcld 11291 |
. . . . 5
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ((((𝑋‘2) − (𝑌‘2))↑2) · (𝑅↑2)) ∈
ℝ) |
| 53 | 47, 52 | resubcld 11691 |
. . . 4
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (((((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))↑2) − ((((𝑋‘2) − (𝑌‘2))↑2) ·
(𝑅↑2))) ∈
ℝ) |
| 54 | | eqidd 2738 |
. . . 4
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘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)))))) =
((-(2 · (((𝑌‘1) − (𝑋‘1)) · (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))))↑2) − (4 ·
(((((𝑋‘2) −
(𝑌‘2))↑2) +
(((𝑌‘1) −
(𝑋‘1))↑2))
· (((((𝑋‘2)
· (𝑌‘1))
− ((𝑋‘1)
· (𝑌‘2)))↑2) − ((((𝑋‘2) − (𝑌‘2))↑2) ·
(𝑅↑2))))))) |
| 55 | 25, 38, 46, 53, 54 | requad2 47610 |
. . 3
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (∃!𝑠 ∈ 𝒫
ℝ((♯‘𝑠) =
2 ∧ ∀𝑦 ∈
𝑠 ((((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) · (𝑦↑2)) + ((-(2 ·
(((𝑌‘1) −
(𝑋‘1)) ·
(((𝑋‘2) ·
(𝑌‘1)) −
((𝑋‘1) ·
(𝑌‘2))))) ·
𝑦) + (((((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))↑2) − ((((𝑋‘2) − (𝑌‘2))↑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)))))))) |
| 56 | 8, 55 | mpbird 257 |
. 2
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ∃!𝑠 ∈ 𝒫
ℝ((♯‘𝑠) =
2 ∧ ∀𝑦 ∈
𝑠 ((((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) · (𝑦↑2)) + ((-(2 ·
(((𝑌‘1) −
(𝑋‘1)) ·
(((𝑋‘2) ·
(𝑌‘1)) −
((𝑋‘1) ·
(𝑌‘2))))) ·
𝑦) + (((((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))↑2) − ((((𝑋‘2) − (𝑌‘2))↑2) ·
(𝑅↑2))))) =
0)) |
| 57 | | 0xr 11308 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℝ* |
| 58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ ℝ+
→ 0 ∈ ℝ*) |
| 59 | | pnfxr 11315 |
. . . . . . . . . . . . . . . . . . 19
⊢ +∞
∈ ℝ* |
| 60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ ℝ+
→ +∞ ∈ ℝ*) |
| 61 | | rpxr 13044 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ*) |
| 62 | | rpge0 13048 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ ℝ+
→ 0 ≤ 𝑅) |
| 63 | | ltpnf 13162 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ ℝ → 𝑅 < +∞) |
| 64 | 48, 63 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ ℝ+
→ 𝑅 <
+∞) |
| 65 | 58, 60, 61, 62, 64 | elicod 13437 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
(0[,)+∞)) |
| 66 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)} = {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)} |
| 67 | 1, 2, 3, 4, 5, 66 | 2sphere0 48671 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ (0[,)+∞) → (
0 𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)}) |
| 68 | 65, 67 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ ℝ+
→ ( 0 𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)}) |
| 69 | 68 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ ℝ+
∧ (𝑋𝐷 0 ) < 𝑅) → ( 0 𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)}) |
| 70 | 69 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ( 0 𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)}) |
| 71 | 70 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) → ( 0 𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)}) |
| 72 | 71 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
→ ( 0 𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)}) |
| 73 | 72 | adantr 480 |
. . . . . . . . . . 11
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → ( 0 𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)}) |
| 74 | 73 | adantr 480 |
. . . . . . . . . 10
⊢
(((((((𝑋 ∈
𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → ( 0 𝑆𝑅) = {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)}) |
| 75 | 74 | eleq2d 2827 |
. . . . . . . . 9
⊢
(((((((𝑋 ∈
𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → (𝑍 ∈ ( 0 𝑆𝑅) ↔ 𝑍 ∈ {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)})) |
| 76 | | fveq1 6905 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑍 → (𝑝‘1) = (𝑍‘1)) |
| 77 | | itscnhlinecirc02p.z |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑍 = {〈1, 𝑥〉, 〈2, 𝑦〉} |
| 78 | 77 | fveq1i 6907 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑍‘1) = ({〈1, 𝑥〉, 〈2, 𝑦〉}‘1) |
| 79 | | 1ne2 12474 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ≠
2 |
| 80 | | 1ex 11257 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
V |
| 81 | | vex 3484 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑥 ∈ V |
| 82 | 80, 81 | fvpr1 7212 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ≠ 2
→ ({〈1, 𝑥〉,
〈2, 𝑦〉}‘1)
= 𝑥) |
| 83 | 79, 82 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
({〈1, 𝑥〉,
〈2, 𝑦〉}‘1)
= 𝑥 |
| 84 | 78, 83 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
⊢ (𝑍‘1) = 𝑥 |
| 85 | 84 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑍 → (𝑍‘1) = 𝑥) |
| 86 | 76, 85 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑍 → (𝑝‘1) = 𝑥) |
| 87 | 86 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑍 → ((𝑝‘1)↑2) = (𝑥↑2)) |
| 88 | | fveq1 6905 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑍 → (𝑝‘2) = (𝑍‘2)) |
| 89 | 77 | fveq1i 6907 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑍‘2) = ({〈1, 𝑥〉, 〈2, 𝑦〉}‘2) |
| 90 | | 2ex 12343 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
V |
| 91 | | vex 3484 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑦 ∈ V |
| 92 | 90, 91 | fvpr2 7213 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ≠ 2
→ ({〈1, 𝑥〉,
〈2, 𝑦〉}‘2)
= 𝑦) |
| 93 | 79, 92 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
({〈1, 𝑥〉,
〈2, 𝑦〉}‘2)
= 𝑦 |
| 94 | 89, 93 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
⊢ (𝑍‘2) = 𝑦 |
| 95 | 94 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑍 → (𝑍‘2) = 𝑦) |
| 96 | 88, 95 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑍 → (𝑝‘2) = 𝑦) |
| 97 | 96 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑍 → ((𝑝‘2)↑2) = (𝑦↑2)) |
| 98 | 87, 97 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑍 → (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = ((𝑥↑2) + (𝑦↑2))) |
| 99 | 98 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑍 → ((((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2) ↔ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2))) |
| 100 | 99 | elrab 3692 |
. . . . . . . . . 10
⊢ (𝑍 ∈ {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)} ↔ (𝑍 ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2))) |
| 101 | 100 | a1i 11 |
. . . . . . . . 9
⊢
(((((((𝑋 ∈
𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → (𝑍 ∈ {𝑝 ∈ 𝑃 ∣ (((𝑝‘1)↑2) + ((𝑝‘2)↑2)) = (𝑅↑2)} ↔ (𝑍 ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)))) |
| 102 | 75, 101 | bitrd 279 |
. . . . . . . 8
⊢
(((((((𝑋 ∈
𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → (𝑍 ∈ ( 0 𝑆𝑅) ↔ (𝑍 ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)))) |
| 103 | | simp1 1137 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → 𝑋 ∈ 𝑃) |
| 104 | | simp2 1138 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → 𝑌 ∈ 𝑃) |
| 105 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑋 = 𝑌 → (𝑋‘2) = (𝑌‘2)) |
| 106 | 105 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋 = 𝑌 → (𝑋‘2) = (𝑌‘2))) |
| 107 | 106 | necon3d 2961 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑋‘2) ≠ (𝑌‘2) → 𝑋 ≠ 𝑌)) |
| 108 | 107 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑋 ∈ 𝑃 → (𝑌 ∈ 𝑃 → ((𝑋‘2) ≠ (𝑌‘2) → 𝑋 ≠ 𝑌))) |
| 109 | 108 | 3imp 1111 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → 𝑋 ≠ 𝑌) |
| 110 | 103, 104,
109 | 3jca 1129 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) |
| 111 | 110 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) |
| 112 | 111 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) |
| 113 | 112 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
→ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) |
| 114 | 113 | adantr 480 |
. . . . . . . . . . . 12
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) |
| 115 | 114 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((((𝑋 ∈
𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌)) |
| 116 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ((𝑋‘2) − (𝑌‘2)) = ((𝑋‘2) − (𝑌‘2)) |
| 117 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ((𝑌‘1) − (𝑋‘1)) = ((𝑌‘1) − (𝑋‘1)) |
| 118 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) |
| 119 | 1, 2, 3, 6, 116, 117, 118 | rrx2linest2 48665 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ((((𝑋‘2) − (𝑌‘2)) · (𝑝‘1)) + (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2))) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))}) |
| 120 | 115, 119 | syl 17 |
. . . . . . . . . 10
⊢
(((((((𝑋 ∈
𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ((((𝑋‘2) − (𝑌‘2)) · (𝑝‘1)) + (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2))) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))}) |
| 121 | 120 | eleq2d 2827 |
. . . . . . . . 9
⊢
(((((((𝑋 ∈
𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → (𝑍 ∈ (𝑋𝐿𝑌) ↔ 𝑍 ∈ {𝑝 ∈ 𝑃 ∣ ((((𝑋‘2) − (𝑌‘2)) · (𝑝‘1)) + (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2))) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))})) |
| 122 | 86 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑍 → (((𝑋‘2) − (𝑌‘2)) · (𝑝‘1)) = (((𝑋‘2) − (𝑌‘2)) · 𝑥)) |
| 123 | 96 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑍 → (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2)) = (((𝑌‘1) − (𝑋‘1)) · 𝑦)) |
| 124 | 122, 123 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑍 → ((((𝑋‘2) − (𝑌‘2)) · (𝑝‘1)) + (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2))) = ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦))) |
| 125 | 124 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑍 → (((((𝑋‘2) − (𝑌‘2)) · (𝑝‘1)) + (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2))) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ↔ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) |
| 126 | 125 | elrab 3692 |
. . . . . . . . . 10
⊢ (𝑍 ∈ {𝑝 ∈ 𝑃 ∣ ((((𝑋‘2) − (𝑌‘2)) · (𝑝‘1)) + (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2))) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))} ↔ (𝑍 ∈ 𝑃 ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) |
| 127 | 126 | a1i 11 |
. . . . . . . . 9
⊢
(((((((𝑋 ∈
𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → (𝑍 ∈ {𝑝 ∈ 𝑃 ∣ ((((𝑋‘2) − (𝑌‘2)) · (𝑝‘1)) + (((𝑌‘1) − (𝑋‘1)) · (𝑝‘2))) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))} ↔ (𝑍 ∈ 𝑃 ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))))) |
| 128 | 121, 127 | bitrd 279 |
. . . . . . . 8
⊢
(((((((𝑋 ∈
𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → (𝑍 ∈ (𝑋𝐿𝑌) ↔ (𝑍 ∈ 𝑃 ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))))) |
| 129 | 102, 128 | anbi12d 632 |
. . . . . . 7
⊢
(((((((𝑋 ∈
𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) ∧ 𝑥 ∈ ℝ) → ((𝑍 ∈ ( 0 𝑆𝑅) ∧ 𝑍 ∈ (𝑋𝐿𝑌)) ↔ ((𝑍 ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (𝑍 ∈ 𝑃 ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))))) |
| 130 | 129 | reubidva 3396 |
. . . . . 6
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → (∃!𝑥 ∈ ℝ (𝑍 ∈ ( 0 𝑆𝑅) ∧ 𝑍 ∈ (𝑋𝐿𝑌)) ↔ ∃!𝑥 ∈ ℝ ((𝑍 ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (𝑍 ∈ 𝑃 ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))))) |
| 131 | | elelpwi 4610 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝑠 ∧ 𝑠 ∈ 𝒫 ℝ) → 𝑦 ∈
ℝ) |
| 132 | 1, 3 | prelrrx2 48634 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
{〈1, 𝑥〉, 〈2,
𝑦〉} ∈ 𝑃) |
| 133 | 132 | ancoms 458 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) →
{〈1, 𝑥〉, 〈2,
𝑦〉} ∈ 𝑃) |
| 134 | 77 | eleq1i 2832 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑍 ∈ 𝑃 ↔ {〈1, 𝑥〉, 〈2, 𝑦〉} ∈ 𝑃) |
| 135 | 133, 134 | sylibr 234 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → 𝑍 ∈ 𝑃) |
| 136 | 135 | biantrurd 532 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ↔ (𝑍 ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)))) |
| 137 | 136 | bicomd 223 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑍 ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ↔ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2))) |
| 138 | 135 | biantrurd 532 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) →
(((((𝑋‘2) −
(𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ↔ (𝑍 ∈ 𝑃 ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))))) |
| 139 | 138 | bicomd 223 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑍 ∈ 𝑃 ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) ↔ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) |
| 140 | 137, 139 | anbi12d 632 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((𝑍 ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (𝑍 ∈ 𝑃 ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))))) |
| 141 | 140 | reubidva 3396 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ →
(∃!𝑥 ∈ ℝ
((𝑍 ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (𝑍 ∈ 𝑃 ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ ∃!𝑥 ∈ ℝ (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))))) |
| 142 | 131, 141 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑠 ∧ 𝑠 ∈ 𝒫 ℝ) →
(∃!𝑥 ∈ ℝ
((𝑍 ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (𝑍 ∈ 𝑃 ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ ∃!𝑥 ∈ ℝ (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))))) |
| 143 | 142 | expcom 413 |
. . . . . . . . . 10
⊢ (𝑠 ∈ 𝒫 ℝ →
(𝑦 ∈ 𝑠 → (∃!𝑥 ∈ ℝ ((𝑍 ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (𝑍 ∈ 𝑃 ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ ∃!𝑥 ∈ ℝ (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))))) |
| 144 | 143 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) → (𝑦 ∈ 𝑠 → (∃!𝑥 ∈ ℝ ((𝑍 ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (𝑍 ∈ 𝑃 ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ ∃!𝑥 ∈ ℝ (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))))) |
| 145 | 144 | adantr 480 |
. . . . . . . 8
⊢
(((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
→ (𝑦 ∈ 𝑠 → (∃!𝑥 ∈ ℝ ((𝑍 ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (𝑍 ∈ 𝑃 ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ ∃!𝑥 ∈ ℝ (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))))) |
| 146 | 145 | imp 406 |
. . . . . . 7
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → (∃!𝑥 ∈ ℝ ((𝑍 ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (𝑍 ∈ 𝑃 ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ ∃!𝑥 ∈ ℝ (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))))) |
| 147 | 26, 33 | jca 511 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) → (((𝑋‘2) − (𝑌‘2)) ∈ ℝ ∧ ((𝑋‘2) − (𝑌‘2)) ≠
0)) |
| 148 | 147 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (((𝑋‘2) − (𝑌‘2)) ∈ ℝ ∧ ((𝑋‘2) − (𝑌‘2)) ≠
0)) |
| 149 | 148 | ad3antrrr 730 |
. . . . . . . . . 10
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → (((𝑋‘2) − (𝑌‘2)) ∈ ℝ ∧ ((𝑋‘2) − (𝑌‘2)) ≠
0)) |
| 150 | 19 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → (𝑌‘1) ∈ ℝ) |
| 151 | 22 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → (𝑋‘1) ∈ ℝ) |
| 152 | 150, 151 | resubcld 11691 |
. . . . . . . . . 10
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → ((𝑌‘1) − (𝑋‘1)) ∈ ℝ) |
| 153 | 11 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → (𝑋‘2) ∈ ℝ) |
| 154 | 153, 150 | remulcld 11291 |
. . . . . . . . . . 11
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → ((𝑋‘2) · (𝑌‘1)) ∈ ℝ) |
| 155 | 14 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → (𝑌‘2) ∈ ℝ) |
| 156 | 151, 155 | remulcld 11291 |
. . . . . . . . . . 11
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → ((𝑋‘1) · (𝑌‘2)) ∈ ℝ) |
| 157 | 154, 156 | resubcld 11691 |
. . . . . . . . . 10
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ∈ ℝ) |
| 158 | 149, 152,
157 | 3jca 1129 |
. . . . . . . . 9
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → ((((𝑋‘2) − (𝑌‘2)) ∈ ℝ ∧ ((𝑋‘2) − (𝑌‘2)) ≠ 0) ∧ ((𝑌‘1) − (𝑋‘1)) ∈ ℝ ∧
(((𝑋‘2) ·
(𝑌‘1)) −
((𝑋‘1) ·
(𝑌‘2))) ∈
ℝ)) |
| 159 | | simplrl 777 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) → 𝑅 ∈
ℝ+) |
| 160 | 159 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
→ 𝑅 ∈
ℝ+) |
| 161 | 160 | adantr 480 |
. . . . . . . . 9
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → 𝑅 ∈
ℝ+) |
| 162 | 131 | expcom 413 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ 𝒫 ℝ →
(𝑦 ∈ 𝑠 → 𝑦 ∈ ℝ)) |
| 163 | 162 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) → (𝑦 ∈ 𝑠 → 𝑦 ∈ ℝ)) |
| 164 | 163 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
→ (𝑦 ∈ 𝑠 → 𝑦 ∈ ℝ)) |
| 165 | 164 | imp 406 |
. . . . . . . . 9
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → 𝑦 ∈ ℝ) |
| 166 | 158, 161,
165 | 3jca 1129 |
. . . . . . . 8
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → (((((𝑋‘2) − (𝑌‘2)) ∈ ℝ ∧ ((𝑋‘2) − (𝑌‘2)) ≠ 0) ∧ ((𝑌‘1) − (𝑋‘1)) ∈ ℝ ∧
(((𝑋‘2) ·
(𝑌‘1)) −
((𝑋‘1) ·
(𝑌‘2))) ∈
ℝ) ∧ 𝑅 ∈
ℝ+ ∧ 𝑦
∈ ℝ)) |
| 167 | | eqid 2737 |
. . . . . . . . 9
⊢ ((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) = ((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) |
| 168 | | eqid 2737 |
. . . . . . . . 9
⊢ -(2
· (((𝑌‘1)
− (𝑋‘1))
· (((𝑋‘2)
· (𝑌‘1))
− ((𝑋‘1)
· (𝑌‘2))))) =
-(2 · (((𝑌‘1)
− (𝑋‘1))
· (((𝑋‘2)
· (𝑌‘1))
− ((𝑋‘1)
· (𝑌‘2))))) |
| 169 | | eqid 2737 |
. . . . . . . . 9
⊢
(((((𝑋‘2)
· (𝑌‘1))
− ((𝑋‘1)
· (𝑌‘2)))↑2) − ((((𝑋‘2) − (𝑌‘2))↑2) ·
(𝑅↑2))) = (((((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))↑2) −
((((𝑋‘2) −
(𝑌‘2))↑2)
· (𝑅↑2))) |
| 170 | 167, 168,
169 | itsclquadeu 48698 |
. . . . . . . 8
⊢
((((((𝑋‘2)
− (𝑌‘2)) ∈
ℝ ∧ ((𝑋‘2)
− (𝑌‘2)) ≠
0) ∧ ((𝑌‘1)
− (𝑋‘1)) ∈
ℝ ∧ (((𝑋‘2)
· (𝑌‘1))
− ((𝑋‘1)
· (𝑌‘2)))
∈ ℝ) ∧ 𝑅
∈ ℝ+ ∧ 𝑦 ∈ ℝ) → (∃!𝑥 ∈ ℝ (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) ↔ ((((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) · (𝑦↑2)) + ((-(2 ·
(((𝑌‘1) −
(𝑋‘1)) ·
(((𝑋‘2) ·
(𝑌‘1)) −
((𝑋‘1) ·
(𝑌‘2))))) ·
𝑦) + (((((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))↑2) − ((((𝑋‘2) − (𝑌‘2))↑2) ·
(𝑅↑2))))) =
0)) |
| 171 | 166, 170 | syl 17 |
. . . . . . 7
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → (∃!𝑥 ∈ ℝ (((𝑥↑2) + (𝑦↑2)) = (𝑅↑2) ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))) ↔ ((((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) · (𝑦↑2)) + ((-(2 ·
(((𝑌‘1) −
(𝑋‘1)) ·
(((𝑋‘2) ·
(𝑌‘1)) −
((𝑋‘1) ·
(𝑌‘2))))) ·
𝑦) + (((((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))↑2) − ((((𝑋‘2) − (𝑌‘2))↑2) ·
(𝑅↑2))))) =
0)) |
| 172 | 146, 171 | bitrd 279 |
. . . . . 6
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → (∃!𝑥 ∈ ℝ ((𝑍 ∈ 𝑃 ∧ ((𝑥↑2) + (𝑦↑2)) = (𝑅↑2)) ∧ (𝑍 ∈ 𝑃 ∧ ((((𝑋‘2) − (𝑌‘2)) · 𝑥) + (((𝑌‘1) − (𝑋‘1)) · 𝑦)) = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))))) ↔ ((((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) · (𝑦↑2)) + ((-(2 ·
(((𝑌‘1) −
(𝑋‘1)) ·
(((𝑋‘2) ·
(𝑌‘1)) −
((𝑋‘1) ·
(𝑌‘2))))) ·
𝑦) + (((((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))↑2) − ((((𝑋‘2) − (𝑌‘2))↑2) ·
(𝑅↑2))))) =
0)) |
| 173 | 130, 172 | bitrd 279 |
. . . . 5
⊢
((((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
∧ 𝑦 ∈ 𝑠) → (∃!𝑥 ∈ ℝ (𝑍 ∈ ( 0 𝑆𝑅) ∧ 𝑍 ∈ (𝑋𝐿𝑌)) ↔ ((((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) · (𝑦↑2)) + ((-(2 ·
(((𝑌‘1) −
(𝑋‘1)) ·
(((𝑋‘2) ·
(𝑌‘1)) −
((𝑋‘1) ·
(𝑌‘2))))) ·
𝑦) + (((((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))↑2) − ((((𝑋‘2) − (𝑌‘2))↑2) ·
(𝑅↑2))))) =
0)) |
| 174 | 173 | ralbidva 3176 |
. . . 4
⊢
(((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) ∧
(♯‘𝑠) = 2)
→ (∀𝑦 ∈
𝑠 ∃!𝑥 ∈ ℝ (𝑍 ∈ ( 0 𝑆𝑅) ∧ 𝑍 ∈ (𝑋𝐿𝑌)) ↔ ∀𝑦 ∈ 𝑠 ((((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) · (𝑦↑2)) + ((-(2 ·
(((𝑌‘1) −
(𝑋‘1)) ·
(((𝑋‘2) ·
(𝑌‘1)) −
((𝑋‘1) ·
(𝑌‘2))))) ·
𝑦) + (((((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))↑2) − ((((𝑋‘2) − (𝑌‘2))↑2) ·
(𝑅↑2))))) =
0)) |
| 175 | 174 | pm5.32da 579 |
. . 3
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) ∧ 𝑠 ∈ 𝒫 ℝ) →
(((♯‘𝑠) = 2
∧ ∀𝑦 ∈
𝑠 ∃!𝑥 ∈ ℝ (𝑍 ∈ ( 0 𝑆𝑅) ∧ 𝑍 ∈ (𝑋𝐿𝑌))) ↔ ((♯‘𝑠) = 2 ∧ ∀𝑦 ∈ 𝑠 ((((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) · (𝑦↑2)) + ((-(2 ·
(((𝑌‘1) −
(𝑋‘1)) ·
(((𝑋‘2) ·
(𝑌‘1)) −
((𝑋‘1) ·
(𝑌‘2))))) ·
𝑦) + (((((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))↑2) − ((((𝑋‘2) − (𝑌‘2))↑2) ·
(𝑅↑2))))) =
0))) |
| 176 | 175 | reubidva 3396 |
. 2
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → (∃!𝑠 ∈ 𝒫
ℝ((♯‘𝑠) =
2 ∧ ∀𝑦 ∈
𝑠 ∃!𝑥 ∈ ℝ (𝑍 ∈ ( 0 𝑆𝑅) ∧ 𝑍 ∈ (𝑋𝐿𝑌))) ↔ ∃!𝑠 ∈ 𝒫
ℝ((♯‘𝑠) =
2 ∧ ∀𝑦 ∈
𝑠 ((((((𝑋‘2) − (𝑌‘2))↑2) + (((𝑌‘1) − (𝑋‘1))↑2)) · (𝑦↑2)) + ((-(2 ·
(((𝑌‘1) −
(𝑋‘1)) ·
(((𝑋‘2) ·
(𝑌‘1)) −
((𝑋‘1) ·
(𝑌‘2))))) ·
𝑦) + (((((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2)))↑2) − ((((𝑋‘2) − (𝑌‘2))↑2) ·
(𝑅↑2))))) =
0))) |
| 177 | 56, 176 | mpbird 257 |
1
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ (𝑋‘2) ≠ (𝑌‘2)) ∧ (𝑅 ∈ ℝ+ ∧ (𝑋𝐷 0 ) < 𝑅)) → ∃!𝑠 ∈ 𝒫
ℝ((♯‘𝑠) =
2 ∧ ∀𝑦 ∈
𝑠 ∃!𝑥 ∈ ℝ (𝑍 ∈ ( 0 𝑆𝑅) ∧ 𝑍 ∈ (𝑋𝐿𝑌)))) |