Step | Hyp | Ref
| Expression |
1 | | itsclinecirc0b.i |
. . . . . . 7
⊢ 𝐼 = {1, 2} |
2 | | itsclinecirc0b.e |
. . . . . . 7
⊢ 𝐸 = (ℝ^‘𝐼) |
3 | | itsclinecirc0b.p |
. . . . . . 7
⊢ 𝑃 = (ℝ ↑m
𝐼) |
4 | | itsclinecirc0b.l |
. . . . . . 7
⊢ 𝐿 = (LineM‘𝐸) |
5 | | itsclinecirc0b.b |
. . . . . . 7
⊢ 𝐵 = ((𝑌‘1) − (𝑋‘1)) |
6 | | eqid 2738 |
. . . . . . 7
⊢ ((𝑌‘2) − (𝑋‘2)) = ((𝑌‘2) − (𝑋‘2)) |
7 | | itsclinecirc0b.c |
. . . . . . 7
⊢ 𝐶 = (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) |
8 | 1, 2, 3, 4, 5, 6, 7 | rrx2linest 46088 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝐵 · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + 𝐶)}) |
9 | 8 | adantr 481 |
. . . . 5
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ (𝐵 · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + 𝐶)}) |
10 | | eqcom 2745 |
. . . . . . . 8
⊢ ((𝐵 · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + 𝐶) ↔ ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + 𝐶) = (𝐵 · (𝑝‘2))) |
11 | 1, 3 | rrx2pxel 46057 |
. . . . . . . . . . . . . . . 16
⊢ (𝑌 ∈ 𝑃 → (𝑌‘1) ∈ ℝ) |
12 | 11 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑌‘1) ∈ ℝ) |
13 | 1, 3 | rrx2pxel 46057 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ 𝑃 → (𝑋‘1) ∈ ℝ) |
14 | 13 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋‘1) ∈ ℝ) |
15 | 12, 14 | resubcld 11403 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑌‘1) − (𝑋‘1)) ∈ ℝ) |
16 | 5, 15 | eqeltrid 2843 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → 𝐵 ∈ ℝ) |
17 | 16 | 3adant3 1131 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝐵 ∈ ℝ) |
18 | 17 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → 𝐵 ∈ ℝ) |
19 | 1, 3 | rrx2pyel 46058 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ 𝑃 → (𝑝‘2) ∈ ℝ) |
20 | 19 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝑝‘2) ∈ ℝ) |
21 | 18, 20 | remulcld 11005 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝐵 · (𝑝‘2)) ∈ ℝ) |
22 | 21 | recnd 11003 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝐵 · (𝑝‘2)) ∈ ℂ) |
23 | 1, 3 | rrx2pyel 46058 |
. . . . . . . . . . . . . . 15
⊢ (𝑌 ∈ 𝑃 → (𝑌‘2) ∈ ℝ) |
24 | 23 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑌‘2) ∈ ℝ) |
25 | 1, 3 | rrx2pyel 46058 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ 𝑃 → (𝑋‘2) ∈ ℝ) |
26 | 25 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (𝑋‘2) ∈ ℝ) |
27 | 24, 26 | resubcld 11403 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑌‘2) − (𝑋‘2)) ∈ ℝ) |
28 | 27 | 3adant3 1131 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → ((𝑌‘2) − (𝑋‘2)) ∈ ℝ) |
29 | 28 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → ((𝑌‘2) − (𝑋‘2)) ∈ ℝ) |
30 | 1, 3 | rrx2pxel 46057 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ 𝑃 → (𝑝‘1) ∈ ℝ) |
31 | 30 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝑝‘1) ∈ ℝ) |
32 | 29, 31 | remulcld 11005 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) ∈ ℝ) |
33 | 32 | recnd 11003 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) ∈ ℂ) |
34 | 26, 12 | remulcld 11005 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑋‘2) · (𝑌‘1)) ∈ ℝ) |
35 | 14, 24 | remulcld 11005 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑋‘1) · (𝑌‘2)) ∈ ℝ) |
36 | 34, 35 | resubcld 11403 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (((𝑋‘2) · (𝑌‘1)) − ((𝑋‘1) · (𝑌‘2))) ∈ ℝ) |
37 | 7, 36 | eqeltrid 2843 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → 𝐶 ∈ ℝ) |
38 | 37 | recnd 11003 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → 𝐶 ∈ ℂ) |
39 | 38 | 3adant3 1131 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝐶 ∈ ℂ) |
40 | 39 | ad2antrr 723 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → 𝐶 ∈ ℂ) |
41 | 22, 33, 40 | subaddd 11350 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (((𝐵 · (𝑝‘2)) − (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1))) = 𝐶 ↔ ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + 𝐶) = (𝐵 · (𝑝‘2)))) |
42 | 10, 41 | bitr4id 290 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → ((𝐵 · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + 𝐶) ↔ ((𝐵 · (𝑝‘2)) − (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1))) = 𝐶)) |
43 | | itsclinecirc0b.a |
. . . . . . . . . . . . . . 15
⊢ 𝐴 = ((𝑋‘2) − (𝑌‘2)) |
44 | 26, 24 | resubcld 11403 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑋‘2) − (𝑌‘2)) ∈ ℝ) |
45 | 43, 44 | eqeltrid 2843 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → 𝐴 ∈ ℝ) |
46 | 45 | 3adant3 1131 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝐴 ∈ ℝ) |
47 | 46 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → 𝐴 ∈ ℝ) |
48 | 47, 31 | remulcld 11005 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) ∈ ℝ) |
49 | 48 | recnd 11003 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) ∈ ℂ) |
50 | 49, 22 | addcomd 11177 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐵 · (𝑝‘2)) + (𝐴 · (𝑝‘1)))) |
51 | 24 | 3adant3 1131 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑌‘2) ∈ ℝ) |
52 | 51 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝑌‘2) ∈ ℝ) |
53 | 52 | recnd 11003 |
. . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝑌‘2) ∈ ℂ) |
54 | 26 | 3adant3 1131 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝑋‘2) ∈ ℝ) |
55 | 54 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝑋‘2) ∈ ℝ) |
56 | 55 | recnd 11003 |
. . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝑋‘2) ∈ ℂ) |
57 | 53, 56 | negsubdi2d 11348 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → -((𝑌‘2) − (𝑋‘2)) = ((𝑋‘2) − (𝑌‘2))) |
58 | 43, 57 | eqtr4id 2797 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → 𝐴 = -((𝑌‘2) − (𝑋‘2))) |
59 | 58 | oveq1d 7290 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝐴 · (𝑝‘1)) = (-((𝑌‘2) − (𝑋‘2)) · (𝑝‘1))) |
60 | 27 | recnd 11003 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑌‘2) − (𝑋‘2)) ∈ ℂ) |
61 | 60 | 3adant3 1131 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → ((𝑌‘2) − (𝑋‘2)) ∈ ℂ) |
62 | 61 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → ((𝑌‘2) − (𝑋‘2)) ∈ ℂ) |
63 | 31 | recnd 11003 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (𝑝‘1) ∈ ℂ) |
64 | 62, 63 | mulneg1d 11428 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (-((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) = -(((𝑌‘2) − (𝑋‘2)) · (𝑝‘1))) |
65 | 59, 64 | eqtr2d 2779 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → -(((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) = (𝐴 · (𝑝‘1))) |
66 | 65 | oveq2d 7291 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → ((𝐵 · (𝑝‘2)) + -(((𝑌‘2) − (𝑋‘2)) · (𝑝‘1))) = ((𝐵 · (𝑝‘2)) + (𝐴 · (𝑝‘1)))) |
67 | 22, 33 | negsubd 11338 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → ((𝐵 · (𝑝‘2)) + -(((𝑌‘2) − (𝑋‘2)) · (𝑝‘1))) = ((𝐵 · (𝑝‘2)) − (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)))) |
68 | 50, 66, 67 | 3eqtr2rd 2785 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → ((𝐵 · (𝑝‘2)) − (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1))) = ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2)))) |
69 | 68 | eqeq1d 2740 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → (((𝐵 · (𝑝‘2)) − (((𝑌‘2) − (𝑋‘2)) · (𝑝‘1))) = 𝐶 ↔ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶)) |
70 | 42, 69 | bitrd 278 |
. . . . . 6
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) ∧ 𝑝 ∈ 𝑃) → ((𝐵 · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + 𝐶) ↔ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶)) |
71 | 70 | rabbidva 3413 |
. . . . 5
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → {𝑝 ∈ 𝑃 ∣ (𝐵 · (𝑝‘2)) = ((((𝑌‘2) − (𝑋‘2)) · (𝑝‘1)) + 𝐶)} = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}) |
72 | 9, 71 | eqtrd 2778 |
. . . 4
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝑋𝐿𝑌) = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}) |
73 | 72 | eleq2d 2824 |
. . 3
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝑍 ∈ (𝑋𝐿𝑌) ↔ 𝑍 ∈ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶})) |
74 | 73 | anbi2d 629 |
. 2
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝑍 ∈ ( 0 𝑆𝑅) ∧ 𝑍 ∈ (𝑋𝐿𝑌)) ↔ (𝑍 ∈ ( 0 𝑆𝑅) ∧ 𝑍 ∈ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}))) |
75 | 46 | adantr 481 |
. . 3
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝐴 ∈
ℝ) |
76 | 17 | adantr 481 |
. . 3
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝐵 ∈
ℝ) |
77 | 37 | 3adant3 1131 |
. . . 4
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → 𝐶 ∈ ℝ) |
78 | 77 | adantr 481 |
. . 3
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → 𝐶 ∈
ℝ) |
79 | 1, 3, 5, 43 | rrx2pnedifcoorneorr 46063 |
. . . . 5
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝐵 ≠ 0 ∨ 𝐴 ≠ 0)) |
80 | 79 | orcomd 868 |
. . . 4
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) |
81 | 80 | adantr 481 |
. . 3
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) |
82 | | simpr 485 |
. . 3
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → (𝑅 ∈ ℝ+
∧ 0 ≤ 𝐷)) |
83 | | itsclinecirc0b.s |
. . . 4
⊢ 𝑆 = (Sphere‘𝐸) |
84 | | itsclinecirc0b.0 |
. . . 4
⊢ 0 = (𝐼 × {0}) |
85 | | itsclinecirc0b.q |
. . . 4
⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2)) |
86 | | itsclinecirc0b.d |
. . . 4
⊢ 𝐷 = (((𝑅↑2) · 𝑄) − (𝐶↑2)) |
87 | | eqid 2738 |
. . . 4
⊢ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} = {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶} |
88 | 1, 2, 3, 83, 84, 85, 86, 87 | itsclc0b 46118 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝑍 ∈ ( 0 𝑆𝑅) ∧ 𝑍 ∈ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}) ↔ (𝑍 ∈ 𝑃 ∧ (((𝑍‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑍‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑍‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑍‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))) |
89 | 75, 76, 78, 81, 82, 88 | syl311anc 1383 |
. 2
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝑍 ∈ ( 0 𝑆𝑅) ∧ 𝑍 ∈ {𝑝 ∈ 𝑃 ∣ ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶}) ↔ (𝑍 ∈ 𝑃 ∧ (((𝑍‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑍‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑍‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑍‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))) |
90 | 74, 89 | bitrd 278 |
1
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌) ∧ (𝑅 ∈ ℝ+ ∧ 0 ≤
𝐷)) → ((𝑍 ∈ ( 0 𝑆𝑅) ∧ 𝑍 ∈ (𝑋𝐿𝑌)) ↔ (𝑍 ∈ 𝑃 ∧ (((𝑍‘1) = (((𝐴 · 𝐶) + (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑍‘2) = (((𝐵 · 𝐶) − (𝐴 · (√‘𝐷))) / 𝑄)) ∨ ((𝑍‘1) = (((𝐴 · 𝐶) − (𝐵 · (√‘𝐷))) / 𝑄) ∧ (𝑍‘2) = (((𝐵 · 𝐶) + (𝐴 · (√‘𝐷))) / 𝑄)))))) |