Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . . . 5
β’ (π β π β β) |
2 | 1 | adantr 482 |
. . . 4
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
π β
β) |
3 | | poimirlem22.s |
. . . 4
β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} |
4 | | poimirlem22.1 |
. . . . 5
β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) |
5 | 4 | adantr 482 |
. . . 4
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) |
6 | | poimirlem22.2 |
. . . . 5
β’ (π β π β π) |
7 | 6 | adantr 482 |
. . . 4
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
π β π) |
8 | | simpr 486 |
. . . 4
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
(2nd βπ)
β (1...(π β
1))) |
9 | 2, 3, 5, 7, 8 | poimirlem15 36122 |
. . 3
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
β¨β¨(1st β(1st βπ)), ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))β©,
(2nd βπ)β© β π) |
10 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π‘ = π β (2nd βπ‘) = (2nd βπ)) |
11 | 10 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π‘ = π β (π¦ < (2nd βπ‘) β π¦ < (2nd βπ))) |
12 | 11 | ifbid 4514 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π‘ = π β if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) = if(π¦ < (2nd βπ), π¦, (π¦ + 1))) |
13 | 12 | csbeq1d 3864 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π‘ = π β β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))) = β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0})))) |
14 | | 2fveq3 6852 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π‘ = π β (1st
β(1st βπ‘)) = (1st β(1st
βπ))) |
15 | | 2fveq3 6852 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π‘ = π β (2nd
β(1st βπ‘)) = (2nd β(1st
βπ))) |
16 | 15 | imaeq1d 6017 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π‘ = π β ((2nd
β(1st βπ‘)) β (1...π)) = ((2nd β(1st
βπ)) β
(1...π))) |
17 | 16 | xpeq1d 5667 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π‘ = π β (((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) = (((2nd
β(1st βπ)) β (1...π)) Γ {1})) |
18 | 15 | imaeq1d 6017 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π‘ = π β ((2nd
β(1st βπ‘)) β ((π + 1)...π)) = ((2nd β(1st
βπ)) β ((π + 1)...π))) |
19 | 18 | xpeq1d 5667 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π‘ = π β (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}) = (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0})) |
20 | 17, 19 | uneq12d 4129 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π‘ = π β ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0})) = ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))) |
21 | 14, 20 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π‘ = π β ((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))) = ((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0})))) |
22 | 21 | csbeq2dv 3867 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π‘ = π β β¦if(π¦ < (2nd βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))) = β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0})))) |
23 | 13, 22 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π‘ = π β β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))) = β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0})))) |
24 | 23 | mpteq2dv 5212 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ = π β (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0})))) = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))))) |
25 | 24 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ = π β (πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0})))) β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0})))))) |
26 | 25, 3 | elrab2 3653 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β (π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β§ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0})))))) |
27 | 26 | simprbi 498 |
. . . . . . . . . . . . . . . 16
β’ (π β π β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))))) |
28 | 6, 27 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))))) |
29 | 28 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))))) |
30 | | elrabi 3644 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} β π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π))) |
31 | 30, 3 | eleq2s 2856 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π))) |
32 | 6, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π))) |
33 | | xp1st 7958 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β (1st βπ) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1st
βπ) β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
35 | | xp1st 7958 |
. . . . . . . . . . . . . . . . . 18
β’
((1st βπ) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β (1st
β(1st βπ)) β ((0..^πΎ) βm (1...π))) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1st
β(1st βπ)) β ((0..^πΎ) βm (1...π))) |
37 | | elmapi 8794 |
. . . . . . . . . . . . . . . . 17
β’
((1st β(1st βπ)) β ((0..^πΎ) βm (1...π)) β (1st
β(1st βπ)):(1...π)βΆ(0..^πΎ)) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (1st
β(1st βπ)):(1...π)βΆ(0..^πΎ)) |
39 | | elfzoelz 13579 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0..^πΎ) β π β β€) |
40 | 39 | ssriv 3953 |
. . . . . . . . . . . . . . . 16
β’
(0..^πΎ) β
β€ |
41 | | fss 6690 |
. . . . . . . . . . . . . . . 16
β’
(((1st β(1st βπ)):(1...π)βΆ(0..^πΎ) β§ (0..^πΎ) β β€) β (1st
β(1st βπ)):(1...π)βΆβ€) |
42 | 38, 40, 41 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ (π β (1st
β(1st βπ)):(1...π)βΆβ€) |
43 | 42 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
(1st β(1st βπ)):(1...π)βΆβ€) |
44 | | xp2nd 7959 |
. . . . . . . . . . . . . . . . 17
β’
((1st βπ) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β (2nd
β(1st βπ)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
45 | 34, 44 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (2nd
β(1st βπ)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
46 | | fvex 6860 |
. . . . . . . . . . . . . . . . 17
β’
(2nd β(1st βπ)) β V |
47 | | f1oeq1 6777 |
. . . . . . . . . . . . . . . . 17
β’ (π = (2nd
β(1st βπ)) β (π:(1...π)β1-1-ontoβ(1...π) β (2nd
β(1st βπ)):(1...π)β1-1-ontoβ(1...π))) |
48 | 46, 47 | elab 3635 |
. . . . . . . . . . . . . . . 16
β’
((2nd β(1st βπ)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)} β (2nd
β(1st βπ)):(1...π)β1-1-ontoβ(1...π)) |
49 | 45, 48 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (π β (2nd
β(1st βπ)):(1...π)β1-1-ontoβ(1...π)) |
50 | 49 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
(2nd β(1st βπ)):(1...π)β1-1-ontoβ(1...π)) |
51 | 2, 29, 43, 50, 8 | poimirlem1 36108 |
. . . . . . . . . . . . 13
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
Β¬ β*π β
(1...π)((πΉβ((2nd βπ) β 1))βπ) β ((πΉβ(2nd βπ))βπ)) |
52 | 51 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β Β¬ β*π β (1...π)((πΉβ((2nd βπ) β 1))βπ) β ((πΉβ(2nd βπ))βπ)) |
53 | 1 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β§ (2nd βπ§) β (2nd
βπ)) β π β
β) |
54 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π‘ = π§ β (2nd βπ‘) = (2nd βπ§)) |
55 | 54 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π‘ = π§ β (π¦ < (2nd βπ‘) β π¦ < (2nd βπ§))) |
56 | 55 | ifbid 4514 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π‘ = π§ β if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) = if(π¦ < (2nd βπ§), π¦, (π¦ + 1))) |
57 | 56 | csbeq1d 3864 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π‘ = π§ β β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))) = β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0})))) |
58 | | 2fveq3 6852 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π‘ = π§ β (1st
β(1st βπ‘)) = (1st β(1st
βπ§))) |
59 | | 2fveq3 6852 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π‘ = π§ β (2nd
β(1st βπ‘)) = (2nd β(1st
βπ§))) |
60 | 59 | imaeq1d 6017 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π‘ = π§ β ((2nd
β(1st βπ‘)) β (1...π)) = ((2nd β(1st
βπ§)) β
(1...π))) |
61 | 60 | xpeq1d 5667 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π‘ = π§ β (((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) = (((2nd
β(1st βπ§)) β (1...π)) Γ {1})) |
62 | 59 | imaeq1d 6017 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π‘ = π§ β ((2nd
β(1st βπ‘)) β ((π + 1)...π)) = ((2nd β(1st
βπ§)) β ((π + 1)...π))) |
63 | 62 | xpeq1d 5667 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π‘ = π§ β (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}) = (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0})) |
64 | 61, 63 | uneq12d 4129 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π‘ = π§ β ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0})) = ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0}))) |
65 | 58, 64 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π‘ = π§ β ((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))) = ((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0})))) |
66 | 65 | csbeq2dv 3867 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π‘ = π§ β β¦if(π¦ < (2nd βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))) = β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0})))) |
67 | 57, 66 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π‘ = π§ β β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))) = β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0})))) |
68 | 67 | mpteq2dv 5212 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ = π§ β (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0})))) = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0}))))) |
69 | 68 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ = π§ β (πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0})))) β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0})))))) |
70 | 69, 3 | elrab2 3653 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β π β (π§ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β§ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0})))))) |
71 | 70 | simprbi 498 |
. . . . . . . . . . . . . . . 16
β’ (π§ β π β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0}))))) |
72 | 71 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β§ (2nd βπ§) β (2nd
βπ)) β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0}))))) |
73 | | elrabi 3644 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π§ β {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} β π§ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π))) |
74 | 73, 3 | eleq2s 2856 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ β π β π§ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π))) |
75 | | xp1st 7958 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β (1st βπ§) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β π β (1st βπ§) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
77 | | xp1st 7958 |
. . . . . . . . . . . . . . . . . . 19
β’
((1st βπ§) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β (1st
β(1st βπ§)) β ((0..^πΎ) βm (1...π))) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β π β (1st
β(1st βπ§)) β ((0..^πΎ) βm (1...π))) |
79 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . 18
β’
((1st β(1st βπ§)) β ((0..^πΎ) βm (1...π)) β (1st
β(1st βπ§)):(1...π)βΆ(0..^πΎ)) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β π β (1st
β(1st βπ§)):(1...π)βΆ(0..^πΎ)) |
81 | | fss 6690 |
. . . . . . . . . . . . . . . . 17
β’
(((1st β(1st βπ§)):(1...π)βΆ(0..^πΎ) β§ (0..^πΎ) β β€) β (1st
β(1st βπ§)):(1...π)βΆβ€) |
82 | 80, 40, 81 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ (π§ β π β (1st
β(1st βπ§)):(1...π)βΆβ€) |
83 | 82 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β§ (2nd βπ§) β (2nd
βπ)) β
(1st β(1st βπ§)):(1...π)βΆβ€) |
84 | | xp2nd 7959 |
. . . . . . . . . . . . . . . . . 18
β’
((1st βπ§) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β (2nd
β(1st βπ§)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
85 | 76, 84 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β π β (2nd
β(1st βπ§)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
86 | | fvex 6860 |
. . . . . . . . . . . . . . . . . 18
β’
(2nd β(1st βπ§)) β V |
87 | | f1oeq1 6777 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (2nd
β(1st βπ§)) β (π:(1...π)β1-1-ontoβ(1...π) β (2nd
β(1st βπ§)):(1...π)β1-1-ontoβ(1...π))) |
88 | 86, 87 | elab 3635 |
. . . . . . . . . . . . . . . . 17
β’
((2nd β(1st βπ§)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)} β (2nd
β(1st βπ§)):(1...π)β1-1-ontoβ(1...π)) |
89 | 85, 88 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ (π§ β π β (2nd
β(1st βπ§)):(1...π)β1-1-ontoβ(1...π)) |
90 | 89 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β§ (2nd βπ§) β (2nd
βπ)) β
(2nd β(1st βπ§)):(1...π)β1-1-ontoβ(1...π)) |
91 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β§ (2nd βπ§) β (2nd
βπ)) β
(2nd βπ)
β (1...(π β
1))) |
92 | | xp2nd 7959 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β (2nd βπ§) β (0...π)) |
93 | 74, 92 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β π β (2nd βπ§) β (0...π)) |
94 | 93 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β (2nd βπ§) β (0...π)) |
95 | | eldifsn 4752 |
. . . . . . . . . . . . . . . . 17
β’
((2nd βπ§) β ((0...π) β {(2nd βπ)}) β ((2nd
βπ§) β (0...π) β§ (2nd
βπ§) β
(2nd βπ))) |
96 | 95 | biimpri 227 |
. . . . . . . . . . . . . . . 16
β’
(((2nd βπ§) β (0...π) β§ (2nd βπ§) β (2nd
βπ)) β
(2nd βπ§)
β ((0...π) β
{(2nd βπ)})) |
97 | 94, 96 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β§ (2nd βπ§) β (2nd
βπ)) β
(2nd βπ§)
β ((0...π) β
{(2nd βπ)})) |
98 | 53, 72, 83, 90, 91, 97 | poimirlem2 36109 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β§ (2nd βπ§) β (2nd
βπ)) β
β*π β (1...π)((πΉβ((2nd βπ) β 1))βπ) β ((πΉβ(2nd βπ))βπ)) |
99 | 98 | ex 414 |
. . . . . . . . . . . . 13
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β ((2nd βπ§) β (2nd
βπ) β
β*π β (1...π)((πΉβ((2nd βπ) β 1))βπ) β ((πΉβ(2nd βπ))βπ))) |
100 | 99 | necon1bd 2962 |
. . . . . . . . . . . 12
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β (Β¬ β*π β (1...π)((πΉβ((2nd βπ) β 1))βπ) β ((πΉβ(2nd βπ))βπ) β (2nd βπ§) = (2nd βπ))) |
101 | 52, 100 | mpd 15 |
. . . . . . . . . . 11
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β (2nd βπ§) = (2nd βπ)) |
102 | | eleq1 2826 |
. . . . . . . . . . . . . . . 16
β’
((2nd βπ§) = (2nd βπ) β ((2nd βπ§) β (1...(π β 1)) β (2nd
βπ) β
(1...(π β
1)))) |
103 | 102 | biimparc 481 |
. . . . . . . . . . . . . . 15
β’
(((2nd βπ) β (1...(π β 1)) β§ (2nd
βπ§) = (2nd
βπ)) β
(2nd βπ§)
β (1...(π β
1))) |
104 | 103 | anim2i 618 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((2nd
βπ) β
(1...(π β 1)) β§
(2nd βπ§) =
(2nd βπ)))
β (π β§
(2nd βπ§)
β (1...(π β
1)))) |
105 | 104 | anassrs 469 |
. . . . . . . . . . . . 13
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
(2nd βπ§) =
(2nd βπ))
β (π β§
(2nd βπ§)
β (1...(π β
1)))) |
106 | 71 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ (2nd
βπ§) β
(1...(π β 1))) β§
π§ β π) β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0}))))) |
107 | | breq1 5113 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = 0 β (π¦ < (2nd βπ§) β 0 < (2nd
βπ§))) |
108 | | id 22 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = 0 β π¦ = 0) |
109 | 107, 108 | ifbieq1d 4515 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = 0 β if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) = if(0 < (2nd
βπ§), 0, (π¦ + 1))) |
110 | | elfznn 13477 |
. . . . . . . . . . . . . . . . . . . 20
β’
((2nd βπ§) β (1...(π β 1)) β (2nd
βπ§) β
β) |
111 | 110 | nngt0d 12209 |
. . . . . . . . . . . . . . . . . . 19
β’
((2nd βπ§) β (1...(π β 1)) β 0 < (2nd
βπ§)) |
112 | 111 | iftrued 4499 |
. . . . . . . . . . . . . . . . . 18
β’
((2nd βπ§) β (1...(π β 1)) β if(0 <
(2nd βπ§),
0, (π¦ + 1)) =
0) |
113 | 112 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (2nd
βπ§) β
(1...(π β 1))) β§
π§ β π) β if(0 < (2nd
βπ§), 0, (π¦ + 1)) = 0) |
114 | 109, 113 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (2nd
βπ§) β
(1...(π β 1))) β§
π§ β π) β§ π¦ = 0) β if(π¦ < (2nd βπ§), π¦, (π¦ + 1)) = 0) |
115 | 114 | csbeq1d 3864 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (2nd
βπ§) β
(1...(π β 1))) β§
π§ β π) β§ π¦ = 0) β β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0}))) = β¦0 / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0})))) |
116 | | c0ex 11156 |
. . . . . . . . . . . . . . . . . 18
β’ 0 β
V |
117 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = 0 β (1...π) = (1...0)) |
118 | | fz10 13469 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (1...0) =
β
|
119 | 117, 118 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = 0 β (1...π) = β
) |
120 | 119 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = 0 β ((2nd
β(1st βπ§)) β (1...π)) = ((2nd β(1st
βπ§)) β
β
)) |
121 | 120 | xpeq1d 5667 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = 0 β (((2nd
β(1st βπ§)) β (1...π)) Γ {1}) = (((2nd
β(1st βπ§)) β β
) Γ
{1})) |
122 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = 0 β (π + 1) = (0 + 1)) |
123 | | 0p1e1 12282 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (0 + 1) =
1 |
124 | 122, 123 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = 0 β (π + 1) = 1) |
125 | 124 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = 0 β ((π + 1)...π) = (1...π)) |
126 | 125 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = 0 β ((2nd
β(1st βπ§)) β ((π + 1)...π)) = ((2nd β(1st
βπ§)) β
(1...π))) |
127 | 126 | xpeq1d 5667 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = 0 β (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0}) = (((2nd
β(1st βπ§)) β (1...π)) Γ {0})) |
128 | 121, 127 | uneq12d 4129 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 0 β ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0})) = ((((2nd
β(1st βπ§)) β β
) Γ {1}) βͺ
(((2nd β(1st βπ§)) β (1...π)) Γ {0}))) |
129 | | ima0 6034 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((2nd β(1st βπ§)) β β
) =
β
|
130 | 129 | xpeq1i 5664 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((2nd β(1st βπ§)) β β
) Γ {1}) = (β
Γ {1}) |
131 | | 0xp 5735 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β
Γ {1}) = β
|
132 | 130, 131 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((2nd β(1st βπ§)) β β
) Γ {1}) =
β
|
133 | 132 | uneq1i 4124 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((2nd β(1st βπ§)) β β
) Γ {1}) βͺ
(((2nd β(1st βπ§)) β (1...π)) Γ {0})) = (β
βͺ
(((2nd β(1st βπ§)) β (1...π)) Γ {0})) |
134 | | uncom 4118 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β
βͺ (((2nd β(1st βπ§)) β (1...π)) Γ {0})) = ((((2nd
β(1st βπ§)) β (1...π)) Γ {0}) βͺ
β
) |
135 | | un0 4355 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((2nd β(1st βπ§)) β (1...π)) Γ {0}) βͺ β
) =
(((2nd β(1st βπ§)) β (1...π)) Γ {0}) |
136 | 133, 134,
135 | 3eqtri 2769 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((2nd β(1st βπ§)) β β
) Γ {1}) βͺ
(((2nd β(1st βπ§)) β (1...π)) Γ {0})) = (((2nd
β(1st βπ§)) β (1...π)) Γ {0}) |
137 | 128, 136 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0})) = (((2nd
β(1st βπ§)) β (1...π)) Γ {0})) |
138 | 137 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β ((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0}))) = ((1st
β(1st βπ§)) βf + (((2nd
β(1st βπ§)) β (1...π)) Γ {0}))) |
139 | 116, 138 | csbie 3896 |
. . . . . . . . . . . . . . . . 17
β’
β¦0 / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0}))) = ((1st
β(1st βπ§)) βf + (((2nd
β(1st βπ§)) β (1...π)) Γ {0})) |
140 | | f1ofo 6796 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((2nd β(1st βπ§)):(1...π)β1-1-ontoβ(1...π) β (2nd
β(1st βπ§)):(1...π)βontoβ(1...π)) |
141 | 89, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π§ β π β (2nd
β(1st βπ§)):(1...π)βontoβ(1...π)) |
142 | | foima 6766 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((2nd β(1st βπ§)):(1...π)βontoβ(1...π) β ((2nd
β(1st βπ§)) β (1...π)) = (1...π)) |
143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ β π β ((2nd
β(1st βπ§)) β (1...π)) = (1...π)) |
144 | 143 | xpeq1d 5667 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β π β (((2nd
β(1st βπ§)) β (1...π)) Γ {0}) = ((1...π) Γ {0})) |
145 | 144 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β π β ((1st
β(1st βπ§)) βf + (((2nd
β(1st βπ§)) β (1...π)) Γ {0})) = ((1st
β(1st βπ§)) βf + ((1...π) Γ
{0}))) |
146 | | ovexd 7397 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β π β (1...π) β V) |
147 | 80 | ffnd 6674 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β π β (1st
β(1st βπ§)) Fn (1...π)) |
148 | | fnconstg 6735 |
. . . . . . . . . . . . . . . . . . . 20
β’ (0 β
V β ((1...π) Γ
{0}) Fn (1...π)) |
149 | 116, 148 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β π β ((1...π) Γ {0}) Fn (1...π)) |
150 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π§ β π β§ π β (1...π)) β ((1st
β(1st βπ§))βπ) = ((1st β(1st
βπ§))βπ)) |
151 | 116 | fvconst2 7158 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...π) β (((1...π) Γ {0})βπ) = 0) |
152 | 151 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π§ β π β§ π β (1...π)) β (((1...π) Γ {0})βπ) = 0) |
153 | 80 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π§ β π β§ π β (1...π)) β ((1st
β(1st βπ§))βπ) β (0..^πΎ)) |
154 | | elfzonn0 13624 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((1st β(1st βπ§))βπ) β (0..^πΎ) β ((1st
β(1st βπ§))βπ) β
β0) |
155 | 153, 154 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π§ β π β§ π β (1...π)) β ((1st
β(1st βπ§))βπ) β
β0) |
156 | 155 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π§ β π β§ π β (1...π)) β ((1st
β(1st βπ§))βπ) β β) |
157 | 156 | addid1d 11362 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π§ β π β§ π β (1...π)) β (((1st
β(1st βπ§))βπ) + 0) = ((1st
β(1st βπ§))βπ)) |
158 | 146, 147,
149, 147, 150, 152, 157 | offveq 7646 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β π β ((1st
β(1st βπ§)) βf + ((1...π) Γ {0})) =
(1st β(1st βπ§))) |
159 | 145, 158 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β π β ((1st
β(1st βπ§)) βf + (((2nd
β(1st βπ§)) β (1...π)) Γ {0})) = (1st
β(1st βπ§))) |
160 | 139, 159 | eqtrid 2789 |
. . . . . . . . . . . . . . . 16
β’ (π§ β π β β¦0 / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0}))) = (1st
β(1st βπ§))) |
161 | 160 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (2nd
βπ§) β
(1...(π β 1))) β§
π§ β π) β§ π¦ = 0) β β¦0 / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0}))) = (1st
β(1st βπ§))) |
162 | 115, 161 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (2nd
βπ§) β
(1...(π β 1))) β§
π§ β π) β§ π¦ = 0) β β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0}))) = (1st
β(1st βπ§))) |
163 | | nnm1nn0 12461 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (π β 1) β
β0) |
164 | 1, 163 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β 1) β
β0) |
165 | | 0elfz 13545 |
. . . . . . . . . . . . . . . 16
β’ ((π β 1) β
β0 β 0 β (0...(π β 1))) |
166 | 164, 165 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β 0 β (0...(π β 1))) |
167 | 166 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (2nd
βπ§) β
(1...(π β 1))) β§
π§ β π) β 0 β (0...(π β 1))) |
168 | | fvexd 6862 |
. . . . . . . . . . . . . 14
β’ (((π β§ (2nd
βπ§) β
(1...(π β 1))) β§
π§ β π) β (1st
β(1st βπ§)) β V) |
169 | 106, 162,
167, 168 | fvmptd 6960 |
. . . . . . . . . . . . 13
β’ (((π β§ (2nd
βπ§) β
(1...(π β 1))) β§
π§ β π) β (πΉβ0) = (1st
β(1st βπ§))) |
170 | 105, 169 | sylan 581 |
. . . . . . . . . . . 12
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
(2nd βπ§) =
(2nd βπ))
β§ π§ β π) β (πΉβ0) = (1st
β(1st βπ§))) |
171 | 170 | an32s 651 |
. . . . . . . . . . 11
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β§ (2nd βπ§) = (2nd βπ)) β (πΉβ0) = (1st
β(1st βπ§))) |
172 | 101, 171 | mpdan 686 |
. . . . . . . . . 10
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β (πΉβ0) = (1st
β(1st βπ§))) |
173 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π β (2nd βπ§) = (2nd βπ)) |
174 | 173 | eleq1d 2823 |
. . . . . . . . . . . . . . 15
β’ (π§ = π β ((2nd βπ§) β (1...(π β 1)) β (2nd
βπ) β
(1...(π β
1)))) |
175 | 174 | anbi2d 630 |
. . . . . . . . . . . . . 14
β’ (π§ = π β ((π β§ (2nd βπ§) β (1...(π β 1))) β (π β§ (2nd βπ) β (1...(π β 1))))) |
176 | | 2fveq3 6852 |
. . . . . . . . . . . . . . 15
β’ (π§ = π β (1st
β(1st βπ§)) = (1st β(1st
βπ))) |
177 | 176 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
β’ (π§ = π β ((πΉβ0) = (1st
β(1st βπ§)) β (πΉβ0) = (1st
β(1st βπ)))) |
178 | 175, 177 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π§ = π β (((π β§ (2nd βπ§) β (1...(π β 1))) β (πΉβ0) = (1st
β(1st βπ§))) β ((π β§ (2nd βπ) β (1...(π β 1))) β (πΉβ0) = (1st
β(1st βπ))))) |
179 | 169 | expcom 415 |
. . . . . . . . . . . . 13
β’ (π§ β π β ((π β§ (2nd βπ§) β (1...(π β 1))) β (πΉβ0) = (1st
β(1st βπ§)))) |
180 | 178, 179 | vtoclga 3537 |
. . . . . . . . . . . 12
β’ (π β π β ((π β§ (2nd βπ) β (1...(π β 1))) β (πΉβ0) = (1st
β(1st βπ)))) |
181 | 7, 180 | mpcom 38 |
. . . . . . . . . . 11
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
(πΉβ0) =
(1st β(1st βπ))) |
182 | 181 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β (πΉβ0) = (1st
β(1st βπ))) |
183 | 172, 182 | eqtr3d 2779 |
. . . . . . . . 9
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β (1st
β(1st βπ§)) = (1st β(1st
βπ))) |
184 | 183 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β§ π§ β π) β (1st
β(1st βπ§)) = (1st β(1st
βπ))) |
185 | 1 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β§ π§ β π) β π β β) |
186 | 6 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β§ π§ β π) β π β π) |
187 | | simpllr 775 |
. . . . . . . . 9
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β§ π§ β π) β (2nd βπ) β (1...(π β 1))) |
188 | | simplr 768 |
. . . . . . . . 9
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β§ π§ β π) β π§ β π) |
189 | 34 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
(1st βπ)
β (((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
190 | | xpopth 7967 |
. . . . . . . . . . . . . 14
β’
(((1st βπ§) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β§ (1st βπ) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) β (((1st
β(1st βπ§)) = (1st β(1st
βπ)) β§
(2nd β(1st βπ§)) = (2nd β(1st
βπ))) β
(1st βπ§) =
(1st βπ))) |
191 | 76, 189, 190 | syl2anr 598 |
. . . . . . . . . . . . 13
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β (((1st
β(1st βπ§)) = (1st β(1st
βπ)) β§
(2nd β(1st βπ§)) = (2nd β(1st
βπ))) β
(1st βπ§) =
(1st βπ))) |
192 | 32 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π))) |
193 | | xpopth 7967 |
. . . . . . . . . . . . . . . 16
β’ ((π§ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β§ π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π))) β (((1st βπ§) = (1st βπ) β§ (2nd
βπ§) = (2nd
βπ)) β π§ = π)) |
194 | 193 | biimpd 228 |
. . . . . . . . . . . . . . 15
β’ ((π§ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β§ π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π))) β (((1st βπ§) = (1st βπ) β§ (2nd
βπ§) = (2nd
βπ)) β π§ = π)) |
195 | 74, 192, 194 | syl2anr 598 |
. . . . . . . . . . . . . 14
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β (((1st βπ§) = (1st βπ) β§ (2nd
βπ§) = (2nd
βπ)) β π§ = π)) |
196 | 101, 195 | mpan2d 693 |
. . . . . . . . . . . . 13
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β ((1st βπ§) = (1st βπ) β π§ = π)) |
197 | 191, 196 | sylbid 239 |
. . . . . . . . . . . 12
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β (((1st
β(1st βπ§)) = (1st β(1st
βπ)) β§
(2nd β(1st βπ§)) = (2nd β(1st
βπ))) β π§ = π)) |
198 | 183, 197 | mpand 694 |
. . . . . . . . . . 11
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β ((2nd
β(1st βπ§)) = (2nd β(1st
βπ)) β π§ = π)) |
199 | 198 | necon3d 2965 |
. . . . . . . . . 10
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β (π§ β π β (2nd
β(1st βπ§)) β (2nd
β(1st βπ)))) |
200 | 199 | imp 408 |
. . . . . . . . 9
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β§ π§ β π) β (2nd
β(1st βπ§)) β (2nd
β(1st βπ))) |
201 | 185, 3, 186, 187, 188, 200 | poimirlem9 36116 |
. . . . . . . 8
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β§ π§ β π) β (2nd
β(1st βπ§)) = ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) +
1)}))))) |
202 | 101 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β§ π§ β π) β (2nd βπ§) = (2nd βπ)) |
203 | 184, 201,
202 | jca31 516 |
. . . . . . 7
β’ ((((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β§ π§ β π) β (((1st
β(1st βπ§)) = (1st β(1st
βπ)) β§
(2nd β(1st βπ§)) = ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))) β§
(2nd βπ§) =
(2nd βπ))) |
204 | 203 | ex 414 |
. . . . . 6
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β (π§ β π β (((1st
β(1st βπ§)) = (1st β(1st
βπ)) β§
(2nd β(1st βπ§)) = ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))) β§
(2nd βπ§) =
(2nd βπ)))) |
205 | | simplr 768 |
. . . . . . . 8
β’
((((1st β(1st βπ§)) = (1st β(1st
βπ)) β§
(2nd β(1st βπ§)) = ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))) β§
(2nd βπ§) =
(2nd βπ))
β (2nd β(1st βπ§)) = ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) +
1)}))))) |
206 | | elfznn 13477 |
. . . . . . . . . . . . . 14
β’
((2nd βπ) β (1...(π β 1)) β (2nd
βπ) β
β) |
207 | 206 | nnred 12175 |
. . . . . . . . . . . . 13
β’
((2nd βπ) β (1...(π β 1)) β (2nd
βπ) β
β) |
208 | 207 | ltp1d 12092 |
. . . . . . . . . . . . 13
β’
((2nd βπ) β (1...(π β 1)) β (2nd
βπ) <
((2nd βπ)
+ 1)) |
209 | 207, 208 | ltned 11298 |
. . . . . . . . . . . 12
β’
((2nd βπ) β (1...(π β 1)) β (2nd
βπ) β
((2nd βπ)
+ 1)) |
210 | 209 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
(2nd βπ)
β ((2nd βπ) + 1)) |
211 | | fveq1 6846 |
. . . . . . . . . . . . 13
β’
((2nd β(1st βπ)) = ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)})))) β
((2nd β(1st βπ))β(2nd βπ)) = (((2nd
β(1st βπ)) β ({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)}))))β(2nd βπ))) |
212 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((2nd βπ) β β β (2nd
βπ) β
β) |
213 | | ltp1 12002 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((2nd βπ) β β β (2nd
βπ) <
((2nd βπ)
+ 1)) |
214 | 212, 213 | ltned 11298 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((2nd βπ) β β β (2nd
βπ) β
((2nd βπ)
+ 1)) |
215 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(2nd βπ) β V |
216 | | ovex 7395 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((2nd βπ) + 1) β V |
217 | 215, 216,
216, 215 | fpr 7105 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((2nd βπ) β ((2nd βπ) + 1) β
{β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©}:{(2nd βπ), ((2nd βπ) + 1)}βΆ{((2nd
βπ) + 1),
(2nd βπ)}) |
218 | 214, 217 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
((2nd βπ) β β β
{β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©}:{(2nd βπ), ((2nd βπ) + 1)}βΆ{((2nd
βπ) + 1),
(2nd βπ)}) |
219 | | f1oi 6827 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ( I
βΎ ((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})):((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})β1-1-ontoβ((1...π) β {(2nd βπ), ((2nd βπ) + 1)}) |
220 | | f1of 6789 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (( I
βΎ ((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})):((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})β1-1-ontoβ((1...π) β {(2nd βπ), ((2nd βπ) + 1)}) β ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})):((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})βΆ((1...π)
β {(2nd βπ), ((2nd βπ) + 1)})) |
221 | 219, 220 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’ ( I
βΎ ((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})):((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})βΆ((1...π)
β {(2nd βπ), ((2nd βπ) + 1)}) |
222 | | disjdif 4436 |
. . . . . . . . . . . . . . . . . . . . 21
β’
({(2nd βπ), ((2nd βπ) + 1)} β© ((1...π) β {(2nd βπ), ((2nd βπ) + 1)})) =
β
|
223 | | fun 6709 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©}:{(2nd βπ), ((2nd βπ) + 1)}βΆ{((2nd
βπ) + 1),
(2nd βπ)}
β§ ( I βΎ ((1...π)
β {(2nd βπ), ((2nd βπ) + 1)})):((1...π) β {(2nd βπ), ((2nd βπ) + 1)})βΆ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)})) β§
({(2nd βπ), ((2nd βπ) + 1)} β© ((1...π) β {(2nd βπ), ((2nd βπ) + 1)})) = β
) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) +
1)}))):({(2nd βπ), ((2nd βπ) + 1)} βͺ ((1...π) β {(2nd βπ), ((2nd βπ) +
1)}))βΆ({((2nd βπ) + 1), (2nd βπ)} βͺ ((1...π) β {(2nd βπ), ((2nd βπ) + 1)}))) |
224 | 222, 223 | mpan2 690 |
. . . . . . . . . . . . . . . . . . . 20
β’
(({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©}:{(2nd βπ), ((2nd βπ) + 1)}βΆ{((2nd
βπ) + 1),
(2nd βπ)}
β§ ( I βΎ ((1...π)
β {(2nd βπ), ((2nd βπ) + 1)})):((1...π) β {(2nd βπ), ((2nd βπ) + 1)})βΆ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)})) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) +
1)}))):({(2nd βπ), ((2nd βπ) + 1)} βͺ ((1...π) β {(2nd βπ), ((2nd βπ) +
1)}))βΆ({((2nd βπ) + 1), (2nd βπ)} βͺ ((1...π) β {(2nd βπ), ((2nd βπ) + 1)}))) |
225 | 218, 221,
224 | sylancl 587 |
. . . . . . . . . . . . . . . . . . 19
β’
((2nd βπ) β β β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) +
1)}))):({(2nd βπ), ((2nd βπ) + 1)} βͺ ((1...π) β {(2nd βπ), ((2nd βπ) +
1)}))βΆ({((2nd βπ) + 1), (2nd βπ)} βͺ ((1...π) β {(2nd βπ), ((2nd βπ) + 1)}))) |
226 | 215 | prid1 4728 |
. . . . . . . . . . . . . . . . . . . 20
β’
(2nd βπ) β {(2nd βπ), ((2nd βπ) + 1)} |
227 | | elun1 4141 |
. . . . . . . . . . . . . . . . . . . 20
β’
((2nd βπ) β {(2nd βπ), ((2nd βπ) + 1)} β (2nd
βπ) β
({(2nd βπ), ((2nd βπ) + 1)} βͺ ((1...π) β {(2nd βπ), ((2nd βπ) + 1)}))) |
228 | 226, 227 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’
(2nd βπ) β ({(2nd βπ), ((2nd βπ) + 1)} βͺ ((1...π) β {(2nd
βπ), ((2nd
βπ) +
1)})) |
229 | | fvco3 6945 |
. . . . . . . . . . . . . . . . . . 19
β’
((({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) +
1)}))):({(2nd βπ), ((2nd βπ) + 1)} βͺ ((1...π) β {(2nd βπ), ((2nd βπ) +
1)}))βΆ({((2nd βπ) + 1), (2nd βπ)} βͺ ((1...π) β {(2nd βπ), ((2nd βπ) + 1)})) β§ (2nd
βπ) β
({(2nd βπ), ((2nd βπ) + 1)} βͺ ((1...π) β {(2nd βπ), ((2nd βπ) + 1)}))) β
(((2nd β(1st βπ)) β ({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)}))))β(2nd βπ)) = ((2nd β(1st
βπ))β(({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})))β(2nd βπ)))) |
230 | 225, 228,
229 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
β’
((2nd βπ) β β β (((2nd
β(1st βπ)) β ({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)}))))β(2nd βπ)) = ((2nd β(1st
βπ))β(({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})))β(2nd βπ)))) |
231 | 218 | ffnd 6674 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((2nd βπ) β β β
{β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} Fn {(2nd βπ), ((2nd βπ) + 1)}) |
232 | | fnresi 6635 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ( I
βΎ ((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})) Fn ((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)}) |
233 | 222, 226 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(({(2nd βπ), ((2nd βπ) + 1)} β© ((1...π) β {(2nd βπ), ((2nd βπ) + 1)})) = β
β§
(2nd βπ)
β {(2nd βπ), ((2nd βπ) + 1)}) |
234 | | fvun1 6937 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} Fn {(2nd βπ), ((2nd βπ) + 1)} β§ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})) Fn ((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)}) β§ (({(2nd βπ), ((2nd βπ) + 1)} β© ((1...π) β {(2nd βπ), ((2nd βπ) + 1)})) = β
β§
(2nd βπ)
β {(2nd βπ), ((2nd βπ) + 1)})) β (({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})))β(2nd βπ)) = ({β¨(2nd βπ), ((2nd βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©}β(2nd
βπ))) |
235 | 232, 233,
234 | mp3an23 1454 |
. . . . . . . . . . . . . . . . . . . . 21
β’
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} Fn {(2nd βπ), ((2nd βπ) + 1)} β
(({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) +
1)})))β(2nd βπ)) = ({β¨(2nd βπ), ((2nd βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©}β(2nd
βπ))) |
236 | 231, 235 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
((2nd βπ) β β β
(({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) +
1)})))β(2nd βπ)) = ({β¨(2nd βπ), ((2nd βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©}β(2nd
βπ))) |
237 | 215, 216 | fvpr1 7144 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((2nd βπ) β ((2nd βπ) + 1) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©}β(2nd βπ)) = ((2nd
βπ) +
1)) |
238 | 214, 237 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
((2nd βπ) β β β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©}β(2nd βπ)) = ((2nd
βπ) +
1)) |
239 | 236, 238 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
β’
((2nd βπ) β β β
(({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) +
1)})))β(2nd βπ)) = ((2nd βπ) + 1)) |
240 | 239 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . 18
β’
((2nd βπ) β β β ((2nd
β(1st βπ))β(({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})))β(2nd βπ))) = ((2nd
β(1st βπ))β((2nd βπ) + 1))) |
241 | 230, 240 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’
((2nd βπ) β β β (((2nd
β(1st βπ)) β ({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)}))))β(2nd βπ)) = ((2nd β(1st
βπ))β((2nd βπ) + 1))) |
242 | 207, 241 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
((2nd βπ) β (1...(π β 1)) β (((2nd
β(1st βπ)) β ({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)}))))β(2nd βπ)) = ((2nd β(1st
βπ))β((2nd βπ) + 1))) |
243 | 242 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
β’
((2nd βπ) β (1...(π β 1)) β (((2nd
β(1st βπ))β(2nd βπ)) = (((2nd
β(1st βπ)) β ({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)}))))β(2nd βπ)) β ((2nd
β(1st βπ))β(2nd βπ)) = ((2nd
β(1st βπ))β((2nd βπ) + 1)))) |
244 | 243 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
(((2nd β(1st βπ))β(2nd βπ)) = (((2nd
β(1st βπ)) β ({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)}))))β(2nd βπ)) β ((2nd
β(1st βπ))β(2nd βπ)) = ((2nd
β(1st βπ))β((2nd βπ) + 1)))) |
245 | | f1of1 6788 |
. . . . . . . . . . . . . . . . 17
β’
((2nd β(1st βπ)):(1...π)β1-1-ontoβ(1...π) β (2nd
β(1st βπ)):(1...π)β1-1β(1...π)) |
246 | 49, 245 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (2nd
β(1st βπ)):(1...π)β1-1β(1...π)) |
247 | 246 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
(2nd β(1st βπ)):(1...π)β1-1β(1...π)) |
248 | 1 | nncnd 12176 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β β) |
249 | | npcan1 11587 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β ((π β 1) + 1) = π) |
250 | 248, 249 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((π β 1) + 1) = π) |
251 | 164 | nn0zd 12532 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β 1) β β€) |
252 | | uzid 12785 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β 1) β β€
β (π β 1) β
(β€β₯β(π β 1))) |
253 | 251, 252 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π β 1) β
(β€β₯β(π β 1))) |
254 | | peano2uz 12833 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β 1) β
(β€β₯β(π β 1)) β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
255 | 253, 254 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
256 | 250, 255 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β (β€β₯β(π β 1))) |
257 | | fzss2 13488 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯β(π β 1)) β (1...(π β 1)) β (1...π)) |
258 | 256, 257 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...(π β 1)) β (1...π)) |
259 | 258 | sselda 3949 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
(2nd βπ)
β (1...π)) |
260 | | fzp1elp1 13501 |
. . . . . . . . . . . . . . . . 17
β’
((2nd βπ) β (1...(π β 1)) β ((2nd
βπ) + 1) β
(1...((π β 1) +
1))) |
261 | 260 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
((2nd βπ)
+ 1) β (1...((π
β 1) + 1))) |
262 | 250 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...((π β 1) + 1)) = (1...π)) |
263 | 262 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
(1...((π β 1) + 1)) =
(1...π)) |
264 | 261, 263 | eleqtrd 2840 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
((2nd βπ)
+ 1) β (1...π)) |
265 | | f1veqaeq 7209 |
. . . . . . . . . . . . . . 15
β’
(((2nd β(1st βπ)):(1...π)β1-1β(1...π) β§ ((2nd βπ) β (1...π) β§ ((2nd βπ) + 1) β (1...π))) β (((2nd
β(1st βπ))β(2nd βπ)) = ((2nd
β(1st βπ))β((2nd βπ) + 1)) β (2nd
βπ) =
((2nd βπ)
+ 1))) |
266 | 247, 259,
264, 265 | syl12anc 836 |
. . . . . . . . . . . . . 14
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
(((2nd β(1st βπ))β(2nd βπ)) = ((2nd
β(1st βπ))β((2nd βπ) + 1)) β (2nd
βπ) =
((2nd βπ)
+ 1))) |
267 | 244, 266 | sylbid 239 |
. . . . . . . . . . . . 13
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
(((2nd β(1st βπ))β(2nd βπ)) = (((2nd
β(1st βπ)) β ({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)}))))β(2nd βπ)) β (2nd βπ) = ((2nd
βπ) +
1))) |
268 | 211, 267 | syl5 34 |
. . . . . . . . . . . 12
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
((2nd β(1st βπ)) = ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)})))) β
(2nd βπ) =
((2nd βπ)
+ 1))) |
269 | 268 | necon3d 2965 |
. . . . . . . . . . 11
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
((2nd βπ)
β ((2nd βπ) + 1) β (2nd
β(1st βπ)) β ((2nd
β(1st βπ)) β ({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})))))) |
270 | 210, 269 | mpd 15 |
. . . . . . . . . 10
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
(2nd β(1st βπ)) β ((2nd
β(1st βπ)) β ({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)}))))) |
271 | | 2fveq3 6852 |
. . . . . . . . . . 11
β’ (π§ = π β (2nd
β(1st βπ§)) = (2nd β(1st
βπ))) |
272 | 271 | neeq1d 3004 |
. . . . . . . . . 10
β’ (π§ = π β ((2nd
β(1st βπ§)) β ((2nd
β(1st βπ)) β ({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})))) β (2nd β(1st βπ)) β ((2nd
β(1st βπ)) β ({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})))))) |
273 | 270, 272 | syl5ibrcom 247 |
. . . . . . . . 9
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
(π§ = π β (2nd
β(1st βπ§)) β ((2nd
β(1st βπ)) β ({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)})))))) |
274 | 273 | necon2d 2967 |
. . . . . . . 8
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
((2nd β(1st βπ§)) = ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)})))) β
π§ β π)) |
275 | 205, 274 | syl5 34 |
. . . . . . 7
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
((((1st β(1st βπ§)) = (1st β(1st
βπ)) β§
(2nd β(1st βπ§)) = ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))) β§
(2nd βπ§) =
(2nd βπ))
β π§ β π)) |
276 | 275 | adantr 482 |
. . . . . 6
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β ((((1st
β(1st βπ§)) = (1st β(1st
βπ)) β§
(2nd β(1st βπ§)) = ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))) β§
(2nd βπ§) =
(2nd βπ))
β π§ β π)) |
277 | 204, 276 | impbid 211 |
. . . . 5
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β (π§ β π β (((1st
β(1st βπ§)) = (1st β(1st
βπ)) β§
(2nd β(1st βπ§)) = ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))) β§
(2nd βπ§) =
(2nd βπ)))) |
278 | | eqop 7968 |
. . . . . . . 8
β’ (π§ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β (π§ = β¨β¨(1st
β(1st βπ)), ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))β©,
(2nd βπ)β© β ((1st βπ§) = β¨(1st
β(1st βπ)), ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))β©
β§ (2nd βπ§) = (2nd βπ)))) |
279 | | eqop 7968 |
. . . . . . . . . 10
β’
((1st βπ§) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β ((1st βπ§) = β¨(1st
β(1st βπ)), ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))β©
β ((1st β(1st βπ§)) = (1st β(1st
βπ)) β§
(2nd β(1st βπ§)) = ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) +
1)}))))))) |
280 | 75, 279 | syl 17 |
. . . . . . . . 9
β’ (π§ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β ((1st βπ§) = β¨(1st
β(1st βπ)), ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))β©
β ((1st β(1st βπ§)) = (1st β(1st
βπ)) β§
(2nd β(1st βπ§)) = ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) +
1)}))))))) |
281 | 280 | anbi1d 631 |
. . . . . . . 8
β’ (π§ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β (((1st βπ§) = β¨(1st
β(1st βπ)), ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))β©
β§ (2nd βπ§) = (2nd βπ)) β (((1st
β(1st βπ§)) = (1st β(1st
βπ)) β§
(2nd β(1st βπ§)) = ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))) β§
(2nd βπ§) =
(2nd βπ)))) |
282 | 278, 281 | bitrd 279 |
. . . . . . 7
β’ (π§ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β (π§ = β¨β¨(1st
β(1st βπ)), ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))β©,
(2nd βπ)β© β (((1st
β(1st βπ§)) = (1st β(1st
βπ)) β§
(2nd β(1st βπ§)) = ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))) β§
(2nd βπ§) =
(2nd βπ)))) |
283 | 74, 282 | syl 17 |
. . . . . 6
β’ (π§ β π β (π§ = β¨β¨(1st
β(1st βπ)), ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))β©,
(2nd βπ)β© β (((1st
β(1st βπ§)) = (1st β(1st
βπ)) β§
(2nd β(1st βπ§)) = ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))) β§
(2nd βπ§) =
(2nd βπ)))) |
284 | 283 | adantl 483 |
. . . . 5
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β (π§ = β¨β¨(1st
β(1st βπ)), ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))β©,
(2nd βπ)β© β (((1st
β(1st βπ§)) = (1st β(1st
βπ)) β§
(2nd β(1st βπ§)) = ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))) β§
(2nd βπ§) =
(2nd βπ)))) |
285 | 277, 284 | bitr4d 282 |
. . . 4
β’ (((π β§ (2nd
βπ) β
(1...(π β 1))) β§
π§ β π) β (π§ β π β π§ = β¨β¨(1st
β(1st βπ)), ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))β©,
(2nd βπ)β©)) |
286 | 285 | ralrimiva 3144 |
. . 3
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
βπ§ β π (π§ β π β π§ = β¨β¨(1st
β(1st βπ)), ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))β©,
(2nd βπ)β©)) |
287 | | reu6i 3691 |
. . 3
β’
((β¨β¨(1st β(1st βπ)), ((2nd
β(1st βπ)) β ({β¨(2nd
βπ), ((2nd
βπ) + 1)β©,
β¨((2nd βπ) + 1), (2nd βπ)β©} βͺ ( I βΎ
((1...π) β
{(2nd βπ),
((2nd βπ)
+ 1)}))))β©, (2nd βπ)β© β π β§ βπ§ β π (π§ β π β π§ = β¨β¨(1st
β(1st βπ)), ((2nd β(1st
βπ)) β
({β¨(2nd βπ), ((2nd βπ) + 1)β©, β¨((2nd
βπ) + 1),
(2nd βπ)β©} βͺ ( I βΎ ((1...π) β {(2nd
βπ), ((2nd
βπ) + 1)}))))β©,
(2nd βπ)β©)) β β!π§ β π π§ β π) |
288 | 9, 286, 287 | syl2anc 585 |
. 2
β’ ((π β§ (2nd
βπ) β
(1...(π β 1))) β
β!π§ β π π§ β π) |
289 | | xp2nd 7959 |
. . . . . . 7
β’ (π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β (2nd βπ) β (0...π)) |
290 | 32, 289 | syl 17 |
. . . . . 6
β’ (π β (2nd
βπ) β (0...π)) |
291 | 290 | biantrurd 534 |
. . . . 5
β’ (π β (Β¬ (2nd
βπ) β
(1...(π β 1)) β
((2nd βπ)
β (0...π) β§ Β¬
(2nd βπ)
β (1...(π β
1))))) |
292 | 1 | nnnn0d 12480 |
. . . . . . . . . . . 12
β’ (π β π β
β0) |
293 | | nn0uz 12812 |
. . . . . . . . . . . 12
β’
β0 = (β€β₯β0) |
294 | 292, 293 | eleqtrdi 2848 |
. . . . . . . . . . 11
β’ (π β π β
(β€β₯β0)) |
295 | | fzpred 13496 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β0) β (0...π) = ({0} βͺ ((0 + 1)...π))) |
296 | 294, 295 | syl 17 |
. . . . . . . . . 10
β’ (π β (0...π) = ({0} βͺ ((0 + 1)...π))) |
297 | 123 | oveq1i 7372 |
. . . . . . . . . . 11
β’ ((0 +
1)...π) = (1...π) |
298 | 297 | uneq2i 4125 |
. . . . . . . . . 10
β’ ({0}
βͺ ((0 + 1)...π)) = ({0}
βͺ (1...π)) |
299 | 296, 298 | eqtrdi 2793 |
. . . . . . . . 9
β’ (π β (0...π) = ({0} βͺ (1...π))) |
300 | 299 | difeq1d 4086 |
. . . . . . . 8
β’ (π β ((0...π) β (1...(π β 1))) = (({0} βͺ (1...π)) β (1...(π β 1)))) |
301 | | difundir 4245 |
. . . . . . . . . 10
β’ (({0}
βͺ (1...π)) β
(1...(π β 1))) =
(({0} β (1...(π
β 1))) βͺ ((1...π)
β (1...(π β
1)))) |
302 | | 0lt1 11684 |
. . . . . . . . . . . . . 14
β’ 0 <
1 |
303 | | 0re 11164 |
. . . . . . . . . . . . . . 15
β’ 0 β
β |
304 | | 1re 11162 |
. . . . . . . . . . . . . . 15
β’ 1 β
β |
305 | 303, 304 | ltnlei 11283 |
. . . . . . . . . . . . . 14
β’ (0 < 1
β Β¬ 1 β€ 0) |
306 | 302, 305 | mpbi 229 |
. . . . . . . . . . . . 13
β’ Β¬ 1
β€ 0 |
307 | | elfzle1 13451 |
. . . . . . . . . . . . 13
β’ (0 β
(1...(π β 1)) β
1 β€ 0) |
308 | 306, 307 | mto 196 |
. . . . . . . . . . . 12
β’ Β¬ 0
β (1...(π β
1)) |
309 | | incom 4166 |
. . . . . . . . . . . . . 14
β’
((1...(π β 1))
β© {0}) = ({0} β© (1...(π β 1))) |
310 | 309 | eqeq1i 2742 |
. . . . . . . . . . . . 13
β’
(((1...(π β
1)) β© {0}) = β
β ({0} β© (1...(π β 1))) = β
) |
311 | | disjsn 4677 |
. . . . . . . . . . . . 13
β’
(((1...(π β
1)) β© {0}) = β
β Β¬ 0 β (1...(π β 1))) |
312 | | disj3 4418 |
. . . . . . . . . . . . 13
β’ (({0}
β© (1...(π β 1)))
= β
β {0} = ({0} β (1...(π β 1)))) |
313 | 310, 311,
312 | 3bitr3i 301 |
. . . . . . . . . . . 12
β’ (Β¬ 0
β (1...(π β 1))
β {0} = ({0} β (1...(π β 1)))) |
314 | 308, 313 | mpbi 229 |
. . . . . . . . . . 11
β’ {0} =
({0} β (1...(π
β 1))) |
315 | 314 | uneq1i 4124 |
. . . . . . . . . 10
β’ ({0}
βͺ ((1...π) β
(1...(π β 1)))) =
(({0} β (1...(π
β 1))) βͺ ((1...π)
β (1...(π β
1)))) |
316 | 301, 315 | eqtr4i 2768 |
. . . . . . . . 9
β’ (({0}
βͺ (1...π)) β
(1...(π β 1))) = ({0}
βͺ ((1...π) β
(1...(π β
1)))) |
317 | | difundir 4245 |
. . . . . . . . . . . 12
β’
(((1...(π β
1)) βͺ {π}) β
(1...(π β 1))) =
(((1...(π β 1))
β (1...(π β
1))) βͺ ({π} β
(1...(π β
1)))) |
318 | | difid 4335 |
. . . . . . . . . . . . 13
β’
((1...(π β 1))
β (1...(π β
1))) = β
|
319 | 318 | uneq1i 4124 |
. . . . . . . . . . . 12
β’
(((1...(π β
1)) β (1...(π β
1))) βͺ ({π} β
(1...(π β 1)))) =
(β
βͺ ({π} β
(1...(π β
1)))) |
320 | | uncom 4118 |
. . . . . . . . . . . . 13
β’ (β
βͺ ({π} β
(1...(π β 1)))) =
(({π} β (1...(π β 1))) βͺ
β
) |
321 | | un0 4355 |
. . . . . . . . . . . . 13
β’ (({π} β (1...(π β 1))) βͺ β
) =
({π} β (1...(π β 1))) |
322 | 320, 321 | eqtri 2765 |
. . . . . . . . . . . 12
β’ (β
βͺ ({π} β
(1...(π β 1)))) =
({π} β (1...(π β 1))) |
323 | 317, 319,
322 | 3eqtri 2769 |
. . . . . . . . . . 11
β’
(((1...(π β
1)) βͺ {π}) β
(1...(π β 1))) =
({π} β (1...(π β 1))) |
324 | | nnuz 12813 |
. . . . . . . . . . . . . . . 16
β’ β =
(β€β₯β1) |
325 | 1, 324 | eleqtrdi 2848 |
. . . . . . . . . . . . . . 15
β’ (π β π β
(β€β₯β1)) |
326 | 250, 325 | eqeltrd 2838 |
. . . . . . . . . . . . . 14
β’ (π β ((π β 1) + 1) β
(β€β₯β1)) |
327 | | fzsplit2 13473 |
. . . . . . . . . . . . . 14
β’ ((((π β 1) + 1) β
(β€β₯β1) β§ π β (β€β₯β(π β 1))) β (1...π) = ((1...(π β 1)) βͺ (((π β 1) + 1)...π))) |
328 | 326, 256,
327 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β (1...π) = ((1...(π β 1)) βͺ (((π β 1) + 1)...π))) |
329 | 250 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
β’ (π β (((π β 1) + 1)...π) = (π...π)) |
330 | 1 | nnzd 12533 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β€) |
331 | | fzsn 13490 |
. . . . . . . . . . . . . . . 16
β’ (π β β€ β (π...π) = {π}) |
332 | 330, 331 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (π...π) = {π}) |
333 | 329, 332 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ (π β (((π β 1) + 1)...π) = {π}) |
334 | 333 | uneq2d 4128 |
. . . . . . . . . . . . 13
β’ (π β ((1...(π β 1)) βͺ (((π β 1) + 1)...π)) = ((1...(π β 1)) βͺ {π})) |
335 | 328, 334 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (π β (1...π) = ((1...(π β 1)) βͺ {π})) |
336 | 335 | difeq1d 4086 |
. . . . . . . . . . 11
β’ (π β ((1...π) β (1...(π β 1))) = (((1...(π β 1)) βͺ {π}) β (1...(π β 1)))) |
337 | 1 | nnred 12175 |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
338 | 337 | ltm1d 12094 |
. . . . . . . . . . . . . 14
β’ (π β (π β 1) < π) |
339 | 164 | nn0red 12481 |
. . . . . . . . . . . . . . 15
β’ (π β (π β 1) β β) |
340 | 339, 337 | ltnled 11309 |
. . . . . . . . . . . . . 14
β’ (π β ((π β 1) < π β Β¬ π β€ (π β 1))) |
341 | 338, 340 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (π β Β¬ π β€ (π β 1)) |
342 | | elfzle2 13452 |
. . . . . . . . . . . . 13
β’ (π β (1...(π β 1)) β π β€ (π β 1)) |
343 | 341, 342 | nsyl 140 |
. . . . . . . . . . . 12
β’ (π β Β¬ π β (1...(π β 1))) |
344 | | incom 4166 |
. . . . . . . . . . . . . 14
β’
((1...(π β 1))
β© {π}) = ({π} β© (1...(π β 1))) |
345 | 344 | eqeq1i 2742 |
. . . . . . . . . . . . 13
β’
(((1...(π β
1)) β© {π}) = β
β ({π} β©
(1...(π β 1))) =
β
) |
346 | | disjsn 4677 |
. . . . . . . . . . . . 13
β’
(((1...(π β
1)) β© {π}) = β
β Β¬ π β
(1...(π β
1))) |
347 | | disj3 4418 |
. . . . . . . . . . . . 13
β’ (({π} β© (1...(π β 1))) = β
β {π} = ({π} β (1...(π β 1)))) |
348 | 345, 346,
347 | 3bitr3i 301 |
. . . . . . . . . . . 12
β’ (Β¬
π β (1...(π β 1)) β {π} = ({π} β (1...(π β 1)))) |
349 | 343, 348 | sylib 217 |
. . . . . . . . . . 11
β’ (π β {π} = ({π} β (1...(π β 1)))) |
350 | 323, 336,
349 | 3eqtr4a 2803 |
. . . . . . . . . 10
β’ (π β ((1...π) β (1...(π β 1))) = {π}) |
351 | 350 | uneq2d 4128 |
. . . . . . . . 9
β’ (π β ({0} βͺ ((1...π) β (1...(π β 1)))) = ({0} βͺ
{π})) |
352 | 316, 351 | eqtrid 2789 |
. . . . . . . 8
β’ (π β (({0} βͺ (1...π)) β (1...(π β 1))) = ({0} βͺ
{π})) |
353 | 300, 352 | eqtrd 2777 |
. . . . . . 7
β’ (π β ((0...π) β (1...(π β 1))) = ({0} βͺ {π})) |
354 | 353 | eleq2d 2824 |
. . . . . 6
β’ (π β ((2nd
βπ) β
((0...π) β
(1...(π β 1))) β
(2nd βπ)
β ({0} βͺ {π}))) |
355 | | eldif 3925 |
. . . . . 6
β’
((2nd βπ) β ((0...π) β (1...(π β 1))) β ((2nd
βπ) β (0...π) β§ Β¬ (2nd
βπ) β
(1...(π β
1)))) |
356 | | elun 4113 |
. . . . . . 7
β’
((2nd βπ) β ({0} βͺ {π}) β ((2nd βπ) β {0} β¨
(2nd βπ)
β {π})) |
357 | 215 | elsn 4606 |
. . . . . . . 8
β’
((2nd βπ) β {0} β (2nd
βπ) =
0) |
358 | 215 | elsn 4606 |
. . . . . . . 8
β’
((2nd βπ) β {π} β (2nd βπ) = π) |
359 | 357, 358 | orbi12i 914 |
. . . . . . 7
β’
(((2nd βπ) β {0} β¨ (2nd
βπ) β {π}) β ((2nd
βπ) = 0 β¨
(2nd βπ) =
π)) |
360 | 356, 359 | bitri 275 |
. . . . . 6
β’
((2nd βπ) β ({0} βͺ {π}) β ((2nd βπ) = 0 β¨ (2nd
βπ) = π)) |
361 | 354, 355,
360 | 3bitr3g 313 |
. . . . 5
β’ (π β (((2nd
βπ) β (0...π) β§ Β¬ (2nd
βπ) β
(1...(π β 1))) β
((2nd βπ)
= 0 β¨ (2nd βπ) = π))) |
362 | 291, 361 | bitrd 279 |
. . . 4
β’ (π β (Β¬ (2nd
βπ) β
(1...(π β 1)) β
((2nd βπ)
= 0 β¨ (2nd βπ) = π))) |
363 | 362 | biimpa 478 |
. . 3
β’ ((π β§ Β¬ (2nd
βπ) β
(1...(π β 1))) β
((2nd βπ)
= 0 β¨ (2nd βπ) = π)) |
364 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ (2nd
βπ) = 0) β π β
β) |
365 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ (2nd
βπ) = 0) β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) |
366 | 6 | adantr 482 |
. . . . 5
β’ ((π β§ (2nd
βπ) = 0) β π β π) |
367 | | poimirlem22.4 |
. . . . . 6
β’ ((π β§ π β (1...π)) β βπ β ran πΉ(πβπ) β πΎ) |
368 | 367 | adantlr 714 |
. . . . 5
β’ (((π β§ (2nd
βπ) = 0) β§ π β (1...π)) β βπ β ran πΉ(πβπ) β πΎ) |
369 | | simpr 486 |
. . . . 5
β’ ((π β§ (2nd
βπ) = 0) β
(2nd βπ) =
0) |
370 | 364, 3, 365, 366, 368, 369 | poimirlem18 36125 |
. . . 4
β’ ((π β§ (2nd
βπ) = 0) β
β!π§ β π π§ β π) |
371 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ (2nd
βπ) = π) β π β β) |
372 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ (2nd
βπ) = π) β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) |
373 | 6 | adantr 482 |
. . . . 5
β’ ((π β§ (2nd
βπ) = π) β π β π) |
374 | | poimirlem22.3 |
. . . . . 6
β’ ((π β§ π β (1...π)) β βπ β ran πΉ(πβπ) β 0) |
375 | 374 | adantlr 714 |
. . . . 5
β’ (((π β§ (2nd
βπ) = π) β§ π β (1...π)) β βπ β ran πΉ(πβπ) β 0) |
376 | | simpr 486 |
. . . . 5
β’ ((π β§ (2nd
βπ) = π) β (2nd
βπ) = π) |
377 | 371, 3, 372, 373, 375, 376 | poimirlem21 36128 |
. . . 4
β’ ((π β§ (2nd
βπ) = π) β β!π§ β π π§ β π) |
378 | 370, 377 | jaodan 957 |
. . 3
β’ ((π β§ ((2nd
βπ) = 0 β¨
(2nd βπ) =
π)) β β!π§ β π π§ β π) |
379 | 363, 378 | syldan 592 |
. 2
β’ ((π β§ Β¬ (2nd
βπ) β
(1...(π β 1))) β
β!π§ β π π§ β π) |
380 | 288, 379 | pm2.61dan 812 |
1
β’ (π β β!π§ β π π§ β π) |