Step | Hyp | Ref
| Expression |
1 | | itsclc0.i |
. . . . . 6
β’ πΌ = {1, 2} |
2 | | itsclc0.e |
. . . . . 6
β’ πΈ = (β^βπΌ) |
3 | | itsclc0.p |
. . . . . 6
β’ π = (β βm
πΌ) |
4 | | itsclinecirc0.l |
. . . . . 6
β’ πΏ = (LineMβπΈ) |
5 | | itsclinecirc0.a |
. . . . . 6
β’ π΄ = ((πβ2) β (πβ2)) |
6 | | itsclinecirc0.b |
. . . . . 6
β’ π΅ = ((πβ1) β (πβ1)) |
7 | | itsclinecirc0.c |
. . . . . 6
β’ πΆ = (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2))) |
8 | 1, 2, 3, 4, 5, 6, 7 | rrx2linest2 46920 |
. . . . 5
β’ ((π β π β§ π β π β§ π β π) β (ππΏπ) = {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ}) |
9 | 8 | adantr 482 |
. . . 4
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (ππΏπ) = {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ}) |
10 | 9 | eleq2d 2820 |
. . 3
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (π β (ππΏπ) β π β {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ})) |
11 | 10 | anbi2d 630 |
. 2
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β ((π β ( 0 ππ
) β§ π β (ππΏπ)) β (π β ( 0 ππ
) β§ π β {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ}))) |
12 | 1, 3 | rrx2pyel 46888 |
. . . . . . 7
β’ (π β π β (πβ2) β β) |
13 | 12 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π β π β§ π β π β§ π β π) β (πβ2) β β) |
14 | 1, 3 | rrx2pyel 46888 |
. . . . . . 7
β’ (π β π β (πβ2) β β) |
15 | 14 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π β π β§ π β π β§ π β π) β (πβ2) β β) |
16 | 13, 15 | resubcld 11591 |
. . . . 5
β’ ((π β π β§ π β π β§ π β π) β ((πβ2) β (πβ2)) β β) |
17 | 5, 16 | eqeltrid 2838 |
. . . 4
β’ ((π β π β§ π β π β§ π β π) β π΄ β β) |
18 | 17 | adantr 482 |
. . 3
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β π΄ β
β) |
19 | 1, 3 | rrx2pxel 46887 |
. . . . . . 7
β’ (π β π β (πβ1) β β) |
20 | 19 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π β π β§ π β π β§ π β π) β (πβ1) β β) |
21 | 1, 3 | rrx2pxel 46887 |
. . . . . . 7
β’ (π β π β (πβ1) β β) |
22 | 21 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π β π β§ π β π β§ π β π) β (πβ1) β β) |
23 | 20, 22 | resubcld 11591 |
. . . . 5
β’ ((π β π β§ π β π β§ π β π) β ((πβ1) β (πβ1)) β β) |
24 | 6, 23 | eqeltrid 2838 |
. . . 4
β’ ((π β π β§ π β π β§ π β π) β π΅ β β) |
25 | 24 | adantr 482 |
. . 3
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β π΅ β
β) |
26 | 13, 20 | remulcld 11193 |
. . . . . 6
β’ ((π β π β§ π β π β§ π β π) β ((πβ2) Β· (πβ1)) β β) |
27 | 22, 15 | remulcld 11193 |
. . . . . 6
β’ ((π β π β§ π β π β§ π β π) β ((πβ1) Β· (πβ2)) β β) |
28 | 26, 27 | resubcld 11591 |
. . . . 5
β’ ((π β π β§ π β π β§ π β π) β (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2))) β β) |
29 | 7, 28 | eqeltrid 2838 |
. . . 4
β’ ((π β π β§ π β π β§ π β π) β πΆ β β) |
30 | 29 | adantr 482 |
. . 3
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β πΆ β
β) |
31 | 1, 3, 6, 5 | rrx2pnedifcoorneorr 46893 |
. . . . 5
β’ ((π β π β§ π β π β§ π β π) β (π΅ β 0 β¨ π΄ β 0)) |
32 | 31 | orcomd 870 |
. . . 4
β’ ((π β π β§ π β π β§ π β π) β (π΄ β 0 β¨ π΅ β 0)) |
33 | 32 | adantr 482 |
. . 3
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (π΄ β 0 β¨ π΅ β 0)) |
34 | | simpr 486 |
. . 3
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β (π
β β+
β§ 0 β€ π·)) |
35 | | itsclc0.s |
. . . 4
β’ π = (SphereβπΈ) |
36 | | itsclc0.0 |
. . . 4
β’ 0 = (πΌ Γ {0}) |
37 | | itsclc0.q |
. . . 4
β’ π = ((π΄β2) + (π΅β2)) |
38 | | itsclc0.d |
. . . 4
β’ π· = (((π
β2) Β· π) β (πΆβ2)) |
39 | | eqid 2733 |
. . . 4
β’ {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ} = {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ} |
40 | 1, 2, 3, 35, 36, 37, 38, 39 | itsclc0 46947 |
. . 3
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β ((π β ( 0 ππ
) β§ π β {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ}) β (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π))))) |
41 | 18, 25, 30, 33, 34, 40 | syl311anc 1385 |
. 2
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β ((π β ( 0 ππ
) β§ π β {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ}) β (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π))))) |
42 | 11, 41 | sylbid 239 |
1
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 β€
π·)) β ((π β ( 0 ππ
) β§ π β (ππΏπ)) β (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π))))) |