Step | Hyp | Ref
| Expression |
1 | | fz1ssnn 13481 |
. . . . 5
β’
(1...π) β
β |
2 | 1 | a1i 11 |
. . . 4
β’ (π β (1...π) β β) |
3 | | breprexplema.m |
. . . . 5
β’ (π β π β
β0) |
4 | 3 | nn0zd 12533 |
. . . 4
β’ (π β π β β€) |
5 | | breprexp.s |
. . . 4
β’ (π β π β
β0) |
6 | | eqid 2733 |
. . . 4
β’ (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©})) = (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©})) |
7 | 2, 4, 5, 6 | reprsuc 33292 |
. . 3
β’ (π β ((1...π)(reprβ(π + 1))π) = βͺ
π β (1...π)ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) |
8 | 7 | sumeq1d 15594 |
. 2
β’ (π β Ξ£π β ((1...π)(reprβ(π + 1))π)βπ β (0..^(π + 1))((πΏβπ)β(πβπ)) = Ξ£π β βͺ
π β (1...π)ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))βπ β (0..^(π + 1))((πΏβπ)β(πβπ))) |
9 | | fzfid 13887 |
. . 3
β’ (π β (1...π) β Fin) |
10 | 1 | a1i 11 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (1...π) β β) |
11 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β π β β€) |
12 | | fzssz 13452 |
. . . . . . . 8
β’
(1...π) β
β€ |
13 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β π β (1...π)) |
14 | 12, 13 | sselid 3946 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β π β β€) |
15 | 11, 14 | zsubcld 12620 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (π β π) β β€) |
16 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (1...π)) β π β
β0) |
17 | 9 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (1...π) β Fin) |
18 | 10, 15, 16, 17 | reprfi 33293 |
. . . . 5
β’ ((π β§ π β (1...π)) β ((1...π)(reprβπ)(π β π)) β Fin) |
19 | | mptfi 9301 |
. . . . 5
β’
(((1...π)(reprβπ)(π β π)) β Fin β (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©})) β Fin) |
20 | 18, 19 | syl 17 |
. . . 4
β’ ((π β§ π β (1...π)) β (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©})) β Fin) |
21 | | rnfi 9285 |
. . . 4
β’ ((π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©})) β Fin β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©})) β Fin) |
22 | 20, 21 | syl 17 |
. . 3
β’ ((π β§ π β (1...π)) β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©})) β Fin) |
23 | 10, 15, 16 | reprval 33287 |
. . . . 5
β’ ((π β§ π β (1...π)) β ((1...π)(reprβπ)(π β π)) = {π β ((1...π) βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = (π β π)}) |
24 | | ssrab2 4041 |
. . . . 5
β’ {π β ((1...π) βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = (π β π)} β ((1...π) βm (0..^π)) |
25 | 23, 24 | eqsstrdi 4002 |
. . . 4
β’ ((π β§ π β (1...π)) β ((1...π)(reprβπ)(π β π)) β ((1...π) βm (0..^π))) |
26 | 9 | elexd 3467 |
. . . 4
β’ (π β (1...π) β V) |
27 | | fzonel 13595 |
. . . . 5
β’ Β¬
π β (0..^π) |
28 | 27 | a1i 11 |
. . . 4
β’ (π β Β¬ π β (0..^π)) |
29 | 25, 26, 5, 28, 6 | actfunsnrndisj 33282 |
. . 3
β’ (π β Disj π β (1...π)ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) |
30 | | fzofi 13888 |
. . . . . 6
β’
(0..^(π + 1)) β
Fin |
31 | 30 | a1i 11 |
. . . . 5
β’ (((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β (0..^(π + 1)) β Fin) |
32 | | breprexplema.l |
. . . . . . . . 9
β’ (((π β§ π₯ β (0..^(π + 1))) β§ π¦ β β) β ((πΏβπ₯)βπ¦) β β) |
33 | 32 | ralrimiva 3140 |
. . . . . . . 8
β’ ((π β§ π₯ β (0..^(π + 1))) β βπ¦ β β ((πΏβπ₯)βπ¦) β β) |
34 | 33 | ralrimiva 3140 |
. . . . . . 7
β’ (π β βπ₯ β (0..^(π + 1))βπ¦ β β ((πΏβπ₯)βπ¦) β β) |
35 | 34 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π β (0..^(π + 1))) β βπ₯ β (0..^(π + 1))βπ¦ β β ((πΏβπ₯)βπ¦) β β) |
36 | | simpr 486 |
. . . . . . 7
β’ ((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π β (0..^(π + 1))) β π β (0..^(π + 1))) |
37 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π£(π β§ π β (1...π)) |
38 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π£π |
39 | | nfmpt1 5217 |
. . . . . . . . . . . . . 14
β’
β²π£(π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©})) |
40 | 39 | nfrn 5911 |
. . . . . . . . . . . . 13
β’
β²π£ran
(π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©})) |
41 | 38, 40 | nfel 2918 |
. . . . . . . . . . . 12
β’
β²π£ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©})) |
42 | 37, 41 | nfan 1903 |
. . . . . . . . . . 11
β’
β²π£((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) |
43 | 1 | a1i 11 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π£ β ((1...π)(reprβπ)(π β π))) β§ π = (π£ βͺ {β¨π, πβ©})) β (1...π) β β) |
44 | 15 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π£ β ((1...π)(reprβπ)(π β π))) β§ π = (π£ βͺ {β¨π, πβ©})) β (π β π) β β€) |
45 | 16 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π£ β ((1...π)(reprβπ)(π β π))) β§ π = (π£ βͺ {β¨π, πβ©})) β π β
β0) |
46 | | simplr 768 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π£ β ((1...π)(reprβπ)(π β π))) β§ π = (π£ βͺ {β¨π, πβ©})) β π£ β ((1...π)(reprβπ)(π β π))) |
47 | 43, 44, 45, 46 | reprf 33289 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π£ β ((1...π)(reprβπ)(π β π))) β§ π = (π£ βͺ {β¨π, πβ©})) β π£:(0..^π)βΆ(1...π)) |
48 | 13 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π£ β ((1...π)(reprβπ)(π β π))) β§ π = (π£ βͺ {β¨π, πβ©})) β π β (1...π)) |
49 | 45, 48 | fsnd 6831 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π£ β ((1...π)(reprβπ)(π β π))) β§ π = (π£ βͺ {β¨π, πβ©})) β {β¨π, πβ©}:{π}βΆ(1...π)) |
50 | | fzodisjsn 13619 |
. . . . . . . . . . . . . 14
β’
((0..^π) β©
{π}) =
β
|
51 | 50 | a1i 11 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π£ β ((1...π)(reprβπ)(π β π))) β§ π = (π£ βͺ {β¨π, πβ©})) β ((0..^π) β© {π}) = β
) |
52 | | fun2 6709 |
. . . . . . . . . . . . 13
β’ (((π£:(0..^π)βΆ(1...π) β§ {β¨π, πβ©}:{π}βΆ(1...π)) β§ ((0..^π) β© {π}) = β
) β (π£ βͺ {β¨π, πβ©}):((0..^π) βͺ {π})βΆ(1...π)) |
53 | 47, 49, 51, 52 | syl21anc 837 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π£ β ((1...π)(reprβπ)(π β π))) β§ π = (π£ βͺ {β¨π, πβ©})) β (π£ βͺ {β¨π, πβ©}):((0..^π) βͺ {π})βΆ(1...π)) |
54 | | simpr 486 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π£ β ((1...π)(reprβπ)(π β π))) β§ π = (π£ βͺ {β¨π, πβ©})) β π = (π£ βͺ {β¨π, πβ©})) |
55 | | nn0uz 12813 |
. . . . . . . . . . . . . . . 16
β’
β0 = (β€β₯β0) |
56 | 5, 55 | eleqtrdi 2844 |
. . . . . . . . . . . . . . 15
β’ (π β π β
(β€β₯β0)) |
57 | | fzosplitsn 13689 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯β0) β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
59 | 58 | ad4antr 731 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π£ β ((1...π)(reprβπ)(π β π))) β§ π = (π£ βͺ {β¨π, πβ©})) β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
60 | 54, 59 | feq12d 6660 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π£ β ((1...π)(reprβπ)(π β π))) β§ π = (π£ βͺ {β¨π, πβ©})) β (π:(0..^(π + 1))βΆ(1...π) β (π£ βͺ {β¨π, πβ©}):((0..^π) βͺ {π})βΆ(1...π))) |
61 | 53, 60 | mpbird 257 |
. . . . . . . . . . 11
β’
(((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π£ β ((1...π)(reprβπ)(π β π))) β§ π = (π£ βͺ {β¨π, πβ©})) β π:(0..^(π + 1))βΆ(1...π)) |
62 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) |
63 | | vex 3451 |
. . . . . . . . . . . . . 14
β’ π£ β V |
64 | | snex 5392 |
. . . . . . . . . . . . . 14
β’
{β¨π, πβ©} β
V |
65 | 63, 64 | unex 7684 |
. . . . . . . . . . . . 13
β’ (π£ βͺ {β¨π, πβ©}) β V |
66 | 6, 65 | elrnmpti 5919 |
. . . . . . . . . . . 12
β’ (π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©})) β βπ£ β ((1...π)(reprβπ)(π β π))π = (π£ βͺ {β¨π, πβ©})) |
67 | 62, 66 | sylib 217 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β βπ£ β ((1...π)(reprβπ)(π β π))π = (π£ βͺ {β¨π, πβ©})) |
68 | 42, 61, 67 | r19.29af 3250 |
. . . . . . . . . 10
β’ (((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β π:(0..^(π + 1))βΆ(1...π)) |
69 | 68 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π β (0..^(π + 1))) β π:(0..^(π + 1))βΆ(1...π)) |
70 | 69, 36 | ffvelcdmd 7040 |
. . . . . . . 8
β’ ((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π β (0..^(π + 1))) β (πβπ) β (1...π)) |
71 | 1, 70 | sselid 3946 |
. . . . . . 7
β’ ((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π β (0..^(π + 1))) β (πβπ) β β) |
72 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π₯ = π β (πΏβπ₯) = (πΏβπ)) |
73 | 72 | fveq1d 6848 |
. . . . . . . . 9
β’ (π₯ = π β ((πΏβπ₯)βπ¦) = ((πΏβπ)βπ¦)) |
74 | 73 | eleq1d 2819 |
. . . . . . . 8
β’ (π₯ = π β (((πΏβπ₯)βπ¦) β β β ((πΏβπ)βπ¦) β β)) |
75 | | fveq2 6846 |
. . . . . . . . 9
β’ (π¦ = (πβπ) β ((πΏβπ)βπ¦) = ((πΏβπ)β(πβπ))) |
76 | 75 | eleq1d 2819 |
. . . . . . . 8
β’ (π¦ = (πβπ) β (((πΏβπ)βπ¦) β β β ((πΏβπ)β(πβπ)) β β)) |
77 | 74, 76 | rspc2v 3592 |
. . . . . . 7
β’ ((π β (0..^(π + 1)) β§ (πβπ) β β) β (βπ₯ β (0..^(π + 1))βπ¦ β β ((πΏβπ₯)βπ¦) β β β ((πΏβπ)β(πβπ)) β β)) |
78 | 36, 71, 77 | syl2anc 585 |
. . . . . 6
β’ ((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π β (0..^(π + 1))) β (βπ₯ β (0..^(π + 1))βπ¦ β β ((πΏβπ₯)βπ¦) β β β ((πΏβπ)β(πβπ)) β β)) |
79 | 35, 78 | mpd 15 |
. . . . 5
β’ ((((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β§ π β (0..^(π + 1))) β ((πΏβπ)β(πβπ)) β β) |
80 | 31, 79 | fprodcl 15843 |
. . . 4
β’ (((π β§ π β (1...π)) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) β βπ β (0..^(π + 1))((πΏβπ)β(πβπ)) β β) |
81 | 80 | anasss 468 |
. . 3
β’ ((π β§ (π β (1...π) β§ π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©})))) β βπ β (0..^(π + 1))((πΏβπ)β(πβπ)) β β) |
82 | 9, 22, 29, 81 | fsumiun 15714 |
. 2
β’ (π β Ξ£π β βͺ
π β (1...π)ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))βπ β (0..^(π + 1))((πΏβπ)β(πβπ)) = Ξ£π β (1...π)Ξ£π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))βπ β (0..^(π + 1))((πΏβπ)β(πβπ))) |
83 | 58 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β (0..^(π + 1)) = ((0..^π) βͺ {π})) |
84 | 83 | prodeq1d 15812 |
. . . . . 6
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β βπ β (0..^(π + 1))((πΏβπ)β((π βͺ {β¨π, πβ©})βπ)) = βπ β ((0..^π) βͺ {π})((πΏβπ)β((π βͺ {β¨π, πβ©})βπ))) |
85 | | nfv 1918 |
. . . . . . 7
β’
β²π((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) |
86 | | nfcv 2904 |
. . . . . . 7
β’
β²π((πΏβπ)β((π βͺ {β¨π, πβ©})βπ)) |
87 | | fzofi 13888 |
. . . . . . . 8
β’
(0..^π) β
Fin |
88 | 87 | a1i 11 |
. . . . . . 7
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β (0..^π) β Fin) |
89 | 16 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β π β
β0) |
90 | 27 | a1i 11 |
. . . . . . 7
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β Β¬ π β (0..^π)) |
91 | 1 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β (1...π) β β) |
92 | 15 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β (π β π) β β€) |
93 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β π β ((1...π)(reprβπ)(π β π))) |
94 | 91, 92, 89, 93 | reprf 33289 |
. . . . . . . . . . . 12
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β π:(0..^π)βΆ(1...π)) |
95 | 94 | ffnd 6673 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β π Fn (0..^π)) |
96 | 95 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β§ π β (0..^π)) β π Fn (0..^π)) |
97 | 13 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β π β (1...π)) |
98 | | fnsng 6557 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π β (1...π)) β {β¨π, πβ©} Fn {π}) |
99 | 89, 97, 98 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β {β¨π, πβ©} Fn {π}) |
100 | 99 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β§ π β (0..^π)) β {β¨π, πβ©} Fn {π}) |
101 | 50 | a1i 11 |
. . . . . . . . . 10
β’ ((((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β§ π β (0..^π)) β ((0..^π) β© {π}) = β
) |
102 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β§ π β (0..^π)) β π β (0..^π)) |
103 | | fvun1 6936 |
. . . . . . . . . 10
β’ ((π Fn (0..^π) β§ {β¨π, πβ©} Fn {π} β§ (((0..^π) β© {π}) = β
β§ π β (0..^π))) β ((π βͺ {β¨π, πβ©})βπ) = (πβπ)) |
104 | 96, 100, 101, 102, 103 | syl112anc 1375 |
. . . . . . . . 9
β’ ((((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β§ π β (0..^π)) β ((π βͺ {β¨π, πβ©})βπ) = (πβπ)) |
105 | 104 | fveq2d 6850 |
. . . . . . . 8
β’ ((((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β§ π β (0..^π)) β ((πΏβπ)β((π βͺ {β¨π, πβ©})βπ)) = ((πΏβπ)β(πβπ))) |
106 | 34 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β βπ₯ β (0..^(π + 1))βπ¦ β β ((πΏβπ₯)βπ¦) β β) |
107 | 106 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β§ π β (0..^π)) β βπ₯ β (0..^(π + 1))βπ¦ β β ((πΏβπ₯)βπ¦) β β) |
108 | | fzossfzop1 13659 |
. . . . . . . . . . . . 13
β’ (π β β0
β (0..^π) β
(0..^(π +
1))) |
109 | 5, 108 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (0..^π) β (0..^(π + 1))) |
110 | 109 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β (0..^π) β (0..^(π + 1))) |
111 | 110 | sselda 3948 |
. . . . . . . . . 10
β’ ((((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β§ π β (0..^π)) β π β (0..^(π + 1))) |
112 | 94 | ffvelcdmda 7039 |
. . . . . . . . . . 11
β’ ((((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β§ π β (0..^π)) β (πβπ) β (1...π)) |
113 | 1, 112 | sselid 3946 |
. . . . . . . . . 10
β’ ((((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β§ π β (0..^π)) β (πβπ) β β) |
114 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π¦ = (πβπ) β ((πΏβπ)βπ¦) = ((πΏβπ)β(πβπ))) |
115 | 114 | eleq1d 2819 |
. . . . . . . . . . 11
β’ (π¦ = (πβπ) β (((πΏβπ)βπ¦) β β β ((πΏβπ)β(πβπ)) β β)) |
116 | 74, 115 | rspc2v 3592 |
. . . . . . . . . 10
β’ ((π β (0..^(π + 1)) β§ (πβπ) β β) β (βπ₯ β (0..^(π + 1))βπ¦ β β ((πΏβπ₯)βπ¦) β β β ((πΏβπ)β(πβπ)) β β)) |
117 | 111, 113,
116 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β§ π β (0..^π)) β (βπ₯ β (0..^(π + 1))βπ¦ β β ((πΏβπ₯)βπ¦) β β β ((πΏβπ)β(πβπ)) β β)) |
118 | 107, 117 | mpd 15 |
. . . . . . . 8
β’ ((((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β§ π β (0..^π)) β ((πΏβπ)β(πβπ)) β β) |
119 | 105, 118 | eqeltrd 2834 |
. . . . . . 7
β’ ((((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β§ π β (0..^π)) β ((πΏβπ)β((π βͺ {β¨π, πβ©})βπ)) β β) |
120 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π β (πΏβπ) = (πΏβπ)) |
121 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π β ((π βͺ {β¨π, πβ©})βπ) = ((π βͺ {β¨π, πβ©})βπ)) |
122 | 120, 121 | fveq12d 6853 |
. . . . . . 7
β’ (π = π β ((πΏβπ)β((π βͺ {β¨π, πβ©})βπ)) = ((πΏβπ)β((π βͺ {β¨π, πβ©})βπ))) |
123 | 50 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β ((0..^π) β© {π}) = β
) |
124 | | snidg 4624 |
. . . . . . . . . . . 12
β’ (π β β0
β π β {π}) |
125 | 89, 124 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β π β {π}) |
126 | | fvun2 6937 |
. . . . . . . . . . 11
β’ ((π Fn (0..^π) β§ {β¨π, πβ©} Fn {π} β§ (((0..^π) β© {π}) = β
β§ π β {π})) β ((π βͺ {β¨π, πβ©})βπ) = ({β¨π, πβ©}βπ)) |
127 | 95, 99, 123, 125, 126 | syl112anc 1375 |
. . . . . . . . . 10
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β ((π βͺ {β¨π, πβ©})βπ) = ({β¨π, πβ©}βπ)) |
128 | | fvsng 7130 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π β (1...π)) β ({β¨π, πβ©}βπ) = π) |
129 | 89, 97, 128 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β ({β¨π, πβ©}βπ) = π) |
130 | 127, 129 | eqtrd 2773 |
. . . . . . . . 9
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β ((π βͺ {β¨π, πβ©})βπ) = π) |
131 | 130 | fveq2d 6850 |
. . . . . . . 8
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β ((πΏβπ)β((π βͺ {β¨π, πβ©})βπ)) = ((πΏβπ)βπ)) |
132 | | fzonn0p1 13658 |
. . . . . . . . . . . 12
β’ (π β β0
β π β (0..^(π + 1))) |
133 | 5, 132 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β (0..^(π + 1))) |
134 | 133 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β π β (0..^(π + 1))) |
135 | 1, 97 | sselid 3946 |
. . . . . . . . . 10
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β π β β) |
136 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (πΏβπ₯) = (πΏβπ)) |
137 | 136 | fveq1d 6848 |
. . . . . . . . . . . 12
β’ (π₯ = π β ((πΏβπ₯)βπ¦) = ((πΏβπ)βπ¦)) |
138 | 137 | eleq1d 2819 |
. . . . . . . . . . 11
β’ (π₯ = π β (((πΏβπ₯)βπ¦) β β β ((πΏβπ)βπ¦) β β)) |
139 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π¦ = π β ((πΏβπ)βπ¦) = ((πΏβπ)βπ)) |
140 | 139 | eleq1d 2819 |
. . . . . . . . . . 11
β’ (π¦ = π β (((πΏβπ)βπ¦) β β β ((πΏβπ)βπ) β β)) |
141 | 138, 140 | rspc2v 3592 |
. . . . . . . . . 10
β’ ((π β (0..^(π + 1)) β§ π β β) β (βπ₯ β (0..^(π + 1))βπ¦ β β ((πΏβπ₯)βπ¦) β β β ((πΏβπ)βπ) β β)) |
142 | 134, 135,
141 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β (βπ₯ β (0..^(π + 1))βπ¦ β β ((πΏβπ₯)βπ¦) β β β ((πΏβπ)βπ) β β)) |
143 | 106, 142 | mpd 15 |
. . . . . . . 8
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β ((πΏβπ)βπ) β β) |
144 | 131, 143 | eqeltrd 2834 |
. . . . . . 7
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β ((πΏβπ)β((π βͺ {β¨π, πβ©})βπ)) β β) |
145 | 85, 86, 88, 89, 90, 119, 122, 144 | fprodsplitsn 15880 |
. . . . . 6
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β βπ β ((0..^π) βͺ {π})((πΏβπ)β((π βͺ {β¨π, πβ©})βπ)) = (βπ β (0..^π)((πΏβπ)β((π βͺ {β¨π, πβ©})βπ)) Β· ((πΏβπ)β((π βͺ {β¨π, πβ©})βπ)))) |
146 | 105 | prodeq2dv 15814 |
. . . . . . 7
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β βπ β (0..^π)((πΏβπ)β((π βͺ {β¨π, πβ©})βπ)) = βπ β (0..^π)((πΏβπ)β(πβπ))) |
147 | 146, 131 | oveq12d 7379 |
. . . . . 6
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β (βπ β (0..^π)((πΏβπ)β((π βͺ {β¨π, πβ©})βπ)) Β· ((πΏβπ)β((π βͺ {β¨π, πβ©})βπ))) = (βπ β (0..^π)((πΏβπ)β(πβπ)) Β· ((πΏβπ)βπ))) |
148 | 84, 145, 147 | 3eqtrd 2777 |
. . . . 5
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β βπ β (0..^(π + 1))((πΏβπ)β((π βͺ {β¨π, πβ©})βπ)) = (βπ β (0..^π)((πΏβπ)β(πβπ)) Β· ((πΏβπ)βπ))) |
149 | 148 | sumeq2dv 15596 |
. . . 4
β’ ((π β§ π β (1...π)) β Ξ£π β ((1...π)(reprβπ)(π β π))βπ β (0..^(π + 1))((πΏβπ)β((π βͺ {β¨π, πβ©})βπ)) = Ξ£π β ((1...π)(reprβπ)(π β π))(βπ β (0..^π)((πΏβπ)β(πβπ)) Β· ((πΏβπ)βπ))) |
150 | | simpl 484 |
. . . . . . . 8
β’ ((π = (π βͺ {β¨π, πβ©}) β§ π β (0..^(π + 1))) β π = (π βͺ {β¨π, πβ©})) |
151 | 150 | fveq1d 6848 |
. . . . . . 7
β’ ((π = (π βͺ {β¨π, πβ©}) β§ π β (0..^(π + 1))) β (πβπ) = ((π βͺ {β¨π, πβ©})βπ)) |
152 | 151 | fveq2d 6850 |
. . . . . 6
β’ ((π = (π βͺ {β¨π, πβ©}) β§ π β (0..^(π + 1))) β ((πΏβπ)β(πβπ)) = ((πΏβπ)β((π βͺ {β¨π, πβ©})βπ))) |
153 | 152 | prodeq2dv 15814 |
. . . . 5
β’ (π = (π βͺ {β¨π, πβ©}) β βπ β (0..^(π + 1))((πΏβπ)β(πβπ)) = βπ β (0..^(π + 1))((πΏβπ)β((π βͺ {β¨π, πβ©})βπ))) |
154 | 25, 26, 5, 28, 6 | actfunsnf1o 33281 |
. . . . 5
β’ ((π β§ π β (1...π)) β (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©})):((1...π)(reprβπ)(π β π))β1-1-ontoβran
(π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) |
155 | 6 | a1i 11 |
. . . . . 6
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©})) = (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))) |
156 | | simpr 486 |
. . . . . . 7
β’ ((((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β§ π£ = π) β π£ = π) |
157 | 156 | uneq1d 4126 |
. . . . . 6
β’ ((((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β§ π£ = π) β (π£ βͺ {β¨π, πβ©}) = (π βͺ {β¨π, πβ©})) |
158 | | vex 3451 |
. . . . . . . 8
β’ π β V |
159 | 158, 64 | unex 7684 |
. . . . . . 7
β’ (π βͺ {β¨π, πβ©}) β V |
160 | 159 | a1i 11 |
. . . . . 6
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β (π βͺ {β¨π, πβ©}) β V) |
161 | 155, 157,
93, 160 | fvmptd 6959 |
. . . . 5
β’ (((π β§ π β (1...π)) β§ π β ((1...π)(reprβπ)(π β π))) β ((π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))βπ) = (π βͺ {β¨π, πβ©})) |
162 | 153, 18, 154, 161, 80 | fsumf1o 15616 |
. . . 4
β’ ((π β§ π β (1...π)) β Ξ£π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))βπ β (0..^(π + 1))((πΏβπ)β(πβπ)) = Ξ£π β ((1...π)(reprβπ)(π β π))βπ β (0..^(π + 1))((πΏβπ)β((π βͺ {β¨π, πβ©})βπ))) |
163 | | simpl 484 |
. . . . . . . . . 10
β’ ((π = π β§ π β (0..^π)) β π = π) |
164 | 163 | fveq1d 6848 |
. . . . . . . . 9
β’ ((π = π β§ π β (0..^π)) β (πβπ) = (πβπ)) |
165 | 164 | fveq2d 6850 |
. . . . . . . 8
β’ ((π = π β§ π β (0..^π)) β ((πΏβπ)β(πβπ)) = ((πΏβπ)β(πβπ))) |
166 | 165 | prodeq2dv 15814 |
. . . . . . 7
β’ (π = π β βπ β (0..^π)((πΏβπ)β(πβπ)) = βπ β (0..^π)((πΏβπ)β(πβπ))) |
167 | 166 | oveq1d 7376 |
. . . . . 6
β’ (π = π β (βπ β (0..^π)((πΏβπ)β(πβπ)) Β· ((πΏβπ)βπ)) = (βπ β (0..^π)((πΏβπ)β(πβπ)) Β· ((πΏβπ)βπ))) |
168 | 167 | cbvsumv 15589 |
. . . . 5
β’
Ξ£π β
((1...π)(reprβπ)(π β π))(βπ β (0..^π)((πΏβπ)β(πβπ)) Β· ((πΏβπ)βπ)) = Ξ£π β ((1...π)(reprβπ)(π β π))(βπ β (0..^π)((πΏβπ)β(πβπ)) Β· ((πΏβπ)βπ)) |
169 | 168 | a1i 11 |
. . . 4
β’ ((π β§ π β (1...π)) β Ξ£π β ((1...π)(reprβπ)(π β π))(βπ β (0..^π)((πΏβπ)β(πβπ)) Β· ((πΏβπ)βπ)) = Ξ£π β ((1...π)(reprβπ)(π β π))(βπ β (0..^π)((πΏβπ)β(πβπ)) Β· ((πΏβπ)βπ))) |
170 | 149, 162,
169 | 3eqtr4d 2783 |
. . 3
β’ ((π β§ π β (1...π)) β Ξ£π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))βπ β (0..^(π + 1))((πΏβπ)β(πβπ)) = Ξ£π β ((1...π)(reprβπ)(π β π))(βπ β (0..^π)((πΏβπ)β(πβπ)) Β· ((πΏβπ)βπ))) |
171 | 170 | sumeq2dv 15596 |
. 2
β’ (π β Ξ£π β (1...π)Ξ£π β ran (π£ β ((1...π)(reprβπ)(π β π)) β¦ (π£ βͺ {β¨π, πβ©}))βπ β (0..^(π + 1))((πΏβπ)β(πβπ)) = Ξ£π β (1...π)Ξ£π β ((1...π)(reprβπ)(π β π))(βπ β (0..^π)((πΏβπ)β(πβπ)) Β· ((πΏβπ)βπ))) |
172 | 8, 82, 171 | 3eqtrd 2777 |
1
β’ (π β Ξ£π β ((1...π)(reprβ(π + 1))π)βπ β (0..^(π + 1))((πΏβπ)β(πβπ)) = Ξ£π β (1...π)Ξ£π β ((1...π)(reprβπ)(π β π))(βπ β (0..^π)((πΏβπ)β(πβπ)) Β· ((πΏβπ)βπ))) |