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 2733 |
. . . . . . 7
β’ ((πβ2) β (πβ2)) = ((πβ2) β (πβ2)) |
7 | | itsclinecirc0b.c |
. . . . . . 7
β’ πΆ = (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2))) |
8 | 1, 2, 3, 4, 5, 6, 7 | rrx2linest 46918 |
. . . . . 6
β’ ((π β π β§ π β π β§ π β π) β (ππΏπ) = {π β π β£ (π΅ Β· (πβ2)) = ((((πβ2) β (πβ2)) Β· (πβ1)) + πΆ)}) |
9 | 8 | adantr 482 |
. . . . 5
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (ππΏπ) = {π β π β£ (π΅ Β· (πβ2)) = ((((πβ2) β (πβ2)) Β· (πβ1)) + πΆ)}) |
10 | | eqcom 2740 |
. . . . . . . 8
β’ ((π΅ Β· (πβ2)) = ((((πβ2) β (πβ2)) Β· (πβ1)) + πΆ) β ((((πβ2) β (πβ2)) Β· (πβ1)) + πΆ) = (π΅ Β· (πβ2))) |
11 | 1, 3 | rrx2pxel 46887 |
. . . . . . . . . . . . . . . 16
β’ (π β π β (πβ1) β β) |
12 | 11 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π β π) β (πβ1) β β) |
13 | 1, 3 | rrx2pxel 46887 |
. . . . . . . . . . . . . . . 16
β’ (π β π β (πβ1) β β) |
14 | 13 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π β π) β (πβ1) β β) |
15 | 12, 14 | resubcld 11591 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β π) β ((πβ1) β (πβ1)) β β) |
16 | 5, 15 | eqeltrid 2838 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β π) β π΅ β β) |
17 | 16 | 3adant3 1133 |
. . . . . . . . . . . 12
β’ ((π β π β§ π β π β§ π β π) β π΅ β β) |
18 | 17 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β π΅ β β) |
19 | 1, 3 | rrx2pyel 46888 |
. . . . . . . . . . . 12
β’ (π β π β (πβ2) β β) |
20 | 19 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (πβ2) β β) |
21 | 18, 20 | remulcld 11193 |
. . . . . . . . . 10
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (π΅ Β· (πβ2)) β β) |
22 | 21 | recnd 11191 |
. . . . . . . . 9
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (π΅ Β· (πβ2)) β β) |
23 | 1, 3 | rrx2pyel 46888 |
. . . . . . . . . . . . . . 15
β’ (π β π β (πβ2) β β) |
24 | 23 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β π) β (πβ2) β β) |
25 | 1, 3 | rrx2pyel 46888 |
. . . . . . . . . . . . . . 15
β’ (π β π β (πβ2) β β) |
26 | 25 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β π) β (πβ2) β β) |
27 | 24, 26 | resubcld 11591 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β π) β ((πβ2) β (πβ2)) β β) |
28 | 27 | 3adant3 1133 |
. . . . . . . . . . . 12
β’ ((π β π β§ π β π β§ π β π) β ((πβ2) β (πβ2)) β β) |
29 | 28 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β ((πβ2) β (πβ2)) β β) |
30 | 1, 3 | rrx2pxel 46887 |
. . . . . . . . . . . 12
β’ (π β π β (πβ1) β β) |
31 | 30 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (πβ1) β β) |
32 | 29, 31 | remulcld 11193 |
. . . . . . . . . 10
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (((πβ2) β (πβ2)) Β· (πβ1)) β β) |
33 | 32 | recnd 11191 |
. . . . . . . . 9
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (((πβ2) β (πβ2)) Β· (πβ1)) β β) |
34 | 26, 12 | remulcld 11193 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β π) β ((πβ2) Β· (πβ1)) β β) |
35 | 14, 24 | remulcld 11193 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β π) β ((πβ1) Β· (πβ2)) β β) |
36 | 34, 35 | resubcld 11591 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β π) β (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2))) β β) |
37 | 7, 36 | eqeltrid 2838 |
. . . . . . . . . . . 12
β’ ((π β π β§ π β π) β πΆ β β) |
38 | 37 | recnd 11191 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β πΆ β β) |
39 | 38 | 3adant3 1133 |
. . . . . . . . . 10
β’ ((π β π β§ π β π β§ π β π) β πΆ β β) |
40 | 39 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β πΆ β β) |
41 | 22, 33, 40 | subaddd 11538 |
. . . . . . . 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 11591 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π β π) β ((πβ2) β (πβ2)) β β) |
45 | 43, 44 | eqeltrid 2838 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β π) β π΄ β β) |
46 | 45 | 3adant3 1133 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β π β§ π β π) β π΄ β β) |
47 | 46 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β π΄ β β) |
48 | 47, 31 | remulcld 11193 |
. . . . . . . . . . 11
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (π΄ Β· (πβ1)) β β) |
49 | 48 | recnd 11191 |
. . . . . . . . . 10
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (π΄ Β· (πβ1)) β β) |
50 | 49, 22 | addcomd 11365 |
. . . . . . . . 9
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = ((π΅ Β· (πβ2)) + (π΄ Β· (πβ1)))) |
51 | 24 | 3adant3 1133 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ π β π β§ π β π) β (πβ2) β β) |
52 | 51 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (πβ2) β β) |
53 | 52 | recnd 11191 |
. . . . . . . . . . . . . 14
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (πβ2) β β) |
54 | 26 | 3adant3 1133 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ π β π β§ π β π) β (πβ2) β β) |
55 | 54 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (πβ2) β β) |
56 | 55 | recnd 11191 |
. . . . . . . . . . . . . 14
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (πβ2) β β) |
57 | 53, 56 | negsubdi2d 11536 |
. . . . . . . . . . . . 13
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β -((πβ2) β (πβ2)) = ((πβ2) β (πβ2))) |
58 | 43, 57 | eqtr4id 2792 |
. . . . . . . . . . . 12
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β π΄ = -((πβ2) β (πβ2))) |
59 | 58 | oveq1d 7376 |
. . . . . . . . . . 11
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (π΄ Β· (πβ1)) = (-((πβ2) β (πβ2)) Β· (πβ1))) |
60 | 27 | recnd 11191 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β π) β ((πβ2) β (πβ2)) β β) |
61 | 60 | 3adant3 1133 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β π β§ π β π) β ((πβ2) β (πβ2)) β β) |
62 | 61 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β ((πβ2) β (πβ2)) β β) |
63 | 31 | recnd 11191 |
. . . . . . . . . . . 12
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (πβ1) β β) |
64 | 62, 63 | mulneg1d 11616 |
. . . . . . . . . . 11
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (-((πβ2) β (πβ2)) Β· (πβ1)) = -(((πβ2) β (πβ2)) Β· (πβ1))) |
65 | 59, 64 | eqtr2d 2774 |
. . . . . . . . . 10
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β -(((πβ2) β (πβ2)) Β· (πβ1)) = (π΄ Β· (πβ1))) |
66 | 65 | oveq2d 7377 |
. . . . . . . . 9
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β ((π΅ Β· (πβ2)) + -(((πβ2) β (πβ2)) Β· (πβ1))) = ((π΅ Β· (πβ2)) + (π΄ Β· (πβ1)))) |
67 | 22, 33 | negsubd 11526 |
. . . . . . . . 9
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β ((π΅ Β· (πβ2)) + -(((πβ2) β (πβ2)) Β· (πβ1))) = ((π΅ Β· (πβ2)) β (((πβ2) β (πβ2)) Β· (πβ1)))) |
68 | 50, 66, 67 | 3eqtr2rd 2780 |
. . . . . . . 8
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β ((π΅ Β· (πβ2)) β (((πβ2) β (πβ2)) Β· (πβ1))) = ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2)))) |
69 | 68 | eqeq1d 2735 |
. . . . . . 7
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (((π΅ Β· (πβ2)) β (((πβ2) β (πβ2)) Β· (πβ1))) = πΆ β ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ)) |
70 | 42, 69 | bitrd 279 |
. . . . . 6
β’ ((((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β ((π΅ Β· (πβ2)) = ((((πβ2) β (πβ2)) Β· (πβ1)) + πΆ) β ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ)) |
71 | 70 | rabbidva 3413 |
. . . . 5
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β {π β π β£ (π΅ Β· (πβ2)) = ((((πβ2) β (πβ2)) Β· (πβ1)) + πΆ)} = {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ}) |
72 | 9, 71 | eqtrd 2773 |
. . . 4
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (ππΏπ) = {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ}) |
73 | 72 | eleq2d 2820 |
. . 3
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (π β (ππΏπ) β π β {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ})) |
74 | 73 | anbi2d 630 |
. 2
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β ((π β ( 0 ππ
) β§ π β (ππΏπ)) β (π β ( 0 ππ
) β§ π β {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ}))) |
75 | 46 | adantr 482 |
. . 3
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β π΄ β
β) |
76 | 17 | adantr 482 |
. . 3
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β π΅ β
β) |
77 | 37 | 3adant3 1133 |
. . . 4
β’ ((π β π β§ π β π β§ π β π) β πΆ β β) |
78 | 77 | adantr 482 |
. . 3
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β πΆ β
β) |
79 | 1, 3, 5, 43 | rrx2pnedifcoorneorr 46893 |
. . . . 5
β’ ((π β π β§ π β π β§ π β π) β (π΅ β 0 β¨ π΄ β 0)) |
80 | 79 | orcomd 870 |
. . . 4
β’ ((π β π β§ π β π β§ π β π) β (π΄ β 0 β¨ π΅ β 0)) |
81 | 80 | adantr 482 |
. . 3
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (π΄ β 0 β¨ π΅ β 0)) |
82 | | simpr 486 |
. . 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 2733 |
. . . 4
β’ {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ} = {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ} |
88 | 1, 2, 3, 83, 84, 85, 86, 87 | itsclc0b 46948 |
. . 3
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β ((π β ( 0 ππ
) β§ π β {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ}) β (π β π β§ (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)))))) |
89 | 75, 76, 78, 81, 82, 88 | syl311anc 1385 |
. 2
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β ((π β ( 0 ππ
) β§ π β {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ}) β (π β π β§ (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)))))) |
90 | 74, 89 | bitrd 279 |
1
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β ((π β ( 0 ππ
) β§ π β (ππΏπ)) β (π β π β§ (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)))))) |