Step | Hyp | Ref
| Expression |
1 | | poimirlem22.2 |
. . 3
β’ (π β π β π) |
2 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π‘ = π β (2nd βπ‘) = (2nd βπ)) |
3 | 2 | breq2d 5122 |
. . . . . . . . 9
β’ (π‘ = π β (π¦ < (2nd βπ‘) β π¦ < (2nd βπ))) |
4 | 3 | ifbid 4514 |
. . . . . . . 8
β’ (π‘ = π β if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) = if(π¦ < (2nd βπ), π¦, (π¦ + 1))) |
5 | | 2fveq3 6852 |
. . . . . . . . 9
β’ (π‘ = π β (1st
β(1st βπ‘)) = (1st β(1st
βπ))) |
6 | | 2fveq3 6852 |
. . . . . . . . . . . 12
β’ (π‘ = π β (2nd
β(1st βπ‘)) = (2nd β(1st
βπ))) |
7 | 6 | imaeq1d 6017 |
. . . . . . . . . . 11
β’ (π‘ = π β ((2nd
β(1st βπ‘)) β (1...π)) = ((2nd β(1st
βπ)) β
(1...π))) |
8 | 7 | xpeq1d 5667 |
. . . . . . . . . 10
β’ (π‘ = π β (((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) = (((2nd
β(1st βπ)) β (1...π)) Γ {1})) |
9 | 6 | imaeq1d 6017 |
. . . . . . . . . . 11
β’ (π‘ = π β ((2nd
β(1st βπ‘)) β ((π + 1)...π)) = ((2nd β(1st
βπ)) β ((π + 1)...π))) |
10 | 9 | xpeq1d 5667 |
. . . . . . . . . 10
β’ (π‘ = π β (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}) = (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0})) |
11 | 8, 10 | uneq12d 4129 |
. . . . . . . . 9
β’ (π‘ = π β ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0})) = ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))) |
12 | 5, 11 | oveq12d 7380 |
. . . . . . . 8
β’ (π‘ = π β ((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))) = ((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0})))) |
13 | 4, 12 | csbeq12dv 3869 |
. . . . . . 7
β’ (π‘ = π β β¦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 | 13 | mpteq2dv 5212 |
. . . . . 6
β’ (π‘ = π β (π¦ β (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}))))) |
15 | 14 | eqeq2d 2748 |
. . . . 5
β’ (π‘ = π β (πΉ = (π¦ β (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})))))) |
16 | | poimirlem22.s |
. . . . 5
β’ π = {π‘ β ((((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}))))} |
17 | 15, 16 | elrab2 3653 |
. . . 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})))))) |
18 | 17 | simprbi 498 |
. . 3
β’ (π β π β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))))) |
19 | 1, 18 | syl 17 |
. 2
β’ (π β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))))) |
20 | | elrabi 3644 |
. . . . . . . . . . . 12
β’ (π β {π‘ β ((((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...π))) |
21 | 20, 16 | eleq2s 2856 |
. . . . . . . . . . 11
β’ (π β π β π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π))) |
22 | 1, 21 | syl 17 |
. . . . . . . . . 10
β’ (π β π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π))) |
23 | | xp1st 7958 |
. . . . . . . . . 10
β’ (π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β (1st βπ) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
β’ (π β (1st
βπ) β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
25 | | xp1st 7958 |
. . . . . . . . 9
β’
((1st βπ) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β (1st
β(1st βπ)) β ((0..^πΎ) βm (1...π))) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
β’ (π β (1st
β(1st βπ)) β ((0..^πΎ) βm (1...π))) |
27 | | elmapfn 8810 |
. . . . . . . 8
β’
((1st β(1st βπ)) β ((0..^πΎ) βm (1...π)) β (1st
β(1st βπ)) Fn (1...π)) |
28 | 26, 27 | syl 17 |
. . . . . . 7
β’ (π β (1st
β(1st βπ)) Fn (1...π)) |
29 | 28 | adantr 482 |
. . . . . 6
β’ ((π β§ π¦ β (0...(π β 1))) β (1st
β(1st βπ)) Fn (1...π)) |
30 | | 1ex 11158 |
. . . . . . . . . 10
β’ 1 β
V |
31 | | fnconstg 6735 |
. . . . . . . . . 10
β’ (1 β
V β (((2nd β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) Fn ((2nd
β(1st βπ)) β (1...(π¦ + 1)))) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . 9
β’
(((2nd β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) Fn ((2nd
β(1st βπ)) β (1...(π¦ + 1))) |
33 | | c0ex 11156 |
. . . . . . . . . 10
β’ 0 β
V |
34 | | fnconstg 6735 |
. . . . . . . . . 10
β’ (0 β
V β (((2nd β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}) Fn ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) |
35 | 33, 34 | ax-mp 5 |
. . . . . . . . 9
β’
(((2nd β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}) Fn ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) |
36 | 32, 35 | pm3.2i 472 |
. . . . . . . 8
β’
((((2nd β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) Fn ((2nd
β(1st βπ)) β (1...(π¦ + 1))) β§ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}) Fn ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) |
37 | | xp2nd 7959 |
. . . . . . . . . . . . 13
β’
((1st βπ) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β (2nd
β(1st βπ)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
38 | 24, 37 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (2nd
β(1st βπ)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
39 | | fvex 6860 |
. . . . . . . . . . . . 13
β’
(2nd β(1st βπ)) β V |
40 | | f1oeq1 6777 |
. . . . . . . . . . . . 13
β’ (π = (2nd
β(1st βπ)) β (π:(1...π)β1-1-ontoβ(1...π) β (2nd
β(1st βπ)):(1...π)β1-1-ontoβ(1...π))) |
41 | 39, 40 | elab 3635 |
. . . . . . . . . . . 12
β’
((2nd β(1st βπ)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)} β (2nd
β(1st βπ)):(1...π)β1-1-ontoβ(1...π)) |
42 | 38, 41 | sylib 217 |
. . . . . . . . . . 11
β’ (π β (2nd
β(1st βπ)):(1...π)β1-1-ontoβ(1...π)) |
43 | | dff1o3 6795 |
. . . . . . . . . . . 12
β’
((2nd β(1st βπ)):(1...π)β1-1-ontoβ(1...π) β ((2nd
β(1st βπ)):(1...π)βontoβ(1...π) β§ Fun β‘(2nd β(1st
βπ)))) |
44 | 43 | simprbi 498 |
. . . . . . . . . . 11
β’
((2nd β(1st βπ)):(1...π)β1-1-ontoβ(1...π) β Fun β‘(2nd β(1st
βπ))) |
45 | 42, 44 | syl 17 |
. . . . . . . . . 10
β’ (π β Fun β‘(2nd β(1st
βπ))) |
46 | | imain 6591 |
. . . . . . . . . 10
β’ (Fun
β‘(2nd β(1st
βπ)) β
((2nd β(1st βπ)) β ((1...(π¦ + 1)) β© (((π¦ + 1) + 1)...π))) = (((2nd
β(1st βπ)) β (1...(π¦ + 1))) β© ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)))) |
47 | 45, 46 | syl 17 |
. . . . . . . . 9
β’ (π β ((2nd
β(1st βπ)) β ((1...(π¦ + 1)) β© (((π¦ + 1) + 1)...π))) = (((2nd
β(1st βπ)) β (1...(π¦ + 1))) β© ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)))) |
48 | | elfznn0 13541 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (0...(π β 1)) β π¦ β β0) |
49 | | nn0p1nn 12459 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β0
β (π¦ + 1) β
β) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π¦ β (0...(π β 1)) β (π¦ + 1) β β) |
51 | 50 | nnred 12175 |
. . . . . . . . . . . . 13
β’ (π¦ β (0...(π β 1)) β (π¦ + 1) β β) |
52 | 51 | ltp1d 12092 |
. . . . . . . . . . . 12
β’ (π¦ β (0...(π β 1)) β (π¦ + 1) < ((π¦ + 1) + 1)) |
53 | | fzdisj 13475 |
. . . . . . . . . . . 12
β’ ((π¦ + 1) < ((π¦ + 1) + 1) β ((1...(π¦ + 1)) β© (((π¦ + 1) + 1)...π)) = β
) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . 11
β’ (π¦ β (0...(π β 1)) β ((1...(π¦ + 1)) β© (((π¦ + 1) + 1)...π)) = β
) |
55 | 54 | imaeq2d 6018 |
. . . . . . . . . 10
β’ (π¦ β (0...(π β 1)) β ((2nd
β(1st βπ)) β ((1...(π¦ + 1)) β© (((π¦ + 1) + 1)...π))) = ((2nd
β(1st βπ)) β β
)) |
56 | | ima0 6034 |
. . . . . . . . . 10
β’
((2nd β(1st βπ)) β β
) =
β
|
57 | 55, 56 | eqtrdi 2793 |
. . . . . . . . 9
β’ (π¦ β (0...(π β 1)) β ((2nd
β(1st βπ)) β ((1...(π¦ + 1)) β© (((π¦ + 1) + 1)...π))) = β
) |
58 | 47, 57 | sylan9req 2798 |
. . . . . . . 8
β’ ((π β§ π¦ β (0...(π β 1))) β (((2nd
β(1st βπ)) β (1...(π¦ + 1))) β© ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) = β
) |
59 | | fnun 6619 |
. . . . . . . 8
β’
((((((2nd β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) Fn ((2nd
β(1st βπ)) β (1...(π¦ + 1))) β§ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}) Fn ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) β§ (((2nd
β(1st βπ)) β (1...(π¦ + 1))) β© ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) = β
) β ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) Fn (((2nd
β(1st βπ)) β (1...(π¦ + 1))) βͺ ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)))) |
60 | 36, 58, 59 | sylancr 588 |
. . . . . . 7
β’ ((π β§ π¦ β (0...(π β 1))) β ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) Fn (((2nd
β(1st βπ)) β (1...(π¦ + 1))) βͺ ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)))) |
61 | | imaundi 6107 |
. . . . . . . . 9
β’
((2nd β(1st βπ)) β ((1...(π¦ + 1)) βͺ (((π¦ + 1) + 1)...π))) = (((2nd
β(1st βπ)) β (1...(π¦ + 1))) βͺ ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) |
62 | | nnuz 12813 |
. . . . . . . . . . . . . 14
β’ β =
(β€β₯β1) |
63 | 50, 62 | eleqtrdi 2848 |
. . . . . . . . . . . . 13
β’ (π¦ β (0...(π β 1)) β (π¦ + 1) β
(β€β₯β1)) |
64 | | peano2uz 12833 |
. . . . . . . . . . . . 13
β’ ((π¦ + 1) β
(β€β₯β1) β ((π¦ + 1) + 1) β
(β€β₯β1)) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . 12
β’ (π¦ β (0...(π β 1)) β ((π¦ + 1) + 1) β
(β€β₯β1)) |
66 | | poimir.0 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β) |
67 | 66 | nncnd 12176 |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
68 | | npcan1 11587 |
. . . . . . . . . . . . . . 15
β’ (π β β β ((π β 1) + 1) = π) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β ((π β 1) + 1) = π) |
70 | 69 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (0...(π β 1))) β ((π β 1) + 1) = π) |
71 | | elfzuz3 13445 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (0...(π β 1)) β (π β 1) β
(β€β₯βπ¦)) |
72 | | eluzp1p1 12798 |
. . . . . . . . . . . . . . 15
β’ ((π β 1) β
(β€β₯βπ¦) β ((π β 1) + 1) β
(β€β₯β(π¦ + 1))) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π¦ β (0...(π β 1)) β ((π β 1) + 1) β
(β€β₯β(π¦ + 1))) |
74 | 73 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (0...(π β 1))) β ((π β 1) + 1) β
(β€β₯β(π¦ + 1))) |
75 | 70, 74 | eqeltrrd 2839 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (0...(π β 1))) β π β (β€β₯β(π¦ + 1))) |
76 | | fzsplit2 13473 |
. . . . . . . . . . . 12
β’ ((((π¦ + 1) + 1) β
(β€β₯β1) β§ π β (β€β₯β(π¦ + 1))) β (1...π) = ((1...(π¦ + 1)) βͺ (((π¦ + 1) + 1)...π))) |
77 | 65, 75, 76 | syl2an2 685 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (0...(π β 1))) β (1...π) = ((1...(π¦ + 1)) βͺ (((π¦ + 1) + 1)...π))) |
78 | 77 | imaeq2d 6018 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (0...(π β 1))) β ((2nd
β(1st βπ)) β (1...π)) = ((2nd β(1st
βπ)) β
((1...(π¦ + 1)) βͺ
(((π¦ + 1) + 1)...π)))) |
79 | | f1ofo 6796 |
. . . . . . . . . . . 12
β’
((2nd β(1st βπ)):(1...π)β1-1-ontoβ(1...π) β (2nd
β(1st βπ)):(1...π)βontoβ(1...π)) |
80 | | foima 6766 |
. . . . . . . . . . . 12
β’
((2nd β(1st βπ)):(1...π)βontoβ(1...π) β ((2nd
β(1st βπ)) β (1...π)) = (1...π)) |
81 | 42, 79, 80 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β ((2nd
β(1st βπ)) β (1...π)) = (1...π)) |
82 | 81 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (0...(π β 1))) β ((2nd
β(1st βπ)) β (1...π)) = (1...π)) |
83 | 78, 82 | eqtr3d 2779 |
. . . . . . . . 9
β’ ((π β§ π¦ β (0...(π β 1))) β ((2nd
β(1st βπ)) β ((1...(π¦ + 1)) βͺ (((π¦ + 1) + 1)...π))) = (1...π)) |
84 | 61, 83 | eqtr3id 2791 |
. . . . . . . 8
β’ ((π β§ π¦ β (0...(π β 1))) β (((2nd
β(1st βπ)) β (1...(π¦ + 1))) βͺ ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) = (1...π)) |
85 | 84 | fneq2d 6601 |
. . . . . . 7
β’ ((π β§ π¦ β (0...(π β 1))) β (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) Fn (((2nd
β(1st βπ)) β (1...(π¦ + 1))) βͺ ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) β ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) Fn (1...π))) |
86 | 60, 85 | mpbid 231 |
. . . . . 6
β’ ((π β§ π¦ β (0...(π β 1))) β ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) Fn (1...π)) |
87 | | ovexd 7397 |
. . . . . 6
β’ ((π β§ π¦ β (0...(π β 1))) β (1...π) β V) |
88 | | inidm 4183 |
. . . . . 6
β’
((1...π) β©
(1...π)) = (1...π) |
89 | | eqidd 2738 |
. . . . . 6
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β ((1st
β(1st βπ))βπ) = ((1st β(1st
βπ))βπ)) |
90 | | eqidd 2738 |
. . . . . 6
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ) = (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ)) |
91 | 29, 86, 87, 87, 88, 89, 90 | offval 7631 |
. . . . 5
β’ ((π β§ π¦ β (0...(π β 1))) β ((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))) = (π β (1...π) β¦ (((1st
β(1st βπ))βπ) + (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ)))) |
92 | | oveq1 7369 |
. . . . . . . . . 10
β’ (1 =
if(π = ((2nd
β(1st βπ))β1), 1, 0) β (1 +
((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)) = (if(π = ((2nd β(1st
βπ))β1), 1, 0)
+ ((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ))) |
93 | 92 | eqeq2d 2748 |
. . . . . . . . 9
β’ (1 =
if(π = ((2nd
β(1st βπ))β1), 1, 0) β
((((((2nd β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ) = (1 + ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)) β (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ) = (if(π = ((2nd β(1st
βπ))β1), 1, 0)
+ ((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)))) |
94 | | oveq1 7369 |
. . . . . . . . . 10
β’ (0 =
if(π = ((2nd
β(1st βπ))β1), 1, 0) β (0 +
((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)) = (if(π = ((2nd β(1st
βπ))β1), 1, 0)
+ ((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ))) |
95 | 94 | eqeq2d 2748 |
. . . . . . . . 9
β’ (0 =
if(π = ((2nd
β(1st βπ))β1), 1, 0) β
((((((2nd β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ) = (0 + ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)) β (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ) = (if(π = ((2nd β(1st
βπ))β1), 1, 0)
+ ((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)))) |
96 | | 1p0e1 12284 |
. . . . . . . . . . . . . 14
β’ (1 + 0) =
1 |
97 | 96 | eqcomi 2746 |
. . . . . . . . . . . . 13
β’ 1 = (1 +
0) |
98 | | f1ofn 6790 |
. . . . . . . . . . . . . . . . . 18
β’
((2nd β(1st βπ)):(1...π)β1-1-ontoβ(1...π) β (2nd
β(1st βπ)) Fn (1...π)) |
99 | 42, 98 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (2nd
β(1st βπ)) Fn (1...π)) |
100 | 99 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (0...(π β 1))) β (2nd
β(1st βπ)) Fn (1...π)) |
101 | | fzss2 13488 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯β(π¦ + 1)) β (1...(π¦ + 1)) β (1...π)) |
102 | 75, 101 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (0...(π β 1))) β (1...(π¦ + 1)) β (1...π)) |
103 | | eluzfz1 13455 |
. . . . . . . . . . . . . . . . . 18
β’ ((π¦ + 1) β
(β€β₯β1) β 1 β (1...(π¦ + 1))) |
104 | 63, 103 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β (0...(π β 1)) β 1 β (1...(π¦ + 1))) |
105 | 104 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (0...(π β 1))) β 1 β (1...(π¦ + 1))) |
106 | | fnfvima 7188 |
. . . . . . . . . . . . . . . 16
β’
(((2nd β(1st βπ)) Fn (1...π) β§ (1...(π¦ + 1)) β (1...π) β§ 1 β (1...(π¦ + 1))) β ((2nd
β(1st βπ))β1) β ((2nd
β(1st βπ)) β (1...(π¦ + 1)))) |
107 | 100, 102,
105, 106 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (0...(π β 1))) β ((2nd
β(1st βπ))β1) β ((2nd
β(1st βπ)) β (1...(π¦ + 1)))) |
108 | | fvun1 6937 |
. . . . . . . . . . . . . . . 16
β’
(((((2nd β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) Fn ((2nd
β(1st βπ)) β (1...(π¦ + 1))) β§ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}) Fn ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) β§ ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) β© ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) = β
β§ ((2nd
β(1st βπ))β1) β ((2nd
β(1st βπ)) β (1...(π¦ + 1))))) β (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))β((2nd
β(1st βπ))β1)) = ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1})β((2nd
β(1st βπ))β1))) |
109 | 32, 35, 108 | mp3an12 1452 |
. . . . . . . . . . . . . . 15
β’
(((((2nd β(1st βπ)) β (1...(π¦ + 1))) β© ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) = β
β§ ((2nd
β(1st βπ))β1) β ((2nd
β(1st βπ)) β (1...(π¦ + 1)))) β (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))β((2nd
β(1st βπ))β1)) = ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1})β((2nd
β(1st βπ))β1))) |
110 | 58, 107, 109 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (0...(π β 1))) β (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))β((2nd
β(1st βπ))β1)) = ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1})β((2nd
β(1st βπ))β1))) |
111 | 30 | fvconst2 7158 |
. . . . . . . . . . . . . . 15
β’
(((2nd β(1st βπ))β1) β ((2nd
β(1st βπ)) β (1...(π¦ + 1))) β ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1})β((2nd
β(1st βπ))β1)) = 1) |
112 | 107, 111 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (0...(π β 1))) β ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1})β((2nd
β(1st βπ))β1)) = 1) |
113 | 110, 112 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (0...(π β 1))) β (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))β((2nd
β(1st βπ))β1)) = 1) |
114 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β (1...(π β 1))) β π β (1...(π β 1))) |
115 | 66 | nnzd 12533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π β β€) |
116 | | peano2zm 12553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β€ β (π β 1) β
β€) |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π β 1) β β€) |
118 | | 1z 12540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ 1 β
β€ |
119 | 117, 118 | jctil 521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (1 β β€ β§
(π β 1) β
β€)) |
120 | | elfzelz 13448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (1...(π β 1)) β π β β€) |
121 | 120, 118 | jctir 522 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (1...(π β 1)) β (π β β€ β§ 1 β
β€)) |
122 | | fzaddel 13482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((1
β β€ β§ (π
β 1) β β€) β§ (π β β€ β§ 1 β β€))
β (π β
(1...(π β 1)) β
(π + 1) β ((1 +
1)...((π β 1) +
1)))) |
123 | 119, 121,
122 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β (1...(π β 1))) β (π β (1...(π β 1)) β (π + 1) β ((1 + 1)...((π β 1) + 1)))) |
124 | 114, 123 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β (1...(π β 1))) β (π + 1) β ((1 + 1)...((π β 1) + 1))) |
125 | 69 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β ((1 + 1)...((π β 1) + 1)) = ((1 +
1)...π)) |
126 | 125 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β (1...(π β 1))) β ((1 + 1)...((π β 1) + 1)) = ((1 +
1)...π)) |
127 | 124, 126 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β (1...(π β 1))) β (π + 1) β ((1 + 1)...π)) |
128 | 127 | ralrimiva 3144 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β βπ β (1...(π β 1))(π + 1) β ((1 + 1)...π)) |
129 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π¦ β ((1 + 1)...π)) β π¦ β ((1 + 1)...π)) |
130 | | peano2z 12551 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (1 β
β€ β (1 + 1) β β€) |
131 | 118, 130 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (1 + 1)
β β€ |
132 | 115, 131 | jctil 521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β ((1 + 1) β β€
β§ π β
β€)) |
133 | | elfzelz 13448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π¦ β ((1 + 1)...π) β π¦ β β€) |
134 | 133, 118 | jctir 522 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π¦ β ((1 + 1)...π) β (π¦ β β€ β§ 1 β
β€)) |
135 | | fzsubel 13484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((1 +
1) β β€ β§ π
β β€) β§ (π¦
β β€ β§ 1 β β€)) β (π¦ β ((1 + 1)...π) β (π¦ β 1) β (((1 + 1) β
1)...(π β
1)))) |
136 | 132, 134,
135 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π¦ β ((1 + 1)...π)) β (π¦ β ((1 + 1)...π) β (π¦ β 1) β (((1 + 1) β
1)...(π β
1)))) |
137 | 129, 136 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π¦ β ((1 + 1)...π)) β (π¦ β 1) β (((1 + 1) β
1)...(π β
1))) |
138 | | ax-1cn 11116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ 1 β
β |
139 | 138, 138 | pncan3oi 11424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((1 + 1)
β 1) = 1 |
140 | 139 | oveq1i 7372 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((1 + 1)
β 1)...(π β 1))
= (1...(π β
1)) |
141 | 137, 140 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π¦ β ((1 + 1)...π)) β (π¦ β 1) β (1...(π β 1))) |
142 | 133 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π¦ β ((1 + 1)...π) β π¦ β β) |
143 | | elfznn 13477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (1...(π β 1)) β π β β) |
144 | 143 | nncnd 12176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (1...(π β 1)) β π β β) |
145 | | subadd2 11412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π¦ β β β§ 1 β
β β§ π β
β) β ((π¦ β
1) = π β (π + 1) = π¦)) |
146 | 138, 145 | mp3an2 1450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π¦ β β β§ π β β) β ((π¦ β 1) = π β (π + 1) = π¦)) |
147 | 146 | bicomd 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π¦ β β β§ π β β) β ((π + 1) = π¦ β (π¦ β 1) = π)) |
148 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π + 1) = π¦ β π¦ = (π + 1)) |
149 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π¦ β 1) = π β π = (π¦ β 1)) |
150 | 147, 148,
149 | 3bitr3g 313 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π¦ β β β§ π β β) β (π¦ = (π + 1) β π = (π¦ β 1))) |
151 | 142, 144,
150 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π¦ β ((1 + 1)...π) β§ π β (1...(π β 1))) β (π¦ = (π + 1) β π = (π¦ β 1))) |
152 | 151 | ralrimiva 3144 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ β ((1 + 1)...π) β βπ β (1...(π β 1))(π¦ = (π + 1) β π = (π¦ β 1))) |
153 | 152 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π¦ β ((1 + 1)...π)) β βπ β (1...(π β 1))(π¦ = (π + 1) β π = (π¦ β 1))) |
154 | | reu6i 3691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π¦ β 1) β (1...(π β 1)) β§ βπ β (1...(π β 1))(π¦ = (π + 1) β π = (π¦ β 1))) β β!π β (1...(π β 1))π¦ = (π + 1)) |
155 | 141, 153,
154 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π¦ β ((1 + 1)...π)) β β!π β (1...(π β 1))π¦ = (π + 1)) |
156 | 155 | ralrimiva 3144 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β βπ¦ β ((1 + 1)...π)β!π β (1...(π β 1))π¦ = (π + 1)) |
157 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (1...(π β 1)) β¦ (π + 1)) = (π β (1...(π β 1)) β¦ (π + 1)) |
158 | 157 | f1ompt 7064 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (1...(π β 1)) β¦ (π + 1)):(1...(π β 1))β1-1-ontoβ((1 +
1)...π) β
(βπ β
(1...(π β 1))(π + 1) β ((1 + 1)...π) β§ βπ¦ β ((1 + 1)...π)β!π β (1...(π β 1))π¦ = (π + 1))) |
159 | 128, 156,
158 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π β (1...(π β 1)) β¦ (π + 1)):(1...(π β 1))β1-1-ontoβ((1 +
1)...π)) |
160 | | f1osng 6830 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ 1 β
V) β {β¨π,
1β©}:{π}β1-1-ontoβ{1}) |
161 | 66, 30, 160 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β {β¨π, 1β©}:{π}β1-1-ontoβ{1}) |
162 | 66 | nnred 12175 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π β β) |
163 | 162 | ltm1d 12094 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (π β 1) < π) |
164 | 117 | zred 12614 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (π β 1) β β) |
165 | 164, 162 | ltnled 11309 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β ((π β 1) < π β Β¬ π β€ (π β 1))) |
166 | 163, 165 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β Β¬ π β€ (π β 1)) |
167 | | elfzle2 13452 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (1...(π β 1)) β π β€ (π β 1)) |
168 | 166, 167 | nsyl 140 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β Β¬ π β (1...(π β 1))) |
169 | | disjsn 4677 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((1...(π β
1)) β© {π}) = β
β Β¬ π β
(1...(π β
1))) |
170 | 168, 169 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((1...(π β 1)) β© {π}) = β
) |
171 | | 1re 11162 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 1 β
β |
172 | 171 | ltp1i 12066 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ 1 < (1
+ 1) |
173 | 171, 171 | readdcli 11177 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (1 + 1)
β β |
174 | 171, 173 | ltnlei 11283 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (1 <
(1 + 1) β Β¬ (1 + 1) β€ 1) |
175 | 172, 174 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ Β¬ (1
+ 1) β€ 1 |
176 | | elfzle1 13451 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (1 β
((1 + 1)...π) β (1 +
1) β€ 1) |
177 | 175, 176 | mto 196 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ Β¬ 1
β ((1 + 1)...π) |
178 | | disjsn 4677 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((1 +
1)...π) β© {1}) =
β
β Β¬ 1 β ((1 + 1)...π)) |
179 | 177, 178 | mpbir 230 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((1 +
1)...π) β© {1}) =
β
|
180 | | f1oun 6808 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β (1...(π β 1)) β¦ (π + 1)):(1...(π β 1))β1-1-ontoβ((1 +
1)...π) β§ {β¨π, 1β©}:{π}β1-1-ontoβ{1})
β§ (((1...(π β 1))
β© {π}) = β
β§
(((1 + 1)...π) β© {1}) =
β
)) β ((π β
(1...(π β 1)) β¦
(π + 1)) βͺ {β¨π, 1β©}):((1...(π β 1)) βͺ {π})β1-1-ontoβ(((1
+ 1)...π) βͺ
{1})) |
181 | 179, 180 | mpanr2 703 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β (1...(π β 1)) β¦ (π + 1)):(1...(π β 1))β1-1-ontoβ((1 +
1)...π) β§ {β¨π, 1β©}:{π}β1-1-ontoβ{1})
β§ ((1...(π β 1))
β© {π}) = β
)
β ((π β
(1...(π β 1)) β¦
(π + 1)) βͺ {β¨π, 1β©}):((1...(π β 1)) βͺ {π})β1-1-ontoβ(((1
+ 1)...π) βͺ
{1})) |
182 | 159, 161,
170, 181 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((π β (1...(π β 1)) β¦ (π + 1)) βͺ {β¨π, 1β©}):((1...(π β 1)) βͺ {π})β1-1-ontoβ(((1
+ 1)...π) βͺ
{1})) |
183 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β 1 β
V) |
184 | 66, 62 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π β
(β€β₯β1)) |
185 | 69, 184 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β ((π β 1) + 1) β
(β€β₯β1)) |
186 | | uzid 12785 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β 1) β β€
β (π β 1) β
(β€β₯β(π β 1))) |
187 | | peano2uz 12833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β 1) β
(β€β₯β(π β 1)) β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
188 | 117, 186,
187 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
189 | 69, 188 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π β (β€β₯β(π β 1))) |
190 | | fzsplit2 13473 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β 1) + 1) β
(β€β₯β1) β§ π β (β€β₯β(π β 1))) β (1...π) = ((1...(π β 1)) βͺ (((π β 1) + 1)...π))) |
191 | 185, 189,
190 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (1...π) = ((1...(π β 1)) βͺ (((π β 1) + 1)...π))) |
192 | 69 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (((π β 1) + 1)...π) = (π...π)) |
193 | | fzsn 13490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β β€ β (π...π) = {π}) |
194 | 115, 193 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (π...π) = {π}) |
195 | 192, 194 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (((π β 1) + 1)...π) = {π}) |
196 | 195 | uneq2d 4128 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β ((1...(π β 1)) βͺ (((π β 1) + 1)...π)) = ((1...(π β 1)) βͺ {π})) |
197 | 191, 196 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β ((1...(π β 1)) βͺ {π}) = (1...π)) |
198 | | iftrue 4497 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π β if(π = π, 1, (π + 1)) = 1) |
199 | 198 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π = π) β if(π = π, 1, (π + 1)) = 1) |
200 | 66, 183, 197, 199 | fmptapd 7122 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ((π β (1...(π β 1)) β¦ if(π = π, 1, (π + 1))) βͺ {β¨π, 1β©}) = (π β (1...π) β¦ if(π = π, 1, (π + 1)))) |
201 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = π β (π β (1...(π β 1)) β π β (1...(π β 1)))) |
202 | 201 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = π β (Β¬ π β (1...(π β 1)) β Β¬ π β (1...(π β 1)))) |
203 | 168, 202 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π = π β Β¬ π β (1...(π β 1)))) |
204 | 203 | necon2ad 2959 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (π β (1...(π β 1)) β π β π)) |
205 | 204 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β (1...(π β 1))) β π β π) |
206 | | ifnefalse 4503 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π β if(π = π, 1, (π + 1)) = (π + 1)) |
207 | 205, 206 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β (1...(π β 1))) β if(π = π, 1, (π + 1)) = (π + 1)) |
208 | 207 | mpteq2dva 5210 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π β (1...(π β 1)) β¦ if(π = π, 1, (π + 1))) = (π β (1...(π β 1)) β¦ (π + 1))) |
209 | 208 | uneq1d 4127 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ((π β (1...(π β 1)) β¦ if(π = π, 1, (π + 1))) βͺ {β¨π, 1β©}) = ((π β (1...(π β 1)) β¦ (π + 1)) βͺ {β¨π, 1β©})) |
210 | 200, 209 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π β (1...π) β¦ if(π = π, 1, (π + 1))) = ((π β (1...(π β 1)) β¦ (π + 1)) βͺ {β¨π, 1β©})) |
211 | 191, 196 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (1...π) = ((1...(π β 1)) βͺ {π})) |
212 | | uzid 12785 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (1 β
β€ β 1 β (β€β₯β1)) |
213 | | peano2uz 12833 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (1 β
(β€β₯β1) β (1 + 1) β
(β€β₯β1)) |
214 | 118, 212,
213 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (1 + 1)
β (β€β₯β1) |
215 | | fzsplit2 13473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((1 + 1)
β (β€β₯β1) β§ π β (β€β₯β1))
β (1...π) = ((1...1)
βͺ ((1 + 1)...π))) |
216 | 214, 184,
215 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (1...π) = ((1...1) βͺ ((1 + 1)...π))) |
217 | | fzsn 13490 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (1 β
β€ β (1...1) = {1}) |
218 | 118, 217 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (1...1) =
{1} |
219 | 218 | uneq1i 4124 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((1...1)
βͺ ((1 + 1)...π)) = ({1}
βͺ ((1 + 1)...π)) |
220 | 219 | equncomi 4120 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((1...1)
βͺ ((1 + 1)...π)) = (((1
+ 1)...π) βͺ
{1}) |
221 | 216, 220 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (1...π) = (((1 + 1)...π) βͺ {1})) |
222 | 210, 211,
221 | f1oeq123d 6783 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((π β (1...π) β¦ if(π = π, 1, (π + 1))):(1...π)β1-1-ontoβ(1...π) β ((π β (1...(π β 1)) β¦ (π + 1)) βͺ {β¨π, 1β©}):((1...(π β 1)) βͺ {π})β1-1-ontoβ(((1
+ 1)...π) βͺ
{1}))) |
223 | 182, 222 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β (1...π) β¦ if(π = π, 1, (π + 1))):(1...π)β1-1-ontoβ(1...π)) |
224 | | f1oco 6812 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((2nd β(1st βπ)):(1...π)β1-1-ontoβ(1...π) β§ (π β (1...π) β¦ if(π = π, 1, (π + 1))):(1...π)β1-1-ontoβ(1...π)) β ((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))):(1...π)β1-1-ontoβ(1...π)) |
225 | 42, 223, 224 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))):(1...π)β1-1-ontoβ(1...π)) |
226 | | dff1o3 6795 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))):(1...π)β1-1-ontoβ(1...π) β (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))):(1...π)βontoβ(1...π) β§ Fun β‘((2nd β(1st
βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))))) |
227 | 226 | simprbi 498 |
. . . . . . . . . . . . . . . . . . 19
β’
(((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))):(1...π)β1-1-ontoβ(1...π) β Fun β‘((2nd β(1st
βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1))))) |
228 | 225, 227 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Fun β‘((2nd β(1st
βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1))))) |
229 | | imain 6591 |
. . . . . . . . . . . . . . . . . 18
β’ (Fun
β‘((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((1...π¦) β© ((π¦ + 1)...π))) = ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) β© (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)))) |
230 | 228, 229 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((1...π¦) β© ((π¦ + 1)...π))) = ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) β© (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)))) |
231 | 48 | nn0red 12481 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ β (0...(π β 1)) β π¦ β β) |
232 | 231 | ltp1d 12092 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ β (0...(π β 1)) β π¦ < (π¦ + 1)) |
233 | | fzdisj 13475 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ < (π¦ + 1) β ((1...π¦) β© ((π¦ + 1)...π)) = β
) |
234 | 232, 233 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β (0...(π β 1)) β ((1...π¦) β© ((π¦ + 1)...π)) = β
) |
235 | 234 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β (0...(π β 1)) β (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((1...π¦) β© ((π¦ + 1)...π))) = (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β β
)) |
236 | | ima0 6034 |
. . . . . . . . . . . . . . . . . 18
β’
(((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β β
) =
β
|
237 | 235, 236 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β (0...(π β 1)) β (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((1...π¦) β© ((π¦ + 1)...π))) = β
) |
238 | 230, 237 | sylan9req 2798 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (0...(π β 1))) β ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) β© (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π))) = β
) |
239 | | imassrn 6029 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...π)) β ran (π β (1...π) β¦ if(π = π, 1, (π + 1))) |
240 | | f1of 6789 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (1...π) β¦ if(π = π, 1, (π + 1))):(1...π)β1-1-ontoβ(1...π) β (π β (1...π) β¦ if(π = π, 1, (π + 1))):(1...π)βΆ(1...π)) |
241 | | frn 6680 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (1...π) β¦ if(π = π, 1, (π + 1))):(1...π)βΆ(1...π) β ran (π β (1...π) β¦ if(π = π, 1, (π + 1))) β (1...π)) |
242 | 223, 240,
241 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ran (π β (1...π) β¦ if(π = π, 1, (π + 1))) β (1...π)) |
243 | 239, 242 | sstrid 3960 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...π)) β (1...π)) |
244 | 243 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β (0...(π β 1))) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...π)) β (1...π)) |
245 | | elfz1end 13478 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β π β (1...π)) |
246 | 66, 245 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β (1...π)) |
247 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (1...π) β¦ if(π = π, 1, (π + 1))) = (π β (1...π) β¦ if(π = π, 1, (π + 1))) |
248 | 198, 247,
30 | fvmpt 6953 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1...π) β ((π β (1...π) β¦ if(π = π, 1, (π + 1)))βπ) = 1) |
249 | 246, 248 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π β (1...π) β¦ if(π = π, 1, (π + 1)))βπ) = 1) |
250 | 249 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β (0...(π β 1))) β ((π β (1...π) β¦ if(π = π, 1, (π + 1)))βπ) = 1) |
251 | | f1ofn 6790 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (1...π) β¦ if(π = π, 1, (π + 1))):(1...π)β1-1-ontoβ(1...π) β (π β (1...π) β¦ if(π = π, 1, (π + 1))) Fn (1...π)) |
252 | 223, 251 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π β (1...π) β¦ if(π = π, 1, (π + 1))) Fn (1...π)) |
253 | 252 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β (0...(π β 1))) β (π β (1...π) β¦ if(π = π, 1, (π + 1))) Fn (1...π)) |
254 | | fzss1 13487 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ + 1) β
(β€β₯β1) β ((π¦ + 1)...π) β (1...π)) |
255 | 63, 254 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ β (0...(π β 1)) β ((π¦ + 1)...π) β (1...π)) |
256 | 255 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β (0...(π β 1))) β ((π¦ + 1)...π) β (1...π)) |
257 | | eluzfz2 13456 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β
(β€β₯β(π¦ + 1)) β π β ((π¦ + 1)...π)) |
258 | 75, 257 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β (0...(π β 1))) β π β ((π¦ + 1)...π)) |
259 | | fnfvima 7188 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β (1...π) β¦ if(π = π, 1, (π + 1))) Fn (1...π) β§ ((π¦ + 1)...π) β (1...π) β§ π β ((π¦ + 1)...π)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1)))βπ) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...π))) |
260 | 253, 256,
258, 259 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β (0...(π β 1))) β ((π β (1...π) β¦ if(π = π, 1, (π + 1)))βπ) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...π))) |
261 | 250, 260 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β (0...(π β 1))) β 1 β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...π))) |
262 | | fnfvima 7188 |
. . . . . . . . . . . . . . . . . 18
β’
(((2nd β(1st βπ)) Fn (1...π) β§ ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...π)) β (1...π) β§ 1 β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...π))) β ((2nd
β(1st βπ))β1) β ((2nd
β(1st βπ)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...π)))) |
263 | 100, 244,
261, 262 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β (0...(π β 1))) β ((2nd
β(1st βπ))β1) β ((2nd
β(1st βπ)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...π)))) |
264 | | imaco 6208 |
. . . . . . . . . . . . . . . . 17
β’
(((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) = ((2nd β(1st
βπ)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...π))) |
265 | 263, 264 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (0...(π β 1))) β ((2nd
β(1st βπ))β1) β (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π))) |
266 | | fnconstg 6735 |
. . . . . . . . . . . . . . . . . 18
β’ (1 β
V β ((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) Fn (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦))) |
267 | 30, 266 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’
((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) Fn (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) |
268 | | fnconstg 6735 |
. . . . . . . . . . . . . . . . . 18
β’ (0 β
V β ((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}) Fn (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π))) |
269 | 33, 268 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’
((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}) Fn (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) |
270 | | fvun2 6938 |
. . . . . . . . . . . . . . . . 17
β’
((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) Fn (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) β§ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}) Fn (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) β§ (((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) β© (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π))) = β
β§ ((2nd
β(1st βπ))β1) β (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)))) β ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))β((2nd
β(1st βπ))β1)) = (((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})β((2nd
β(1st βπ))β1))) |
271 | 267, 269,
270 | mp3an12 1452 |
. . . . . . . . . . . . . . . 16
β’
((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) β© (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π))) = β
β§ ((2nd
β(1st βπ))β1) β (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π))) β ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))β((2nd
β(1st βπ))β1)) = (((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})β((2nd
β(1st βπ))β1))) |
272 | 238, 265,
271 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (0...(π β 1))) β ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))β((2nd
β(1st βπ))β1)) = (((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})β((2nd
β(1st βπ))β1))) |
273 | 33 | fvconst2 7158 |
. . . . . . . . . . . . . . . 16
β’
(((2nd β(1st βπ))β1) β (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) β (((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})β((2nd
β(1st βπ))β1)) = 0) |
274 | 265, 273 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (0...(π β 1))) β (((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})β((2nd
β(1st βπ))β1)) = 0) |
275 | 272, 274 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (0...(π β 1))) β ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))β((2nd
β(1st βπ))β1)) = 0) |
276 | 275 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (0...(π β 1))) β (1 +
((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))β((2nd
β(1st βπ))β1))) = (1 + 0)) |
277 | 97, 113, 276 | 3eqtr4a 2803 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (0...(π β 1))) β (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))β((2nd
β(1st βπ))β1)) = (1 + ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))β((2nd
β(1st βπ))β1)))) |
278 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = ((2nd
β(1st βπ))β1) β (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ) = (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))β((2nd
β(1st βπ))β1))) |
279 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = ((2nd
β(1st βπ))β1) β ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ) = ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))β((2nd
β(1st βπ))β1))) |
280 | 279 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (π = ((2nd
β(1st βπ))β1) β (1 + ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)) = (1 + ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))β((2nd
β(1st βπ))β1)))) |
281 | 278, 280 | eqeq12d 2753 |
. . . . . . . . . . . 12
β’ (π = ((2nd
β(1st βπ))β1) β ((((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ) = (1 + ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)) β (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))β((2nd
β(1st βπ))β1)) = (1 + ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))β((2nd
β(1st βπ))β1))))) |
282 | 277, 281 | syl5ibrcom 247 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (0...(π β 1))) β (π = ((2nd β(1st
βπ))β1) β
(((((2nd β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ) = (1 + ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)))) |
283 | 282 | imp 408 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (0...(π β 1))) β§ π = ((2nd β(1st
βπ))β1)) β
(((((2nd β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ) = (1 + ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ))) |
284 | 283 | adantlr 714 |
. . . . . . . . 9
β’ ((((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β§ π = ((2nd β(1st
βπ))β1)) β
(((((2nd β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ) = (1 + ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ))) |
285 | | eldifsn 4752 |
. . . . . . . . . . . . . 14
β’ (π β ((1...π) β {((2nd
β(1st βπ))β1)}) β (π β (1...π) β§ π β ((2nd β(1st
βπ))β1))) |
286 | | df-ne 2945 |
. . . . . . . . . . . . . . 15
β’ (π β ((2nd
β(1st βπ))β1) β Β¬ π = ((2nd β(1st
βπ))β1)) |
287 | 286 | anbi2i 624 |
. . . . . . . . . . . . . 14
β’ ((π β (1...π) β§ π β ((2nd β(1st
βπ))β1)) β
(π β (1...π) β§ Β¬ π = ((2nd β(1st
βπ))β1))) |
288 | 285, 287 | bitri 275 |
. . . . . . . . . . . . 13
β’ (π β ((1...π) β {((2nd
β(1st βπ))β1)}) β (π β (1...π) β§ Β¬ π = ((2nd β(1st
βπ))β1))) |
289 | | fnconstg 6735 |
. . . . . . . . . . . . . . . . . 18
β’ (1 β
V β (((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) Fn ((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1)))) |
290 | 30, 289 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’
(((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) Fn ((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) |
291 | 290, 35 | pm3.2i 472 |
. . . . . . . . . . . . . . . 16
β’
((((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) Fn ((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) β§ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}) Fn ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) |
292 | | imain 6591 |
. . . . . . . . . . . . . . . . . 18
β’ (Fun
β‘(2nd β(1st
βπ)) β
((2nd β(1st βπ)) β (((1 + 1)...(π¦ + 1)) β© (((π¦ + 1) + 1)...π))) = (((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) β© ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)))) |
293 | 45, 292 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((2nd
β(1st βπ)) β (((1 + 1)...(π¦ + 1)) β© (((π¦ + 1) + 1)...π))) = (((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) β© ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)))) |
294 | | fzdisj 13475 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π¦ + 1) < ((π¦ + 1) + 1) β (((1 + 1)...(π¦ + 1)) β© (((π¦ + 1) + 1)...π)) = β
) |
295 | 52, 294 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β (0...(π β 1)) β (((1 + 1)...(π¦ + 1)) β© (((π¦ + 1) + 1)...π)) = β
) |
296 | 295 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β (0...(π β 1)) β ((2nd
β(1st βπ)) β (((1 + 1)...(π¦ + 1)) β© (((π¦ + 1) + 1)...π))) = ((2nd
β(1st βπ)) β β
)) |
297 | 296, 56 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β (0...(π β 1)) β ((2nd
β(1st βπ)) β (((1 + 1)...(π¦ + 1)) β© (((π¦ + 1) + 1)...π))) = β
) |
298 | 293, 297 | sylan9req 2798 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (0...(π β 1))) β (((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) β© ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) = β
) |
299 | | fnun 6619 |
. . . . . . . . . . . . . . . 16
β’
((((((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) Fn ((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) β§ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}) Fn ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) β§ (((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) β© ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) = β
) β ((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) Fn (((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) βͺ ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)))) |
300 | 291, 298,
299 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (0...(π β 1))) β ((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) Fn (((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) βͺ ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)))) |
301 | | imaundi 6107 |
. . . . . . . . . . . . . . . . 17
β’
((2nd β(1st βπ)) β (((1 + 1)...(π¦ + 1)) βͺ (((π¦ + 1) + 1)...π))) = (((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) βͺ ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) |
302 | | fzpred 13496 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β
(β€β₯β1) β (1...π) = ({1} βͺ ((1 + 1)...π))) |
303 | 184, 302 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (1...π) = ({1} βͺ ((1 + 1)...π))) |
304 | | uncom 4118 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ({1}
βͺ ((1 + 1)...π)) = (((1
+ 1)...π) βͺ
{1}) |
305 | 303, 304 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (1...π) = (((1 + 1)...π) βͺ {1})) |
306 | 305 | difeq1d 4086 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((1...π) β {1}) = ((((1 + 1)...π) βͺ {1}) β
{1})) |
307 | | difun2 4445 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((1 +
1)...π) βͺ {1}) β
{1}) = (((1 + 1)...π)
β {1}) |
308 | | disj3 4418 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((1 +
1)...π) β© {1}) =
β
β ((1 + 1)...π) = (((1 + 1)...π) β {1})) |
309 | 179, 308 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((1 +
1)...π) = (((1 + 1)...π) β {1}) |
310 | 307, 309 | eqtr4i 2768 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((1 +
1)...π) βͺ {1}) β
{1}) = ((1 + 1)...π) |
311 | 306, 310 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((1...π) β {1}) = ((1 + 1)...π)) |
312 | 311 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β (0...(π β 1))) β ((1...π) β {1}) = ((1 + 1)...π)) |
313 | | eluzp1p1 12798 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ + 1) β
(β€β₯β1) β ((π¦ + 1) + 1) β
(β€β₯β(1 + 1))) |
314 | 63, 313 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ β (0...(π β 1)) β ((π¦ + 1) + 1) β
(β€β₯β(1 + 1))) |
315 | | fzsplit2 13473 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π¦ + 1) + 1) β
(β€β₯β(1 + 1)) β§ π β (β€β₯β(π¦ + 1))) β ((1 + 1)...π) = (((1 + 1)...(π¦ + 1)) βͺ (((π¦ + 1) + 1)...π))) |
316 | 314, 75, 315 | syl2an2 685 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β (0...(π β 1))) β ((1 + 1)...π) = (((1 + 1)...(π¦ + 1)) βͺ (((π¦ + 1) + 1)...π))) |
317 | 312, 316 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β (0...(π β 1))) β ((1...π) β {1}) = (((1 + 1)...(π¦ + 1)) βͺ (((π¦ + 1) + 1)...π))) |
318 | 317 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β (0...(π β 1))) β ((2nd
β(1st βπ)) β ((1...π) β {1})) = ((2nd
β(1st βπ)) β (((1 + 1)...(π¦ + 1)) βͺ (((π¦ + 1) + 1)...π)))) |
319 | | imadif 6590 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Fun
β‘(2nd β(1st
βπ)) β
((2nd β(1st βπ)) β ((1...π) β {1})) = (((2nd
β(1st βπ)) β (1...π)) β ((2nd
β(1st βπ)) β {1}))) |
320 | 45, 319 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((2nd
β(1st βπ)) β ((1...π) β {1})) = (((2nd
β(1st βπ)) β (1...π)) β ((2nd
β(1st βπ)) β {1}))) |
321 | | eluzfz1 13455 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β
(β€β₯β1) β 1 β (1...π)) |
322 | 184, 321 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β 1 β (1...π)) |
323 | | fnsnfv 6925 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((2nd β(1st βπ)) Fn (1...π) β§ 1 β (1...π)) β {((2nd
β(1st βπ))β1)} = ((2nd
β(1st βπ)) β {1})) |
324 | 99, 322, 323 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β {((2nd
β(1st βπ))β1)} = ((2nd
β(1st βπ)) β {1})) |
325 | 324 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((2nd
β(1st βπ)) β {1}) = {((2nd
β(1st βπ))β1)}) |
326 | 81, 325 | difeq12d 4088 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (((2nd
β(1st βπ)) β (1...π)) β ((2nd
β(1st βπ)) β {1})) = ((1...π) β {((2nd
β(1st βπ))β1)})) |
327 | 320, 326 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((2nd
β(1st βπ)) β ((1...π) β {1})) = ((1...π) β {((2nd
β(1st βπ))β1)})) |
328 | 327 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β (0...(π β 1))) β ((2nd
β(1st βπ)) β ((1...π) β {1})) = ((1...π) β {((2nd
β(1st βπ))β1)})) |
329 | 318, 328 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β (0...(π β 1))) β ((2nd
β(1st βπ)) β (((1 + 1)...(π¦ + 1)) βͺ (((π¦ + 1) + 1)...π))) = ((1...π) β {((2nd
β(1st βπ))β1)})) |
330 | 301, 329 | eqtr3id 2791 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (0...(π β 1))) β (((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) βͺ ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) = ((1...π) β {((2nd
β(1st βπ))β1)})) |
331 | 330 | fneq2d 6601 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (0...(π β 1))) β (((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) Fn (((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) βͺ ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) β ((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) Fn ((1...π) β {((2nd
β(1st βπ))β1)}))) |
332 | 300, 331 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (0...(π β 1))) β ((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) Fn ((1...π) β {((2nd
β(1st βπ))β1)})) |
333 | | disjdifr 4437 |
. . . . . . . . . . . . . . 15
β’
(((1...π) β
{((2nd β(1st βπ))β1)}) β© {((2nd
β(1st βπ))β1)}) = β
|
334 | | fnconstg 6735 |
. . . . . . . . . . . . . . . . . 18
β’ (1 β
V β ({((2nd β(1st βπ))β1)} Γ {1}) Fn
{((2nd β(1st βπ))β1)}) |
335 | 30, 334 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’
({((2nd β(1st βπ))β1)} Γ {1}) Fn
{((2nd β(1st βπ))β1)} |
336 | | fvun1 6937 |
. . . . . . . . . . . . . . . . 17
β’
((((((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) Fn ((1...π) β {((2nd
β(1st βπ))β1)}) β§ ({((2nd
β(1st βπ))β1)} Γ {1}) Fn
{((2nd β(1st βπ))β1)} β§ ((((1...π) β {((2nd
β(1st βπ))β1)}) β© {((2nd
β(1st βπ))β1)}) = β
β§ π β ((1...π) β {((2nd
β(1st βπ))β1)}))) β ((((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {1}))βπ) = (((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ)) |
337 | 335, 336 | mp3an2 1450 |
. . . . . . . . . . . . . . . 16
β’
((((((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) Fn ((1...π) β {((2nd
β(1st βπ))β1)}) β§ ((((1...π) β {((2nd
β(1st βπ))β1)}) β© {((2nd
β(1st βπ))β1)}) = β
β§ π β ((1...π) β {((2nd
β(1st βπ))β1)}))) β ((((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {1}))βπ) = (((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ)) |
338 | | fnconstg 6735 |
. . . . . . . . . . . . . . . . . 18
β’ (0 β
V β ({((2nd β(1st βπ))β1)} Γ {0}) Fn
{((2nd β(1st βπ))β1)}) |
339 | 33, 338 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’
({((2nd β(1st βπ))β1)} Γ {0}) Fn
{((2nd β(1st βπ))β1)} |
340 | | fvun1 6937 |
. . . . . . . . . . . . . . . . 17
β’
((((((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) Fn ((1...π) β {((2nd
β(1st βπ))β1)}) β§ ({((2nd
β(1st βπ))β1)} Γ {0}) Fn
{((2nd β(1st βπ))β1)} β§ ((((1...π) β {((2nd
β(1st βπ))β1)}) β© {((2nd
β(1st βπ))β1)}) = β
β§ π β ((1...π) β {((2nd
β(1st βπ))β1)}))) β ((((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {0}))βπ) = (((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ)) |
341 | 339, 340 | mp3an2 1450 |
. . . . . . . . . . . . . . . 16
β’
((((((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) Fn ((1...π) β {((2nd
β(1st βπ))β1)}) β§ ((((1...π) β {((2nd
β(1st βπ))β1)}) β© {((2nd
β(1st βπ))β1)}) = β
β§ π β ((1...π) β {((2nd
β(1st βπ))β1)}))) β ((((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {0}))βπ) = (((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ)) |
342 | 337, 341 | eqtr4d 2780 |
. . . . . . . . . . . . . . 15
β’
((((((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) Fn ((1...π) β {((2nd
β(1st βπ))β1)}) β§ ((((1...π) β {((2nd
β(1st βπ))β1)}) β© {((2nd
β(1st βπ))β1)}) = β
β§ π β ((1...π) β {((2nd
β(1st βπ))β1)}))) β ((((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {1}))βπ) = ((((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {0}))βπ)) |
343 | 333, 342 | mpanr1 702 |
. . . . . . . . . . . . . 14
β’
((((((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) Fn ((1...π) β {((2nd
β(1st βπ))β1)}) β§ π β ((1...π) β {((2nd
β(1st βπ))β1)})) β ((((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {1}))βπ) = ((((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {0}))βπ)) |
344 | 332, 343 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β ((1...π) β {((2nd
β(1st βπ))β1)})) β ((((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {1}))βπ) = ((((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {0}))βπ)) |
345 | 288, 344 | sylan2br 596 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (0...(π β 1))) β§ (π β (1...π) β§ Β¬ π = ((2nd β(1st
βπ))β1)))
β ((((((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {1}))βπ) = ((((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {0}))βπ)) |
346 | 345 | anassrs 469 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β§ Β¬ π = ((2nd β(1st
βπ))β1)) β
((((((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {1}))βπ) = ((((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {0}))βπ)) |
347 | | fzpred 13496 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π¦ + 1) β
(β€β₯β1) β (1...(π¦ + 1)) = ({1} βͺ ((1 + 1)...(π¦ + 1)))) |
348 | 63, 347 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ β (0...(π β 1)) β (1...(π¦ + 1)) = ({1} βͺ ((1 + 1)...(π¦ + 1)))) |
349 | 348 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β (0...(π β 1)) β ((2nd
β(1st βπ)) β (1...(π¦ + 1))) = ((2nd
β(1st βπ)) β ({1} βͺ ((1 + 1)...(π¦ + 1))))) |
350 | 349 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β (0...(π β 1))) β ((2nd
β(1st βπ)) β (1...(π¦ + 1))) = ((2nd
β(1st βπ)) β ({1} βͺ ((1 + 1)...(π¦ + 1))))) |
351 | 324 | uneq1d 4127 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ({((2nd
β(1st βπ))β1)} βͺ ((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1)))) = (((2nd
β(1st βπ)) β {1}) βͺ ((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))))) |
352 | | uncom 4118 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) βͺ {((2nd
β(1st βπ))β1)}) = ({((2nd
β(1st βπ))β1)} βͺ ((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1)))) |
353 | | imaundi 6107 |
. . . . . . . . . . . . . . . . . . . 20
β’
((2nd β(1st βπ)) β ({1} βͺ ((1 + 1)...(π¦ + 1)))) = (((2nd
β(1st βπ)) β {1}) βͺ ((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1)))) |
354 | 351, 352,
353 | 3eqtr4g 2802 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) βͺ {((2nd
β(1st βπ))β1)}) = ((2nd
β(1st βπ)) β ({1} βͺ ((1 + 1)...(π¦ + 1))))) |
355 | 354 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β (0...(π β 1))) β (((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) βͺ {((2nd
β(1st βπ))β1)}) = ((2nd
β(1st βπ)) β ({1} βͺ ((1 + 1)...(π¦ + 1))))) |
356 | 350, 355 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β (0...(π β 1))) β ((2nd
β(1st βπ)) β (1...(π¦ + 1))) = (((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) βͺ {((2nd
β(1st βπ))β1)})) |
357 | 356 | xpeq1d 5667 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (0...(π β 1))) β (((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) = ((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) βͺ {((2nd
β(1st βπ))β1)}) Γ {1})) |
358 | | xpundir 5706 |
. . . . . . . . . . . . . . . 16
β’
((((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) βͺ {((2nd
β(1st βπ))β1)}) Γ {1}) =
((((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ ({((2nd
β(1st βπ))β1)} Γ {1})) |
359 | 357, 358 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (0...(π β 1))) β (((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) = ((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ ({((2nd
β(1st βπ))β1)} Γ {1}))) |
360 | 359 | uneq1d 4127 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (0...(π β 1))) β ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) = (((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ ({((2nd
β(1st βπ))β1)} Γ {1})) βͺ
(((2nd β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))) |
361 | | un23 4133 |
. . . . . . . . . . . . . 14
β’
(((((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ ({((2nd
β(1st βπ))β1)} Γ {1})) βͺ
(((2nd β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) = (((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {1})) |
362 | 360, 361 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (0...(π β 1))) β ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) = (((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {1}))) |
363 | 362 | fveq1d 6849 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (0...(π β 1))) β (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ) = ((((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {1}))βπ)) |
364 | 363 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β§ Β¬ π = ((2nd β(1st
βπ))β1)) β
(((((2nd β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ) = ((((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {1}))βπ)) |
365 | | imaco 6208 |
. . . . . . . . . . . . . . . . 17
β’
(((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) = ((2nd β(1st
βπ)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β (1...π¦))) |
366 | | df-ima 5651 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β (1...π¦)) = ran ((π β (1...π) β¦ if(π = π, 1, (π + 1))) βΎ (1...π¦)) |
367 | | peano2uz 12833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β 1) β
(β€β₯βπ¦) β ((π β 1) + 1) β
(β€β₯βπ¦)) |
368 | 71, 367 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ β (0...(π β 1)) β ((π β 1) + 1) β
(β€β₯βπ¦)) |
369 | 368 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π¦ β (0...(π β 1))) β ((π β 1) + 1) β
(β€β₯βπ¦)) |
370 | 70, 369 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π¦ β (0...(π β 1))) β π β (β€β₯βπ¦)) |
371 | | fzss2 13488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β
(β€β₯βπ¦) β (1...π¦) β (1...π)) |
372 | 370, 371 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π¦ β (0...(π β 1))) β (1...π¦) β (1...π)) |
373 | 372 | resmptd 5999 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π¦ β (0...(π β 1))) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) βΎ (1...π¦)) = (π β (1...π¦) β¦ if(π = π, 1, (π + 1)))) |
374 | | fzss2 13488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β 1) β
(β€β₯βπ¦) β (1...π¦) β (1...(π β 1))) |
375 | 71, 374 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π¦ β (0...(π β 1)) β (1...π¦) β (1...(π β 1))) |
376 | 375 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π¦ β (0...(π β 1))) β (1...π¦) β (1...(π β 1))) |
377 | 168 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π¦ β (0...(π β 1))) β Β¬ π β (1...(π β 1))) |
378 | 376, 377 | ssneldd 3952 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π¦ β (0...(π β 1))) β Β¬ π β (1...π¦)) |
379 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = π β (π β (1...π¦) β π β (1...π¦))) |
380 | 379 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = π β (Β¬ π β (1...π¦) β Β¬ π β (1...π¦))) |
381 | 378, 380 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π¦ β (0...(π β 1))) β (π = π β Β¬ π β (1...π¦))) |
382 | 381 | necon2ad 2959 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π¦ β (0...(π β 1))) β (π β (1...π¦) β π β π)) |
383 | 382 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (1...π¦)) β π β π) |
384 | 383, 206 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (1...π¦)) β if(π = π, 1, (π + 1)) = (π + 1)) |
385 | 384 | mpteq2dva 5210 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π¦ β (0...(π β 1))) β (π β (1...π¦) β¦ if(π = π, 1, (π + 1))) = (π β (1...π¦) β¦ (π + 1))) |
386 | 373, 385 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ β (0...(π β 1))) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) βΎ (1...π¦)) = (π β (1...π¦) β¦ (π + 1))) |
387 | 386 | rneqd 5898 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β (0...(π β 1))) β ran ((π β (1...π) β¦ if(π = π, 1, (π + 1))) βΎ (1...π¦)) = ran (π β (1...π¦) β¦ (π + 1))) |
388 | 366, 387 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β (0...(π β 1))) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β (1...π¦)) = ran (π β (1...π¦) β¦ (π + 1))) |
389 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (1...π¦) β¦ (π + 1)) = (π β (1...π¦) β¦ (π + 1)) |
390 | 389 | elrnmpt 5916 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β V β (π β ran (π β (1...π¦) β¦ (π + 1)) β βπ β (1...π¦)π = (π + 1))) |
391 | 390 | elv 3454 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ran (π β (1...π¦) β¦ (π + 1)) β βπ β (1...π¦)π = (π + 1)) |
392 | | elfzelz 13448 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π¦ β (0...(π β 1)) β π¦ β β€) |
393 | 392 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π¦ β (0...(π β 1))) β π¦ β β€) |
394 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π¦ β β€ β§ π β (1...π¦)) β π β (1...π¦)) |
395 | 118 | jctl 525 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π¦ β β€ β (1 β
β€ β§ π¦ β
β€)) |
396 | | elfzelz 13448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (1...π¦) β π β β€) |
397 | 396, 118 | jctir 522 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (1...π¦) β (π β β€ β§ 1 β
β€)) |
398 | | fzaddel 13482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((1
β β€ β§ π¦
β β€) β§ (π
β β€ β§ 1 β β€)) β (π β (1...π¦) β (π + 1) β ((1 + 1)...(π¦ + 1)))) |
399 | 395, 397,
398 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π¦ β β€ β§ π β (1...π¦)) β (π β (1...π¦) β (π + 1) β ((1 + 1)...(π¦ + 1)))) |
400 | 394, 399 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π¦ β β€ β§ π β (1...π¦)) β (π + 1) β ((1 + 1)...(π¦ + 1))) |
401 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (π + 1) β (π β ((1 + 1)...(π¦ + 1)) β (π + 1) β ((1 + 1)...(π¦ + 1)))) |
402 | 400, 401 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π¦ β β€ β§ π β (1...π¦)) β (π = (π + 1) β π β ((1 + 1)...(π¦ + 1)))) |
403 | 402 | rexlimdva 3153 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π¦ β β€ β
(βπ β (1...π¦)π = (π + 1) β π β ((1 + 1)...(π¦ + 1)))) |
404 | | elfzelz 13448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β ((1 + 1)...(π¦ + 1)) β π β β€) |
405 | 404 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β ((1 + 1)...(π¦ + 1)) β π β β) |
406 | | npcan1 11587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β β β ((π β 1) + 1) = π) |
407 | 405, 406 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β ((1 + 1)...(π¦ + 1)) β ((π β 1) + 1) = π) |
408 | 407 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β ((1 + 1)...(π¦ + 1)) β (((π β 1) + 1) β ((1 +
1)...(π¦ + 1)) β π β ((1 + 1)...(π¦ + 1)))) |
409 | 408 | ibir 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ((1 + 1)...(π¦ + 1)) β ((π β 1) + 1) β ((1 +
1)...(π¦ +
1))) |
410 | 409 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π¦ β β€ β§ π β ((1 + 1)...(π¦ + 1))) β ((π β 1) + 1) β ((1 +
1)...(π¦ +
1))) |
411 | | peano2zm 12553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β€ β (π β 1) β
β€) |
412 | 404, 411 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β ((1 + 1)...(π¦ + 1)) β (π β 1) β
β€) |
413 | 412, 118 | jctir 522 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ((1 + 1)...(π¦ + 1)) β ((π β 1) β β€ β§
1 β β€)) |
414 | | fzaddel 13482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((1
β β€ β§ π¦
β β€) β§ ((π
β 1) β β€ β§ 1 β β€)) β ((π β 1) β (1...π¦) β ((π β 1) + 1) β ((1 + 1)...(π¦ + 1)))) |
415 | 395, 413,
414 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π¦ β β€ β§ π β ((1 + 1)...(π¦ + 1))) β ((π β 1) β (1...π¦) β ((π β 1) + 1) β ((1 + 1)...(π¦ + 1)))) |
416 | 410, 415 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π¦ β β€ β§ π β ((1 + 1)...(π¦ + 1))) β (π β 1) β (1...π¦)) |
417 | 405 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π¦ β β€ β§ π β ((1 + 1)...(π¦ + 1))) β π β
β) |
418 | 406 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β π = ((π β 1) + 1)) |
419 | 417, 418 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π¦ β β€ β§ π β ((1 + 1)...(π¦ + 1))) β π = ((π β 1) + 1)) |
420 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = (π β 1) β (π + 1) = ((π β 1) + 1)) |
421 | 420 | rspceeqv 3600 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β 1) β (1...π¦) β§ π = ((π β 1) + 1)) β βπ β (1...π¦)π = (π + 1)) |
422 | 416, 419,
421 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π¦ β β€ β§ π β ((1 + 1)...(π¦ + 1))) β βπ β (1...π¦)π = (π + 1)) |
423 | 422 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π¦ β β€ β (π β ((1 + 1)...(π¦ + 1)) β βπ β (1...π¦)π = (π + 1))) |
424 | 403, 423 | impbid 211 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ β β€ β
(βπ β (1...π¦)π = (π + 1) β π β ((1 + 1)...(π¦ + 1)))) |
425 | 393, 424 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ β (0...(π β 1))) β (βπ β (1...π¦)π = (π + 1) β π β ((1 + 1)...(π¦ + 1)))) |
426 | 391, 425 | bitrid 283 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β (0...(π β 1))) β (π β ran (π β (1...π¦) β¦ (π + 1)) β π β ((1 + 1)...(π¦ + 1)))) |
427 | 426 | eqrdv 2735 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β (0...(π β 1))) β ran (π β (1...π¦) β¦ (π + 1)) = ((1 + 1)...(π¦ + 1))) |
428 | 388, 427 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β (0...(π β 1))) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β (1...π¦)) = ((1 + 1)...(π¦ + 1))) |
429 | 428 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β (0...(π β 1))) β ((2nd
β(1st βπ)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β (1...π¦))) = ((2nd β(1st
βπ)) β ((1 +
1)...(π¦ +
1)))) |
430 | 365, 429 | eqtrid 2789 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (0...(π β 1))) β (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) = ((2nd β(1st
βπ)) β ((1 +
1)...(π¦ +
1)))) |
431 | 430 | xpeq1d 5667 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (0...(π β 1))) β ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) = (((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1})) |
432 | | imaundi 6107 |
. . . . . . . . . . . . . . . . . . 19
β’
(((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ({π} βͺ ((π¦ + 1)...(π β 1)))) = ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β {π}) βͺ (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...(π β 1)))) |
433 | | imaco 6208 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β {π}) = ((2nd β(1st
βπ)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β {π})) |
434 | | imaco 6208 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...(π β 1))) = ((2nd
β(1st βπ)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...(π β 1)))) |
435 | 433, 434 | uneq12i 4126 |
. . . . . . . . . . . . . . . . . . 19
β’
((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β {π}) βͺ (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...(π β 1)))) = (((2nd
β(1st βπ)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β {π})) βͺ ((2nd
β(1st βπ)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...(π β 1))))) |
436 | 432, 435 | eqtri 2765 |
. . . . . . . . . . . . . . . . . 18
β’
(((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ({π} βͺ ((π¦ + 1)...(π β 1)))) = (((2nd
β(1st βπ)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β {π})) βͺ ((2nd
β(1st βπ)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...(π β 1))))) |
437 | 189 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π¦ β (0...(π β 1))) β π β (β€β₯β(π β 1))) |
438 | | fzsplit2 13473 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β 1) + 1) β
(β€β₯β(π¦ + 1)) β§ π β (β€β₯β(π β 1))) β ((π¦ + 1)...π) = (((π¦ + 1)...(π β 1)) βͺ (((π β 1) + 1)...π))) |
439 | 73, 437, 438 | syl2an2 685 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ β (0...(π β 1))) β ((π¦ + 1)...π) = (((π¦ + 1)...(π β 1)) βͺ (((π β 1) + 1)...π))) |
440 | 195 | uneq2d 4128 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (((π¦ + 1)...(π β 1)) βͺ (((π β 1) + 1)...π)) = (((π¦ + 1)...(π β 1)) βͺ {π})) |
441 | 440 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ β (0...(π β 1))) β (((π¦ + 1)...(π β 1)) βͺ (((π β 1) + 1)...π)) = (((π¦ + 1)...(π β 1)) βͺ {π})) |
442 | 439, 441 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β (0...(π β 1))) β ((π¦ + 1)...π) = (((π¦ + 1)...(π β 1)) βͺ {π})) |
443 | | uncom 4118 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π¦ + 1)...(π β 1)) βͺ {π}) = ({π} βͺ ((π¦ + 1)...(π β 1))) |
444 | 442, 443 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β (0...(π β 1))) β ((π¦ + 1)...π) = ({π} βͺ ((π¦ + 1)...(π β 1)))) |
445 | 444 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β (0...(π β 1))) β (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) = (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ({π} βͺ ((π¦ + 1)...(π β 1))))) |
446 | 249 | sneqd 4603 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β {((π β (1...π) β¦ if(π = π, 1, (π + 1)))βπ)} = {1}) |
447 | | fnsnfv 6925 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β (1...π) β¦ if(π = π, 1, (π + 1))) Fn (1...π) β§ π β (1...π)) β {((π β (1...π) β¦ if(π = π, 1, (π + 1)))βπ)} = ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β {π})) |
448 | 252, 246,
447 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β {((π β (1...π) β¦ if(π = π, 1, (π + 1)))βπ)} = ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β {π})) |
449 | 446, 448 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β {1} = ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β {π})) |
450 | 449 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((2nd
β(1st βπ)) β {1}) = ((2nd
β(1st βπ)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β {π}))) |
451 | 324, 450 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β {((2nd
β(1st βπ))β1)} = ((2nd
β(1st βπ)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β {π}))) |
452 | 451 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β (0...(π β 1))) β {((2nd
β(1st βπ))β1)} = ((2nd
β(1st βπ)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β {π}))) |
453 | | df-ima 5651 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...(π β 1))) = ran ((π β (1...π) β¦ if(π = π, 1, (π + 1))) βΎ ((π¦ + 1)...(π β 1))) |
454 | | fzss1 13487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π¦ + 1) β
(β€β₯β1) β ((π¦ + 1)...(π β 1)) β (1...(π β 1))) |
455 | 63, 454 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ β (0...(π β 1)) β ((π¦ + 1)...(π β 1)) β (1...(π β 1))) |
456 | | fzss2 13488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β
(β€β₯β(π β 1)) β (1...(π β 1)) β (1...π)) |
457 | 189, 456 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (1...(π β 1)) β (1...π)) |
458 | 455, 457 | sylan9ssr 3963 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π¦ β (0...(π β 1))) β ((π¦ + 1)...(π β 1)) β (1...π)) |
459 | 458 | resmptd 5999 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π¦ β (0...(π β 1))) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) βΎ ((π¦ + 1)...(π β 1))) = (π β ((π¦ + 1)...(π β 1)) β¦ if(π = π, 1, (π + 1)))) |
460 | | elfzle2 13452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β ((π¦ + 1)...(π β 1)) β π β€ (π β 1)) |
461 | 166, 460 | nsyl 140 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β Β¬ π β ((π¦ + 1)...(π β 1))) |
462 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = π β (π β ((π¦ + 1)...(π β 1)) β π β ((π¦ + 1)...(π β 1)))) |
463 | 462 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = π β (Β¬ π β ((π¦ + 1)...(π β 1)) β Β¬ π β ((π¦ + 1)...(π β 1)))) |
464 | 461, 463 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (π = π β Β¬ π β ((π¦ + 1)...(π β 1)))) |
465 | 464 | con2d 134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π β ((π¦ + 1)...(π β 1)) β Β¬ π = π)) |
466 | 465 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π β ((π¦ + 1)...(π β 1))) β Β¬ π = π) |
467 | 466 | iffalsed 4502 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β ((π¦ + 1)...(π β 1))) β if(π = π, 1, (π + 1)) = (π + 1)) |
468 | 467 | mpteq2dva 5210 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (π β ((π¦ + 1)...(π β 1)) β¦ if(π = π, 1, (π + 1))) = (π β ((π¦ + 1)...(π β 1)) β¦ (π + 1))) |
469 | 468 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π¦ β (0...(π β 1))) β (π β ((π¦ + 1)...(π β 1)) β¦ if(π = π, 1, (π + 1))) = (π β ((π¦ + 1)...(π β 1)) β¦ (π + 1))) |
470 | 459, 469 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π¦ β (0...(π β 1))) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) βΎ ((π¦ + 1)...(π β 1))) = (π β ((π¦ + 1)...(π β 1)) β¦ (π + 1))) |
471 | 470 | rneqd 5898 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π¦ β (0...(π β 1))) β ran ((π β (1...π) β¦ if(π = π, 1, (π + 1))) βΎ ((π¦ + 1)...(π β 1))) = ran (π β ((π¦ + 1)...(π β 1)) β¦ (π + 1))) |
472 | 453, 471 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ β (0...(π β 1))) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...(π β 1))) = ran (π β ((π¦ + 1)...(π β 1)) β¦ (π + 1))) |
473 | | elfzelz 13448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β (((π¦ + 1) + 1)...((π β 1) + 1)) β π β β€) |
474 | 473 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β (((π¦ + 1) + 1)...((π β 1) + 1)) β π β β) |
475 | 474, 406 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β (((π¦ + 1) + 1)...((π β 1) + 1)) β ((π β 1) + 1) = π) |
476 | 475 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (((π¦ + 1) + 1)...((π β 1) + 1)) β (((π β 1) + 1) β (((π¦ + 1) + 1)...((π β 1) + 1)) β π β (((π¦ + 1) + 1)...((π β 1) + 1)))) |
477 | 476 | ibir 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (((π¦ + 1) + 1)...((π β 1) + 1)) β ((π β 1) + 1) β (((π¦ + 1) + 1)...((π β 1) + 1))) |
478 | 477 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (((π¦ + 1) + 1)...((π β 1) + 1))) β ((π β 1) + 1) β (((π¦ + 1) + 1)...((π β 1) + 1))) |
479 | 50 | nnzd 12533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π¦ β (0...(π β 1)) β (π¦ + 1) β β€) |
480 | 117, 479 | anim12ci 615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π¦ β (0...(π β 1))) β ((π¦ + 1) β β€ β§ (π β 1) β
β€)) |
481 | 473, 411 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (((π¦ + 1) + 1)...((π β 1) + 1)) β (π β 1) β β€) |
482 | 481, 118 | jctir 522 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (((π¦ + 1) + 1)...((π β 1) + 1)) β ((π β 1) β β€ β§
1 β β€)) |
483 | | fzaddel 13482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π¦ + 1) β β€ β§
(π β 1) β
β€) β§ ((π β
1) β β€ β§ 1 β β€)) β ((π β 1) β ((π¦ + 1)...(π β 1)) β ((π β 1) + 1) β (((π¦ + 1) + 1)...((π β 1) + 1)))) |
484 | 480, 482,
483 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (((π¦ + 1) + 1)...((π β 1) + 1))) β ((π β 1) β ((π¦ + 1)...(π β 1)) β ((π β 1) + 1) β (((π¦ + 1) + 1)...((π β 1) + 1)))) |
485 | 478, 484 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (((π¦ + 1) + 1)...((π β 1) + 1))) β (π β 1) β ((π¦ + 1)...(π β 1))) |
486 | 474, 418 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (((π¦ + 1) + 1)...((π β 1) + 1)) β π = ((π β 1) + 1)) |
487 | 486 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (((π¦ + 1) + 1)...((π β 1) + 1))) β π = ((π β 1) + 1)) |
488 | 420 | rspceeqv 3600 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β 1) β ((π¦ + 1)...(π β 1)) β§ π = ((π β 1) + 1)) β βπ β ((π¦ + 1)...(π β 1))π = (π + 1)) |
489 | 485, 487,
488 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (((π¦ + 1) + 1)...((π β 1) + 1))) β βπ β ((π¦ + 1)...(π β 1))π = (π + 1)) |
490 | 489 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π¦ β (0...(π β 1))) β (π β (((π¦ + 1) + 1)...((π β 1) + 1)) β βπ β ((π¦ + 1)...(π β 1))π = (π + 1))) |
491 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β ((π¦ + 1)...(π β 1))) β π β ((π¦ + 1)...(π β 1))) |
492 | | elfzelz 13448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β ((π¦ + 1)...(π β 1)) β π β β€) |
493 | 492, 118 | jctir 522 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β ((π¦ + 1)...(π β 1)) β (π β β€ β§ 1 β
β€)) |
494 | | fzaddel 13482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π¦ + 1) β β€ β§
(π β 1) β
β€) β§ (π β
β€ β§ 1 β β€)) β (π β ((π¦ + 1)...(π β 1)) β (π + 1) β (((π¦ + 1) + 1)...((π β 1) + 1)))) |
495 | 480, 493,
494 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β ((π¦ + 1)...(π β 1))) β (π β ((π¦ + 1)...(π β 1)) β (π + 1) β (((π¦ + 1) + 1)...((π β 1) + 1)))) |
496 | 491, 495 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β ((π¦ + 1)...(π β 1))) β (π + 1) β (((π¦ + 1) + 1)...((π β 1) + 1))) |
497 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = (π + 1) β (π β (((π¦ + 1) + 1)...((π β 1) + 1)) β (π + 1) β (((π¦ + 1) + 1)...((π β 1) + 1)))) |
498 | 496, 497 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β ((π¦ + 1)...(π β 1))) β (π = (π + 1) β π β (((π¦ + 1) + 1)...((π β 1) + 1)))) |
499 | 498 | rexlimdva 3153 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π¦ β (0...(π β 1))) β (βπ β ((π¦ + 1)...(π β 1))π = (π + 1) β π β (((π¦ + 1) + 1)...((π β 1) + 1)))) |
500 | 490, 499 | impbid 211 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π¦ β (0...(π β 1))) β (π β (((π¦ + 1) + 1)...((π β 1) + 1)) β βπ β ((π¦ + 1)...(π β 1))π = (π + 1))) |
501 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β ((π¦ + 1)...(π β 1)) β¦ (π + 1)) = (π β ((π¦ + 1)...(π β 1)) β¦ (π + 1)) |
502 | 501 | elrnmpt 5916 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β V β (π β ran (π β ((π¦ + 1)...(π β 1)) β¦ (π + 1)) β βπ β ((π¦ + 1)...(π β 1))π = (π + 1))) |
503 | 502 | elv 3454 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ran (π β ((π¦ + 1)...(π β 1)) β¦ (π + 1)) β βπ β ((π¦ + 1)...(π β 1))π = (π + 1)) |
504 | 500, 503 | bitr4di 289 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π¦ β (0...(π β 1))) β (π β (((π¦ + 1) + 1)...((π β 1) + 1)) β π β ran (π β ((π¦ + 1)...(π β 1)) β¦ (π + 1)))) |
505 | 504 | eqrdv 2735 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ β (0...(π β 1))) β (((π¦ + 1) + 1)...((π β 1) + 1)) = ran (π β ((π¦ + 1)...(π β 1)) β¦ (π + 1))) |
506 | 69 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (((π¦ + 1) + 1)...((π β 1) + 1)) = (((π¦ + 1) + 1)...π)) |
507 | 506 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ β (0...(π β 1))) β (((π¦ + 1) + 1)...((π β 1) + 1)) = (((π¦ + 1) + 1)...π)) |
508 | 472, 505,
507 | 3eqtr2rd 2784 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ β (0...(π β 1))) β (((π¦ + 1) + 1)...π) = ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...(π β 1)))) |
509 | 508 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β (0...(π β 1))) β ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) = ((2nd β(1st
βπ)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...(π β 1))))) |
510 | 452, 509 | uneq12d 4129 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β (0...(π β 1))) β ({((2nd
β(1st βπ))β1)} βͺ ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) = (((2nd
β(1st βπ)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β {π})) βͺ ((2nd
β(1st βπ)) β ((π β (1...π) β¦ if(π = π, 1, (π + 1))) β ((π¦ + 1)...(π β 1)))))) |
511 | 436, 445,
510 | 3eqtr4a 2803 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β (0...(π β 1))) β (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) = ({((2nd
β(1st βπ))β1)} βͺ ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)))) |
512 | 511 | xpeq1d 5667 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (0...(π β 1))) β ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}) = (({((2nd
β(1st βπ))β1)} βͺ ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) Γ {0})) |
513 | | xpundir 5706 |
. . . . . . . . . . . . . . . 16
β’
(({((2nd β(1st βπ))β1)} βͺ ((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π))) Γ {0}) = (({((2nd
β(1st βπ))β1)} Γ {0}) βͺ
(((2nd β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) |
514 | 512, 513 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (0...(π β 1))) β ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}) = (({((2nd
β(1st βπ))β1)} Γ {0}) βͺ
(((2nd β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))) |
515 | 431, 514 | uneq12d 4129 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (0...(π β 1))) β (((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})) = ((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ
(({((2nd β(1st βπ))β1)} Γ {0}) βͺ
(((2nd β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})))) |
516 | | unass 4131 |
. . . . . . . . . . . . . . 15
β’
(((((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ ({((2nd
β(1st βπ))β1)} Γ {0})) βͺ
(((2nd β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) = ((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ
(({((2nd β(1st βπ))β1)} Γ {0}) βͺ
(((2nd β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))) |
517 | | un23 4133 |
. . . . . . . . . . . . . . 15
β’
(((((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ ({((2nd
β(1st βπ))β1)} Γ {0})) βͺ
(((2nd β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) = (((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {0})) |
518 | 516, 517 | eqtr3i 2767 |
. . . . . . . . . . . . . 14
β’
((((2nd β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ
(({((2nd β(1st βπ))β1)} Γ {0}) βͺ
(((2nd β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))) = (((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {0})) |
519 | 515, 518 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (0...(π β 1))) β (((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})) = (((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {0}))) |
520 | 519 | fveq1d 6849 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (0...(π β 1))) β ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ) = ((((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {0}))βπ)) |
521 | 520 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β§ Β¬ π = ((2nd β(1st
βπ))β1)) β
((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ) = ((((((2nd
β(1st βπ)) β ((1 + 1)...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) βͺ ({((2nd
β(1st βπ))β1)} Γ {0}))βπ)) |
522 | 346, 364,
521 | 3eqtr4d 2787 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β§ Β¬ π = ((2nd β(1st
βπ))β1)) β
(((((2nd β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ) = ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)) |
523 | | snssi 4773 |
. . . . . . . . . . . . . . 15
β’ (1 β
β β {1} β β) |
524 | 138, 523 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ {1}
β β |
525 | | 0cn 11154 |
. . . . . . . . . . . . . . 15
β’ 0 β
β |
526 | | snssi 4773 |
. . . . . . . . . . . . . . 15
β’ (0 β
β β {0} β β) |
527 | 525, 526 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ {0}
β β |
528 | 524, 527 | unssi 4150 |
. . . . . . . . . . . . 13
β’ ({1}
βͺ {0}) β β |
529 | 30 | fconst 6733 |
. . . . . . . . . . . . . . . . 17
β’
((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}):(((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦))βΆ{1} |
530 | 33 | fconst 6733 |
. . . . . . . . . . . . . . . . 17
β’
((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}):(((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π))βΆ{0} |
531 | 529, 530 | pm3.2i 472 |
. . . . . . . . . . . . . . . 16
β’
(((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}):(((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦))βΆ{1} β§ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}):(((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π))βΆ{0}) |
532 | | fun 6709 |
. . . . . . . . . . . . . . . 16
β’
(((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}):(((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦))βΆ{1} β§ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}):(((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π))βΆ{0}) β§ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) β© (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π))) = β
) β (((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})):((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) βͺ (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)))βΆ({1} βͺ {0})) |
533 | 531, 238,
532 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (0...(π β 1))) β (((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})):((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) βͺ (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)))βΆ({1} βͺ {0})) |
534 | | imaundi 6107 |
. . . . . . . . . . . . . . . . 17
β’
(((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((1...π¦) βͺ ((π¦ + 1)...π))) = ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) βͺ (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π))) |
535 | | fzsplit2 13473 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π¦ + 1) β
(β€β₯β1) β§ π β (β€β₯βπ¦)) β (1...π) = ((1...π¦) βͺ ((π¦ + 1)...π))) |
536 | 63, 370, 535 | syl2an2 685 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β (0...(π β 1))) β (1...π) = ((1...π¦) βͺ ((π¦ + 1)...π))) |
537 | 536 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β (0...(π β 1))) β (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π)) = (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((1...π¦) βͺ ((π¦ + 1)...π)))) |
538 | | f1ofo 6796 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))):(1...π)β1-1-ontoβ(1...π) β ((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))):(1...π)βontoβ(1...π)) |
539 | | foima 6766 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))):(1...π)βontoβ(1...π) β (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π)) = (1...π)) |
540 | 225, 538,
539 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π)) = (1...π)) |
541 | 540 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π¦ β (0...(π β 1))) β (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π)) = (1...π)) |
542 | 537, 541 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β (0...(π β 1))) β (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((1...π¦) βͺ ((π¦ + 1)...π))) = (1...π)) |
543 | 534, 542 | eqtr3id 2791 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π¦ β (0...(π β 1))) β ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) βͺ (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π))) = (1...π)) |
544 | 543 | feq2d 6659 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π¦ β (0...(π β 1))) β ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})):((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) βͺ (((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)))βΆ({1} βͺ {0}) β
(((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})):(1...π)βΆ({1} βͺ {0}))) |
545 | 533, 544 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (0...(π β 1))) β (((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})):(1...π)βΆ({1} βͺ {0})) |
546 | 545 | ffvelcdmda 7040 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ) β ({1} βͺ {0})) |
547 | 528, 546 | sselid 3947 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ) β β) |
548 | 547 | addid2d 11363 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β (0 + ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)) = ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)) |
549 | 548 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β§ Β¬ π = ((2nd β(1st
βπ))β1)) β
(0 + ((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)) = ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)) |
550 | 522, 549 | eqtr4d 2780 |
. . . . . . . . 9
β’ ((((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β§ Β¬ π = ((2nd β(1st
βπ))β1)) β
(((((2nd β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ) = (0 + ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ))) |
551 | 93, 95, 284, 550 | ifbothda 4529 |
. . . . . . . 8
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ) = (if(π = ((2nd β(1st
βπ))β1), 1, 0)
+ ((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ))) |
552 | 551 | oveq2d 7378 |
. . . . . . 7
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β (((1st
β(1st βπ))βπ) + (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ)) = (((1st β(1st
βπ))βπ) + (if(π = ((2nd β(1st
βπ))β1), 1, 0)
+ ((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)))) |
553 | | elmapi 8794 |
. . . . . . . . . . . . 13
β’
((1st β(1st βπ)) β ((0..^πΎ) βm (1...π)) β (1st
β(1st βπ)):(1...π)βΆ(0..^πΎ)) |
554 | 26, 553 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (1st
β(1st βπ)):(1...π)βΆ(0..^πΎ)) |
555 | 554 | ffvelcdmda 7040 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β ((1st
β(1st βπ))βπ) β (0..^πΎ)) |
556 | | elfzonn0 13624 |
. . . . . . . . . . 11
β’
(((1st β(1st βπ))βπ) β (0..^πΎ) β ((1st
β(1st βπ))βπ) β
β0) |
557 | 555, 556 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β ((1st
β(1st βπ))βπ) β
β0) |
558 | 557 | nn0cnd 12482 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β ((1st
β(1st βπ))βπ) β β) |
559 | 558 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β ((1st
β(1st βπ))βπ) β β) |
560 | 138, 525 | ifcli 4538 |
. . . . . . . . 9
β’ if(π = ((2nd
β(1st βπ))β1), 1, 0) β
β |
561 | 560 | a1i 11 |
. . . . . . . 8
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β if(π = ((2nd β(1st
βπ))β1), 1, 0)
β β) |
562 | 559, 561,
547 | addassd 11184 |
. . . . . . 7
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β ((((1st
β(1st βπ))βπ) + if(π = ((2nd β(1st
βπ))β1), 1, 0))
+ ((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)) = (((1st β(1st
βπ))βπ) + (if(π = ((2nd β(1st
βπ))β1), 1, 0)
+ ((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)))) |
563 | 552, 562 | eqtr4d 2780 |
. . . . . 6
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β (((1st
β(1st βπ))βπ) + (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ)) = ((((1st
β(1st βπ))βπ) + if(π = ((2nd β(1st
βπ))β1), 1, 0))
+ ((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ))) |
564 | 563 | mpteq2dva 5210 |
. . . . 5
β’ ((π β§ π¦ β (0...(π β 1))) β (π β (1...π) β¦ (((1st
β(1st βπ))βπ) + (((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))βπ))) = (π β (1...π) β¦ ((((1st
β(1st βπ))βπ) + if(π = ((2nd β(1st
βπ))β1), 1, 0))
+ ((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)))) |
565 | 91, 564 | eqtrd 2777 |
. . . 4
β’ ((π β§ π¦ β (0...(π β 1))) β ((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))) = (π β (1...π) β¦ ((((1st
β(1st βπ))βπ) + if(π = ((2nd β(1st
βπ))β1), 1, 0))
+ ((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)))) |
566 | | poimirlem18.4 |
. . . . . . . . . 10
β’ (π β (2nd
βπ) =
0) |
567 | 566 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β (0...(π β 1))) β (2nd
βπ) =
0) |
568 | | elfzle1 13451 |
. . . . . . . . . 10
β’ (π¦ β (0...(π β 1)) β 0 β€ π¦) |
569 | 568 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π¦ β (0...(π β 1))) β 0 β€ π¦) |
570 | 567, 569 | eqbrtrd 5132 |
. . . . . . . 8
β’ ((π β§ π¦ β (0...(π β 1))) β (2nd
βπ) β€ π¦) |
571 | | 0re 11164 |
. . . . . . . . . 10
β’ 0 β
β |
572 | 566, 571 | eqeltrdi 2846 |
. . . . . . . . 9
β’ (π β (2nd
βπ) β
β) |
573 | | lenlt 11240 |
. . . . . . . . 9
β’
(((2nd βπ) β β β§ π¦ β β) β ((2nd
βπ) β€ π¦ β Β¬ π¦ < (2nd βπ))) |
574 | 572, 231,
573 | syl2an 597 |
. . . . . . . 8
β’ ((π β§ π¦ β (0...(π β 1))) β ((2nd
βπ) β€ π¦ β Β¬ π¦ < (2nd βπ))) |
575 | 570, 574 | mpbid 231 |
. . . . . . 7
β’ ((π β§ π¦ β (0...(π β 1))) β Β¬ π¦ < (2nd
βπ)) |
576 | 575 | iffalsed 4502 |
. . . . . 6
β’ ((π β§ π¦ β (0...(π β 1))) β if(π¦ < (2nd βπ), π¦, (π¦ + 1)) = (π¦ + 1)) |
577 | 576 | csbeq1d 3864 |
. . . . 5
β’ ((π β§ π¦ β (0...(π β 1))) β β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))) = β¦(π¦ + 1) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0})))) |
578 | | ovex 7395 |
. . . . . 6
β’ (π¦ + 1) β V |
579 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = (π¦ + 1) β (1...π) = (1...(π¦ + 1))) |
580 | 579 | imaeq2d 6018 |
. . . . . . . . 9
β’ (π = (π¦ + 1) β ((2nd
β(1st βπ)) β (1...π)) = ((2nd β(1st
βπ)) β
(1...(π¦ +
1)))) |
581 | 580 | xpeq1d 5667 |
. . . . . . . 8
β’ (π = (π¦ + 1) β (((2nd
β(1st βπ)) β (1...π)) Γ {1}) = (((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1})) |
582 | | oveq1 7369 |
. . . . . . . . . . 11
β’ (π = (π¦ + 1) β (π + 1) = ((π¦ + 1) + 1)) |
583 | 582 | oveq1d 7377 |
. . . . . . . . . 10
β’ (π = (π¦ + 1) β ((π + 1)...π) = (((π¦ + 1) + 1)...π)) |
584 | 583 | imaeq2d 6018 |
. . . . . . . . 9
β’ (π = (π¦ + 1) β ((2nd
β(1st βπ)) β ((π + 1)...π)) = ((2nd β(1st
βπ)) β (((π¦ + 1) + 1)...π))) |
585 | 584 | xpeq1d 5667 |
. . . . . . . 8
β’ (π = (π¦ + 1) β (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}) = (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})) |
586 | 581, 585 | uneq12d 4129 |
. . . . . . 7
β’ (π = (π¦ + 1) β ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0})) = ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))) |
587 | 586 | oveq2d 7378 |
. . . . . 6
β’ (π = (π¦ + 1) β ((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))) = ((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})))) |
588 | 578, 587 | csbie 3896 |
. . . . 5
β’
β¦(π¦ +
1) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))) = ((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0}))) |
589 | 577, 588 | eqtrdi 2793 |
. . . 4
β’ ((π β§ π¦ β (0...(π β 1))) β β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))) = ((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...(π¦ + 1))) Γ {1}) βͺ (((2nd
β(1st βπ)) β (((π¦ + 1) + 1)...π)) Γ {0})))) |
590 | | ovexd 7397 |
. . . . 5
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β (((1st
β(1st βπ))βπ) + if(π = ((2nd β(1st
βπ))β1), 1, 0))
β V) |
591 | | fvexd 6862 |
. . . . 5
β’ (((π β§ π¦ β (0...(π β 1))) β§ π β (1...π)) β ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ) β V) |
592 | | eqidd 2738 |
. . . . 5
β’ ((π β§ π¦ β (0...(π β 1))) β (π β (1...π) β¦ (((1st
β(1st βπ))βπ) + if(π = ((2nd β(1st
βπ))β1), 1,
0))) = (π β (1...π) β¦ (((1st
β(1st βπ))βπ) + if(π = ((2nd β(1st
βπ))β1), 1,
0)))) |
593 | 545 | ffnd 6674 |
. . . . . 6
β’ ((π β§ π¦ β (0...(π β 1))) β (((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})) Fn (1...π)) |
594 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²π(2nd β(1st
βπ)) |
595 | | nfmpt1 5218 |
. . . . . . . . . . 11
β’
β²π(π β (1...π) β¦ if(π = π, 1, (π + 1))) |
596 | 594, 595 | nfco 5826 |
. . . . . . . . . 10
β’
β²π((2nd β(1st
βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) |
597 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²π(1...π¦) |
598 | 596, 597 | nfima 6026 |
. . . . . . . . 9
β’
β²π(((2nd β(1st
βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) |
599 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π{1} |
600 | 598, 599 | nfxp 5671 |
. . . . . . . 8
β’
β²π((((2nd β(1st
βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) |
601 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²π((π¦ + 1)...π) |
602 | 596, 601 | nfima 6026 |
. . . . . . . . 9
β’
β²π(((2nd β(1st
βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) |
603 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π{0} |
604 | 602, 603 | nfxp 5671 |
. . . . . . . 8
β’
β²π((((2nd β(1st
βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}) |
605 | 600, 604 | nfun 4130 |
. . . . . . 7
β’
β²π(((((2nd β(1st
βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})) |
606 | 605 | dffn5f 6918 |
. . . . . 6
β’
((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})) Fn (1...π) β (((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})) = (π β (1...π) β¦ ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ))) |
607 | 593, 606 | sylib 217 |
. . . . 5
β’ ((π β§ π¦ β (0...(π β 1))) β (((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})) = (π β (1...π) β¦ ((((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ))) |
608 | 87, 590, 591, 592, 607 | offval2 7642 |
. . . 4
β’ ((π β§ π¦ β (0...(π β 1))) β ((π β (1...π) β¦ (((1st
β(1st βπ))βπ) + if(π = ((2nd β(1st
βπ))β1), 1,
0))) βf + (((((2nd β(1st
βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))) = (π β (1...π) β¦ ((((1st
β(1st βπ))βπ) + if(π = ((2nd β(1st
βπ))β1), 1, 0))
+ ((((((2nd β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))βπ)))) |
609 | 565, 589,
608 | 3eqtr4rd 2788 |
. . 3
β’ ((π β§ π¦ β (0...(π β 1))) β ((π β (1...π) β¦ (((1st
β(1st βπ))βπ) + if(π = ((2nd β(1st
βπ))β1), 1,
0))) βf + (((((2nd β(1st
βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))) = β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0})))) |
610 | 609 | mpteq2dva 5210 |
. 2
β’ (π β (π¦ β (0...(π β 1)) β¦ ((π β (1...π) β¦ (((1st
β(1st βπ))βπ) + if(π = ((2nd β(1st
βπ))β1), 1,
0))) βf + (((((2nd β(1st
βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0})))) = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))))) |
611 | 19, 610 | eqtr4d 2780 |
1
β’ (π β πΉ = (π¦ β (0...(π β 1)) β¦ ((π β (1...π) β¦ (((1st
β(1st βπ))βπ) + if(π = ((2nd β(1st
βπ))β1), 1,
0))) βf + (((((2nd β(1st
βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β (1...π¦)) Γ {1}) βͺ ((((2nd
β(1st βπ)) β (π β (1...π) β¦ if(π = π, 1, (π + 1)))) β ((π¦ + 1)...π)) Γ {0}))))) |