Step | Hyp | Ref
| Expression |
1 | | 2sphere.i |
. . . 4
β’ πΌ = {1, 2} |
2 | | prfi 9267 |
. . . 4
β’ {1, 2}
β Fin |
3 | 1, 2 | eqeltri 2834 |
. . 3
β’ πΌ β Fin |
4 | | simpl 484 |
. . 3
β’ ((π β π β§ π
β (0[,)+β)) β π β π) |
5 | | elrege0 13372 |
. . . . 5
β’ (π
β (0[,)+β) β
(π
β β β§ 0
β€ π
)) |
6 | 5 | simplbi 499 |
. . . 4
β’ (π
β (0[,)+β) β
π
β
β) |
7 | 6 | adantl 483 |
. . 3
β’ ((π β π β§ π
β (0[,)+β)) β π
β
β) |
8 | | 2sphere.e |
. . . 4
β’ πΈ = (β^βπΌ) |
9 | | 2sphere.p |
. . . 4
β’ π = (β βm
πΌ) |
10 | | eqid 2737 |
. . . 4
β’
(distβπΈ) =
(distβπΈ) |
11 | | 2sphere.s |
. . . 4
β’ π = (SphereβπΈ) |
12 | 8, 9, 10, 11 | rrxsphere 46841 |
. . 3
β’ ((πΌ β Fin β§ π β π β§ π
β β) β (πππ
) = {π β π β£ (π(distβπΈ)π) = π
}) |
13 | 3, 4, 7, 12 | mp3an2i 1467 |
. 2
β’ ((π β π β§ π
β (0[,)+β)) β (πππ
) = {π β π β£ (π(distβπΈ)π) = π
}) |
14 | | 2sphere.c |
. . 3
β’ πΆ = {π β π β£ ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2)) = (π
β2)} |
15 | 5 | biimpi 215 |
. . . . . . . 8
β’ (π
β (0[,)+β) β
(π
β β β§ 0
β€ π
)) |
16 | 15 | ad2antlr 726 |
. . . . . . 7
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β (π
β β β§ 0 β€ π
)) |
17 | | sqrtsq 15155 |
. . . . . . 7
β’ ((π
β β β§ 0 β€
π
) β
(ββ(π
β2))
= π
) |
18 | 16, 17 | syl 17 |
. . . . . 6
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β (ββ(π
β2)) = π
) |
19 | 18 | eqeq2d 2748 |
. . . . 5
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β ((ββ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2))) =
(ββ(π
β2))
β (ββ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2))) = π
)) |
20 | 1, 9 | rrx2pxel 46804 |
. . . . . . . . . . . 12
β’ (π β π β (πβ1) β β) |
21 | 20 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β (πβ1) β β) |
22 | 1, 9 | rrx2pxel 46804 |
. . . . . . . . . . . 12
β’ (π β π β (πβ1) β β) |
23 | 22 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β (πβ1) β β) |
24 | 21, 23 | resubcld 11584 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β ((πβ1) β (πβ1)) β β) |
25 | 24 | resqcld 14031 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β (((πβ1) β (πβ1))β2) β
β) |
26 | 1, 9 | rrx2pyel 46805 |
. . . . . . . . . . . 12
β’ (π β π β (πβ2) β β) |
27 | 26 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β (πβ2) β β) |
28 | 1, 9 | rrx2pyel 46805 |
. . . . . . . . . . . 12
β’ (π β π β (πβ2) β β) |
29 | 28 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β (πβ2) β β) |
30 | 27, 29 | resubcld 11584 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β ((πβ2) β (πβ2)) β β) |
31 | 30 | resqcld 14031 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β (((πβ2) β (πβ2))β2) β
β) |
32 | 25, 31 | readdcld 11185 |
. . . . . . . 8
β’ ((π β π β§ π β π) β ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2)) β
β) |
33 | 24 | sqge0d 14043 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β 0 β€ (((πβ1) β (πβ1))β2)) |
34 | 30 | sqge0d 14043 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β 0 β€ (((πβ2) β (πβ2))β2)) |
35 | 25, 31, 33, 34 | addge0d 11732 |
. . . . . . . 8
β’ ((π β π β§ π β π) β 0 β€ ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2))) |
36 | 32, 35 | jca 513 |
. . . . . . 7
β’ ((π β π β§ π β π) β (((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2)) β β β§ 0
β€ ((((πβ1) β
(πβ1))β2) +
(((πβ2) β
(πβ2))β2)))) |
37 | 36 | adantlr 714 |
. . . . . 6
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β (((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2)) β β β§ 0
β€ ((((πβ1) β
(πβ1))β2) +
(((πβ2) β
(πβ2))β2)))) |
38 | | resqcl 14030 |
. . . . . . . . 9
β’ (π
β β β (π
β2) β
β) |
39 | | sqge0 14042 |
. . . . . . . . 9
β’ (π
β β β 0 β€
(π
β2)) |
40 | 38, 39 | jca 513 |
. . . . . . . 8
β’ (π
β β β ((π
β2) β β β§ 0
β€ (π
β2))) |
41 | 6, 40 | syl 17 |
. . . . . . 7
β’ (π
β (0[,)+β) β
((π
β2) β β
β§ 0 β€ (π
β2))) |
42 | 41 | ad2antlr 726 |
. . . . . 6
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β ((π
β2) β β β§ 0 β€ (π
β2))) |
43 | | sqrt11 15148 |
. . . . . 6
β’
(((((((πβ1)
β (πβ1))β2) + (((πβ2) β (πβ2))β2)) β β β§ 0
β€ ((((πβ1) β
(πβ1))β2) +
(((πβ2) β
(πβ2))β2)))
β§ ((π
β2) β
β β§ 0 β€ (π
β2))) β ((ββ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2))) =
(ββ(π
β2))
β ((((πβ1)
β (πβ1))β2) + (((πβ2) β (πβ2))β2)) = (π
β2))) |
44 | 37, 42, 43 | syl2anc 585 |
. . . . 5
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β ((ββ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2))) =
(ββ(π
β2))
β ((((πβ1)
β (πβ1))β2) + (((πβ2) β (πβ2))β2)) = (π
β2))) |
45 | 4 | anim1ci 617 |
. . . . . . . 8
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β (π β π β§ π β π)) |
46 | | 2nn0 12431 |
. . . . . . . . . . . 12
β’ 2 β
β0 |
47 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(πΌhilβ2) =
(πΌhilβ2) |
48 | 47 | ehlval 24781 |
. . . . . . . . . . . 12
β’ (2 β
β0 β (πΌhilβ2) =
(β^β(1...2))) |
49 | 46, 48 | ax-mp 5 |
. . . . . . . . . . 11
β’
(πΌhilβ2) =
(β^β(1...2)) |
50 | | fz12pr 13499 |
. . . . . . . . . . . . 13
β’ (1...2) =
{1, 2} |
51 | 50, 1 | eqtr4i 2768 |
. . . . . . . . . . . 12
β’ (1...2) =
πΌ |
52 | 51 | fveq2i 6846 |
. . . . . . . . . . 11
β’
(β^β(1...2)) = (β^βπΌ) |
53 | 49, 52 | eqtri 2765 |
. . . . . . . . . 10
β’
(πΌhilβ2) = (β^βπΌ) |
54 | 8, 53 | eqtr4i 2768 |
. . . . . . . . 9
β’ πΈ =
(πΌhilβ2) |
55 | 1 | oveq2i 7369 |
. . . . . . . . . 10
β’ (β
βm πΌ) =
(β βm {1, 2}) |
56 | 9, 55 | eqtri 2765 |
. . . . . . . . 9
β’ π = (β βm
{1, 2}) |
57 | 54, 56, 10 | ehl2eudisval 24790 |
. . . . . . . 8
β’ ((π β π β§ π β π) β (π(distβπΈ)π) = (ββ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2)))) |
58 | 45, 57 | syl 17 |
. . . . . . 7
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β (π(distβπΈ)π) = (ββ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2)))) |
59 | 58 | eqcomd 2743 |
. . . . . 6
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β (ββ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2))) = (π(distβπΈ)π)) |
60 | 59 | eqeq1d 2739 |
. . . . 5
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β ((ββ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2))) = π
β (π(distβπΈ)π) = π
)) |
61 | 19, 44, 60 | 3bitr3d 309 |
. . . 4
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β (((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2)) = (π
β2) β (π(distβπΈ)π) = π
)) |
62 | 61 | rabbidva 3415 |
. . 3
β’ ((π β π β§ π
β (0[,)+β)) β {π β π β£ ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2)) = (π
β2)} = {π β π β£ (π(distβπΈ)π) = π
}) |
63 | 14, 62 | eqtr2id 2790 |
. 2
β’ ((π β π β§ π
β (0[,)+β)) β {π β π β£ (π(distβπΈ)π) = π
} = πΆ) |
64 | 13, 63 | eqtrd 2777 |
1
β’ ((π β π β§ π
β (0[,)+β)) β (πππ
) = πΆ) |