Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . . . . . 7
β’ (π β π β β) |
2 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β π β β) |
3 | | fvoveq1 7427 |
. . . . . . . . . . . . 13
β’ (π = ((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) β (πΉβ(π βf / ((1...π) Γ {π}))) = (πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))) |
4 | 3 | fveq1d 6890 |
. . . . . . . . . . . 12
β’ (π = ((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) β ((πΉβ(π βf / ((1...π) Γ {π})))βπ) = ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ)) |
5 | 4 | breq2d 5159 |
. . . . . . . . . . 11
β’ (π = ((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) β (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β 0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ))) |
6 | | fveq1 6887 |
. . . . . . . . . . . 12
β’ (π = ((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) β (πβπ) = (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ)) |
7 | 6 | neeq1d 3001 |
. . . . . . . . . . 11
β’ (π = ((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) β ((πβπ) β 0 β (((1st
βπ )
βf + ((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)) |
8 | 5, 7 | anbi12d 632 |
. . . . . . . . . 10
β’ (π = ((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) β ((0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β (0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0))) |
9 | 8 | ralbidv 3178 |
. . . . . . . . 9
β’ (π = ((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) β (βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0))) |
10 | 9 | rabbidv 3441 |
. . . . . . . 8
β’ (π = ((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) β {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)} = {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}) |
11 | 10 | uneq2d 4162 |
. . . . . . 7
β’ (π = ((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) = ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)})) |
12 | 11 | supeq1d 9437 |
. . . . . 6
β’ (π = ((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) β sup(({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) = sup(({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
)) |
13 | 1 | nnnn0d 12528 |
. . . . . . . . . . 11
β’ (π β π β
β0) |
14 | | 0elfz 13594 |
. . . . . . . . . . 11
β’ (π β β0
β 0 β (0...π)) |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
β’ (π β 0 β (0...π)) |
16 | 15 | snssd 4811 |
. . . . . . . . 9
β’ (π β {0} β (0...π)) |
17 | | ssrab2 4076 |
. . . . . . . . . . 11
β’ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)} β (1...π) |
18 | | fz1ssfz0 13593 |
. . . . . . . . . . 11
β’
(1...π) β
(0...π) |
19 | 17, 18 | sstri 3990 |
. . . . . . . . . 10
β’ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)} β (0...π) |
20 | 19 | a1i 11 |
. . . . . . . . 9
β’ (π β {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)} β (0...π)) |
21 | 16, 20 | unssd 4185 |
. . . . . . . 8
β’ (π β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β (0...π)) |
22 | | ltso 11290 |
. . . . . . . . 9
β’ < Or
β |
23 | | snfi 9040 |
. . . . . . . . . . 11
β’ {0}
β Fin |
24 | | fzfi 13933 |
. . . . . . . . . . . 12
β’
(1...π) β
Fin |
25 | | rabfi 9265 |
. . . . . . . . . . . 12
β’
((1...π) β Fin
β {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)} β Fin) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . . 11
β’ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)} β Fin |
27 | | unfi 9168 |
. . . . . . . . . . 11
β’ (({0}
β Fin β§ {π β
(1...π) β£
βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)} β Fin) β ({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β Fin) |
28 | 23, 26, 27 | mp2an 691 |
. . . . . . . . . 10
β’ ({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β Fin |
29 | | c0ex 11204 |
. . . . . . . . . . . 12
β’ 0 β
V |
30 | 29 | snid 4663 |
. . . . . . . . . . 11
β’ 0 β
{0} |
31 | | elun1 4175 |
. . . . . . . . . . 11
β’ (0 β
{0} β 0 β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)})) |
32 | | ne0i 4333 |
. . . . . . . . . . 11
β’ (0 β
({0} βͺ {π β
(1...π) β£
βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β β
) |
33 | 30, 31, 32 | mp2b 10 |
. . . . . . . . . 10
β’ ({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β β
|
34 | | 0red 11213 |
. . . . . . . . . . . . 13
β’ ((π β π β β) β 0 β
β) |
35 | 34 | snssd 4811 |
. . . . . . . . . . . 12
β’ ((π β π β β) β {0} β
β) |
36 | 1, 35 | ax-mp 5 |
. . . . . . . . . . 11
β’ {0}
β β |
37 | | elfzelz 13497 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β π β β€) |
38 | 37 | ssriv 3985 |
. . . . . . . . . . . . 13
β’
(1...π) β
β€ |
39 | | zssre 12561 |
. . . . . . . . . . . . 13
β’ β€
β β |
40 | 38, 39 | sstri 3990 |
. . . . . . . . . . . 12
β’
(1...π) β
β |
41 | 17, 40 | sstri 3990 |
. . . . . . . . . . 11
β’ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)} β β |
42 | 36, 41 | unssi 4184 |
. . . . . . . . . 10
β’ ({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β β |
43 | 28, 33, 42 | 3pm3.2i 1340 |
. . . . . . . . 9
β’ (({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β Fin β§ ({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β β
β§ ({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β β) |
44 | | fisupcl 9460 |
. . . . . . . . 9
β’ (( <
Or β β§ (({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β Fin β§ ({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β β
β§ ({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β β)) β sup(({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β ({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)})) |
45 | 22, 43, 44 | mp2an 691 |
. . . . . . . 8
β’ sup(({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β ({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) |
46 | | ssel 3974 |
. . . . . . . 8
β’ (({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β (0...π) β (sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β ({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β
(0...π))) |
47 | 21, 45, 46 | mpisyl 21 |
. . . . . . 7
β’ (π β sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β
(0...π)) |
48 | 47 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ π:(1...π)βΆ(0...π)) β sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β
(0...π)) |
49 | | elfznn 13526 |
. . . . . . . . 9
β’ (π β (1...π) β π β β) |
50 | | nngt0 12239 |
. . . . . . . . . . . 12
β’ (π β β β 0 <
π) |
51 | 50 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β β β§ (πβπ) = 0) β 0 < π) |
52 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((0 β€
((πΉβ(π βf /
((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β (πβπ) β 0) |
53 | 52 | ralimi 3084 |
. . . . . . . . . . . . 13
β’
(βπ β
(1...π )(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β βπ β (1...π )(πβπ) β 0) |
54 | | elfznn 13526 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β π β β) |
55 | | nnre 12215 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β π β
β) |
56 | | nnre 12215 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β π β
β) |
57 | | lenlt 11288 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π β β) β (π β€ π β Β¬ π < π)) |
58 | 55, 56, 57 | syl2an 597 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β) β (π β€ π β Β¬ π < π)) |
59 | | elfz1b 13566 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1...π ) β (π β β β§ π β β β§ π β€ π )) |
60 | 59 | biimpri 227 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π β β β§ π β€ π ) β π β (1...π )) |
61 | 60 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β) β (π β€ π β π β (1...π ))) |
62 | 58, 61 | sylbird 260 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β β) β (Β¬
π < π β π β (1...π ))) |
63 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (πβπ) = (πβπ)) |
64 | 63 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ((πβπ) = 0 β (πβπ) = 0)) |
65 | 64 | rspcev 3612 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (1...π ) β§ (πβπ) = 0) β βπ β (1...π )(πβπ) = 0) |
66 | 65 | expcom 415 |
. . . . . . . . . . . . . . . . . 18
β’ ((πβπ) = 0 β (π β (1...π ) β βπ β (1...π )(πβπ) = 0)) |
67 | 62, 66 | sylan9 509 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β) β§ (πβπ) = 0) β (Β¬ π < π β βπ β (1...π )(πβπ) = 0)) |
68 | 67 | an32s 651 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ (πβπ) = 0) β§ π β β) β (Β¬ π < π β βπ β (1...π )(πβπ) = 0)) |
69 | | nne 2945 |
. . . . . . . . . . . . . . . . . 18
β’ (Β¬
(πβπ) β 0 β (πβπ) = 0) |
70 | 69 | rexbii 3095 |
. . . . . . . . . . . . . . . . 17
β’
(βπ β
(1...π ) Β¬ (πβπ) β 0 β βπ β (1...π )(πβπ) = 0) |
71 | | rexnal 3101 |
. . . . . . . . . . . . . . . . 17
β’
(βπ β
(1...π ) Β¬ (πβπ) β 0 β Β¬ βπ β (1...π )(πβπ) β 0) |
72 | 70, 71 | bitr3i 277 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
(1...π )(πβπ) = 0 β Β¬ βπ β (1...π )(πβπ) β 0) |
73 | 68, 72 | syl6ib 251 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ (πβπ) = 0) β§ π β β) β (Β¬ π < π β Β¬ βπ β (1...π )(πβπ) β 0)) |
74 | 73 | con4d 115 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (πβπ) = 0) β§ π β β) β (βπ β (1...π )(πβπ) β 0 β π < π)) |
75 | 54, 74 | sylan2 594 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (πβπ) = 0) β§ π β (1...π)) β (βπ β (1...π )(πβπ) β 0 β π < π)) |
76 | 53, 75 | syl5 34 |
. . . . . . . . . . . 12
β’ (((π β β β§ (πβπ) = 0) β§ π β (1...π)) β (βπ β (1...π )(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β π < π)) |
77 | 76 | ralrimiva 3147 |
. . . . . . . . . . 11
β’ ((π β β β§ (πβπ) = 0) β βπ β (1...π)(βπ β (1...π )(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β π < π)) |
78 | | ralunb 4190 |
. . . . . . . . . . . 12
β’
(βπ β
({0} βͺ {π β
(1...π) β£
βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)})π < π β (βπ β {0}π < π β§ βπ β {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}π < π)) |
79 | | breq1 5150 |
. . . . . . . . . . . . . 14
β’ (π = 0 β (π < π β 0 < π)) |
80 | 29, 79 | ralsn 4684 |
. . . . . . . . . . . . 13
β’
(βπ β
{0}π < π β 0 < π) |
81 | | oveq2 7412 |
. . . . . . . . . . . . . . 15
β’ (π = π β (1...π) = (1...π )) |
82 | 81 | raleqdv 3326 |
. . . . . . . . . . . . . 14
β’ (π = π β (βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β βπ β (1...π )(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0))) |
83 | 82 | ralrab 3688 |
. . . . . . . . . . . . 13
β’
(βπ β
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}π < π β βπ β (1...π)(βπ β (1...π )(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β π < π)) |
84 | 80, 83 | anbi12i 628 |
. . . . . . . . . . . 12
β’
((βπ β
{0}π < π β§ βπ β {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}π < π) β (0 < π β§ βπ β (1...π)(βπ β (1...π )(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β π < π))) |
85 | 78, 84 | bitri 275 |
. . . . . . . . . . 11
β’
(βπ β
({0} βͺ {π β
(1...π) β£
βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)})π < π β (0 < π β§ βπ β (1...π)(βπ β (1...π )(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β π < π))) |
86 | 51, 77, 85 | sylanbrc 584 |
. . . . . . . . . 10
β’ ((π β β β§ (πβπ) = 0) β βπ β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)})π < π) |
87 | | breq1 5150 |
. . . . . . . . . . 11
β’ (π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β (π < π β sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) < π)) |
88 | 87 | rspcva 3610 |
. . . . . . . . . 10
β’
((sup(({0} βͺ {π
β (1...π) β£
βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β ({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β§ βπ β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)})π < π) β sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) < π) |
89 | 45, 86, 88 | sylancr 588 |
. . . . . . . . 9
β’ ((π β β β§ (πβπ) = 0) β sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) < π) |
90 | 49, 89 | sylan 581 |
. . . . . . . 8
β’ ((π β (1...π) β§ (πβπ) = 0) β sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) < π) |
91 | 90 | 3adant2 1132 |
. . . . . . 7
β’ ((π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = 0) β sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) < π) |
92 | 91 | adantl 483 |
. . . . . 6
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = 0)) β sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) < π) |
93 | 37 | zred 12662 |
. . . . . . . . . . 11
β’ (π β (1...π) β π β β) |
94 | 93 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π) β π β β) |
95 | 94 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β π β β) |
96 | | simpr1 1195 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β π β (1...π)) |
97 | | simpll 766 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β π) |
98 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π))) β π β β) |
99 | | elfzelz 13497 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0...π) β π β β€) |
100 | 99 | zred 12662 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0...π) β π β β) |
101 | | nndivre 12249 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§ π β β) β (π / π) β β) |
102 | 100, 101 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0...π) β§ π β β) β (π / π) β β) |
103 | | elfzle1 13500 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0...π) β 0 β€ π) |
104 | 100, 103 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0...π) β (π β β β§ 0 β€ π)) |
105 | | nnrp 12981 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β π β
β+) |
106 | 105 | rpregt0d 13018 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β (π β β β§ 0 <
π)) |
107 | | divge0 12079 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β β β§ 0 β€
π) β§ (π β β β§ 0 <
π)) β 0 β€ (π / π)) |
108 | 104, 106,
107 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0...π) β§ π β β) β 0 β€ (π / π)) |
109 | | elfzle2 13501 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0...π) β π β€ π) |
110 | 109 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0...π) β§ π β β) β π β€ π) |
111 | 100 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0...π) β§ π β β) β π β β) |
112 | | 1red 11211 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0...π) β§ π β β) β 1 β
β) |
113 | 105 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0...π) β§ π β β) β π β β+) |
114 | 111, 112,
113 | ledivmuld 13065 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0...π) β§ π β β) β ((π / π) β€ 1 β π β€ (π Β· 1))) |
115 | | nncn 12216 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β π β
β) |
116 | 115 | mulridd 11227 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β (π Β· 1) = π) |
117 | 116 | breq2d 5159 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β (π β€ (π Β· 1) β π β€ π)) |
118 | 117 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0...π) β§ π β β) β (π β€ (π Β· 1) β π β€ π)) |
119 | 114, 118 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0...π) β§ π β β) β ((π / π) β€ 1 β π β€ π)) |
120 | 110, 119 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0...π) β§ π β β) β (π / π) β€ 1) |
121 | | elicc01 13439 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π / π) β (0[,]1) β ((π / π) β β β§ 0 β€ (π / π) β§ (π / π) β€ 1)) |
122 | 102, 108,
120, 121 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0...π) β§ π β β) β (π / π) β (0[,]1)) |
123 | 122 | ancoms 460 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β (0...π)) β (π / π) β (0[,]1)) |
124 | | elsni 4644 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β {π} β π = π) |
125 | 124 | oveq2d 7420 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β {π} β (π / π) = (π / π)) |
126 | 125 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {π} β ((π / π) β (0[,]1) β (π / π) β (0[,]1))) |
127 | 123, 126 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β (0...π)) β (π β {π} β (π / π) β (0[,]1))) |
128 | 127 | impr 456 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ (π β (0...π) β§ π β {π})) β (π / π) β (0[,]1)) |
129 | 98, 128 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π))) β§ (π β (0...π) β§ π β {π})) β (π / π) β (0[,]1)) |
130 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π))) β π:(1...π)βΆ(0...π)) |
131 | | vex 3479 |
. . . . . . . . . . . . . . . . . 18
β’ π β V |
132 | 131 | fconst 6774 |
. . . . . . . . . . . . . . . . 17
β’
((1...π) Γ
{π}):(1...π)βΆ{π} |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π))) β ((1...π) Γ {π}):(1...π)βΆ{π}) |
134 | | fzfid 13934 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π))) β (1...π) β Fin) |
135 | | inidm 4217 |
. . . . . . . . . . . . . . . 16
β’
((1...π) β©
(1...π)) = (1...π) |
136 | 129, 130,
133, 134, 134, 135 | off 7683 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π))) β (π βf / ((1...π) Γ {π})):(1...π)βΆ(0[,]1)) |
137 | | poimir.i |
. . . . . . . . . . . . . . . . 17
β’ πΌ = ((0[,]1) βm
(1...π)) |
138 | 137 | eleq2i 2826 |
. . . . . . . . . . . . . . . 16
β’ ((π βf /
((1...π) Γ {π})) β πΌ β (π βf / ((1...π) Γ {π})) β ((0[,]1) βm
(1...π))) |
139 | | ovex 7437 |
. . . . . . . . . . . . . . . . 17
β’ (0[,]1)
β V |
140 | | ovex 7437 |
. . . . . . . . . . . . . . . . 17
β’
(1...π) β
V |
141 | 139, 140 | elmap 8861 |
. . . . . . . . . . . . . . . 16
β’ ((π βf /
((1...π) Γ {π})) β ((0[,]1)
βm (1...π))
β (π
βf / ((1...π) Γ {π})):(1...π)βΆ(0[,]1)) |
142 | 138, 141 | bitri 275 |
. . . . . . . . . . . . . . 15
β’ ((π βf /
((1...π) Γ {π})) β πΌ β (π βf / ((1...π) Γ {π})):(1...π)βΆ(0[,]1)) |
143 | 136, 142 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π))) β (π βf / ((1...π) Γ {π})) β πΌ) |
144 | 143 | 3adantr3 1172 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β (π βf / ((1...π) Γ {π})) β πΌ) |
145 | | 3anass 1096 |
. . . . . . . . . . . . . . . 16
β’ ((π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π) β (π β (1...π) β§ (π:(1...π)βΆ(0...π) β§ (πβπ) = π))) |
146 | | ancom 462 |
. . . . . . . . . . . . . . . 16
β’ ((π β (1...π) β§ (π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β ((π:(1...π)βΆ(0...π) β§ (πβπ) = π) β§ π β (1...π))) |
147 | 145, 146 | bitri 275 |
. . . . . . . . . . . . . . 15
β’ ((π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π) β ((π:(1...π)βΆ(0...π) β§ (πβπ) = π) β§ π β (1...π))) |
148 | | ffn 6714 |
. . . . . . . . . . . . . . . . . 18
β’ (π:(1...π)βΆ(0...π) β π Fn (1...π)) |
149 | 148 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ (π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β π Fn (1...π)) |
150 | | fnconstg 6776 |
. . . . . . . . . . . . . . . . . 18
β’ (π β V β ((1...π) Γ {π}) Fn (1...π)) |
151 | 131, 150 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ (π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β ((1...π) Γ {π}) Fn (1...π)) |
152 | | fzfid 13934 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ (π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β (1...π) β Fin) |
153 | | simplrr 777 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β β) β§ (π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β§ π β (1...π)) β (πβπ) = π) |
154 | 131 | fvconst2 7200 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β (((1...π) Γ {π})βπ) = π) |
155 | 154 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β β) β§ (π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β§ π β (1...π)) β (((1...π) Γ {π})βπ) = π) |
156 | 149, 151,
152, 152, 135, 153, 155 | ofval 7676 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β) β§ (π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β§ π β (1...π)) β ((π βf / ((1...π) Γ {π}))βπ) = (π / π)) |
157 | 156 | anasss 468 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ ((π:(1...π)βΆ(0...π) β§ (πβπ) = π) β§ π β (1...π))) β ((π βf / ((1...π) Γ {π}))βπ) = (π / π)) |
158 | 147, 157 | sylan2b 595 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β ((π βf / ((1...π) Γ {π}))βπ) = (π / π)) |
159 | | nnne0 12242 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β 0) |
160 | 115, 159 | dividd 11984 |
. . . . . . . . . . . . . . 15
β’ (π β β β (π / π) = 1) |
161 | 160 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β (π / π) = 1) |
162 | 158, 161 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β ((π βf / ((1...π) Γ {π}))βπ) = 1) |
163 | | ovex 7437 |
. . . . . . . . . . . . . 14
β’ (π βf /
((1...π) Γ {π})) β V |
164 | | eleq1 2822 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = (π βf / ((1...π) Γ {π})) β (π§ β πΌ β (π βf / ((1...π) Γ {π})) β πΌ)) |
165 | | fveq1 6887 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = (π βf / ((1...π) Γ {π})) β (π§βπ) = ((π βf / ((1...π) Γ {π}))βπ)) |
166 | 165 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = (π βf / ((1...π) Γ {π})) β ((π§βπ) = 1 β ((π βf / ((1...π) Γ {π}))βπ) = 1)) |
167 | 164, 166 | 3anbi23d 1440 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (π βf / ((1...π) Γ {π})) β ((π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 1) β (π β (1...π) β§ (π βf / ((1...π) Γ {π})) β πΌ β§ ((π βf / ((1...π) Γ {π}))βπ) = 1))) |
168 | 167 | anbi2d 630 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π βf / ((1...π) Γ {π})) β ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 1)) β (π β§ (π β (1...π) β§ (π βf / ((1...π) Γ {π})) β πΌ β§ ((π βf / ((1...π) Γ {π}))βπ) = 1)))) |
169 | | fveq2 6888 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = (π βf / ((1...π) Γ {π})) β (πΉβπ§) = (πΉβ(π βf / ((1...π) Γ {π})))) |
170 | 169 | fveq1d 6890 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (π βf / ((1...π) Γ {π})) β ((πΉβπ§)βπ) = ((πΉβ(π βf / ((1...π) Γ {π})))βπ)) |
171 | 170 | breq2d 5159 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π βf / ((1...π) Γ {π})) β (0 β€ ((πΉβπ§)βπ) β 0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ))) |
172 | 168, 171 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π§ = (π βf / ((1...π) Γ {π})) β (((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 1)) β 0 β€ ((πΉβπ§)βπ)) β ((π β§ (π β (1...π) β§ (π βf / ((1...π) Γ {π})) β πΌ β§ ((π βf / ((1...π) Γ {π}))βπ) = 1)) β 0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ)))) |
173 | | poimir.3 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 1)) β 0 β€ ((πΉβπ§)βπ)) |
174 | 163, 172,
173 | vtocl 3549 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β (1...π) β§ (π βf / ((1...π) Γ {π})) β πΌ β§ ((π βf / ((1...π) Γ {π}))βπ) = 1)) β 0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ)) |
175 | 97, 96, 144, 162, 174 | syl13anc 1373 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β 0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ)) |
176 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β β) |
177 | | simp3 1139 |
. . . . . . . . . . . . 13
β’ ((π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π) β (πβπ) = π) |
178 | | neeq1 3004 |
. . . . . . . . . . . . . . 15
β’ ((πβπ) = π β ((πβπ) β 0 β π β 0)) |
179 | 159, 178 | syl5ibrcom 246 |
. . . . . . . . . . . . . 14
β’ (π β β β ((πβπ) = π β (πβπ) β 0)) |
180 | 179 | imp 408 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (πβπ) = π) β (πβπ) β 0) |
181 | 176, 177,
180 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β (πβπ) β 0) |
182 | | vex 3479 |
. . . . . . . . . . . . 13
β’ π β V |
183 | | fveq2 6888 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πΉβ(π βf / ((1...π) Γ {π})))βπ) = ((πΉβ(π βf / ((1...π) Γ {π})))βπ)) |
184 | 183 | breq2d 5159 |
. . . . . . . . . . . . . 14
β’ (π = π β (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β 0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ))) |
185 | 63 | neeq1d 3001 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πβπ) β 0 β (πβπ) β 0)) |
186 | 184, 185 | anbi12d 632 |
. . . . . . . . . . . . 13
β’ (π = π β ((0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0))) |
187 | 182, 186 | ralsn 4684 |
. . . . . . . . . . . 12
β’
(βπ β
{π} (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)) |
188 | 175, 181,
187 | sylanbrc 584 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β βπ β {π} (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)) |
189 | 37 | zcnd 12663 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β π β β) |
190 | | 1cnd 11205 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β 1 β β) |
191 | 189, 190 | subeq0ad 11577 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β ((π β 1) = 0 β π = 1)) |
192 | 191 | biimpcd 248 |
. . . . . . . . . . . . . . . . 17
β’ ((π β 1) = 0 β (π β (1...π) β π = 1)) |
193 | | 1z 12588 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 1 β
β€ |
194 | | fzsn 13539 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (1 β
β€ β (1...1) = {1}) |
195 | 193, 194 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’ (1...1) =
{1} |
196 | | oveq2 7412 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 1 β (1...π) = (1...1)) |
197 | | sneq 4637 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 1 β {π} = {1}) |
198 | 195, 196,
197 | 3eqtr4a 2799 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 1 β (1...π) = {π}) |
199 | 198 | raleqdv 3326 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 1 β (βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β βπ β {π} (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0))) |
200 | 199 | biimprd 247 |
. . . . . . . . . . . . . . . . 17
β’ (π = 1 β (βπ β {π} (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0))) |
201 | 192, 200 | syl6 35 |
. . . . . . . . . . . . . . . 16
β’ ((π β 1) = 0 β (π β (1...π) β (βπ β {π} (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)))) |
202 | | ralun 4191 |
. . . . . . . . . . . . . . . . . . . 20
β’
((βπ β
(1...(π β 1))(0 β€
((πΉβ(π βf /
((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β§ βπ β {π} (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)) β βπ β ((1...(π β 1)) βͺ {π})(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)) |
203 | | npcan1 11635 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β ((π β 1) + 1) = π) |
204 | 189, 203 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (1...π) β ((π β 1) + 1) = π) |
205 | | elfzuz 13493 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (1...π) β π β
(β€β₯β1)) |
206 | 204, 205 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (1...π) β ((π β 1) + 1) β
(β€β₯β1)) |
207 | | peano2zm 12601 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β€ β (π β 1) β
β€) |
208 | | uzid 12833 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β 1) β β€
β (π β 1) β
(β€β₯β(π β 1))) |
209 | | peano2uz 12881 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β 1) β
(β€β₯β(π β 1)) β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
210 | 37, 207, 208, 209 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (1...π) β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
211 | 204, 210 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (1...π) β π β (β€β₯β(π β 1))) |
212 | | fzsplit2 13522 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β 1) + 1) β
(β€β₯β1) β§ π β (β€β₯β(π β 1))) β (1...π) = ((1...(π β 1)) βͺ (((π β 1) + 1)...π))) |
213 | 206, 211,
212 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (1...π) β (1...π) = ((1...(π β 1)) βͺ (((π β 1) + 1)...π))) |
214 | 204 | oveq1d 7419 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (1...π) β (((π β 1) + 1)...π) = (π...π)) |
215 | | fzsn 13539 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β€ β (π...π) = {π}) |
216 | 37, 215 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (1...π) β (π...π) = {π}) |
217 | 214, 216 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (1...π) β (((π β 1) + 1)...π) = {π}) |
218 | 217 | uneq2d 4162 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (1...π) β ((1...(π β 1)) βͺ (((π β 1) + 1)...π)) = ((1...(π β 1)) βͺ {π})) |
219 | 213, 218 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1...π) β (1...π) = ((1...(π β 1)) βͺ {π})) |
220 | 219 | raleqdv 3326 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...π) β (βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β βπ β ((1...(π β 1)) βͺ {π})(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0))) |
221 | 202, 220 | imbitrrid 245 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β ((βπ β (1...(π β 1))(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β§ βπ β {π} (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)) β βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0))) |
222 | 221 | expd 417 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...π) β (βπ β (1...(π β 1))(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β (βπ β {π} (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)))) |
223 | 222 | com12 32 |
. . . . . . . . . . . . . . . . 17
β’
(βπ β
(1...(π β 1))(0 β€
((πΉβ(π βf /
((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β (π β (1...π) β (βπ β {π} (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)))) |
224 | 223 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β 1) β (1...π) β§ βπ β (1...(π β 1))(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)) β (π β (1...π) β (βπ β {π} (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)))) |
225 | 201, 224 | jaoi 856 |
. . . . . . . . . . . . . . 15
β’ (((π β 1) = 0 β¨ ((π β 1) β (1...π) β§ βπ β (1...(π β 1))(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0))) β (π β (1...π) β (βπ β {π} (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)))) |
226 | 225 | imdistand 572 |
. . . . . . . . . . . . . 14
β’ (((π β 1) = 0 β¨ ((π β 1) β (1...π) β§ βπ β (1...(π β 1))(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0))) β ((π β (1...π) β§ βπ β {π} (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)) β (π β (1...π) β§ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)))) |
227 | 226 | com12 32 |
. . . . . . . . . . . . 13
β’ ((π β (1...π) β§ βπ β {π} (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)) β (((π β 1) = 0 β¨ ((π β 1) β (1...π) β§ βπ β (1...(π β 1))(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0))) β (π β (1...π) β§ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)))) |
228 | | elun 4147 |
. . . . . . . . . . . . . 14
β’ ((π β 1) β ({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β ((π β 1) β {0} β¨ (π β 1) β {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)})) |
229 | | ovex 7437 |
. . . . . . . . . . . . . . . 16
β’ (π β 1) β
V |
230 | 229 | elsn 4642 |
. . . . . . . . . . . . . . 15
β’ ((π β 1) β {0} β
(π β 1) =
0) |
231 | | oveq2 7412 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π β 1) β (1...π) = (1...(π β 1))) |
232 | 231 | raleqdv 3326 |
. . . . . . . . . . . . . . . 16
β’ (π = (π β 1) β (βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β βπ β (1...(π β 1))(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0))) |
233 | 232 | elrab 3682 |
. . . . . . . . . . . . . . 15
β’ ((π β 1) β {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)} β ((π β 1) β (1...π) β§ βπ β (1...(π β 1))(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0))) |
234 | 230, 233 | orbi12i 914 |
. . . . . . . . . . . . . 14
β’ (((π β 1) β {0} β¨
(π β 1) β {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β ((π β 1) = 0 β¨ ((π β 1) β (1...π) β§ βπ β (1...(π β 1))(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)))) |
235 | 228, 234 | bitri 275 |
. . . . . . . . . . . . 13
β’ ((π β 1) β ({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β ((π β 1) = 0 β¨ ((π β 1) β (1...π) β§ βπ β (1...(π β 1))(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)))) |
236 | | oveq2 7412 |
. . . . . . . . . . . . . . 15
β’ (π = π β (1...π) = (1...π)) |
237 | 236 | raleqdv 3326 |
. . . . . . . . . . . . . 14
β’ (π = π β (βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0) β βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0))) |
238 | 237 | elrab 3682 |
. . . . . . . . . . . . 13
β’ (π β {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)} β (π β (1...π) β§ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0))) |
239 | 227, 235,
238 | 3imtr4g 296 |
. . . . . . . . . . . 12
β’ ((π β (1...π) β§ βπ β {π} (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)) β ((π β 1) β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β π β {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)})) |
240 | | elun2 4176 |
. . . . . . . . . . . 12
β’ (π β {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)} β π β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)})) |
241 | 239, 240 | syl6 35 |
. . . . . . . . . . 11
β’ ((π β (1...π) β§ βπ β {π} (0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)) β ((π β 1) β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β π β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}))) |
242 | 96, 188, 241 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β ((π β 1) β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β π β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}))) |
243 | | fimaxre2 12155 |
. . . . . . . . . . . . 13
β’ ((({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β β β§ ({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β Fin) β βπ β β βπ β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)})π β€ π) |
244 | 42, 28, 243 | mp2an 691 |
. . . . . . . . . . . 12
β’
βπ β
β βπ β
({0} βͺ {π β
(1...π) β£
βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)})π β€ π |
245 | 42, 33, 244 | 3pm3.2i 1340 |
. . . . . . . . . . 11
β’ (({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β β β§ ({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β β
β§ βπ β β βπ β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)})π β€ π) |
246 | 245 | suprubii 12185 |
. . . . . . . . . 10
β’ (π β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β π β€ sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, <
)) |
247 | 242, 246 | syl6 35 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β ((π β 1) β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β π β€ sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, <
))) |
248 | | ltm1 12052 |
. . . . . . . . . 10
β’ (π β β β (π β 1) < π) |
249 | | peano2rem 11523 |
. . . . . . . . . . 11
β’ (π β β β (π β 1) β
β) |
250 | 42, 45 | sselii 3978 |
. . . . . . . . . . . 12
β’ sup(({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β
β |
251 | | ltletr 11302 |
. . . . . . . . . . . 12
β’ (((π β 1) β β β§
π β β β§
sup(({0} βͺ {π β
(1...π) β£
βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β β)
β (((π β 1) <
π β§ π β€ sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < )) β (π β 1) < sup(({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, <
))) |
252 | 250, 251 | mp3an3 1451 |
. . . . . . . . . . 11
β’ (((π β 1) β β β§
π β β) β
(((π β 1) < π β§ π β€ sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < )) β (π β 1) < sup(({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, <
))) |
253 | 249, 252 | mpancom 687 |
. . . . . . . . . 10
β’ (π β β β (((π β 1) < π β§ π β€ sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < )) β (π β 1) < sup(({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, <
))) |
254 | 248, 253 | mpand 694 |
. . . . . . . . 9
β’ (π β β β (π β€ sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β (π β 1) < sup(({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, <
))) |
255 | 95, 247, 254 | sylsyld 61 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β ((π β 1) β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β (π β 1) < sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, <
))) |
256 | 250 | ltnri 11319 |
. . . . . . . . . 10
β’ Β¬
sup(({0} βͺ {π β
(1...π) β£
βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) < sup(({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) |
257 | | breq1 5150 |
. . . . . . . . . 10
β’ (sup(({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) = (π β 1) β (sup(({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) < sup(({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β (π β 1) < sup(({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, <
))) |
258 | 256, 257 | mtbii 326 |
. . . . . . . . 9
β’ (sup(({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) = (π β 1) β Β¬ (π β 1) < sup(({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, <
)) |
259 | 258 | necon2ai 2971 |
. . . . . . . 8
β’ ((π β 1) < sup(({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β sup(({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β (π β 1)) |
260 | 255, 259 | syl6 35 |
. . . . . . 7
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β ((π β 1) β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β (π β 1))) |
261 | | eleq1 2822 |
. . . . . . . . 9
β’ (sup(({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) = (π β 1) β (sup(({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β ({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β (π β 1) β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}))) |
262 | 45, 261 | mpbii 232 |
. . . . . . . 8
β’ (sup(({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) = (π β 1) β (π β 1) β ({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)})) |
263 | 262 | necon3bi 2968 |
. . . . . . 7
β’ (Β¬
(π β 1) β ({0}
βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}) β sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β (π β 1)) |
264 | 260, 263 | pm2.61d1 180 |
. . . . . 6
β’ (((π β§ π β β) β§ (π β (1...π) β§ π:(1...π)βΆ(0...π) β§ (πβπ) = π)) β sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(π βf / ((1...π) Γ {π})))βπ) β§ (πβπ) β 0)}), β, < ) β (π β 1)) |
265 | 2, 12, 48, 92, 264, 176 | poimirlem28 36454 |
. . . . 5
β’ ((π β§ π β β) β βπ β (((0..^π) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
)) |
266 | | nn0ex 12474 |
. . . . . . . . . . . 12
β’
β0 β V |
267 | | fzo0ssnn0 13709 |
. . . . . . . . . . . 12
β’
(0..^π) β
β0 |
268 | | mapss 8879 |
. . . . . . . . . . . 12
β’
((β0 β V β§ (0..^π) β β0) β
((0..^π) βm
(1...π)) β
(β0 βm (1...π))) |
269 | 266, 267,
268 | mp2an 691 |
. . . . . . . . . . 11
β’
((0..^π)
βm (1...π))
β (β0 βm (1...π)) |
270 | | xpss1 5694 |
. . . . . . . . . . 11
β’
(((0..^π)
βm (1...π))
β (β0 βm (1...π)) β (((0..^π) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
271 | 269, 270 | ax-mp 5 |
. . . . . . . . . 10
β’
(((0..^π)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
272 | 271 | sseli 3977 |
. . . . . . . . 9
β’ (π β (((0..^π) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β π β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
273 | | xp1st 8002 |
. . . . . . . . . 10
β’ (π β (((0..^π) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β (1st βπ ) β ((0..^π) βm (1...π))) |
274 | | elmapi 8839 |
. . . . . . . . . 10
β’
((1st βπ ) β ((0..^π) βm (1...π)) β (1st βπ ):(1...π)βΆ(0..^π)) |
275 | | frn 6721 |
. . . . . . . . . 10
β’
((1st βπ ):(1...π)βΆ(0..^π) β ran (1st βπ ) β (0..^π)) |
276 | 273, 274,
275 | 3syl 18 |
. . . . . . . . 9
β’ (π β (((0..^π) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β ran (1st βπ ) β (0..^π)) |
277 | 272, 276 | jca 513 |
. . . . . . . 8
β’ (π β (((0..^π) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β (π β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β§ ran (1st βπ ) β (0..^π))) |
278 | 277 | anim1i 616 |
. . . . . . 7
β’ ((π β (((0..^π) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < )) β ((π β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β§ ran (1st βπ ) β (0..^π)) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
))) |
279 | | anass 470 |
. . . . . . 7
β’ (((π β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β§ ran (1st βπ ) β (0..^π)) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < )) β (π β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β§ (ran (1st βπ ) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
)))) |
280 | 278, 279 | sylib 217 |
. . . . . 6
β’ ((π β (((0..^π) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < )) β (π β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β§ (ran (1st βπ ) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
)))) |
281 | 280 | reximi2 3080 |
. . . . 5
β’
(βπ β
(((0..^π)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ) β
βπ β
((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})(ran (1st βπ ) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
))) |
282 | 265, 281 | syl 17 |
. . . 4
β’ ((π β§ π β β) β βπ β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})(ran (1st βπ ) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
))) |
283 | 282 | ralrimiva 3147 |
. . 3
β’ (π β βπ β β βπ β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})(ran (1st βπ ) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
))) |
284 | | nnex 12214 |
. . . 4
β’ β
β V |
285 | 140, 266 | ixpconst 8897 |
. . . . . . 7
β’ Xπ β
(1...π)β0
= (β0 βm (1...π)) |
286 | | omelon 9637 |
. . . . . . . . . 10
β’ Ο
β On |
287 | | nn0ennn 13940 |
. . . . . . . . . . 11
β’
β0 β β |
288 | | nnenom 13941 |
. . . . . . . . . . 11
β’ β
β Ο |
289 | 287, 288 | entr2i 9001 |
. . . . . . . . . 10
β’ Ο
β β0 |
290 | | isnumi 9937 |
. . . . . . . . . 10
β’ ((Ο
β On β§ Ο β β0) β β0
β dom card) |
291 | 286, 289,
290 | mp2an 691 |
. . . . . . . . 9
β’
β0 β dom card |
292 | 291 | rgenw 3066 |
. . . . . . . 8
β’
βπ β
(1...π)β0
β dom card |
293 | | finixpnum 36411 |
. . . . . . . 8
β’
(((1...π) β Fin
β§ βπ β
(1...π)β0
β dom card) β Xπ β (1...π)β0 β dom
card) |
294 | 24, 292, 293 | mp2an 691 |
. . . . . . 7
β’ Xπ β
(1...π)β0
β dom card |
295 | 285, 294 | eqeltrri 2831 |
. . . . . 6
β’
(β0 βm (1...π)) β dom card |
296 | 140, 140 | mapval 8828 |
. . . . . . . . 9
β’
((1...π)
βm (1...π))
= {π β£ π:(1...π)βΆ(1...π)} |
297 | | mapfi 9344 |
. . . . . . . . . 10
β’
(((1...π) β Fin
β§ (1...π) β Fin)
β ((1...π)
βm (1...π))
β Fin) |
298 | 24, 24, 297 | mp2an 691 |
. . . . . . . . 9
β’
((1...π)
βm (1...π))
β Fin |
299 | 296, 298 | eqeltrri 2831 |
. . . . . . . 8
β’ {π β£ π:(1...π)βΆ(1...π)} β Fin |
300 | | f1of 6830 |
. . . . . . . . 9
β’ (π:(1...π)β1-1-ontoβ(1...π) β π:(1...π)βΆ(1...π)) |
301 | 300 | ss2abi 4062 |
. . . . . . . 8
β’ {π β£ π:(1...π)β1-1-ontoβ(1...π)} β {π β£ π:(1...π)βΆ(1...π)} |
302 | | ssfi 9169 |
. . . . . . . 8
β’ (({π β£ π:(1...π)βΆ(1...π)} β Fin β§ {π β£ π:(1...π)β1-1-ontoβ(1...π)} β {π β£ π:(1...π)βΆ(1...π)}) β {π β£ π:(1...π)β1-1-ontoβ(1...π)} β Fin) |
303 | 299, 301,
302 | mp2an 691 |
. . . . . . 7
β’ {π β£ π:(1...π)β1-1-ontoβ(1...π)} β Fin |
304 | | finnum 9939 |
. . . . . . 7
β’ ({π β£ π:(1...π)β1-1-ontoβ(1...π)} β Fin β {π β£ π:(1...π)β1-1-ontoβ(1...π)} β dom card) |
305 | 303, 304 | ax-mp 5 |
. . . . . 6
β’ {π β£ π:(1...π)β1-1-ontoβ(1...π)} β dom card |
306 | | xpnum 9942 |
. . . . . 6
β’
(((β0 βm (1...π)) β dom card β§ {π β£ π:(1...π)β1-1-ontoβ(1...π)} β dom card) β
((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β dom card) |
307 | 295, 305,
306 | mp2an 691 |
. . . . 5
β’
((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β dom card |
308 | | ssrab2 4076 |
. . . . . . . 8
β’ {π β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ (ran (1st
βπ ) β
(0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))} β
((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
309 | 308 | rgenw 3066 |
. . . . . . 7
β’
βπ β
β {π β
((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ (ran (1st
βπ ) β
(0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))} β
((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
310 | | ss2iun 5014 |
. . . . . . 7
β’
(βπ β
β {π β
((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ (ran (1st
βπ ) β
(0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))} β
((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β βͺ π β β {π β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ (ran (1st
βπ ) β
(0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))} β
βͺ π β β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
311 | 309, 310 | ax-mp 5 |
. . . . . 6
β’ βͺ π β β {π β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ (ran (1st
βπ ) β
(0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))} β
βͺ π β β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
312 | | 1nn 12219 |
. . . . . . 7
β’ 1 β
β |
313 | | ne0i 4333 |
. . . . . . 7
β’ (1 β
β β β β β
) |
314 | | iunconst 5005 |
. . . . . . 7
β’ (β
β β
β βͺ π β β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) = ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
315 | 312, 313,
314 | mp2b 10 |
. . . . . 6
β’ βͺ π β β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) = ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
316 | 311, 315 | sseqtri 4017 |
. . . . 5
β’ βͺ π β β {π β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ (ran (1st
βπ ) β
(0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))} β
((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
317 | | ssnum 10030 |
. . . . 5
β’
((((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β dom card β§ βͺ π β β {π β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ (ran (1st
βπ ) β
(0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))} β
((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) β βͺ π β β {π β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ (ran (1st
βπ ) β
(0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))} β dom
card) |
318 | 307, 316,
317 | mp2an 691 |
. . . 4
β’ βͺ π β β {π β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ (ran (1st
βπ ) β
(0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))} β dom
card |
319 | | fveq2 6888 |
. . . . . . . 8
β’ (π = (πβπ) β (1st βπ ) = (1st
β(πβπ))) |
320 | 319 | rneqd 5935 |
. . . . . . 7
β’ (π = (πβπ) β ran (1st βπ ) = ran (1st
β(πβπ))) |
321 | 320 | sseq1d 4012 |
. . . . . 6
β’ (π = (πβπ) β (ran (1st βπ ) β (0..^π) β ran (1st
β(πβπ)) β (0..^π))) |
322 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (πβπ) β (2nd βπ ) = (2nd
β(πβπ))) |
323 | 322 | imaeq1d 6056 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (πβπ) β ((2nd βπ ) β (1...π)) = ((2nd
β(πβπ)) β (1...π))) |
324 | 323 | xpeq1d 5704 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πβπ) β (((2nd βπ ) β (1...π)) Γ {1}) =
(((2nd β(πβπ)) β (1...π)) Γ {1})) |
325 | 322 | imaeq1d 6056 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (πβπ) β ((2nd βπ ) β ((π + 1)...π)) = ((2nd β(πβπ)) β ((π + 1)...π))) |
326 | 325 | xpeq1d 5704 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πβπ) β (((2nd βπ ) β ((π + 1)...π)) Γ {0}) = (((2nd
β(πβπ)) β ((π + 1)...π)) Γ {0})) |
327 | 324, 326 | uneq12d 4163 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβπ) β ((((2nd βπ ) β (1...π)) Γ {1}) βͺ
(((2nd βπ )
β ((π + 1)...π)) Γ {0})) =
((((2nd β(πβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πβπ)) β ((π + 1)...π)) Γ {0}))) |
328 | 319, 327 | oveq12d 7422 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβπ) β ((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) = ((1st
β(πβπ)) βf +
((((2nd β(πβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πβπ)) β ((π + 1)...π)) Γ {0})))) |
329 | 328 | fvoveq1d 7426 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β (πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))) = (πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))) |
330 | 329 | fveq1d 6890 |
. . . . . . . . . . . . . . 15
β’ (π = (πβπ) β ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) = ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ)) |
331 | 330 | breq2d 5159 |
. . . . . . . . . . . . . 14
β’ (π = (πβπ) β (0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β 0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ))) |
332 | 328 | fveq1d 6890 |
. . . . . . . . . . . . . . 15
β’ (π = (πβπ) β (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) = (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ)) |
333 | 332 | neeq1d 3001 |
. . . . . . . . . . . . . 14
β’ (π = (πβπ) β ((((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0 β (((1st
β(πβπ)) βf +
((((2nd β(πβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)) |
334 | 331, 333 | anbi12d 632 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β ((0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0) β (0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0))) |
335 | 334 | ralbidv 3178 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β (βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0) β βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0))) |
336 | 335 | rabbidv 3441 |
. . . . . . . . . . 11
β’ (π = (πβπ) β {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)} = {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}) |
337 | 336 | uneq2d 4162 |
. . . . . . . . . 10
β’ (π = (πβπ) β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}) = ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)})) |
338 | 337 | supeq1d 9437 |
. . . . . . . . 9
β’ (π = (πβπ) β sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ) = sup(({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
)) |
339 | 338 | eqeq2d 2744 |
. . . . . . . 8
β’ (π = (πβπ) β (π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ) β π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
))) |
340 | 339 | rexbidv 3179 |
. . . . . . 7
β’ (π = (πβπ) β (βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ) β
βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
))) |
341 | 340 | ralbidv 3178 |
. . . . . 6
β’ (π = (πβπ) β (βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ) β
βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
))) |
342 | 321, 341 | anbi12d 632 |
. . . . 5
β’ (π = (πβπ) β ((ran (1st βπ ) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < )) β (ran
(1st β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
)))) |
343 | 342 | ac6num 10470 |
. . . 4
β’ ((β
β V β§ βͺ π β β {π β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β£ (ran (1st
βπ ) β
(0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))} β dom
card β§ βπ β
β βπ β
((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})(ran (1st βπ ) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))) β
βπ(π:ββΆ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β§ βπ β β (ran (1st
β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
)))) |
344 | 284, 318,
343 | mp3an12 1452 |
. . 3
β’
(βπ β
β βπ β
((β0 βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})(ran (1st βπ ) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st βπ ) βf +
((((2nd βπ ) β (1...π)) Γ {1}) βͺ (((2nd
βπ ) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < )) β
βπ(π:ββΆ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β§ βπ β β (ran (1st
β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
)))) |
345 | 283, 344 | syl 17 |
. 2
β’ (π β βπ(π:ββΆ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β§ βπ β β (ran (1st
β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
)))) |
346 | 1 | ad2antrr 725 |
. . . 4
β’ (((π β§ π:ββΆ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) β§ βπ β β (ran (1st
β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))) β π β
β) |
347 | | poimir.r |
. . . 4
β’ π
=
(βtβ((1...π) Γ {(topGenβran
(,))})) |
348 | | poimir.1 |
. . . . 5
β’ (π β πΉ β ((π
βΎt πΌ) Cn π
)) |
349 | 348 | ad2antrr 725 |
. . . 4
β’ (((π β§ π:ββΆ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) β§ βπ β β (ran (1st
β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))) β πΉ β ((π
βΎt πΌ) Cn π
)) |
350 | | eqid 2733 |
. . . 4
β’ ((πΉβ(((1st
β(πβπ)) βf +
((((2nd β(πβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) = ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) |
351 | | simplr 768 |
. . . 4
β’ (((π β§ π:ββΆ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) β§ βπ β β (ran (1st
β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))) β π:ββΆ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
352 | | simpl 484 |
. . . . . . 7
β’ ((ran
(1st β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < )) β ran
(1st β(πβπ)) β (0..^π)) |
353 | 352 | ralimi 3084 |
. . . . . 6
β’
(βπ β
β (ran (1st β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < )) β
βπ β β
ran (1st β(πβπ)) β (0..^π)) |
354 | 353 | adantl 483 |
. . . . 5
β’ (((π β§ π:ββΆ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) β§ βπ β β (ran (1st
β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))) β
βπ β β
ran (1st β(πβπ)) β (0..^π)) |
355 | | 2fveq3 6893 |
. . . . . . . 8
β’ (π = π β (1st β(πβπ)) = (1st β(πβπ))) |
356 | 355 | rneqd 5935 |
. . . . . . 7
β’ (π = π β ran (1st β(πβπ)) = ran (1st β(πβπ))) |
357 | | oveq2 7412 |
. . . . . . 7
β’ (π = π β (0..^π) = (0..^π)) |
358 | 356, 357 | sseq12d 4014 |
. . . . . 6
β’ (π = π β (ran (1st β(πβπ)) β (0..^π) β ran (1st β(πβπ)) β (0..^π))) |
359 | 358 | rspccva 3611 |
. . . . 5
β’
((βπ β
β ran (1st β(πβπ)) β (0..^π) β§ π β β) β ran (1st
β(πβπ)) β (0..^π)) |
360 | 354, 359 | sylan 581 |
. . . 4
β’ ((((π β§ π:ββΆ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) β§ βπ β β (ran (1st
β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))) β§ π β β) β ran
(1st β(πβπ)) β (0..^π)) |
361 | | simpll 766 |
. . . . . 6
β’ (((π β§ π:ββΆ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) β§ βπ β β (ran (1st
β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))) β π) |
362 | | poimir.2 |
. . . . . 6
β’ ((π β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 0)) β ((πΉβπ§)βπ) β€ 0) |
363 | 361, 362 | sylan 581 |
. . . . 5
β’ ((((π β§ π:ββΆ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) β§ βπ β β (ran (1st
β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))) β§ (π β (1...π) β§ π§ β πΌ β§ (π§βπ) = 0)) β ((πΉβπ§)βπ) β€ 0) |
364 | | eqid 2733 |
. . . . 5
β’
((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) = ((1st
β(πβπ)) βf +
((((2nd β(πβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πβπ)) β ((π + 1)...π)) Γ {0}))) |
365 | | simpr 486 |
. . . . . . . 8
β’ ((ran
(1st β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < )) β
βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
)) |
366 | 365 | ralimi 3084 |
. . . . . . 7
β’
(βπ β
β (ran (1st β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < )) β
βπ β β
βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
)) |
367 | 366 | adantl 483 |
. . . . . 6
β’ (((π β§ π:ββΆ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) β§ βπ β β (ran (1st
β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))) β
βπ β β
βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
)) |
368 | | 2fveq3 6893 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (2nd β(πβπ)) = (2nd β(πβπ))) |
369 | 368 | imaeq1d 6056 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((2nd β(πβπ)) β (1...π)) = ((2nd β(πβπ)) β (1...π))) |
370 | 369 | xpeq1d 5704 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (((2nd β(πβπ)) β (1...π)) Γ {1}) = (((2nd
β(πβπ)) β (1...π)) Γ
{1})) |
371 | 368 | imaeq1d 6056 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((2nd β(πβπ)) β ((π + 1)...π)) = ((2nd β(πβπ)) β ((π + 1)...π))) |
372 | 371 | xpeq1d 5704 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}) = (((2nd
β(πβπ)) β ((π + 1)...π)) Γ {0})) |
373 | 370, 372 | uneq12d 4163 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((((2nd β(πβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πβπ)) β ((π + 1)...π)) Γ {0})) = ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) |
374 | 355, 373 | oveq12d 7422 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) = ((1st
β(πβπ)) βf +
((((2nd β(πβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πβπ)) β ((π + 1)...π)) Γ {0})))) |
375 | | sneq 4637 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β {π} = {π}) |
376 | 375 | xpeq2d 5705 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((1...π) Γ {π}) = ((1...π) Γ {π})) |
377 | 374, 376 | oveq12d 7422 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) = (((1st
β(πβπ)) βf +
((((2nd β(πβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))) |
378 | 377 | fveq2d 6892 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))) = (πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))) |
379 | 378 | fveq1d 6890 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) = ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ)) |
380 | 379 | breq2d 5159 |
. . . . . . . . . . . . . 14
β’ (π = π β (0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β 0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ))) |
381 | 374 | fveq1d 6890 |
. . . . . . . . . . . . . . 15
β’ (π = π β (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) = (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ)) |
382 | 381 | neeq1d 3001 |
. . . . . . . . . . . . . 14
β’ (π = π β ((((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0 β (((1st
β(πβπ)) βf +
((((2nd β(πβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)) |
383 | 380, 382 | anbi12d 632 |
. . . . . . . . . . . . 13
β’ (π = π β ((0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0) β (0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0))) |
384 | 383 | ralbidv 3178 |
. . . . . . . . . . . 12
β’ (π = π β (βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0) β βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0))) |
385 | 384 | rabbidv 3441 |
. . . . . . . . . . 11
β’ (π = π β {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)} = {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}) |
386 | 385 | uneq2d 4162 |
. . . . . . . . . 10
β’ (π = π β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}) = ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)})) |
387 | 386 | supeq1d 9437 |
. . . . . . . . 9
β’ (π = π β sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ) = sup(({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
)) |
388 | 387 | eqeq2d 2744 |
. . . . . . . 8
β’ (π = π β (π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ) β π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
))) |
389 | 388 | rexbidv 3179 |
. . . . . . 7
β’ (π = π β (βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ) β
βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
))) |
390 | | eqeq1 2737 |
. . . . . . . . 9
β’ (π = π β (π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ) β π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
))) |
391 | 390 | rexbidv 3179 |
. . . . . . . 8
β’ (π = π β (βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ) β
βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
))) |
392 | | oveq2 7412 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (1...π) = (1...π)) |
393 | 392 | imaeq2d 6057 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((2nd β(πβπ)) β (1...π)) = ((2nd β(πβπ)) β (1...π))) |
394 | 393 | xpeq1d 5704 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (((2nd β(πβπ)) β (1...π)) Γ {1}) = (((2nd
β(πβπ)) β (1...π)) Γ
{1})) |
395 | | oveq1 7411 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (π + 1) = (π + 1)) |
396 | 395 | oveq1d 7419 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β ((π + 1)...π) = ((π + 1)...π)) |
397 | 396 | imaeq2d 6057 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((2nd β(πβπ)) β ((π + 1)...π)) = ((2nd β(πβπ)) β ((π + 1)...π))) |
398 | 397 | xpeq1d 5704 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}) = (((2nd
β(πβπ)) β ((π + 1)...π)) Γ {0})) |
399 | 394, 398 | uneq12d 4163 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((((2nd β(πβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πβπ)) β ((π + 1)...π)) Γ {0})) = ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) |
400 | 399 | oveq2d 7420 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) = ((1st
β(πβπ)) βf +
((((2nd β(πβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πβπ)) β ((π + 1)...π)) Γ {0})))) |
401 | 400 | fvoveq1d 7426 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))) = (πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))) |
402 | 401 | fveq1d 6890 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) = ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ)) |
403 | 402 | breq2d 5159 |
. . . . . . . . . . . . . . 15
β’ (π = π β (0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β 0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ))) |
404 | 400 | fveq1d 6890 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) = (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ)) |
405 | 404 | neeq1d 3001 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0 β (((1st
β(πβπ)) βf +
((((2nd β(πβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)) |
406 | 403, 405 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ (π = π β ((0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0) β (0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0))) |
407 | 406 | ralbidv 3178 |
. . . . . . . . . . . . 13
β’ (π = π β (βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0) β βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0))) |
408 | 407 | rabbidv 3441 |
. . . . . . . . . . . 12
β’ (π = π β {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)} = {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}) |
409 | 408 | uneq2d 4162 |
. . . . . . . . . . 11
β’ (π = π β ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}) = ({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)})) |
410 | 409 | supeq1d 9437 |
. . . . . . . . . 10
β’ (π = π β sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ) = sup(({0} βͺ
{π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
)) |
411 | 410 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π = π β (π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ) β π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
))) |
412 | 411 | cbvrexvw 3236 |
. . . . . . . 8
β’
(βπ β
(0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ) β
βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
)) |
413 | 391, 412 | bitrdi 287 |
. . . . . . 7
β’ (π = π β (βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ) β
βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
))) |
414 | 389, 413 | rspc2v 3621 |
. . . . . 6
β’ ((π β β β§ π β (0...π)) β (βπ β β βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ) β
βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
))) |
415 | 367, 414 | mpan9 508 |
. . . . 5
β’ ((((π β§ π:ββΆ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) β§ βπ β β (ran (1st
β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))) β§ (π β β β§ π β (0...π))) β βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, <
)) |
416 | 346, 137,
347, 349, 363, 364, 351, 360, 415 | poimirlem31 36457 |
. . . 4
β’ ((((π β§ π:ββΆ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) β§ βπ β β (ran (1st
β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))) β§ (π β β β§ π β (1...π) β§ π β { β€ , β‘ β€ })) β βπ β (0...π)0π((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ)) |
417 | 346, 137,
347, 349, 350, 351, 360, 416 | poimirlem30 36456 |
. . 3
β’ (((π β§ π:ββΆ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) β§ βπ β β (ran (1st
β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < ))) β
βπ β πΌ βπ β (1...π)βπ£ β (π
βΎt πΌ)(π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
418 | 417 | anasss 468 |
. 2
β’ ((π β§ (π:ββΆ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β§ βπ β β (ran (1st
β(πβπ)) β (0..^π) β§ βπ β (0...π)βπ β (0...π)π = sup(({0} βͺ {π β (1...π) β£ βπ β (1...π)(0 β€ ((πΉβ(((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) β§ (((1st β(πβπ)) βf + ((((2nd
β(πβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πβπ)) β ((π + 1)...π)) Γ {0})))βπ) β 0)}), β, < )))) β
βπ β πΌ βπ β (1...π)βπ£ β (π
βΎt πΌ)(π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
419 | 345, 418 | exlimddv 1939 |
1
β’ (π β βπ β πΌ βπ β (1...π)βπ£ β (π
βΎt πΌ)(π β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |