Step | Hyp | Ref
| Expression |
1 | | rprege0 12938 |
. . . . . . 7
β’ (π
β β+
β (π
β β
β§ 0 β€ π
)) |
2 | | elrege0 13380 |
. . . . . . 7
β’ (π
β (0[,)+β) β
(π
β β β§ 0
β€ π
)) |
3 | 1, 2 | sylibr 233 |
. . . . . 6
β’ (π
β β+
β π
β
(0[,)+β)) |
4 | 3 | adantr 482 |
. . . . 5
β’ ((π
β β+
β§ 0 β€ π·) β
π
β
(0[,)+β)) |
5 | 4 | 3ad2ant3 1136 |
. . . 4
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β π
β
(0[,)+β)) |
6 | | itsclc0.i |
. . . . . 6
β’ πΌ = {1, 2} |
7 | | itsclc0.e |
. . . . . 6
β’ πΈ = (β^βπΌ) |
8 | | itsclc0.p |
. . . . . 6
β’ π = (β βm
πΌ) |
9 | | itsclc0.s |
. . . . . 6
β’ π = (SphereβπΈ) |
10 | | itsclc0.0 |
. . . . . 6
β’ 0 = (πΌ Γ {0}) |
11 | | eqid 2733 |
. . . . . 6
β’ {π β π β£ (((πβ1)β2) + ((πβ2)β2)) = (π
β2)} = {π β π β£ (((πβ1)β2) + ((πβ2)β2)) = (π
β2)} |
12 | 6, 7, 8, 9, 10, 11 | 2sphere0 46926 |
. . . . 5
β’ (π
β (0[,)+β) β (
0 ππ
) = {π β π β£ (((πβ1)β2) + ((πβ2)β2)) = (π
β2)}) |
13 | 12 | eleq2d 2820 |
. . . 4
β’ (π
β (0[,)+β) β
(π β ( 0 ππ
) β π β {π β π β£ (((πβ1)β2) + ((πβ2)β2)) = (π
β2)})) |
14 | 5, 13 | syl 17 |
. . 3
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β (π β ( 0 ππ
) β π β {π β π β£ (((πβ1)β2) + ((πβ2)β2)) = (π
β2)})) |
15 | | fveq1 6845 |
. . . . . . . 8
β’ (π = π β (πβ1) = (πβ1)) |
16 | 15 | oveq2d 7377 |
. . . . . . 7
β’ (π = π β (π΄ Β· (πβ1)) = (π΄ Β· (πβ1))) |
17 | | fveq1 6845 |
. . . . . . . 8
β’ (π = π β (πβ2) = (πβ2)) |
18 | 17 | oveq2d 7377 |
. . . . . . 7
β’ (π = π β (π΅ Β· (πβ2)) = (π΅ Β· (πβ2))) |
19 | 16, 18 | oveq12d 7379 |
. . . . . 6
β’ (π = π β ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2)))) |
20 | 19 | eqeq1d 2735 |
. . . . 5
β’ (π = π β (((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ β ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ)) |
21 | | itsclc0.l |
. . . . 5
β’ πΏ = {π β π β£ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ} |
22 | 20, 21 | elrab2 3652 |
. . . 4
β’ (π β πΏ β (π β π β§ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ)) |
23 | 22 | a1i 11 |
. . 3
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β (π β πΏ β (π β π β§ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ))) |
24 | 14, 23 | anbi12d 632 |
. 2
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β ((π β ( 0 ππ
) β§ π β πΏ) β (π β {π β π β£ (((πβ1)β2) + ((πβ2)β2)) = (π
β2)} β§ (π β π β§ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ)))) |
25 | 15 | oveq1d 7376 |
. . . . . . 7
β’ (π = π β ((πβ1)β2) = ((πβ1)β2)) |
26 | 17 | oveq1d 7376 |
. . . . . . 7
β’ (π = π β ((πβ2)β2) = ((πβ2)β2)) |
27 | 25, 26 | oveq12d 7379 |
. . . . . 6
β’ (π = π β (((πβ1)β2) + ((πβ2)β2)) = (((πβ1)β2) + ((πβ2)β2))) |
28 | 27 | eqeq1d 2735 |
. . . . 5
β’ (π = π β ((((πβ1)β2) + ((πβ2)β2)) = (π
β2) β (((πβ1)β2) + ((πβ2)β2)) = (π
β2))) |
29 | 28 | elrab 3649 |
. . . 4
β’ (π β {π β π β£ (((πβ1)β2) + ((πβ2)β2)) = (π
β2)} β (π β π β§ (((πβ1)β2) + ((πβ2)β2)) = (π
β2))) |
30 | | 3simpa 1149 |
. . . . . . . . . 10
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β ((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0))) |
31 | 30 | adantr 482 |
. . . . . . . . 9
β’ ((((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β ((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0))) |
32 | | simpl3 1194 |
. . . . . . . . 9
β’ ((((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (π
β β+ β§ 0 β€
π·)) |
33 | 6, 8 | rrx2pxel 46887 |
. . . . . . . . . . 11
β’ (π β π β (πβ1) β β) |
34 | 6, 8 | rrx2pyel 46888 |
. . . . . . . . . . 11
β’ (π β π β (πβ2) β β) |
35 | 33, 34 | jca 513 |
. . . . . . . . . 10
β’ (π β π β ((πβ1) β β β§ (πβ2) β
β)) |
36 | 35 | adantl 483 |
. . . . . . . . 9
β’ ((((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β ((πβ1) β β β§ (πβ2) β
β)) |
37 | | itsclc0.q |
. . . . . . . . . 10
β’ π = ((π΄β2) + (π΅β2)) |
38 | | itsclc0.d |
. . . . . . . . . 10
β’ π· = (((π
β2) Β· π) β (πΆβ2)) |
39 | 37, 38 | itsclc0xyqsol 46944 |
. . . . . . . . 9
β’ ((((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0)) β§ (π
β β+ β§ 0 β€
π·) β§ ((πβ1) β β β§
(πβ2) β
β)) β (((((πβ1)β2) + ((πβ2)β2)) = (π
β2) β§ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ) β (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π))))) |
40 | 31, 32, 36, 39 | syl3anc 1372 |
. . . . . . . 8
β’ ((((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (((((πβ1)β2) + ((πβ2)β2)) = (π
β2) β§ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ) β (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π))))) |
41 | 40 | expcomd 418 |
. . . . . . 7
β’ ((((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β§ π β π) β (((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ β ((((πβ1)β2) + ((πβ2)β2)) = (π
β2) β (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)))))) |
42 | 41 | expimpd 455 |
. . . . . 6
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β ((π β π β§ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ) β ((((πβ1)β2) + ((πβ2)β2)) = (π
β2) β (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)))))) |
43 | 42 | com23 86 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β ((((πβ1)β2) + ((πβ2)β2)) = (π
β2) β ((π β π β§ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ) β (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)))))) |
44 | 43 | adantld 492 |
. . . 4
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β ((π β π β§ (((πβ1)β2) + ((πβ2)β2)) = (π
β2)) β ((π β π β§ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ) β (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)))))) |
45 | 29, 44 | biimtrid 241 |
. . 3
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β (π β {π β π β£ (((πβ1)β2) + ((πβ2)β2)) = (π
β2)} β ((π β π β§ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ) β (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π)))))) |
46 | 45 | impd 412 |
. 2
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β ((π β {π β π β£ (((πβ1)β2) + ((πβ2)β2)) = (π
β2)} β§ (π β π β§ ((π΄ Β· (πβ1)) + (π΅ Β· (πβ2))) = πΆ)) β (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π))))) |
47 | 24, 46 | sylbid 239 |
1
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ (π΄ β 0 β¨ π΅ β 0) β§ (π
β β+ β§ 0 β€
π·)) β ((π β ( 0 ππ
) β§ π β πΏ) β (((πβ1) = (((π΄ Β· πΆ) + (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) β (π΄ Β· (ββπ·))) / π)) β¨ ((πβ1) = (((π΄ Β· πΆ) β (π΅ Β· (ββπ·))) / π) β§ (πβ2) = (((π΅ Β· πΆ) + (π΄ Β· (ββπ·))) / π))))) |