Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . . . . 6
β’ (π β π β β) |
2 | 1 | nnnn0d 12480 |
. . . . 5
β’ (π β π β
β0) |
3 | 1 | nnred 12175 |
. . . . . 6
β’ (π β π β β) |
4 | 3 | leidd 11728 |
. . . . 5
β’ (π β π β€ π) |
5 | 2, 2, 4 | 3jca 1129 |
. . . 4
β’ (π β (π β β0 β§ π β β0
β§ π β€ π)) |
6 | | oveq2 7370 |
. . . . . . . . . . . . . . . 16
β’ (π = 0 β (1...π) = (1...0)) |
7 | | fz10 13469 |
. . . . . . . . . . . . . . . 16
β’ (1...0) =
β
|
8 | 6, 7 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
β’ (π = 0 β (1...π) = β
) |
9 | 8 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π = 0 β ((0..^πΎ) βm (1...π)) = ((0..^πΎ) βm
β
)) |
10 | | fzofi 13886 |
. . . . . . . . . . . . . . . 16
β’
(0..^πΎ) β
Fin |
11 | | map0e 8827 |
. . . . . . . . . . . . . . . 16
β’
((0..^πΎ) β Fin
β ((0..^πΎ)
βm β
) = 1o) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’
((0..^πΎ)
βm β
) = 1o |
13 | | df1o2 8424 |
. . . . . . . . . . . . . . 15
β’
1o = {β
} |
14 | 12, 13 | eqtri 2765 |
. . . . . . . . . . . . . 14
β’
((0..^πΎ)
βm β
) = {β
} |
15 | 9, 14 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ (π = 0 β ((0..^πΎ) βm (1...π)) = {β
}) |
16 | | eqidd 2738 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β π = π) |
17 | 16, 8, 8 | f1oeq123d 6783 |
. . . . . . . . . . . . . . . 16
β’ (π = 0 β (π:(1...π)β1-1-ontoβ(1...π) β π:β
β1-1-ontoββ
)) |
18 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’ β
=
β
|
19 | | f1o00 6824 |
. . . . . . . . . . . . . . . . 17
β’ (π:β
β1-1-ontoββ
β (π = β
β§ β
=
β
)) |
20 | 18, 19 | mpbiran2 709 |
. . . . . . . . . . . . . . . 16
β’ (π:β
β1-1-ontoββ
β π = β
) |
21 | 17, 20 | bitrdi 287 |
. . . . . . . . . . . . . . 15
β’ (π = 0 β (π:(1...π)β1-1-ontoβ(1...π) β π = β
)) |
22 | 21 | abbidv 2806 |
. . . . . . . . . . . . . 14
β’ (π = 0 β {π β£ π:(1...π)β1-1-ontoβ(1...π)} = {π β£ π = β
}) |
23 | | df-sn 4592 |
. . . . . . . . . . . . . 14
β’ {β
}
= {π β£ π = β
} |
24 | 22, 23 | eqtr4di 2795 |
. . . . . . . . . . . . 13
β’ (π = 0 β {π β£ π:(1...π)β1-1-ontoβ(1...π)} = {β
}) |
25 | 15, 24 | xpeq12d 5669 |
. . . . . . . . . . . 12
β’ (π = 0 β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) = ({β
} Γ
{β
})) |
26 | | 0ex 5269 |
. . . . . . . . . . . . 13
β’ β
β V |
27 | 26, 26 | xpsn 7092 |
. . . . . . . . . . . 12
β’
({β
} Γ {β
}) = {β¨β
,
β
β©} |
28 | 25, 27 | eqtr2di 2794 |
. . . . . . . . . . 11
β’ (π = 0 β {β¨β
,
β
β©} = (((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
29 | | elsni 4608 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {β¨β
,
β
β©} β π =
β¨β
, β
β©) |
30 | 26, 26 | op1std 7936 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = β¨β
, β
β©
β (1st βπ ) = β
) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β {β¨β
,
β
β©} β (1st βπ ) = β
) |
32 | 31 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ (π β {β¨β
,
β
β©} β ((1st βπ ) βf + β
) = (β
βf + β
)) |
33 | | f0 6728 |
. . . . . . . . . . . . . . . . . . . 20
β’
β
:β
βΆβ
|
34 | | ffn 6673 |
. . . . . . . . . . . . . . . . . . . 20
β’
(β
:β
βΆβ
β β
Fn
β
) |
35 | 33, 34 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {β¨β
,
β
β©} β β
Fn β
) |
36 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {β¨β
,
β
β©} β β
β V) |
37 | | inidm 4183 |
. . . . . . . . . . . . . . . . . . 19
β’ (β
β© β
) = β
|
38 | | 0fv 6891 |
. . . . . . . . . . . . . . . . . . . 20
β’
(β
βπ) =
β
|
39 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β {β¨β
,
β
β©} β§ π
β β
) β (β
βπ) = β
) |
40 | 35, 35, 36, 36, 37, 39, 39 | offval 7631 |
. . . . . . . . . . . . . . . . . 18
β’ (π β {β¨β
,
β
β©} β (β
βf + β
) = (π β β
β¦ (β
+ β
))) |
41 | | mpt0 6648 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β
β¦ (β
+ β
)) = β
|
42 | 40, 41 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
β’ (π β {β¨β
,
β
β©} β (β
βf + β
) =
β
) |
43 | 32, 42 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ (π β {β¨β
,
β
β©} β ((1st βπ ) βf + β
) =
β
) |
44 | 43 | uneq1d 4127 |
. . . . . . . . . . . . . . 15
β’ (π β {β¨β
,
β
β©} β (((1st βπ ) βf + β
) βͺ
((1...π) Γ {0})) =
(β
βͺ ((1...π)
Γ {0}))) |
45 | | uncom 4118 |
. . . . . . . . . . . . . . . 16
β’ (β
βͺ ((1...π) Γ
{0})) = (((1...π) Γ
{0}) βͺ β
) |
46 | | un0 4355 |
. . . . . . . . . . . . . . . 16
β’
(((1...π) Γ
{0}) βͺ β
) = ((1...π) Γ {0}) |
47 | 45, 46 | eqtri 2765 |
. . . . . . . . . . . . . . 15
β’ (β
βͺ ((1...π) Γ
{0})) = ((1...π) Γ
{0}) |
48 | 44, 47 | eqtr2di 2794 |
. . . . . . . . . . . . . 14
β’ (π β {β¨β
,
β
β©} β ((1...π) Γ {0}) = (((1st
βπ )
βf + β
) βͺ ((1...π) Γ {0}))) |
49 | 48 | csbeq1d 3864 |
. . . . . . . . . . . . 13
β’ (π β {β¨β
,
β
β©} β β¦((1...π) Γ {0}) / πβ¦π΅ = β¦(((1st
βπ )
βf + β
) βͺ ((1...π) Γ {0})) / πβ¦π΅) |
50 | 49 | eqeq2d 2748 |
. . . . . . . . . . . 12
β’ (π β {β¨β
,
β
β©} β (0 = β¦((1...π) Γ {0}) / πβ¦π΅ β 0 = β¦(((1st
βπ )
βf + β
) βͺ ((1...π) Γ {0})) / πβ¦π΅)) |
51 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
β’ (π = 0 β (0...π) = (0...0)) |
52 | | 0z 12517 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β€ |
53 | | fzsn 13490 |
. . . . . . . . . . . . . . . 16
β’ (0 β
β€ β (0...0) = {0}) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ (0...0) =
{0} |
55 | 51, 54 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
β’ (π = 0 β (0...π) = {0}) |
56 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = 0 β ((π + 1)...π) = ((π + 1)...0)) |
57 | 56 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = 0 β ((2nd
βπ ) β ((π + 1)...π)) = ((2nd βπ ) β ((π + 1)...0))) |
58 | 57 | xpeq1d 5667 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = 0 β (((2nd
βπ ) β ((π + 1)...π)) Γ {0}) = (((2nd
βπ ) β ((π + 1)...0)) Γ
{0})) |
59 | 58 | uneq2d 4128 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 0 β ((((2nd
βπ ) β
(1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...π)) Γ {0})) =
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...0)) Γ
{0}))) |
60 | 59 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β ((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) = ((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...0)) Γ
{0})))) |
61 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = 0 β (π + 1) = (0 + 1)) |
62 | | 0p1e1 12282 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (0 + 1) =
1 |
63 | 61, 62 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = 0 β (π + 1) = 1) |
64 | 63 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 0 β ((π + 1)...π) = (1...π)) |
65 | 64 | xpeq1d 5667 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β (((π + 1)...π) Γ {0}) = ((1...π) Γ {0})) |
66 | 60, 65 | uneq12d 4129 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β (((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) = (((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...0)) Γ {0}))) βͺ
((1...π) Γ
{0}))) |
67 | 66 | csbeq1d 3864 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β
β¦(((1st βπ ) βf + ((((2nd
βπ ) β
(1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...0)) Γ {0}))) βͺ
((1...π) Γ {0})) /
πβ¦π΅) |
68 | 67 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
β’ (π = 0 β (π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ β π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...0)) Γ {0}))) βͺ
((1...π) Γ {0})) /
πβ¦π΅)) |
69 | 55, 68 | rexeqbidv 3323 |
. . . . . . . . . . . . . . 15
β’ (π = 0 β (βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ β βπ β {0}π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...0)) Γ {0}))) βͺ
((1...π) Γ {0})) /
πβ¦π΅)) |
70 | | c0ex 11156 |
. . . . . . . . . . . . . . . 16
β’ 0 β
V |
71 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = 0 β (1...π) = (1...0)) |
72 | 71, 7 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = 0 β (1...π) = β
) |
73 | 72 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = 0 β ((2nd
βπ ) β
(1...π)) = ((2nd
βπ ) β
β
)) |
74 | | ima0 6034 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((2nd βπ ) β β
) = β
|
75 | 73, 74 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = 0 β ((2nd
βπ ) β
(1...π)) =
β
) |
76 | 75 | xpeq1d 5667 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = 0 β (((2nd
βπ ) β
(1...π)) Γ {1}) =
(β
Γ {1})) |
77 | | 0xp 5735 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β
Γ {1}) = β
|
78 | 76, 77 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = 0 β (((2nd
βπ ) β
(1...π)) Γ {1}) =
β
) |
79 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = 0 β (π + 1) = (0 + 1)) |
80 | 79, 62 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = 0 β (π + 1) = 1) |
81 | 80 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = 0 β ((π + 1)...0) = (1...0)) |
82 | 81, 7 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = 0 β ((π + 1)...0) = β
) |
83 | 82 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = 0 β ((2nd
βπ ) β ((π + 1)...0)) = ((2nd
βπ ) β
β
)) |
84 | 83, 74 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = 0 β ((2nd
βπ ) β ((π + 1)...0)) =
β
) |
85 | 84 | xpeq1d 5667 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = 0 β (((2nd
βπ ) β ((π + 1)...0)) Γ {0}) =
(β
Γ {0})) |
86 | | 0xp 5735 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β
Γ {0}) = β
|
87 | 85, 86 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = 0 β (((2nd
βπ ) β ((π + 1)...0)) Γ {0}) =
β
) |
88 | 78, 87 | uneq12d 4129 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = 0 β ((((2nd
βπ ) β
(1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...0))
Γ {0})) = (β
βͺ β
)) |
89 | | un0 4355 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β
βͺ β
) = β
|
90 | 88, 89 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 0 β ((((2nd
βπ ) β
(1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...0))
Γ {0})) = β
) |
91 | 90 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β ((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...0)) Γ {0}))) =
((1st βπ )
βf + β
)) |
92 | 91 | uneq1d 4127 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β (((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...0)) Γ {0}))) βͺ
((1...π) Γ {0})) =
(((1st βπ )
βf + β
) βͺ ((1...π) Γ {0}))) |
93 | 92 | csbeq1d 3864 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β
β¦(((1st βπ ) βf + ((((2nd
βπ ) β
(1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...0))
Γ {0}))) βͺ ((1...π) Γ {0})) / πβ¦π΅ = β¦(((1st
βπ )
βf + β
) βͺ ((1...π) Γ {0})) / πβ¦π΅) |
94 | 93 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
β’ (π = 0 β (π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...0)) Γ {0}))) βͺ
((1...π) Γ {0})) /
πβ¦π΅ β π = β¦(((1st
βπ )
βf + β
) βͺ ((1...π) Γ {0})) / πβ¦π΅)) |
95 | 70, 94 | rexsn 4648 |
. . . . . . . . . . . . . . 15
β’
(βπ β
{0}π =
β¦(((1st βπ ) βf + ((((2nd
βπ ) β
(1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...0))
Γ {0}))) βͺ ((1...π) Γ {0})) / πβ¦π΅ β π = β¦(((1st
βπ )
βf + β
) βͺ ((1...π) Γ {0})) / πβ¦π΅) |
96 | 69, 95 | bitrdi 287 |
. . . . . . . . . . . . . 14
β’ (π = 0 β (βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ β π = β¦(((1st
βπ )
βf + β
) βͺ ((1...π) Γ {0})) / πβ¦π΅)) |
97 | 55, 96 | raleqbidv 3322 |
. . . . . . . . . . . . 13
β’ (π = 0 β (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ β βπ β {0}π = β¦(((1st
βπ )
βf + β
) βͺ ((1...π) Γ {0})) / πβ¦π΅)) |
98 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
β’ (π = 0 β (π = β¦(((1st
βπ )
βf + β
) βͺ ((1...π) Γ {0})) / πβ¦π΅ β 0 = β¦(((1st
βπ )
βf + β
) βͺ ((1...π) Γ {0})) / πβ¦π΅)) |
99 | 70, 98 | ralsn 4647 |
. . . . . . . . . . . . 13
β’
(βπ β
{0}π =
β¦(((1st βπ ) βf + β
) βͺ
((1...π) Γ {0})) /
πβ¦π΅ β 0 =
β¦(((1st βπ ) βf + β
) βͺ
((1...π) Γ {0})) /
πβ¦π΅) |
100 | 97, 99 | bitr2di 288 |
. . . . . . . . . . . 12
β’ (π = 0 β (0 =
β¦(((1st βπ ) βf + β
) βͺ
((1...π) Γ {0})) /
πβ¦π΅ β βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅)) |
101 | 50, 100 | sylan9bbr 512 |
. . . . . . . . . . 11
β’ ((π = 0 β§ π β {β¨β
, β
β©})
β (0 = β¦((1...π) Γ {0}) / πβ¦π΅ β βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅)) |
102 | 28, 101 | rabeqbidva 3426 |
. . . . . . . . . 10
β’ (π = 0 β {π β {β¨β
, β
β©}
β£ 0 = β¦((1...π) Γ {0}) / πβ¦π΅} = {π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) |
103 | 102 | eqcomd 2743 |
. . . . . . . . 9
β’ (π = 0 β {π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅} = {π β {β¨β
, β
β©}
β£ 0 = β¦((1...π) Γ {0}) / πβ¦π΅}) |
104 | 103 | fveq2d 6851 |
. . . . . . . 8
β’ (π = 0 β
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) = (β―β{π β {β¨β
, β
β©}
β£ 0 = β¦((1...π) Γ {0}) / πβ¦π΅})) |
105 | 104 | breq2d 5122 |
. . . . . . 7
β’ (π = 0 β (2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) β 2 β₯ (β―β{π β {β¨β
,
β
β©} β£ 0 = β¦((1...π) Γ {0}) / πβ¦π΅}))) |
106 | 105 | notbid 318 |
. . . . . 6
β’ (π = 0 β (Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) β Β¬ 2 β₯
(β―β{π β
{β¨β
, β
β©} β£ 0 = β¦((1...π) Γ {0}) / πβ¦π΅}))) |
107 | 106 | imbi2d 341 |
. . . . 5
β’ (π = 0 β ((π β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅})) β (π β Β¬ 2 β₯
(β―β{π β
{β¨β
, β
β©} β£ 0 = β¦((1...π) Γ {0}) / πβ¦π΅})))) |
108 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π = π β (1...π) = (1...π)) |
109 | 108 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = π β ((0..^πΎ) βm (1...π)) = ((0..^πΎ) βm (1...π))) |
110 | | eqidd 2738 |
. . . . . . . . . . . . 13
β’ (π = π β π = π) |
111 | 110, 108,
108 | f1oeq123d 6783 |
. . . . . . . . . . . 12
β’ (π = π β (π:(1...π)β1-1-ontoβ(1...π) β π:(1...π)β1-1-ontoβ(1...π))) |
112 | 111 | abbidv 2806 |
. . . . . . . . . . 11
β’ (π = π β {π β£ π:(1...π)β1-1-ontoβ(1...π)} = {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
113 | 109, 112 | xpeq12d 5669 |
. . . . . . . . . 10
β’ (π = π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) = (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
114 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π = π β (0...π) = (0...π)) |
115 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((π + 1)...π) = ((π + 1)...π)) |
116 | 115 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((2nd βπ ) β ((π + 1)...π)) = ((2nd βπ ) β ((π + 1)...π))) |
117 | 116 | xpeq1d 5667 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (((2nd βπ ) β ((π + 1)...π)) Γ {0}) = (((2nd
βπ ) β ((π + 1)...π)) Γ {0})) |
118 | 117 | uneq2d 4128 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((((2nd βπ ) β (1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...π)) Γ {0})) =
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) |
119 | 118 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) = ((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))) |
120 | | oveq1 7369 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π + 1) = (π + 1)) |
121 | 120 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π + 1)...π) = ((π + 1)...π)) |
122 | 121 | xpeq1d 5667 |
. . . . . . . . . . . . . . 15
β’ (π = π β (((π + 1)...π) Γ {0}) = (((π + 1)...π) Γ {0})) |
123 | 119, 122 | uneq12d 4129 |
. . . . . . . . . . . . . 14
β’ (π = π β (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) = (((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0}))) |
124 | 123 | csbeq1d 3864 |
. . . . . . . . . . . . 13
β’ (π = π β β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅) |
125 | 124 | eqeq2d 2748 |
. . . . . . . . . . . 12
β’ (π = π β (π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ β π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅)) |
126 | 114, 125 | rexeqbidv 3323 |
. . . . . . . . . . 11
β’ (π = π β (βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ β βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅)) |
127 | 114, 126 | raleqbidv 3322 |
. . . . . . . . . 10
β’ (π = π β (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ β βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅)) |
128 | 113, 127 | rabeqbidv 3427 |
. . . . . . . . 9
β’ (π = π β {π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅} = {π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) |
129 | 128 | fveq2d 6851 |
. . . . . . . 8
β’ (π = π β (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) = (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅})) |
130 | 129 | breq2d 5122 |
. . . . . . 7
β’ (π = π β (2 β₯ (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) β 2 β₯ (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}))) |
131 | 130 | notbid 318 |
. . . . . 6
β’ (π = π β (Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}))) |
132 | 131 | imbi2d 341 |
. . . . 5
β’ (π = π β ((π β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅})) β (π β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅})))) |
133 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π = (π + 1) β (1...π) = (1...(π + 1))) |
134 | 133 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = (π + 1) β ((0..^πΎ) βm (1...π)) = ((0..^πΎ) βm (1...(π + 1)))) |
135 | | eqidd 2738 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β π = π) |
136 | 135, 133,
133 | f1oeq123d 6783 |
. . . . . . . . . . . 12
β’ (π = (π + 1) β (π:(1...π)β1-1-ontoβ(1...π) β π:(1...(π + 1))β1-1-ontoβ(1...(π + 1)))) |
137 | 136 | abbidv 2806 |
. . . . . . . . . . 11
β’ (π = (π + 1) β {π β£ π:(1...π)β1-1-ontoβ(1...π)} = {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) |
138 | 134, 137 | xpeq12d 5669 |
. . . . . . . . . 10
β’ (π = (π + 1) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) = (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))})) |
139 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π = (π + 1) β (0...π) = (0...(π + 1))) |
140 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π + 1) β ((π + 1)...π) = ((π + 1)...(π + 1))) |
141 | 140 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π + 1) β ((2nd βπ ) β ((π + 1)...π)) = ((2nd βπ ) β ((π + 1)...(π + 1)))) |
142 | 141 | xpeq1d 5667 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β (((2nd βπ ) β ((π + 1)...π)) Γ {0}) = (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0})) |
143 | 142 | uneq2d 4128 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β ((((2nd βπ ) β (1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...π)) Γ {0})) =
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) |
144 | 143 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β ((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) = ((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0})))) |
145 | | oveq1 7369 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β (π + 1) = ((π + 1) + 1)) |
146 | 145 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β ((π + 1)...π) = (((π + 1) + 1)...π)) |
147 | 146 | xpeq1d 5667 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β (((π + 1)...π) Γ {0}) = ((((π + 1) + 1)...π) Γ {0})) |
148 | 144, 147 | uneq12d 4129 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) = (((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0}))) |
149 | 148 | csbeq1d 3864 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅) |
150 | 149 | eqeq2d 2748 |
. . . . . . . . . . . 12
β’ (π = (π + 1) β (π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ β π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅)) |
151 | 139, 150 | rexeqbidv 3323 |
. . . . . . . . . . 11
β’ (π = (π + 1) β (βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ β βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅)) |
152 | 139, 151 | raleqbidv 3322 |
. . . . . . . . . 10
β’ (π = (π + 1) β (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ β βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅)) |
153 | 138, 152 | rabeqbidv 3427 |
. . . . . . . . 9
β’ (π = (π + 1) β {π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅} = {π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) |
154 | 153 | fveq2d 6851 |
. . . . . . . 8
β’ (π = (π + 1) β (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) = (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅})) |
155 | 154 | breq2d 5122 |
. . . . . . 7
β’ (π = (π + 1) β (2 β₯ (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) β 2 β₯ (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}))) |
156 | 155 | notbid 318 |
. . . . . 6
β’ (π = (π + 1) β (Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}))) |
157 | 156 | imbi2d 341 |
. . . . 5
β’ (π = (π + 1) β ((π β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅})) β (π β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅})))) |
158 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π = π β (1...π) = (1...π)) |
159 | 158 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = π β ((0..^πΎ) βm (1...π)) = ((0..^πΎ) βm (1...π))) |
160 | | eqidd 2738 |
. . . . . . . . . . . . 13
β’ (π = π β π = π) |
161 | 160, 158,
158 | f1oeq123d 6783 |
. . . . . . . . . . . 12
β’ (π = π β (π:(1...π)β1-1-ontoβ(1...π) β π:(1...π)β1-1-ontoβ(1...π))) |
162 | 161 | abbidv 2806 |
. . . . . . . . . . 11
β’ (π = π β {π β£ π:(1...π)β1-1-ontoβ(1...π)} = {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
163 | 159, 162 | xpeq12d 5669 |
. . . . . . . . . 10
β’ (π = π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) = (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
164 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π = π β (0...π) = (0...π)) |
165 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((π + 1)...π) = ((π + 1)...π)) |
166 | 165 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((2nd βπ ) β ((π + 1)...π)) = ((2nd βπ ) β ((π + 1)...π))) |
167 | 166 | xpeq1d 5667 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (((2nd βπ ) β ((π + 1)...π)) Γ {0}) = (((2nd
βπ ) β ((π + 1)...π)) Γ {0})) |
168 | 167 | uneq2d 4128 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((((2nd βπ ) β (1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...π)) Γ {0})) =
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) |
169 | 168 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) = ((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))) |
170 | | oveq1 7369 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π + 1) = (π + 1)) |
171 | 170 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π + 1)...π) = ((π + 1)...π)) |
172 | 171 | xpeq1d 5667 |
. . . . . . . . . . . . . . 15
β’ (π = π β (((π + 1)...π) Γ {0}) = (((π + 1)...π) Γ {0})) |
173 | 169, 172 | uneq12d 4129 |
. . . . . . . . . . . . . 14
β’ (π = π β (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) = (((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0}))) |
174 | 173 | csbeq1d 3864 |
. . . . . . . . . . . . 13
β’ (π = π β β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅) |
175 | 174 | eqeq2d 2748 |
. . . . . . . . . . . 12
β’ (π = π β (π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ β π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅)) |
176 | 164, 175 | rexeqbidv 3323 |
. . . . . . . . . . 11
β’ (π = π β (βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ β βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅)) |
177 | 164, 176 | raleqbidv 3322 |
. . . . . . . . . 10
β’ (π = π β (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ β βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅)) |
178 | 163, 177 | rabeqbidv 3427 |
. . . . . . . . 9
β’ (π = π β {π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅} = {π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) |
179 | 178 | fveq2d 6851 |
. . . . . . . 8
β’ (π = π β (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) = (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅})) |
180 | 179 | breq2d 5122 |
. . . . . . 7
β’ (π = π β (2 β₯ (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) β 2 β₯ (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}))) |
181 | 180 | notbid 318 |
. . . . . 6
β’ (π = π β (Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}))) |
182 | 181 | imbi2d 341 |
. . . . 5
β’ (π = π β ((π β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅})) β (π β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅})))) |
183 | | n2dvds1 16257 |
. . . . . . 7
β’ Β¬ 2
β₯ 1 |
184 | | opex 5426 |
. . . . . . . . . 10
β’
β¨β
, β
β© β V |
185 | | hashsng 14276 |
. . . . . . . . . 10
β’
(β¨β
, β
β© β V β
(β―β{β¨β
, β
β©}) = 1) |
186 | 184, 185 | ax-mp 5 |
. . . . . . . . 9
β’
(β―β{β¨β
, β
β©}) = 1 |
187 | | nnuz 12813 |
. . . . . . . . . . . . . . . . 17
β’ β =
(β€β₯β1) |
188 | 1, 187 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . 16
β’ (π β π β
(β€β₯β1)) |
189 | | eluzfz1 13455 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β1) β 1 β (1...π)) |
190 | 188, 189 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β 1 β (1...π)) |
191 | | poimirlem28.5 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΎ β β) |
192 | 191 | nnnn0d 12480 |
. . . . . . . . . . . . . . . 16
β’ (π β πΎ β
β0) |
193 | | 0elfz 13545 |
. . . . . . . . . . . . . . . 16
β’ (πΎ β β0
β 0 β (0...πΎ)) |
194 | | fconst6g 6736 |
. . . . . . . . . . . . . . . 16
β’ (0 β
(0...πΎ) β ((1...π) Γ {0}):(1...π)βΆ(0...πΎ)) |
195 | 192, 193,
194 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (π β ((1...π) Γ {0}):(1...π)βΆ(0...πΎ)) |
196 | 70 | fvconst2 7158 |
. . . . . . . . . . . . . . . 16
β’ (1 β
(1...π) β (((1...π) Γ {0})β1) =
0) |
197 | 190, 196 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (((1...π) Γ {0})β1) =
0) |
198 | 190, 195,
197 | 3jca 1129 |
. . . . . . . . . . . . . 14
β’ (π β (1 β (1...π) β§ ((1...π) Γ {0}):(1...π)βΆ(0...πΎ) β§ (((1...π) Γ {0})β1) =
0)) |
199 | | nfv 1918 |
. . . . . . . . . . . . . . . 16
β’
β²π(π β§ (1 β (1...π) β§ ((1...π) Γ {0}):(1...π)βΆ(0...πΎ) β§ (((1...π) Γ {0})β1) =
0)) |
200 | | nfcsb1v 3885 |
. . . . . . . . . . . . . . . . 17
β’
β²πβ¦((1...π) Γ {0}) / πβ¦π΅ |
201 | 200 | nfeq1 2923 |
. . . . . . . . . . . . . . . 16
β’
β²πβ¦((1...π) Γ {0}) / πβ¦π΅ = 0 |
202 | 199, 201 | nfim 1900 |
. . . . . . . . . . . . . . 15
β’
β²π((π β§ (1 β (1...π) β§ ((1...π) Γ {0}):(1...π)βΆ(0...πΎ) β§ (((1...π) Γ {0})β1) = 0)) β
β¦((1...π)
Γ {0}) / πβ¦π΅ = 0) |
203 | | ovex 7395 |
. . . . . . . . . . . . . . . 16
β’
(1...π) β
V |
204 | | snex 5393 |
. . . . . . . . . . . . . . . 16
β’ {0}
β V |
205 | 203, 204 | xpex 7692 |
. . . . . . . . . . . . . . 15
β’
((1...π) Γ
{0}) β V |
206 | | feq1 6654 |
. . . . . . . . . . . . . . . . . 18
β’ (π = ((1...π) Γ {0}) β (π:(1...π)βΆ(0...πΎ) β ((1...π) Γ {0}):(1...π)βΆ(0...πΎ))) |
207 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = ((1...π) Γ {0}) β (πβ1) = (((1...π) Γ {0})β1)) |
208 | 207 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . 18
β’ (π = ((1...π) Γ {0}) β ((πβ1) = 0 β (((1...π) Γ {0})β1) =
0)) |
209 | 206, 208 | 3anbi23d 1440 |
. . . . . . . . . . . . . . . . 17
β’ (π = ((1...π) Γ {0}) β ((1 β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβ1) = 0) β (1 β (1...π) β§ ((1...π) Γ {0}):(1...π)βΆ(0...πΎ) β§ (((1...π) Γ {0})β1) =
0))) |
210 | 209 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
β’ (π = ((1...π) Γ {0}) β ((π β§ (1 β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβ1) = 0)) β (π β§ (1 β (1...π) β§ ((1...π) Γ {0}):(1...π)βΆ(0...πΎ) β§ (((1...π) Γ {0})β1) =
0)))) |
211 | | csbeq1a 3874 |
. . . . . . . . . . . . . . . . 17
β’ (π = ((1...π) Γ {0}) β π΅ = β¦((1...π) Γ {0}) / πβ¦π΅) |
212 | 211 | eqeq1d 2739 |
. . . . . . . . . . . . . . . 16
β’ (π = ((1...π) Γ {0}) β (π΅ = 0 β β¦((1...π) Γ {0}) / πβ¦π΅ = 0)) |
213 | 210, 212 | imbi12d 345 |
. . . . . . . . . . . . . . 15
β’ (π = ((1...π) Γ {0}) β (((π β§ (1 β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβ1) = 0)) β π΅ = 0) β ((π β§ (1 β (1...π) β§ ((1...π) Γ {0}):(1...π)βΆ(0...πΎ) β§ (((1...π) Γ {0})β1) = 0)) β
β¦((1...π)
Γ {0}) / πβ¦π΅ = 0))) |
214 | | 1ex 11158 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
V |
215 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 1 β (π β (1...π) β 1 β (1...π))) |
216 | | fveqeq2 6856 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 1 β ((πβπ) = 0 β (πβ1) = 0)) |
217 | 215, 216 | 3anbi13d 1439 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 1 β ((π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = 0) β (1 β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβ1) = 0))) |
218 | 217 | anbi2d 630 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 1 β ((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = 0)) β (π β§ (1 β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβ1) = 0)))) |
219 | | breq2 5114 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 1 β (π΅ < π β π΅ < 1)) |
220 | 218, 219 | imbi12d 345 |
. . . . . . . . . . . . . . . . 17
β’ (π = 1 β (((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = 0)) β π΅ < π) β ((π β§ (1 β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβ1) = 0)) β π΅ < 1))) |
221 | | poimirlem28.3 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = 0)) β π΅ < π) |
222 | 214, 220,
221 | vtocl 3521 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (1 β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβ1) = 0)) β π΅ < 1) |
223 | | poimirlem28.2 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π:(1...π)βΆ(0...πΎ)) β π΅ β (0...π)) |
224 | | elfznn0 13541 |
. . . . . . . . . . . . . . . . . 18
β’ (π΅ β (0...π) β π΅ β
β0) |
225 | | nn0lt10b 12572 |
. . . . . . . . . . . . . . . . . 18
β’ (π΅ β β0
β (π΅ < 1 β
π΅ = 0)) |
226 | 223, 224,
225 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π:(1...π)βΆ(0...πΎ)) β (π΅ < 1 β π΅ = 0)) |
227 | 226 | 3ad2antr2 1190 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (1 β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβ1) = 0)) β (π΅ < 1 β π΅ = 0)) |
228 | 222, 227 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (1 β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβ1) = 0)) β π΅ = 0) |
229 | 202, 205,
213, 228 | vtoclf 3519 |
. . . . . . . . . . . . . 14
β’ ((π β§ (1 β (1...π) β§ ((1...π) Γ {0}):(1...π)βΆ(0...πΎ) β§ (((1...π) Γ {0})β1) = 0)) β
β¦((1...π)
Γ {0}) / πβ¦π΅ = 0) |
230 | 198, 229 | mpdan 686 |
. . . . . . . . . . . . 13
β’ (π β β¦((1...π) Γ {0}) / πβ¦π΅ = 0) |
231 | 230 | eqcomd 2743 |
. . . . . . . . . . . 12
β’ (π β 0 =
β¦((1...π)
Γ {0}) / πβ¦π΅) |
232 | 231 | ralrimivw 3148 |
. . . . . . . . . . 11
β’ (π β βπ β {β¨β
, β
β©}0 =
β¦((1...π)
Γ {0}) / πβ¦π΅) |
233 | | rabid2 3439 |
. . . . . . . . . . 11
β’
({β¨β
, β
β©} = {π β {β¨β
, β
β©}
β£ 0 = β¦((1...π) Γ {0}) / πβ¦π΅} β βπ β {β¨β
, β
β©}0 =
β¦((1...π)
Γ {0}) / πβ¦π΅) |
234 | 232, 233 | sylibr 233 |
. . . . . . . . . 10
β’ (π β {β¨β
,
β
β©} = {π β
{β¨β
, β
β©} β£ 0 = β¦((1...π) Γ {0}) / πβ¦π΅}) |
235 | 234 | fveq2d 6851 |
. . . . . . . . 9
β’ (π β
(β―β{β¨β
, β
β©}) = (β―β{π β {β¨β
,
β
β©} β£ 0 = β¦((1...π) Γ {0}) / πβ¦π΅})) |
236 | 186, 235 | eqtr3id 2791 |
. . . . . . . 8
β’ (π β 1 = (β―β{π β {β¨β
,
β
β©} β£ 0 = β¦((1...π) Γ {0}) / πβ¦π΅})) |
237 | 236 | breq2d 5122 |
. . . . . . 7
β’ (π β (2 β₯ 1 β 2
β₯ (β―β{π
β {β¨β
, β
β©} β£ 0 = β¦((1...π) Γ {0}) / πβ¦π΅}))) |
238 | 183, 237 | mtbii 326 |
. . . . . 6
β’ (π β Β¬ 2 β₯
(β―β{π β
{β¨β
, β
β©} β£ 0 = β¦((1...π) Γ {0}) / πβ¦π΅})) |
239 | 238 | a1i 11 |
. . . . 5
β’ (π β β0
β (π β Β¬ 2
β₯ (β―β{π
β {β¨β
, β
β©} β£ 0 = β¦((1...π) Γ {0}) / πβ¦π΅}))) |
240 | | 2z 12542 |
. . . . . . . . . . . . 13
β’ 2 β
β€ |
241 | | fzfi 13884 |
. . . . . . . . . . . . . . . . 17
β’
(1...(π + 1)) β
Fin |
242 | | mapfi 9299 |
. . . . . . . . . . . . . . . . 17
β’
(((0..^πΎ) β Fin
β§ (1...(π + 1)) β
Fin) β ((0..^πΎ)
βm (1...(π
+ 1))) β Fin) |
243 | 10, 241, 242 | mp2an 691 |
. . . . . . . . . . . . . . . 16
β’
((0..^πΎ)
βm (1...(π
+ 1))) β Fin |
244 | | ovex 7395 |
. . . . . . . . . . . . . . . . . . 19
β’
(1...(π + 1)) β
V |
245 | 244, 244 | mapval 8784 |
. . . . . . . . . . . . . . . . . 18
β’
((1...(π + 1))
βm (1...(π
+ 1))) = {π β£ π:(1...(π + 1))βΆ(1...(π + 1))} |
246 | | mapfi 9299 |
. . . . . . . . . . . . . . . . . . 19
β’
(((1...(π + 1))
β Fin β§ (1...(π +
1)) β Fin) β ((1...(π + 1)) βm (1...(π + 1))) β
Fin) |
247 | 241, 241,
246 | mp2an 691 |
. . . . . . . . . . . . . . . . . 18
β’
((1...(π + 1))
βm (1...(π
+ 1))) β Fin |
248 | 245, 247 | eqeltrri 2835 |
. . . . . . . . . . . . . . . . 17
β’ {π β£ π:(1...(π + 1))βΆ(1...(π + 1))} β Fin |
249 | | f1of 6789 |
. . . . . . . . . . . . . . . . . 18
β’ (π:(1...(π + 1))β1-1-ontoβ(1...(π + 1)) β π:(1...(π + 1))βΆ(1...(π + 1))) |
250 | 249 | ss2abi 4028 |
. . . . . . . . . . . . . . . . 17
β’ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))} β {π β£ π:(1...(π + 1))βΆ(1...(π + 1))} |
251 | | ssfi 9124 |
. . . . . . . . . . . . . . . . 17
β’ (({π β£ π:(1...(π + 1))βΆ(1...(π + 1))} β Fin β§ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))} β {π β£ π:(1...(π + 1))βΆ(1...(π + 1))}) β {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))} β Fin) |
252 | 248, 250,
251 | mp2an 691 |
. . . . . . . . . . . . . . . 16
β’ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))} β Fin |
253 | | xpfi 9268 |
. . . . . . . . . . . . . . . 16
β’
((((0..^πΎ)
βm (1...(π
+ 1))) β Fin β§ {π
β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))} β Fin) β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β Fin) |
254 | 243, 252,
253 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’
(((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β Fin |
255 | | rabfi 9220 |
. . . . . . . . . . . . . . 15
β’
((((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β Fin β {π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅} β Fin) |
256 | | hashcl 14263 |
. . . . . . . . . . . . . . 15
β’ ({π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅} β Fin β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β
β0) |
257 | 254, 255,
256 | mp2b 10 |
. . . . . . . . . . . . . 14
β’
(β―β{π
β (((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β
β0 |
258 | 257 | nn0zi 12535 |
. . . . . . . . . . . . 13
β’
(β―β{π
β (((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β β€ |
259 | | rabfi 9220 |
. . . . . . . . . . . . . . 15
β’
((((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β Fin β {π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))} β Fin) |
260 | | hashcl 14263 |
. . . . . . . . . . . . . . 15
β’ ({π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))} β Fin β
(β―β{π β
(((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}) β
β0) |
261 | 254, 259,
260 | mp2b 10 |
. . . . . . . . . . . . . 14
β’
(β―β{π
β (((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}) β
β0 |
262 | 261 | nn0zi 12535 |
. . . . . . . . . . . . 13
β’
(β―β{π
β (((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}) β β€ |
263 | 240, 258,
262 | 3pm3.2i 1340 |
. . . . . . . . . . . 12
β’ (2 β
β€ β§ (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β β€ β§
(β―β{π β
(((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}) β β€) |
264 | | nn0p1nn 12459 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (π + 1) β
β) |
265 | 264 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β0 β§ π < π)) β (π + 1) β β) |
266 | | uneq1 4121 |
. . . . . . . . . . . . . . . 16
β’ (π = ((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) β (π βͺ ((((π + 1) + 1)...π) Γ {0})) = (((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0}))) |
267 | 266 | csbeq1d 3864 |
. . . . . . . . . . . . . . 15
β’ (π = ((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) β
β¦(π βͺ
((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅) |
268 | 70 | fconst 6733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π + 1) + 1)...π) Γ {0}):(((π + 1) + 1)...π)βΆ{0} |
269 | 268 | jctr 526 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π:(1...(π + 1))βΆ(0...πΎ) β (π:(1...(π + 1))βΆ(0...πΎ) β§ ((((π + 1) + 1)...π) Γ {0}):(((π + 1) + 1)...π)βΆ{0})) |
270 | 264 | nnred 12175 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β0
β (π + 1) β
β) |
271 | 270 | ltp1d 12092 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β0
β (π + 1) < ((π + 1) + 1)) |
272 | | fzdisj 13475 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π + 1) < ((π + 1) + 1) β ((1...(π + 1)) β© (((π + 1) + 1)...π)) = β
) |
273 | 271, 272 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β0
β ((1...(π + 1)) β©
(((π + 1) + 1)...π)) = β
) |
274 | | fun 6709 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π:(1...(π + 1))βΆ(0...πΎ) β§ ((((π + 1) + 1)...π) Γ {0}):(((π + 1) + 1)...π)βΆ{0}) β§ ((1...(π + 1)) β© (((π + 1) + 1)...π)) = β
) β (π βͺ ((((π + 1) + 1)...π) Γ {0})):((1...(π + 1)) βͺ (((π + 1) + 1)...π))βΆ((0...πΎ) βͺ {0})) |
275 | 269, 273,
274 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β0
β§ π:(1...(π + 1))βΆ(0...πΎ)) β (π βͺ ((((π + 1) + 1)...π) Γ {0})):((1...(π + 1)) βͺ (((π + 1) + 1)...π))βΆ((0...πΎ) βͺ {0})) |
276 | 275 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β0
β§ π < π) β§ π:(1...(π + 1))βΆ(0...πΎ)) β (π βͺ ((((π + 1) + 1)...π) Γ {0})):((1...(π + 1)) βͺ (((π + 1) + 1)...π))βΆ((0...πΎ) βͺ {0})) |
277 | 276 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ ((π β β0 β§ π < π) β§ π:(1...(π + 1))βΆ(0...πΎ))) β (π βͺ ((((π + 1) + 1)...π) Γ {0})):((1...(π + 1)) βͺ (((π + 1) + 1)...π))βΆ((0...πΎ) βͺ {0})) |
278 | 264 | peano2nnd 12177 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β0
β ((π + 1) + 1) β
β) |
279 | 278, 187 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β0
β ((π + 1) + 1) β
(β€β₯β1)) |
280 | 279 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π β β0 β§ π < π)) β ((π + 1) + 1) β
(β€β₯β1)) |
281 | | nn0z 12531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β β0
β π β
β€) |
282 | 1 | nnzd 12533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β π β β€) |
283 | | zltp1le 12560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β β€ β§ π β β€) β (π < π β (π + 1) β€ π)) |
284 | 281, 282,
283 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π β β0) β (π < π β (π + 1) β€ π)) |
285 | 284 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β β0) β§ π < π) β (π + 1) β€ π) |
286 | 285 | anasss 468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (π β β0 β§ π < π)) β (π + 1) β€ π) |
287 | 281 | peano2zd 12617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β0
β (π + 1) β
β€) |
288 | 287 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β β0
β§ π < π) β (π + 1) β β€) |
289 | | eluz 12784 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π + 1) β β€ β§ π β β€) β (π β
(β€β₯β(π + 1)) β (π + 1) β€ π)) |
290 | 288, 282,
289 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (π β β0 β§ π < π)) β (π β (β€β₯β(π + 1)) β (π + 1) β€ π)) |
291 | 286, 290 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π β β0 β§ π < π)) β π β (β€β₯β(π + 1))) |
292 | | fzsplit2 13473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π + 1) + 1) β
(β€β₯β1) β§ π β (β€β₯β(π + 1))) β (1...π) = ((1...(π + 1)) βͺ (((π + 1) + 1)...π))) |
293 | 280, 291,
292 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π β β0 β§ π < π)) β (1...π) = ((1...(π + 1)) βͺ (((π + 1) + 1)...π))) |
294 | 293 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β β0 β§ π < π)) β ((1...(π + 1)) βͺ (((π + 1) + 1)...π)) = (1...π)) |
295 | 192, 193 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β 0 β (0...πΎ)) |
296 | 295 | snssd 4774 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β {0} β (0...πΎ)) |
297 | | ssequn2 4148 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ({0}
β (0...πΎ) β
((0...πΎ) βͺ {0}) =
(0...πΎ)) |
298 | 296, 297 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ((0...πΎ) βͺ {0}) = (0...πΎ)) |
299 | 298 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β β0 β§ π < π)) β ((0...πΎ) βͺ {0}) = (0...πΎ)) |
300 | 294, 299 | feq23d 6668 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π β β0 β§ π < π)) β ((π βͺ ((((π + 1) + 1)...π) Γ {0})):((1...(π + 1)) βͺ (((π + 1) + 1)...π))βΆ((0...πΎ) βͺ {0}) β (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ))) |
301 | 300 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ ((π β β0 β§ π < π) β§ π:(1...(π + 1))βΆ(0...πΎ))) β ((π βͺ ((((π + 1) + 1)...π) Γ {0})):((1...(π + 1)) βͺ (((π + 1) + 1)...π))βΆ((0...πΎ) βͺ {0}) β (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ))) |
302 | 277, 301 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ ((π β β0 β§ π < π) β§ π:(1...(π + 1))βΆ(0...πΎ))) β (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ)) |
303 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π(π β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ)) |
304 | | nfcsb1v 3885 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²πβ¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ |
305 | 304 | nfel1 2924 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²πβ¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β (0...π) |
306 | 303, 305 | nfim 1900 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π((π β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β (0...π)) |
307 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π β V |
308 | | ovex 7395 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π + 1) + 1)...π) β V |
309 | 308, 204 | xpex 7692 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π + 1) + 1)...π) Γ {0}) β V |
310 | 307, 309 | unex 7685 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π βͺ ((((π + 1) + 1)...π) Γ {0})) β V |
311 | | feq1 6654 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β (π:(1...π)βΆ(0...πΎ) β (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ))) |
312 | 311 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β ((π β§ π:(1...π)βΆ(0...πΎ)) β (π β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ)))) |
313 | | csbeq1a 3874 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β π΅ = β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅) |
314 | 313 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β (π΅ β (0...π) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β (0...π))) |
315 | 312, 314 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β (((π β§ π:(1...π)βΆ(0...πΎ)) β π΅ β (0...π)) β ((π β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β (0...π)))) |
316 | 306, 310,
315, 223 | vtoclf 3519 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β (0...π)) |
317 | 302, 316 | syldan 592 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β0 β§ π < π) β§ π:(1...(π + 1))βΆ(0...πΎ))) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β (0...π)) |
318 | 317 | anassrs 469 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β0 β§ π < π)) β§ π:(1...(π + 1))βΆ(0...πΎ)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β (0...π)) |
319 | | elfznn0 13541 |
. . . . . . . . . . . . . . . . 17
β’
(β¦(π
βͺ ((((π + 1) +
1)...π) Γ {0})) /
πβ¦π΅ β (0...π) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β
β0) |
320 | 318, 319 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β0 β§ π < π)) β§ π:(1...(π + 1))βΆ(0...πΎ)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β
β0) |
321 | 264 | nnnn0d 12480 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β (π + 1) β
β0) |
322 | 321 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β0
β§ π < π) β (π + 1) β
β0) |
323 | 322 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β0 β§ π < π)) β§ π:(1...(π + 1))βΆ(0...πΎ)) β (π + 1) β
β0) |
324 | | leloe 11248 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π + 1) β β β§ π β β) β ((π + 1) β€ π β ((π + 1) < π β¨ (π + 1) = π))) |
325 | 270, 3, 324 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β0) β ((π + 1) β€ π β ((π + 1) < π β¨ (π + 1) = π))) |
326 | 284, 325 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β0) β (π < π β ((π + 1) < π β¨ (π + 1) = π))) |
327 | 326 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β0) β (π < π β ((π + 1) < π β¨ (π + 1) = π))) |
328 | 327 | imdistani 570 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β0) β§ π < π) β ((π β§ π β β0) β§ ((π + 1) < π β¨ (π + 1) = π))) |
329 | 328 | anasss 468 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β β0 β§ π < π)) β ((π β§ π β β0) β§ ((π + 1) < π β¨ (π + 1) = π))) |
330 | | simplll 774 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) < π) β π) |
331 | 278 | nnge1d 12208 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β0
β 1 β€ ((π + 1) +
1)) |
332 | 331 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β β0) β§ (π + 1) < π) β 1 β€ ((π + 1) + 1)) |
333 | | zltp1le 12560 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π + 1) β β€ β§ π β β€) β ((π + 1) < π β ((π + 1) + 1) β€ π)) |
334 | 287, 282,
333 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β0) β ((π + 1) < π β ((π + 1) + 1) β€ π)) |
335 | 334 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β β0) β§ (π + 1) < π) β ((π + 1) + 1) β€ π) |
336 | 287 | peano2zd 12617 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β0
β ((π + 1) + 1) β
β€) |
337 | | 1z 12540 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ 1 β
β€ |
338 | | elfz 13437 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π + 1) + 1) β β€ β§
1 β β€ β§ π
β β€) β (((π
+ 1) + 1) β (1...π)
β (1 β€ ((π + 1) +
1) β§ ((π + 1) + 1) β€
π))) |
339 | 337, 338 | mp3an2 1450 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π + 1) + 1) β β€ β§
π β β€) β
(((π + 1) + 1) β
(1...π) β (1 β€
((π + 1) + 1) β§ ((π + 1) + 1) β€ π))) |
340 | 336, 282,
339 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β0) β (((π + 1) + 1) β (1...π) β (1 β€ ((π + 1) + 1) β§ ((π + 1) + 1) β€ π))) |
341 | 340 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β β0) β§ (π + 1) < π) β (((π + 1) + 1) β (1...π) β (1 β€ ((π + 1) + 1) β§ ((π + 1) + 1) β€ π))) |
342 | 332, 335,
341 | mpbir2and 712 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β0) β§ (π + 1) < π) β ((π + 1) + 1) β (1...π)) |
343 | 342 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) < π) β ((π + 1) + 1) β (1...π)) |
344 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β0
β π β
β) |
345 | 344 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β0) β§ (π + 1) < π) β π β β) |
346 | 270 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β0) β§ (π + 1) < π) β (π + 1) β β) |
347 | 3 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β0) β§ (π + 1) < π) β π β β) |
348 | 344 | ltp1d 12092 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β0
β π < (π + 1)) |
349 | 348 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β0) β§ (π + 1) < π) β π < (π + 1)) |
350 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β0) β§ (π + 1) < π) β (π + 1) < π) |
351 | 345, 346,
347, 349, 350 | lttrd 11323 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β β0) β§ (π + 1) < π) β π < π) |
352 | 351 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) < π) β π < π) |
353 | | anass 470 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β0) β§ π < π) β (π β§ (π β β0 β§ π < π))) |
354 | 302 | anassrs 469 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ (π β β0 β§ π < π)) β§ π:(1...(π + 1))βΆ(0...πΎ)) β (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ)) |
355 | 353, 354 | sylanb 582 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β β0) β§ π < π) β§ π:(1...(π + 1))βΆ(0...πΎ)) β (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ)) |
356 | 355 | an32s 651 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ π < π) β (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ)) |
357 | 352, 356 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) < π) β (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ)) |
358 | | ffn 6673 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π:(1...(π + 1))βΆ(0...πΎ) β π Fn (1...(π + 1))) |
359 | 358 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) < π) β π Fn (1...(π + 1))) |
360 | 273 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) < π) β ((1...(π + 1)) β© (((π + 1) + 1)...π)) = β
) |
361 | | eluz 12784 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π + 1) + 1) β β€ β§
π β β€) β
(π β
(β€β₯β((π + 1) + 1)) β ((π + 1) + 1) β€ π)) |
362 | 336, 282,
361 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π β β0) β (π β
(β€β₯β((π + 1) + 1)) β ((π + 1) + 1) β€ π)) |
363 | 362 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β β0) β§ (π + 1) < π) β (π β
(β€β₯β((π + 1) + 1)) β ((π + 1) + 1) β€ π)) |
364 | 335, 363 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β0) β§ (π + 1) < π) β π β
(β€β₯β((π + 1) + 1))) |
365 | | eluzfz1 13455 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β
(β€β₯β((π + 1) + 1)) β ((π + 1) + 1) β (((π + 1) + 1)...π)) |
366 | 364, 365 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β0) β§ (π + 1) < π) β ((π + 1) + 1) β (((π + 1) + 1)...π)) |
367 | 366 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) < π) β ((π + 1) + 1) β (((π + 1) + 1)...π)) |
368 | | fnconstg 6735 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (0 β
V β ((((π + 1) +
1)...π) Γ {0}) Fn
(((π + 1) + 1)...π)) |
369 | 70, 368 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π + 1) + 1)...π) Γ {0}) Fn (((π + 1) + 1)...π) |
370 | | fvun2 6938 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π Fn (1...(π + 1)) β§ ((((π + 1) + 1)...π) Γ {0}) Fn (((π + 1) + 1)...π) β§ (((1...(π + 1)) β© (((π + 1) + 1)...π)) = β
β§ ((π + 1) + 1) β (((π + 1) + 1)...π))) β ((π βͺ ((((π + 1) + 1)...π) Γ {0}))β((π + 1) + 1)) = (((((π + 1) + 1)...π) Γ {0})β((π + 1) + 1))) |
371 | 369, 370 | mp3an2 1450 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π Fn (1...(π + 1)) β§ (((1...(π + 1)) β© (((π + 1) + 1)...π)) = β
β§ ((π + 1) + 1) β (((π + 1) + 1)...π))) β ((π βͺ ((((π + 1) + 1)...π) Γ {0}))β((π + 1) + 1)) = (((((π + 1) + 1)...π) Γ {0})β((π + 1) + 1))) |
372 | 359, 360,
367, 371 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) < π) β ((π βͺ ((((π + 1) + 1)...π) Γ {0}))β((π + 1) + 1)) = (((((π + 1) + 1)...π) Γ {0})β((π + 1) + 1))) |
373 | 70 | fvconst2 7158 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π + 1) + 1) β (((π + 1) + 1)...π) β (((((π + 1) + 1)...π) Γ {0})β((π + 1) + 1)) = 0) |
374 | 367, 373 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) < π) β (((((π + 1) + 1)...π) Γ {0})β((π + 1) + 1)) = 0) |
375 | 372, 374 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) < π) β ((π βͺ ((((π + 1) + 1)...π) Γ {0}))β((π + 1) + 1)) = 0) |
376 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π(π β§ (((π + 1) + 1) β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))β((π + 1) + 1)) = 0)) |
377 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π
< |
378 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π((π + 1) + 1) |
379 | 304, 377,
378 | nfbr 5157 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²πβ¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ < ((π + 1) + 1) |
380 | 376, 379 | nfim 1900 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π((π β§ (((π + 1) + 1) β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))β((π + 1) + 1)) = 0)) β
β¦(π βͺ
((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ < ((π + 1) + 1)) |
381 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β (πβ((π + 1) + 1)) = ((π βͺ ((((π + 1) + 1)...π) Γ {0}))β((π + 1) + 1))) |
382 | 381 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β ((πβ((π + 1) + 1)) = 0 β ((π βͺ ((((π + 1) + 1)...π) Γ {0}))β((π + 1) + 1)) = 0)) |
383 | 311, 382 | 3anbi23d 1440 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β ((((π + 1) + 1) β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβ((π + 1) + 1)) = 0) β (((π + 1) + 1) β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))β((π + 1) + 1)) = 0))) |
384 | 383 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β ((π β§ (((π + 1) + 1) β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβ((π + 1) + 1)) = 0)) β (π β§ (((π + 1) + 1) β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))β((π + 1) + 1)) = 0)))) |
385 | 313 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β (π΅ < ((π + 1) + 1) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ < ((π + 1) + 1))) |
386 | 384, 385 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β (((π β§ (((π + 1) + 1) β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβ((π + 1) + 1)) = 0)) β π΅ < ((π + 1) + 1)) β ((π β§ (((π + 1) + 1) β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))β((π + 1) + 1)) = 0)) β
β¦(π βͺ
((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ < ((π + 1) + 1)))) |
387 | | ovex 7395 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π + 1) + 1) β
V |
388 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = ((π + 1) + 1) β (π β (1...π) β ((π + 1) + 1) β (1...π))) |
389 | | fveqeq2 6856 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = ((π + 1) + 1) β ((πβπ) = 0 β (πβ((π + 1) + 1)) = 0)) |
390 | 388, 389 | 3anbi13d 1439 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = ((π + 1) + 1) β ((π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = 0) β (((π + 1) + 1) β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβ((π + 1) + 1)) = 0))) |
391 | 390 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = ((π + 1) + 1) β ((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = 0)) β (π β§ (((π + 1) + 1) β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβ((π + 1) + 1)) = 0)))) |
392 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = ((π + 1) + 1) β (π΅ < π β π΅ < ((π + 1) + 1))) |
393 | 391, 392 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = ((π + 1) + 1) β (((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = 0)) β π΅ < π) β ((π β§ (((π + 1) + 1) β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβ((π + 1) + 1)) = 0)) β π΅ < ((π + 1) + 1)))) |
394 | 387, 393,
221 | vtocl 3521 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (((π + 1) + 1) β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβ((π + 1) + 1)) = 0)) β π΅ < ((π + 1) + 1)) |
395 | 380, 310,
386, 394 | vtoclf 3519 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (((π + 1) + 1) β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))β((π + 1) + 1)) = 0)) β
β¦(π βͺ
((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ < ((π + 1) + 1)) |
396 | 330, 343,
357, 375, 395 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) < π) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ < ((π + 1) + 1)) |
397 | 353, 318 | sylanb 582 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β β0) β§ π < π) β§ π:(1...(π + 1))βΆ(0...πΎ)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β (0...π)) |
398 | 397 | an32s 651 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ π < π) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β (0...π)) |
399 | 398 | elfzelzd 13449 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ π < π) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β β€) |
400 | 352, 399 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) < π) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β β€) |
401 | 287 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) < π) β (π + 1) β β€) |
402 | | zleltp1 12561 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β¦(π
βͺ ((((π + 1) +
1)...π) Γ {0})) /
πβ¦π΅ β β€ β§ (π + 1) β β€) β
(β¦(π βͺ
((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β€ (π + 1) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ < ((π + 1) + 1))) |
403 | 400, 401,
402 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) < π) β (β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β€ (π + 1) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ < ((π + 1) + 1))) |
404 | 396, 403 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) < π) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β€ (π + 1)) |
405 | 348 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β π < (π + 1)) |
406 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π + 1) = π β (π < (π + 1) β π < π)) |
407 | 406 | biimpac 480 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π < (π + 1) β§ (π + 1) = π) β π < π) |
408 | 405, 407 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) = π) β π < π) |
409 | | elfzle2 13452 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(β¦(π
βͺ ((((π + 1) +
1)...π) Γ {0})) /
πβ¦π΅ β (0...π) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β€ π) |
410 | 398, 409 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ π < π) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β€ π) |
411 | 408, 410 | syldan 592 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) = π) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β€ π) |
412 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) = π) β (π + 1) = π) |
413 | 411, 412 | breqtrrd 5138 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ (π + 1) = π) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β€ (π + 1)) |
414 | 404, 413 | jaodan 957 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β β0) β§ π:(1...(π + 1))βΆ(0...πΎ)) β§ ((π + 1) < π β¨ (π + 1) = π)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β€ (π + 1)) |
415 | 414 | an32s 651 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β β0) β§ ((π + 1) < π β¨ (π + 1) = π)) β§ π:(1...(π + 1))βΆ(0...πΎ)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β€ (π + 1)) |
416 | 329, 415 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β0 β§ π < π)) β§ π:(1...(π + 1))βΆ(0...πΎ)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β€ (π + 1)) |
417 | | elfz2nn0 13539 |
. . . . . . . . . . . . . . . 16
β’
(β¦(π
βͺ ((((π + 1) +
1)...π) Γ {0})) /
πβ¦π΅ β (0...(π + 1)) β (β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β β0 β§ (π + 1) β β0
β§ β¦(π
βͺ ((((π + 1) +
1)...π) Γ {0})) /
πβ¦π΅ β€ (π + 1))) |
418 | 320, 323,
416, 417 | syl3anbrc 1344 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β0 β§ π < π)) β§ π:(1...(π + 1))βΆ(0...πΎ)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β (0...(π + 1))) |
419 | | fzss2 13488 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β
(β€β₯β(π + 1)) β (1...(π + 1)) β (1...π)) |
420 | 291, 419 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β β0 β§ π < π)) β (1...(π + 1)) β (1...π)) |
421 | 420 | sselda 3949 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β β0 β§ π < π)) β§ π β (1...(π + 1))) β π β (1...π)) |
422 | 421 | 3ad2antr1 1189 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β0 β§ π < π)) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = 0)) β π β (1...π)) |
423 | 354 | 3ad2antr2 1190 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β0 β§ π < π)) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = 0)) β (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ)) |
424 | 358 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β0) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ))) β π Fn (1...(π + 1))) |
425 | 273 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β0) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ))) β ((1...(π + 1)) β© (((π + 1) + 1)...π)) = β
) |
426 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β0) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ))) β π β (1...(π + 1))) |
427 | | fvun1 6937 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π Fn (1...(π + 1)) β§ ((((π + 1) + 1)...π) Γ {0}) Fn (((π + 1) + 1)...π) β§ (((1...(π + 1)) β© (((π + 1) + 1)...π)) = β
β§ π β (1...(π + 1)))) β ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = (πβπ)) |
428 | 369, 427 | mp3an2 1450 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π Fn (1...(π + 1)) β§ (((1...(π + 1)) β© (((π + 1) + 1)...π)) = β
β§ π β (1...(π + 1)))) β ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = (πβπ)) |
429 | 424, 425,
426, 428 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β0) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ))) β ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = (πβπ)) |
430 | 429 | adantlrr 720 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β β0 β§ π < π)) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ))) β ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = (πβπ)) |
431 | 430 | 3adantr3 1172 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β β0 β§ π < π)) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = 0)) β ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = (πβπ)) |
432 | | simpr3 1197 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β β0 β§ π < π)) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = 0)) β (πβπ) = 0) |
433 | 431, 432 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β0 β§ π < π)) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = 0)) β ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = 0) |
434 | 422, 423,
433 | 3jca 1129 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β0 β§ π < π)) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = 0)) β (π β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = 0)) |
435 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π(π β§ (π β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = 0)) |
436 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²ππ |
437 | 304, 377,
436 | nfbr 5157 |
. . . . . . . . . . . . . . . . . . 19
β’
β²πβ¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ < π |
438 | 435, 437 | nfim 1900 |
. . . . . . . . . . . . . . . . . 18
β’
β²π((π β§ (π β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = 0)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ < π) |
439 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β (πβπ) = ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ)) |
440 | 439 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β ((πβπ) = 0 β ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = 0)) |
441 | 311, 440 | 3anbi23d 1440 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β ((π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = 0) β (π β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = 0))) |
442 | 441 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β ((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = 0)) β (π β§ (π β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = 0)))) |
443 | 313 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β (π΅ < π β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ < π)) |
444 | 442, 443 | imbi12d 345 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β (((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = 0)) β π΅ < π) β ((π β§ (π β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = 0)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ < π))) |
445 | 438, 310,
444, 221 | vtoclf 3519 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = 0)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ < π) |
446 | 445 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β0 β§ π < π)) β§ (π β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = 0)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ < π) |
447 | 434, 446 | syldan 592 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β0 β§ π < π)) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = 0)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ < π) |
448 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = πΎ) β π β (1...(π + 1))) |
449 | 421 | anasss 468 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ ((π β β0 β§ π < π) β§ π β (1...(π + 1)))) β π β (1...π)) |
450 | 448, 449 | sylanr2 682 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β0 β§ π < π) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = πΎ))) β π β (1...π)) |
451 | | simp2 1138 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = πΎ) β π:(1...(π + 1))βΆ(0...πΎ)) |
452 | 451, 302 | sylanr2 682 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β0 β§ π < π) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = πΎ))) β (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ)) |
453 | 429 | 3adantr3 1172 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β0) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = πΎ)) β ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = (πβπ)) |
454 | | simpr3 1197 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β0) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = πΎ)) β (πβπ) = πΎ) |
455 | 453, 454 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β0) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = πΎ)) β ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = πΎ) |
456 | 455 | anasss 468 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β β0 β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = πΎ))) β ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = πΎ) |
457 | 456 | adantrlr 722 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β0 β§ π < π) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = πΎ))) β ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = πΎ) |
458 | 450, 452,
457 | 3jca 1129 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π β β0 β§ π < π) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = πΎ))) β (π β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = πΎ)) |
459 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π(π β§ (π β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = πΎ)) |
460 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π(π β 1) |
461 | 304, 460 | nfne 3046 |
. . . . . . . . . . . . . . . . . . 19
β’
β²πβ¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β (π β 1) |
462 | 459, 461 | nfim 1900 |
. . . . . . . . . . . . . . . . . 18
β’
β²π((π β§ (π β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = πΎ)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β (π β 1)) |
463 | 439 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β ((πβπ) = πΎ β ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = πΎ)) |
464 | 311, 463 | 3anbi23d 1440 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β ((π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = πΎ) β (π β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = πΎ))) |
465 | 464 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β ((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = πΎ)) β (π β§ (π β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = πΎ)))) |
466 | 313 | neeq1d 3004 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β (π΅ β (π β 1) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β (π β 1))) |
467 | 465, 466 | imbi12d 345 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π βͺ ((((π + 1) + 1)...π) Γ {0})) β (((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = πΎ)) β π΅ β (π β 1)) β ((π β§ (π β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = πΎ)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β (π β 1)))) |
468 | | poimirlem28.4 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β (1...π) β§ π:(1...π)βΆ(0...πΎ) β§ (πβπ) = πΎ)) β π΅ β (π β 1)) |
469 | 462, 310,
467, 468 | vtoclf 3519 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β (1...π) β§ (π βͺ ((((π + 1) + 1)...π) Γ {0})):(1...π)βΆ(0...πΎ) β§ ((π βͺ ((((π + 1) + 1)...π) Γ {0}))βπ) = πΎ)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β (π β 1)) |
470 | 458, 469 | syldan 592 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π β β0 β§ π < π) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = πΎ))) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β (π β 1)) |
471 | 470 | anassrs 469 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β0 β§ π < π)) β§ (π β (1...(π + 1)) β§ π:(1...(π + 1))βΆ(0...πΎ) β§ (πβπ) = πΎ)) β β¦(π βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β (π β 1)) |
472 | 265, 267,
418, 447, 471 | poimirlem27 36134 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β0 β§ π < π)) β 2 β₯ ((β―β{π‘ β ((((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st
βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd βπ )β(π + 1)) = (π + 1))}))) |
473 | 265, 267,
418 | poimirlem26 36133 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β0 β§ π < π)) β 2 β₯ ((β―β{π‘ β ((((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st
βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}))) |
474 | | fzfi 13884 |
. . . . . . . . . . . . . . . . . . 19
β’
(0...(π + 1)) β
Fin |
475 | | xpfi 9268 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β Fin β§ (0...(π + 1)) β Fin) β
((((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β Fin) |
476 | 254, 474,
475 | mp2an 691 |
. . . . . . . . . . . . . . . . . 18
β’
((((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β Fin |
477 | | rabfi 9220 |
. . . . . . . . . . . . . . . . . 18
β’
(((((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β Fin β {π‘ β ((((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st
βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅} β Fin) |
478 | | hashcl 14263 |
. . . . . . . . . . . . . . . . . 18
β’ ({π‘ β ((((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st
βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅} β Fin β (β―β{π‘ β ((((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β
β0) |
479 | 476, 477,
478 | mp2b 10 |
. . . . . . . . . . . . . . . . 17
β’
(β―β{π‘
β ((((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st
βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β β0 |
480 | 479 | nn0zi 12535 |
. . . . . . . . . . . . . . . 16
β’
(β―β{π‘
β ((((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st
βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β β€ |
481 | | zsubcl 12552 |
. . . . . . . . . . . . . . . 16
β’
(((β―β{π‘
β ((((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st
βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β β€ β§ (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd βπ )β(π + 1)) = (π + 1))}) β β€) β
((β―β{π‘ β
((((0..^πΎ) βm
(1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd βπ )β(π + 1)) = (π + 1))})) β β€) |
482 | 480, 262,
481 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’
((β―β{π‘
β ((((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st
βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd βπ )β(π + 1)) = (π + 1))})) β β€ |
483 | | zsubcl 12552 |
. . . . . . . . . . . . . . . 16
β’
(((β―β{π‘
β ((((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st
βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β β€ β§ (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β β€) β
((β―β{π‘ β
((((0..^πΎ) βm
(1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅})) β β€) |
484 | 480, 258,
483 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’
((β―β{π‘
β ((((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st
βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅})) β β€ |
485 | | dvds2sub 16180 |
. . . . . . . . . . . . . . 15
β’ ((2
β β€ β§ ((β―β{π‘ β ((((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st
βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd βπ )β(π + 1)) = (π + 1))})) β β€ β§
((β―β{π‘ β
((((0..^πΎ) βm
(1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅})) β β€) β ((2 β₯
((β―β{π‘ β
((((0..^πΎ) βm
(1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd βπ )β(π + 1)) = (π + 1))})) β§ 2 β₯
((β―β{π‘ β
((((0..^πΎ) βm
(1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}))) β 2 β₯ (((β―β{π‘ β ((((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd βπ )β(π + 1)) = (π + 1))})) β ((β―β{π‘ β ((((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}))))) |
486 | 240, 482,
484, 485 | mp3an 1462 |
. . . . . . . . . . . . . 14
β’ ((2
β₯ ((β―β{π‘
β ((((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st
βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd βπ )β(π + 1)) = (π + 1))})) β§ 2 β₯
((β―β{π‘ β
((((0..^πΎ) βm
(1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}))) β 2 β₯ (((β―β{π‘ β ((((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd βπ )β(π + 1)) = (π + 1))})) β ((β―β{π‘ β ((((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅})))) |
487 | 472, 473,
486 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β0 β§ π < π)) β 2 β₯ (((β―β{π‘ β ((((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st
βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd βπ )β(π + 1)) = (π + 1))})) β ((β―β{π‘ β ((((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅})))) |
488 | 479 | nn0cni 12432 |
. . . . . . . . . . . . . 14
β’
(β―β{π‘
β ((((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st
βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β β |
489 | 261 | nn0cni 12432 |
. . . . . . . . . . . . . 14
β’
(β―β{π
β (((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}) β β |
490 | 257 | nn0cni 12432 |
. . . . . . . . . . . . . 14
β’
(β―β{π
β (((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β β |
491 | | nnncan1 11444 |
. . . . . . . . . . . . . 14
β’
(((β―β{π‘
β ((((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st
βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β β β§ (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd βπ )β(π + 1)) = (π + 1))}) β β β§
(β―β{π β
(((0..^πΎ) βm
(1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β β) β
(((β―β{π‘ β
((((0..^πΎ) βm
(1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd βπ )β(π + 1)) = (π + 1))})) β ((β―β{π‘ β ((((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}))) = ((β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd βπ )β(π + 1)) = (π + 1))}))) |
492 | 488, 489,
490, 491 | mp3an 1462 |
. . . . . . . . . . . . 13
β’
(((β―β{π‘
β ((((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st
βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd βπ )β(π + 1)) = (π + 1))})) β ((β―β{π‘ β ((((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) Γ (0...(π + 1))) β£ βπ β (0...((π + 1) β 1))βπ β ((0...(π + 1)) β {(2nd βπ‘)})π = β¦(1st βπ‘) / π β¦β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}))) = ((β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ ) βf
+ ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd βπ )β(π + 1)) = (π + 1))})) |
493 | 487, 492 | breqtrdi 5151 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β0 β§ π < π)) β 2 β₯ ((β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}))) |
494 | | dvdssub2 16190 |
. . . . . . . . . . . 12
β’ (((2
β β€ β§ (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β β€ β§
(β―β{π β
(((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}) β β€) β§ 2 β₯
((β―β{π β
(((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}))) β (2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β 2 β₯ (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}))) |
495 | 263, 493,
494 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π β§ (π β β0 β§ π < π)) β (2 β₯ (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β 2 β₯ (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}))) |
496 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β π β
β) |
497 | | pncan1 11586 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β ((π + 1) β 1) = π) |
498 | 496, 497 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β ((π + 1) β 1)
= π) |
499 | 498 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β (0...((π + 1)
β 1)) = (0...π)) |
500 | 499 | rexeqdv 3317 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β (βπ β
(0...((π + 1) β
1))π =
β¦(((1st βπ ) βf + ((((2nd
βπ ) β
(1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...(π + 1))) Γ {0}))) βͺ
((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅)) |
501 | 499, 500 | raleqbidv 3322 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β (βπ β
(0...((π + 1) β
1))βπ β
(0...((π + 1) β
1))π =
β¦(((1st βπ ) βf + ((((2nd
βπ ) β
(1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...(π + 1))) Γ {0}))) βͺ
((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅)) |
502 | 501 | 3anbi1d 1441 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β ((βπ β
(0...((π + 1) β
1))βπ β
(0...((π + 1) β
1))π =
β¦(((1st βπ ) βf + ((((2nd
βπ ) β
(1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...(π + 1))) Γ {0}))) βͺ
((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1)) β (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1)))) |
503 | 502 | rabbidv 3418 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β {π β
(((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))} = {π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}) |
504 | 503 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (β―β{π
β (((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}) = (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))})) |
505 | 504 | ad2antrl 727 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β0 β§ π < π)) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}) = (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))})) |
506 | 1 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β0 β§ π < π)) β π β β) |
507 | 191 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β0 β§ π < π)) β πΎ β β) |
508 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β0 β§ π < π)) β π β β0) |
509 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β0 β§ π < π)) β π < π) |
510 | 506, 507,
508, 509 | poimirlem4 36111 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β0 β§ π < π)) β {π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅} β {π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}) |
511 | | fzfi 13884 |
. . . . . . . . . . . . . . . . . 18
β’
(1...π) β
Fin |
512 | | mapfi 9299 |
. . . . . . . . . . . . . . . . . 18
β’
(((0..^πΎ) β Fin
β§ (1...π) β Fin)
β ((0..^πΎ)
βm (1...π))
β Fin) |
513 | 10, 511, 512 | mp2an 691 |
. . . . . . . . . . . . . . . . 17
β’
((0..^πΎ)
βm (1...π))
β Fin |
514 | | ovex 7395 |
. . . . . . . . . . . . . . . . . . . 20
β’
(1...π) β
V |
515 | 514, 514 | mapval 8784 |
. . . . . . . . . . . . . . . . . . 19
β’
((1...π)
βm (1...π))
= {π β£ π:(1...π)βΆ(1...π)} |
516 | | mapfi 9299 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((1...π) β Fin
β§ (1...π) β Fin)
β ((1...π)
βm (1...π))
β Fin) |
517 | 511, 511,
516 | mp2an 691 |
. . . . . . . . . . . . . . . . . . 19
β’
((1...π)
βm (1...π))
β Fin |
518 | 515, 517 | eqeltrri 2835 |
. . . . . . . . . . . . . . . . . 18
β’ {π β£ π:(1...π)βΆ(1...π)} β Fin |
519 | | f1of 6789 |
. . . . . . . . . . . . . . . . . . 19
β’ (π:(1...π)β1-1-ontoβ(1...π) β π:(1...π)βΆ(1...π)) |
520 | 519 | ss2abi 4028 |
. . . . . . . . . . . . . . . . . 18
β’ {π β£ π:(1...π)β1-1-ontoβ(1...π)} β {π β£ π:(1...π)βΆ(1...π)} |
521 | | ssfi 9124 |
. . . . . . . . . . . . . . . . . 18
β’ (({π β£ π:(1...π)βΆ(1...π)} β Fin β§ {π β£ π:(1...π)β1-1-ontoβ(1...π)} β {π β£ π:(1...π)βΆ(1...π)}) β {π β£ π:(1...π)β1-1-ontoβ(1...π)} β Fin) |
522 | 518, 520,
521 | mp2an 691 |
. . . . . . . . . . . . . . . . 17
β’ {π β£ π:(1...π)β1-1-ontoβ(1...π)} β Fin |
523 | | xpfi 9268 |
. . . . . . . . . . . . . . . . 17
β’
((((0..^πΎ)
βm (1...π))
β Fin β§ {π β£
π:(1...π)β1-1-ontoβ(1...π)} β Fin) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β Fin) |
524 | 513, 522,
523 | mp2an 691 |
. . . . . . . . . . . . . . . 16
β’
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β Fin |
525 | | rabfi 9220 |
. . . . . . . . . . . . . . . 16
β’
((((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β Fin β {π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅} β Fin) |
526 | 524, 525 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ {π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅} β Fin |
527 | | rabfi 9220 |
. . . . . . . . . . . . . . . 16
β’
((((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β Fin β {π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))} β Fin) |
528 | 254, 527 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ {π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))} β Fin |
529 | | hashen 14254 |
. . . . . . . . . . . . . . 15
β’ (({π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅} β Fin β§ {π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))} β Fin) β
((β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) = (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}) β {π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅} β {π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))})) |
530 | 526, 528,
529 | mp2an 691 |
. . . . . . . . . . . . . 14
β’
((β―β{π
β (((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) = (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}) β {π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅} β {π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}) |
531 | 510, 530 | sylibr 233 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β0 β§ π < π)) β (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) = (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))})) |
532 | 505, 531 | eqtr4d 2780 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β0 β§ π < π)) β (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}) = (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅})) |
533 | 532 | breq2d 5122 |
. . . . . . . . . . 11
β’ ((π β§ (π β β0 β§ π < π)) β (2 β₯ (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ (βπ β (0...((π + 1) β 1))βπ β (0...((π + 1) β 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅ β§ ((1st βπ )β(π + 1)) = 0 β§ ((2nd
βπ )β(π + 1)) = (π + 1))}) β 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}))) |
534 | 495, 533 | bitrd 279 |
. . . . . . . . . 10
β’ ((π β§ (π β β0 β§ π < π)) β (2 β₯ (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β 2 β₯ (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}))) |
535 | 534 | biimpd 228 |
. . . . . . . . 9
β’ ((π β§ (π β β0 β§ π < π)) β (2 β₯ (β―β{π β (((0..^πΎ) βm (1...(π + 1))) Γ {π β£ π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}) β 2 β₯ (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}))) |
536 | 535 | con3d 152 |
. . . . . . . 8
β’ ((π β§ (π β β0 β§ π < π)) β (Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅}))) |
537 | 536 | expcom 415 |
. . . . . . 7
β’ ((π β β0
β§ π < π) β (π β (Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅})))) |
538 | 537 | a2d 29 |
. . . . . 6
β’ ((π β β0
β§ π < π) β ((π β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅})) β (π β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅})))) |
539 | 538 | 3adant1 1131 |
. . . . 5
β’ ((π β β0
β§ π β
β0 β§ π
< π) β ((π β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅})) β (π β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...(π
+ 1))) Γ {π β£
π:(1...(π + 1))β1-1-ontoβ(1...(π + 1))}) β£ βπ β (0...(π + 1))βπ β (0...(π + 1))π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...(π + 1))) Γ {0}))) βͺ ((((π + 1) + 1)...π) Γ {0})) / πβ¦π΅})))) |
540 | 107, 132,
157, 182, 239, 539 | fnn0ind 12609 |
. . . 4
β’ ((π β β0
β§ π β
β0 β§ π
β€ π) β (π β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}))) |
541 | 5, 540 | mpcom 38 |
. . 3
β’ (π β Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅})) |
542 | | dvds0 16161 |
. . . . . . . 8
β’ (2 β
β€ β 2 β₯ 0) |
543 | 240, 542 | ax-mp 5 |
. . . . . . 7
β’ 2 β₯
0 |
544 | | hash0 14274 |
. . . . . . 7
β’
(β―ββ
) = 0 |
545 | 543, 544 | breqtrri 5137 |
. . . . . 6
β’ 2 β₯
(β―ββ
) |
546 | | fveq2 6847 |
. . . . . 6
β’ ({π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = πΆ} = β
β (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = πΆ}) =
(β―ββ
)) |
547 | 545, 546 | breqtrrid 5148 |
. . . . 5
β’ ({π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = πΆ} = β
β 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = πΆ})) |
548 | 3 | ltp1d 12092 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π < (π + 1)) |
549 | 282 | peano2zd 12617 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π + 1) β β€) |
550 | | fzn 13464 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π + 1) β β€ β§ π β β€) β (π < (π + 1) β ((π + 1)...π) = β
)) |
551 | 549, 282,
550 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π < (π + 1) β ((π + 1)...π) = β
)) |
552 | 548, 551 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π + 1)...π) = β
) |
553 | 552 | xpeq1d 5667 |
. . . . . . . . . . . . . . . 16
β’ (π β (((π + 1)...π) Γ {0}) = (β
Γ
{0})) |
554 | 553, 86 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
β’ (π β (((π + 1)...π) Γ {0}) = β
) |
555 | 554 | uneq2d 4128 |
. . . . . . . . . . . . . 14
β’ (π β (((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) = (((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ
β
)) |
556 | | un0 4355 |
. . . . . . . . . . . . . 14
β’
(((1st βπ ) βf + ((((2nd
βπ ) β
(1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...π)) Γ {0}))) βͺ β
)
= ((1st βπ ) βf + ((((2nd
βπ ) β
(1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...π)) Γ
{0}))) |
557 | 555, 556 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ (π β (((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) = ((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))) |
558 | 557 | csbeq1d 3864 |
. . . . . . . . . . . 12
β’ (π β
β¦(((1st βπ ) βf + ((((2nd
βπ ) β
(1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ = β¦((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) / πβ¦π΅) |
559 | | ovex 7395 |
. . . . . . . . . . . . 13
β’
((1st βπ ) βf + ((((2nd
βπ ) β
(1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...π)) Γ {0}))) β
V |
560 | | poimirlem28.1 |
. . . . . . . . . . . . 13
β’ (π = ((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) β π΅ = πΆ) |
561 | 559, 560 | csbie 3896 |
. . . . . . . . . . . 12
β’
β¦((1st βπ ) βf + ((((2nd
βπ ) β
(1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...π)) Γ {0}))) / πβ¦π΅ = πΆ |
562 | 558, 561 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ (π β
β¦(((1st βπ ) βf + ((((2nd
βπ ) β
(1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ = πΆ) |
563 | 562 | eqeq2d 2748 |
. . . . . . . . . 10
β’ (π β (π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ β π = πΆ)) |
564 | 563 | rexbidv 3176 |
. . . . . . . . 9
β’ (π β (βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ β βπ β (0...π)π = πΆ)) |
565 | 564 | ralbidv 3175 |
. . . . . . . 8
β’ (π β (βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅ β βπ β (0...π)βπ β (0...π)π = πΆ)) |
566 | 565 | rabbidv 3418 |
. . . . . . 7
β’ (π β {π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅} = {π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = πΆ}) |
567 | 566 | fveq2d 6851 |
. . . . . 6
β’ (π β (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) = (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = πΆ})) |
568 | 567 | breq2d 5122 |
. . . . 5
β’ (π β (2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) β 2 β₯ (β―β{π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = πΆ}))) |
569 | 547, 568 | syl5ibr 246 |
. . . 4
β’ (π β ({π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = πΆ} = β
β 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}))) |
570 | 569 | necon3bd 2958 |
. . 3
β’ (π β (Β¬ 2 β₯
(β―β{π β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = β¦(((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βͺ (((π + 1)...π) Γ {0})) / πβ¦π΅}) β {π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = πΆ} β β
)) |
571 | 541, 570 | mpd 15 |
. 2
β’ (π β {π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = πΆ} β β
) |
572 | | rabn0 4350 |
. 2
β’ ({π β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ βπ β (0...π)βπ β (0...π)π = πΆ} β β
β βπ β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})βπ β (0...π)βπ β (0...π)π = πΆ) |
573 | 571, 572 | sylib 217 |
1
β’ (π β βπ β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})βπ β (0...π)βπ β (0...π)π = πΆ) |