Step | Hyp | Ref
| Expression |
1 | | simpll 783 |
. . . . . 6
⊢ (((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝑌 ∈ 𝑃) |
2 | | simplr 785 |
. . . . . 6
⊢ (((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝑍 ∈ 𝑃) |
3 | | fveq1 6436 |
. . . . . . . . . . . . . 14
⊢ (𝑌 = 𝑍 → (𝑌‘2) = (𝑍‘2)) |
4 | 3 | oveq1d 6925 |
. . . . . . . . . . . . 13
⊢ (𝑌 = 𝑍 → ((𝑌‘2) − (𝑍‘2)) = ((𝑍‘2) − (𝑍‘2))) |
5 | | itsclc0.i |
. . . . . . . . . . . . . . . 16
⊢ 𝐼 = {1, 2} |
6 | | itsclc0.p |
. . . . . . . . . . . . . . . 16
⊢ 𝑃 = (ℝ
↑𝑚 𝐼) |
7 | 5, 6 | rrx2pyel 42272 |
. . . . . . . . . . . . . . 15
⊢ (𝑍 ∈ 𝑃 → (𝑍‘2) ∈ ℝ) |
8 | | recn 10349 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑍‘2) ∈ ℝ →
(𝑍‘2) ∈
ℂ) |
9 | 8 | subidd 10708 |
. . . . . . . . . . . . . . 15
⊢ ((𝑍‘2) ∈ ℝ →
((𝑍‘2) − (𝑍‘2)) = 0) |
10 | 7, 9 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑍 ∈ 𝑃 → ((𝑍‘2) − (𝑍‘2)) = 0) |
11 | 10 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → ((𝑍‘2) − (𝑍‘2)) = 0) |
12 | 4, 11 | sylan9eqr 2883 |
. . . . . . . . . . . 12
⊢ (((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ 𝑌 = 𝑍) → ((𝑌‘2) − (𝑍‘2)) = 0) |
13 | 12 | ex 403 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (𝑌 = 𝑍 → ((𝑌‘2) − (𝑍‘2)) = 0)) |
14 | | itsclinecirc0.a |
. . . . . . . . . . . 12
⊢ 𝐴 = ((𝑌‘2) − (𝑍‘2)) |
15 | 14 | eqeq1i 2830 |
. . . . . . . . . . 11
⊢ (𝐴 = 0 ↔ ((𝑌‘2) − (𝑍‘2)) = 0) |
16 | 13, 15 | syl6ibr 244 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (𝑌 = 𝑍 → 𝐴 = 0)) |
17 | 16 | necon3d 3020 |
. . . . . . . . 9
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (𝐴 ≠ 0 → 𝑌 ≠ 𝑍)) |
18 | 17 | com12 32 |
. . . . . . . 8
⊢ (𝐴 ≠ 0 → ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → 𝑌 ≠ 𝑍)) |
19 | 18 | 3ad2ant1 1167 |
. . . . . . 7
⊢ ((𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) → ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → 𝑌 ≠ 𝑍)) |
20 | 19 | impcom 398 |
. . . . . 6
⊢ (((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝑌 ≠ 𝑍) |
21 | | itsclc0.e |
. . . . . . 7
⊢ 𝐸 = (ℝ^‘𝐼) |
22 | | itsclinecirc0.l |
. . . . . . 7
⊢ 𝐿 = (LineM‘𝐸) |
23 | | itsclinecirc0.b |
. . . . . . 7
⊢ 𝐵 = ((𝑍‘1) − (𝑌‘1)) |
24 | | eqid 2825 |
. . . . . . 7
⊢ ((𝑍‘2) − (𝑌‘2)) = ((𝑍‘2) − (𝑌‘2)) |
25 | | itsclinecirc0.c |
. . . . . . 7
⊢ 𝐶 = (((𝑌‘2) · (𝑍‘1)) − ((𝑌‘1) · (𝑍‘2))) |
26 | 5, 21, 6, 22, 23, 24, 25 | rrx2linest 43306 |
. . . . . 6
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ∧ 𝑌 ≠ 𝑍) → (𝑌𝐿𝑍) = {𝑝 ∈ 𝑃 ∣ (𝐵 · (𝑝‘2)) = ((((𝑍‘2) − (𝑌‘2)) · (𝑝‘1)) + 𝐶)}) |
27 | 1, 2, 20, 26 | syl3anc 1494 |
. . . . 5
⊢ (((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝑌𝐿𝑍) = {𝑝 ∈ 𝑃 ∣ (𝐵 · (𝑝‘2)) = ((((𝑍‘2) − (𝑌‘2)) · (𝑝‘1)) + 𝐶)}) |
28 | 5, 6 | rrx2pxel 42271 |
. . . . . . . . . . . . . . 15
⊢ (𝑍 ∈ 𝑃 → (𝑍‘1) ∈ ℝ) |
29 | 28 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (𝑍‘1) ∈ ℝ) |
30 | 5, 6 | rrx2pxel 42271 |
. . . . . . . . . . . . . . 15
⊢ (𝑌 ∈ 𝑃 → (𝑌‘1) ∈ ℝ) |
31 | 30 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (𝑌‘1) ∈ ℝ) |
32 | 29, 31 | resubcld 10789 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → ((𝑍‘1) − (𝑌‘1)) ∈ ℝ) |
33 | 23, 32 | syl5eqel 2910 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → 𝐵 ∈ ℝ) |
34 | 33 | ad2antrr 717 |
. . . . . . . . . . 11
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → 𝐵 ∈ ℝ) |
35 | 5, 6 | rrx2pyel 42272 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℝ) |
36 | 35 | adantl 475 |
. . . . . . . . . . 11
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝑝‘2) ∈ ℝ) |
37 | 34, 36 | remulcld 10394 |
. . . . . . . . . 10
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝐵 · (𝑝‘2)) ∈ ℝ) |
38 | 37 | recnd 10392 |
. . . . . . . . 9
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝐵 · (𝑝‘2)) ∈ ℂ) |
39 | 7 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (𝑍‘2) ∈ ℝ) |
40 | 5, 6 | rrx2pyel 42272 |
. . . . . . . . . . . . . 14
⊢ (𝑌 ∈ 𝑃 → (𝑌‘2) ∈ ℝ) |
41 | 40 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (𝑌‘2) ∈ ℝ) |
42 | 39, 41 | resubcld 10789 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → ((𝑍‘2) − (𝑌‘2)) ∈ ℝ) |
43 | 42 | ad2antrr 717 |
. . . . . . . . . . 11
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → ((𝑍‘2) − (𝑌‘2)) ∈ ℝ) |
44 | 5, 6 | rrx2pxel 42271 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℝ) |
45 | 44 | adantl 475 |
. . . . . . . . . . 11
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝑝‘1) ∈ ℝ) |
46 | 43, 45 | remulcld 10394 |
. . . . . . . . . 10
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (((𝑍‘2) − (𝑌‘2)) · (𝑝‘1)) ∈ ℝ) |
47 | 46 | recnd 10392 |
. . . . . . . . 9
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (((𝑍‘2) − (𝑌‘2)) · (𝑝‘1)) ∈ ℂ) |
48 | 41, 29 | remulcld 10394 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → ((𝑌‘2) · (𝑍‘1)) ∈ ℝ) |
49 | 31, 39 | remulcld 10394 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → ((𝑌‘1) · (𝑍‘2)) ∈ ℝ) |
50 | 48, 49 | resubcld 10789 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (((𝑌‘2) · (𝑍‘1)) − ((𝑌‘1) · (𝑍‘2))) ∈ ℝ) |
51 | 25, 50 | syl5eqel 2910 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → 𝐶 ∈ ℝ) |
52 | 51 | recnd 10392 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → 𝐶 ∈ ℂ) |
53 | 52 | ad2antrr 717 |
. . . . . . . . 9
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → 𝐶 ∈ ℂ) |
54 | 38, 47, 53 | subaddd 10738 |
. . . . . . . 8
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (((𝐵 · (𝑝‘2)) − (((𝑍‘2) − (𝑌‘2)) · (𝑝‘1))) = 𝐶 ↔ ((((𝑍‘2) − (𝑌‘2)) · (𝑝‘1)) + 𝐶) = (𝐵 · (𝑝‘2)))) |
55 | | eqcom 2832 |
. . . . . . . 8
⊢ ((𝐵 · (𝑝‘2)) = ((((𝑍‘2) − (𝑌‘2)) · (𝑝‘1)) + 𝐶) ↔ ((((𝑍‘2) − (𝑌‘2)) · (𝑝‘1)) + 𝐶) = (𝐵 · (𝑝‘2))) |
56 | 54, 55 | syl6rbbr 282 |
. . . . . . 7
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → ((𝐵 · (𝑝‘2)) = ((((𝑍‘2) − (𝑌‘2)) · (𝑝‘1)) + 𝐶) ↔ ((𝐵 · (𝑝‘2)) − (((𝑍‘2) − (𝑌‘2)) · (𝑝‘1))) = 𝐶)) |
57 | 41, 39 | resubcld 10789 |
. . . . . . . . . . . . . 14
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → ((𝑌‘2) − (𝑍‘2)) ∈ ℝ) |
58 | 14, 57 | syl5eqel 2910 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → 𝐴 ∈ ℝ) |
59 | 58 | ad2antrr 717 |
. . . . . . . . . . . 12
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → 𝐴 ∈ ℝ) |
60 | 59, 45 | remulcld 10394 |
. . . . . . . . . . 11
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) ∈ ℝ) |
61 | 60 | recnd 10392 |
. . . . . . . . . 10
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) ∈ ℂ) |
62 | 61, 38 | addcomd 10564 |
. . . . . . . . 9
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐵 · (𝑝‘2)) + (𝐴 · (𝑝‘1)))) |
63 | 39 | ad2antrr 717 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝑍‘2) ∈ ℝ) |
64 | 63 | recnd 10392 |
. . . . . . . . . . . . . 14
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝑍‘2) ∈ ℂ) |
65 | 41 | ad2antrr 717 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝑌‘2) ∈ ℝ) |
66 | 65 | recnd 10392 |
. . . . . . . . . . . . . 14
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝑌‘2) ∈ ℂ) |
67 | 64, 66 | negsubdi2d 10736 |
. . . . . . . . . . . . 13
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → -((𝑍‘2) − (𝑌‘2)) = ((𝑌‘2) − (𝑍‘2))) |
68 | 67, 14 | syl6reqr 2880 |
. . . . . . . . . . . 12
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → 𝐴 = -((𝑍‘2) − (𝑌‘2))) |
69 | 68 | oveq1d 6925 |
. . . . . . . . . . 11
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) = (-((𝑍‘2) − (𝑌‘2)) · (𝑝‘1))) |
70 | 42 | recnd 10392 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → ((𝑍‘2) − (𝑌‘2)) ∈ ℂ) |
71 | 70 | ad2antrr 717 |
. . . . . . . . . . . 12
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → ((𝑍‘2) − (𝑌‘2)) ∈ ℂ) |
72 | 45 | recnd 10392 |
. . . . . . . . . . . 12
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝑝‘1) ∈ ℂ) |
73 | 71, 72 | mulneg1d 10814 |
. . . . . . . . . . 11
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (-((𝑍‘2) − (𝑌‘2)) · (𝑝‘1)) = -(((𝑍‘2) − (𝑌‘2)) · (𝑝‘1))) |
74 | 69, 73 | eqtr2d 2862 |
. . . . . . . . . 10
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → -(((𝑍‘2) − (𝑌‘2)) · (𝑝‘1)) = (𝐴 · (𝑝‘1))) |
75 | 74 | oveq2d 6926 |
. . . . . . . . 9
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → ((𝐵 · (𝑝‘2)) + -(((𝑍‘2) − (𝑌‘2)) · (𝑝‘1))) = ((𝐵 · (𝑝‘2)) + (𝐴 · (𝑝‘1)))) |
76 | 38, 47 | negsubd 10726 |
. . . . . . . . 9
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → ((𝐵 · (𝑝‘2)) + -(((𝑍‘2) − (𝑌‘2)) · (𝑝‘1))) = ((𝐵 · (𝑝‘2)) − (((𝑍‘2) − (𝑌‘2)) · (𝑝‘1)))) |
77 | 62, 75, 76 | 3eqtr2rd 2868 |
. . . . . . . 8
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → ((𝐵 · (𝑝‘2)) − (((𝑍‘2) − (𝑌‘2)) · (𝑝‘1))) = ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2)))) |
78 | 77 | eqeq1d 2827 |
. . . . . . 7
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (((𝐵 · (𝑝‘2)) − (((𝑍‘2) − (𝑌‘2)) · (𝑝‘1))) = 𝐶 ↔ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶)) |
79 | 56, 78 | bitrd 271 |
. . . . . 6
⊢ ((((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → ((𝐵 · (𝑝‘2)) = ((((𝑍‘2) − (𝑌‘2)) · (𝑝‘1)) + 𝐶) ↔ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶)) |
80 | 79 | rabbidva 3401 |
. . . . 5
⊢ (((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → {𝑝 ∈ 𝑃 ∣ (𝐵 · (𝑝‘2)) = ((((𝑍‘2) − (𝑌‘2)) · (𝑝‘1)) + 𝐶)} = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}) |
81 | 27, 80 | eqtrd 2861 |
. . . 4
⊢ (((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝑌𝐿𝑍) = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}) |
82 | 81 | eleq2d 2892 |
. . 3
⊢ (((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝑋 ∈ (𝑌𝐿𝑍) ↔ 𝑋 ∈ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶})) |
83 | 82 | anbi2d 622 |
. 2
⊢ (((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝑋 ∈ ( 0 𝑆𝑅) ∧ 𝑋 ∈ (𝑌𝐿𝑍)) ↔ (𝑋 ∈ ( 0 𝑆𝑅) ∧ 𝑋 ∈ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}))) |
84 | | simp1 1170 |
. . . 4
⊢ ((𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) → 𝐴 ≠ 0) |
85 | 58, 84 | anim12i 606 |
. . 3
⊢ (((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝐴 ∈ ℝ ∧ 𝐴 ≠ 0)) |
86 | 33 | adantr 474 |
. . 3
⊢ (((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝐵 ∈
ℝ) |
87 | 51 | adantr 474 |
. . 3
⊢ (((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝐶 ∈
ℝ) |
88 | | simpr2 1254 |
. . 3
⊢ (((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝑅 ∈
ℝ+) |
89 | | simpr3 1256 |
. . 3
⊢ (((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 0 ≤ 𝐷) |
90 | | itsclc0.s |
. . . 4
⊢ 𝑆 = (Sphere‘𝐸) |
91 | | itsclc0.0 |
. . . 4
⊢ 0 = (𝐼 × {0}) |
92 | | itsclc0.q |
. . . 4
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) |
93 | | itsclc0.d |
. . . 4
⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) |
94 | | eqid 2825 |
. . . 4
⊢ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} |
95 | 5, 21, 6, 90, 91, 92, 93, 94 | itsclc0 43323 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷) → ((𝑋 ∈ ( 0 𝑆𝑅) ∧ 𝑋 ∈ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}) → (((𝑋‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑋‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))) |
96 | 85, 86, 87, 88, 89, 95 | syl311anc 1507 |
. 2
⊢ (((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝑋 ∈ ( 0 𝑆𝑅) ∧ 𝑋 ∈ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}) → (((𝑋‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑋‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))) |
97 | 83, 96 | sylbid 232 |
1
⊢ (((𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) ∧ (𝐴 ≠ 0 ∧ 𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝑋 ∈ ( 0 𝑆𝑅) ∧ 𝑋 ∈ (𝑌𝐿𝑍)) → (((𝑋‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑋‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑋‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄))))) |