Step | Hyp | Ref
| Expression |
1 | | 2sphere.i |
. . . 4
β’ πΌ = {1, 2} |
2 | | prfi 9321 |
. . . 4
β’ {1, 2}
β Fin |
3 | 1, 2 | eqeltri 2823 |
. . 3
β’ πΌ β Fin |
4 | | simpl 482 |
. . 3
β’ ((π β π β§ π
β (0[,)+β)) β π β π) |
5 | | elrege0 13434 |
. . . . 5
β’ (π
β (0[,)+β) β
(π
β β β§ 0
β€ π
)) |
6 | 5 | simplbi 497 |
. . . 4
β’ (π
β (0[,)+β) β
π
β
β) |
7 | 6 | adantl 481 |
. . 3
β’ ((π β π β§ π
β (0[,)+β)) β π
β
β) |
8 | | 2sphere.e |
. . . 4
β’ πΈ = (β^βπΌ) |
9 | | 2sphere.p |
. . . 4
β’ π = (β βm
πΌ) |
10 | | eqid 2726 |
. . . 4
β’
(distβπΈ) =
(distβπΈ) |
11 | | 2sphere.s |
. . . 4
β’ π = (SphereβπΈ) |
12 | 8, 9, 10, 11 | rrxsphere 47691 |
. . 3
β’ ((πΌ β Fin β§ π β π β§ π
β β) β (πππ
) = {π β π β£ (π(distβπΈ)π) = π
}) |
13 | 3, 4, 7, 12 | mp3an2i 1462 |
. 2
β’ ((π β π β§ π
β (0[,)+β)) β (πππ
) = {π β π β£ (π(distβπΈ)π) = π
}) |
14 | | 2sphere.c |
. . 3
β’ πΆ = {π β π β£ ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2)) = (π
β2)} |
15 | 5 | biimpi 215 |
. . . . . . . 8
β’ (π
β (0[,)+β) β
(π
β β β§ 0
β€ π
)) |
16 | 15 | ad2antlr 724 |
. . . . . . 7
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β (π
β β β§ 0 β€ π
)) |
17 | | sqrtsq 15219 |
. . . . . . 7
β’ ((π
β β β§ 0 β€
π
) β
(ββ(π
β2))
= π
) |
18 | 16, 17 | syl 17 |
. . . . . 6
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β (ββ(π
β2)) = π
) |
19 | 18 | eqeq2d 2737 |
. . . . 5
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β ((ββ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2))) =
(ββ(π
β2))
β (ββ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2))) = π
)) |
20 | 1, 9 | rrx2pxel 47654 |
. . . . . . . . . . . 12
β’ (π β π β (πβ1) β β) |
21 | 20 | adantl 481 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β (πβ1) β β) |
22 | 1, 9 | rrx2pxel 47654 |
. . . . . . . . . . . 12
β’ (π β π β (πβ1) β β) |
23 | 22 | adantr 480 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β (πβ1) β β) |
24 | 21, 23 | resubcld 11643 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β ((πβ1) β (πβ1)) β β) |
25 | 24 | resqcld 14092 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β (((πβ1) β (πβ1))β2) β
β) |
26 | 1, 9 | rrx2pyel 47655 |
. . . . . . . . . . . 12
β’ (π β π β (πβ2) β β) |
27 | 26 | adantl 481 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β (πβ2) β β) |
28 | 1, 9 | rrx2pyel 47655 |
. . . . . . . . . . . 12
β’ (π β π β (πβ2) β β) |
29 | 28 | adantr 480 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β (πβ2) β β) |
30 | 27, 29 | resubcld 11643 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β ((πβ2) β (πβ2)) β β) |
31 | 30 | resqcld 14092 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β (((πβ2) β (πβ2))β2) β
β) |
32 | 25, 31 | readdcld 11244 |
. . . . . . . 8
β’ ((π β π β§ π β π) β ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2)) β
β) |
33 | 24 | sqge0d 14104 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β 0 β€ (((πβ1) β (πβ1))β2)) |
34 | 30 | sqge0d 14104 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β 0 β€ (((πβ2) β (πβ2))β2)) |
35 | 25, 31, 33, 34 | addge0d 11791 |
. . . . . . . 8
β’ ((π β π β§ π β π) β 0 β€ ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2))) |
36 | 32, 35 | jca 511 |
. . . . . . 7
β’ ((π β π β§ π β π) β (((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2)) β β β§ 0
β€ ((((πβ1) β
(πβ1))β2) +
(((πβ2) β
(πβ2))β2)))) |
37 | 36 | adantlr 712 |
. . . . . 6
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β (((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2)) β β β§ 0
β€ ((((πβ1) β
(πβ1))β2) +
(((πβ2) β
(πβ2))β2)))) |
38 | | resqcl 14091 |
. . . . . . . . 9
β’ (π
β β β (π
β2) β
β) |
39 | | sqge0 14103 |
. . . . . . . . 9
β’ (π
β β β 0 β€
(π
β2)) |
40 | 38, 39 | jca 511 |
. . . . . . . 8
β’ (π
β β β ((π
β2) β β β§ 0
β€ (π
β2))) |
41 | 6, 40 | syl 17 |
. . . . . . 7
β’ (π
β (0[,)+β) β
((π
β2) β β
β§ 0 β€ (π
β2))) |
42 | 41 | ad2antlr 724 |
. . . . . 6
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β ((π
β2) β β β§ 0 β€ (π
β2))) |
43 | | sqrt11 15212 |
. . . . . 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 583 |
. . . . 5
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β ((ββ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2))) =
(ββ(π
β2))
β ((((πβ1)
β (πβ1))β2) + (((πβ2) β (πβ2))β2)) = (π
β2))) |
45 | 4 | anim1ci 615 |
. . . . . . . 8
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β (π β π β§ π β π)) |
46 | | 2nn0 12490 |
. . . . . . . . . . . 12
β’ 2 β
β0 |
47 | | eqid 2726 |
. . . . . . . . . . . . 13
β’
(πΌhilβ2) =
(πΌhilβ2) |
48 | 47 | ehlval 25292 |
. . . . . . . . . . . 12
β’ (2 β
β0 β (πΌhilβ2) =
(β^β(1...2))) |
49 | 46, 48 | ax-mp 5 |
. . . . . . . . . . 11
β’
(πΌhilβ2) =
(β^β(1...2)) |
50 | | fz12pr 13561 |
. . . . . . . . . . . . 13
β’ (1...2) =
{1, 2} |
51 | 50, 1 | eqtr4i 2757 |
. . . . . . . . . . . 12
β’ (1...2) =
πΌ |
52 | 51 | fveq2i 6887 |
. . . . . . . . . . 11
β’
(β^β(1...2)) = (β^βπΌ) |
53 | 49, 52 | eqtri 2754 |
. . . . . . . . . 10
β’
(πΌhilβ2) = (β^βπΌ) |
54 | 8, 53 | eqtr4i 2757 |
. . . . . . . . 9
β’ πΈ =
(πΌhilβ2) |
55 | 1 | oveq2i 7415 |
. . . . . . . . . 10
β’ (β
βm πΌ) =
(β βm {1, 2}) |
56 | 9, 55 | eqtri 2754 |
. . . . . . . . 9
β’ π = (β βm
{1, 2}) |
57 | 54, 56, 10 | ehl2eudisval 25301 |
. . . . . . . 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 2732 |
. . . . . 6
β’ (((π β π β§ π
β (0[,)+β)) β§ π β π) β (ββ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2))) = (π(distβπΈ)π)) |
60 | 59 | eqeq1d 2728 |
. . . . 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 3433 |
. . 3
β’ ((π β π β§ π
β (0[,)+β)) β {π β π β£ ((((πβ1) β (πβ1))β2) + (((πβ2) β (πβ2))β2)) = (π
β2)} = {π β π β£ (π(distβπΈ)π) = π
}) |
63 | 14, 62 | eqtr2id 2779 |
. 2
β’ ((π β π β§ π
β (0[,)+β)) β {π β π β£ (π(distβπΈ)π) = π
} = πΆ) |
64 | 13, 63 | eqtrd 2766 |
1
β’ ((π β π β§ π
β (0[,)+β)) β (πππ
) = πΆ) |