Step | Hyp | Ref
| Expression |
1 | | elin 3930 |
. . . 4
β’ (π§ β (( 0 ππ
) β© (ππΏπ)) β (π§ β ( 0 ππ
) β§ π§ β (ππΏπ))) |
2 | | itsclinecirc0b.i |
. . . . 5
β’ πΌ = {1, 2} |
3 | | itsclinecirc0b.e |
. . . . 5
β’ πΈ = (β^βπΌ) |
4 | | itsclinecirc0b.p |
. . . . 5
β’ π = (β βm
πΌ) |
5 | | itsclinecirc0b.s |
. . . . 5
β’ π = (SphereβπΈ) |
6 | | itsclinecirc0b.0 |
. . . . 5
β’ 0 = (πΌ Γ {0}) |
7 | | itsclinecirc0b.q |
. . . . 5
β’ π = ((π΄β2) + (π΅β2)) |
8 | | itsclinecirc0b.d |
. . . . 5
β’ π· = (((π
β2) Β· π) β (πΆβ2)) |
9 | | itsclinecirc0b.l |
. . . . 5
β’ πΏ = (LineMβπΈ) |
10 | | itsclinecirc0b.a |
. . . . 5
β’ π΄ = ((πβ2) β (πβ2)) |
11 | | itsclinecirc0b.b |
. . . . 5
β’ π΅ = ((πβ1) β (πβ1)) |
12 | | itsclinecirc0b.c |
. . . . 5
β’ πΆ = (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2))) |
13 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 | itsclinecirc0b 46950 |
. . . 4
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β ((π§ β ( 0 ππ
) β§ π§ β (ππΏπ)) β (π§ β π β§ (((π§β1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (π§β2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((π§β1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (π§β2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)))))) |
14 | 1, 13 | bitrid 283 |
. . 3
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (π§ β (( 0 ππ
) β© (ππΏπ)) β (π§ β π β§ (((π§β1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (π§β2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((π§β1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (π§β2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)))))) |
15 | 2, 4 | rrx2pyel 46888 |
. . . . . . . . . . 11
β’ (π β π β (πβ2) β β) |
16 | 15 | adantr 482 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β (πβ2) β β) |
17 | 2, 4 | rrx2pyel 46888 |
. . . . . . . . . . 11
β’ (π β π β (πβ2) β β) |
18 | 17 | adantl 483 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β (πβ2) β β) |
19 | 16, 18 | resubcld 11591 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β ((πβ2) β (πβ2)) β β) |
20 | 10, 19 | eqeltrid 2838 |
. . . . . . . 8
β’ ((π β π β§ π β π) β π΄ β β) |
21 | 20 | 3adant3 1133 |
. . . . . . 7
β’ ((π β π β§ π β π β§ π β π) β π΄ β β) |
22 | 21 | adantr 482 |
. . . . . 6
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β π΄ β
β) |
23 | 2, 4 | rrx2pxel 46887 |
. . . . . . . . . . 11
β’ (π β π β (πβ1) β β) |
24 | 23 | adantl 483 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β (πβ1) β β) |
25 | 2, 4 | rrx2pxel 46887 |
. . . . . . . . . . 11
β’ (π β π β (πβ1) β β) |
26 | 25 | adantr 482 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β (πβ1) β β) |
27 | 24, 26 | resubcld 11591 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β ((πβ1) β (πβ1)) β β) |
28 | 11, 27 | eqeltrid 2838 |
. . . . . . . 8
β’ ((π β π β§ π β π) β π΅ β β) |
29 | 28 | 3adant3 1133 |
. . . . . . 7
β’ ((π β π β§ π β π β§ π β π) β π΅ β β) |
30 | 29 | adantr 482 |
. . . . . 6
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β π΅ β
β) |
31 | 16, 24 | remulcld 11193 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β ((πβ2) Β· (πβ1)) β β) |
32 | 26, 18 | remulcld 11193 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β ((πβ1) Β· (πβ2)) β β) |
33 | 31, 32 | resubcld 11591 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2))) β β) |
34 | 12, 33 | eqeltrid 2838 |
. . . . . . . 8
β’ ((π β π β§ π β π) β πΆ β β) |
35 | 34 | 3adant3 1133 |
. . . . . . 7
β’ ((π β π β§ π β π β§ π β π) β πΆ β β) |
36 | 35 | adantr 482 |
. . . . . 6
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β πΆ β
β) |
37 | 22, 30, 36 | 3jca 1129 |
. . . . 5
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (π΄ β β β§ π΅ β β β§ πΆ β
β)) |
38 | 21, 29, 35 | 3jca 1129 |
. . . . . . 7
β’ ((π β π β§ π β π β§ π β π) β (π΄ β β β§ π΅ β β β§ πΆ β β)) |
39 | | rpre 12931 |
. . . . . . . 8
β’ (π
β β+
β π
β
β) |
40 | 39 | adantr 482 |
. . . . . . 7
β’ ((π
β β+
β§ 0 β€ π·) β
π
β
β) |
41 | 7, 8 | itsclc0lem3 46934 |
. . . . . . 7
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π
β β) β π· β
β) |
42 | 38, 40, 41 | syl2an 597 |
. . . . . 6
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β π· β
β) |
43 | | simprr 772 |
. . . . . 6
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β 0 β€ π·) |
44 | 42, 43 | jca 513 |
. . . . 5
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (π· β β β§ 0 β€
π·)) |
45 | 20, 28 | jca 513 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β (π΄ β β β§ π΅ β β)) |
46 | 7 | resum2sqcl 46882 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΅ β β) β π β
β) |
47 | 45, 46 | syl 17 |
. . . . . . . 8
β’ ((π β π β§ π β π) β π β β) |
48 | 47 | 3adant3 1133 |
. . . . . . 7
β’ ((π β π β§ π β π β§ π β π) β π β β) |
49 | 2, 4, 11, 10 | rrx2pnedifcoorneorr 46893 |
. . . . . . . . . 10
β’ ((π β π β§ π β π β§ π β π) β (π΅ β 0 β¨ π΄ β 0)) |
50 | 49 | orcomd 870 |
. . . . . . . . 9
β’ ((π β π β§ π β π β§ π β π) β (π΄ β 0 β¨ π΅ β 0)) |
51 | 7 | resum2sqorgt0 46885 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΅ β β β§ (π΄ β 0 β¨ π΅ β 0)) β 0 < π) |
52 | 21, 29, 50, 51 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β π β§ π β π β§ π β π) β 0 < π) |
53 | 52 | gt0ne0d 11727 |
. . . . . . 7
β’ ((π β π β§ π β π β§ π β π) β π β 0) |
54 | 48, 53 | jca 513 |
. . . . . 6
β’ ((π β π β§ π β π β§ π β π) β (π β β β§ π β 0)) |
55 | 54 | adantr 482 |
. . . . 5
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (π β β β§ π β 0)) |
56 | | itsclc0lem1 46932 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π· β β β§ 0 β€
π·) β§ (π β β β§ π β 0)) β (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β β) |
57 | 37, 44, 55, 56 | syl3anc 1372 |
. . . 4
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β β) |
58 | 30, 22, 36 | 3jca 1129 |
. . . . 5
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (π΅ β β β§ π΄ β β β§ πΆ β
β)) |
59 | 48 | adantr 482 |
. . . . . 6
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β π β
β) |
60 | 53 | adantr 482 |
. . . . . 6
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β π β 0) |
61 | 59, 60 | jca 513 |
. . . . 5
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (π β β β§ π β 0)) |
62 | | itsclc0lem2 46933 |
. . . . 5
β’ (((π΅ β β β§ π΄ β β β§ πΆ β β) β§ (π· β β β§ 0 β€
π·) β§ (π β β β§ π β 0)) β (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π) β β) |
63 | 58, 44, 61, 62 | syl3anc 1372 |
. . . 4
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π) β β) |
64 | | itsclc0lem2 46933 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π· β β β§ 0 β€
π·) β§ (π β β β§ π β 0)) β (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β β) |
65 | 37, 44, 61, 64 | syl3anc 1372 |
. . . 4
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β β) |
66 | | itsclc0lem1 46932 |
. . . . 5
β’ (((π΅ β β β§ π΄ β β β§ πΆ β β) β§ (π· β β β§ 0 β€
π·) β§ (π β β β§ π β 0)) β (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π) β β) |
67 | 58, 44, 61, 66 | syl3anc 1372 |
. . . 4
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π) β β) |
68 | 2, 4 | prelrrx2b 46890 |
. . . 4
β’
((((((π΄ Β·
πΆ) + (π΅ Β· (ββπ·))) / π) β β β§ (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π) β β) β§ ((((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β β β§ (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π) β β)) β ((π§ β π β§ (((π§β1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (π§β2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((π§β1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (π§β2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)))) β π§ β {{β¨1, (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π)β©, β¨2, (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)β©}, {β¨1, (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π)β©, β¨2, (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)β©}})) |
69 | 57, 63, 65, 67, 68 | syl22anc 838 |
. . 3
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β ((π§ β π β§ (((π§β1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (π§β2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((π§β1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (π§β2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)))) β π§ β {{β¨1, (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π)β©, β¨2, (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)β©}, {β¨1, (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π)β©, β¨2, (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)β©}})) |
70 | 14, 69 | bitrd 279 |
. 2
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (π§ β (( 0 ππ
) β© (ππΏπ)) β π§ β {{β¨1, (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π)β©, β¨2, (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)β©}, {β¨1, (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π)β©, β¨2, (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)β©}})) |
71 | 70 | eqrdv 2731 |
1
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (( 0 ππ
) β© (ππΏπ)) = {{β¨1, (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π)β©, β¨2, (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)β©}, {β¨1, (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π)β©, β¨2, (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)β©}}) |