Step | Hyp | Ref
| Expression |
1 | | jensen.7 |
. . . . . 6
β’ (π β 0 <
(βfld Ξ£g π)) |
2 | | jensen.5 |
. . . . . . . . 9
β’ (π β π:π΄βΆ(0[,)+β)) |
3 | 2 | ffnd 6674 |
. . . . . . . 8
β’ (π β π Fn π΄) |
4 | | fnresdm 6625 |
. . . . . . . 8
β’ (π Fn π΄ β (π βΎ π΄) = π) |
5 | 3, 4 | syl 17 |
. . . . . . 7
β’ (π β (π βΎ π΄) = π) |
6 | 5 | oveq2d 7378 |
. . . . . 6
β’ (π β (βfld
Ξ£g (π βΎ π΄)) = (βfld
Ξ£g π)) |
7 | 1, 6 | breqtrrd 5138 |
. . . . 5
β’ (π β 0 <
(βfld Ξ£g (π βΎ π΄))) |
8 | | ssid 3971 |
. . . . 5
β’ π΄ β π΄ |
9 | 7, 8 | jctil 521 |
. . . 4
β’ (π β (π΄ β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π΄)))) |
10 | | jensen.4 |
. . . . 5
β’ (π β π΄ β Fin) |
11 | | sseq1 3974 |
. . . . . . . . 9
β’ (π = β
β (π β π΄ β β
β π΄)) |
12 | | reseq2 5937 |
. . . . . . . . . . . . 13
β’ (π = β
β (π βΎ π) = (π βΎ β
)) |
13 | | res0 5946 |
. . . . . . . . . . . . 13
β’ (π βΎ β
) =
β
|
14 | 12, 13 | eqtrdi 2793 |
. . . . . . . . . . . 12
β’ (π = β
β (π βΎ π) = β
) |
15 | 14 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = β
β
(βfld Ξ£g (π βΎ π)) = (βfld
Ξ£g β
)) |
16 | | cnfld0 20837 |
. . . . . . . . . . . 12
β’ 0 =
(0gββfld) |
17 | 16 | gsum0 18546 |
. . . . . . . . . . 11
β’
(βfld Ξ£g β
) =
0 |
18 | 15, 17 | eqtrdi 2793 |
. . . . . . . . . 10
β’ (π = β
β
(βfld Ξ£g (π βΎ π)) = 0) |
19 | 18 | breq2d 5122 |
. . . . . . . . 9
β’ (π = β
β (0 <
(βfld Ξ£g (π βΎ π)) β 0 < 0)) |
20 | 11, 19 | anbi12d 632 |
. . . . . . . 8
β’ (π = β
β ((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β (β
β π΄ β§ 0 < 0))) |
21 | | reseq2 5937 |
. . . . . . . . . . 11
β’ (π = β
β ((π βf Β·
π) βΎ π) = ((π βf Β· π) βΎ
β
)) |
22 | 21 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π = β
β
(βfld Ξ£g ((π βf Β· π) βΎ π)) = (βfld
Ξ£g ((π βf Β· π) βΎ
β
))) |
23 | 22, 18 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = β
β
((βfld Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) = ((βfld
Ξ£g ((π βf Β· π) βΎ β
)) /
0)) |
24 | | reseq2 5937 |
. . . . . . . . . . . . 13
β’ (π = β
β ((π βf Β·
(πΉ β π)) βΎ π) = ((π βf Β· (πΉ β π)) βΎ β
)) |
25 | 24 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π = β
β
(βfld Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) = (βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ β
))) |
26 | 25, 18 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = β
β
((βfld Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π))) = ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ β
)) / 0)) |
27 | 26 | breq2d 5122 |
. . . . . . . . . 10
β’ (π = β
β ((πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ β
)) / 0))) |
28 | 27 | rabbidv 3418 |
. . . . . . . . 9
β’ (π = β
β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))} = {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ β
)) / 0)}) |
29 | 23, 28 | eleq12d 2832 |
. . . . . . . 8
β’ (π = β
β
(((βfld Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))} β ((βfld
Ξ£g ((π βf Β· π) βΎ β
)) / 0) β
{π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ β
)) /
0)})) |
30 | 20, 29 | imbi12d 345 |
. . . . . . 7
β’ (π = β
β (((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))}) β ((β
β π΄ β§ 0 < 0) β
((βfld Ξ£g ((π βf Β· π) βΎ β
)) / 0) β
{π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ β
)) /
0)}))) |
31 | 30 | imbi2d 341 |
. . . . . 6
β’ (π = β
β ((π β ((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β (π β ((β
β π΄ β§ 0 < 0) β
((βfld Ξ£g ((π βf Β· π) βΎ β
)) / 0) β
{π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ β
)) /
0)})))) |
32 | | sseq1 3974 |
. . . . . . . . 9
β’ (π = π β (π β π΄ β π β π΄)) |
33 | | reseq2 5937 |
. . . . . . . . . . 11
β’ (π = π β (π βΎ π) = (π βΎ π)) |
34 | 33 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π = π β (βfld
Ξ£g (π βΎ π)) = (βfld
Ξ£g (π βΎ π))) |
35 | 34 | breq2d 5122 |
. . . . . . . . 9
β’ (π = π β (0 < (βfld
Ξ£g (π βΎ π)) β 0 < (βfld
Ξ£g (π βΎ π)))) |
36 | 32, 35 | anbi12d 632 |
. . . . . . . 8
β’ (π = π β ((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β (π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))))) |
37 | | reseq2 5937 |
. . . . . . . . . . 11
β’ (π = π β ((π βf Β· π) βΎ π) = ((π βf Β· π) βΎ π)) |
38 | 37 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π = π β (βfld
Ξ£g ((π βf Β· π) βΎ π)) = (βfld
Ξ£g ((π βf Β· π) βΎ π))) |
39 | 38, 34 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = π β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) = ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π)))) |
40 | | reseq2 5937 |
. . . . . . . . . . . . 13
β’ (π = π β ((π βf Β· (πΉ β π)) βΎ π) = ((π βf Β· (πΉ β π)) βΎ π)) |
41 | 40 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π = π β (βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) = (βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π))) |
42 | 41, 34 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = π β ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π))) = ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))) |
43 | 42 | breq2d 5122 |
. . . . . . . . . 10
β’ (π = π β ((πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π))))) |
44 | 43 | rabbidv 3418 |
. . . . . . . . 9
β’ (π = π β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))} = {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))}) |
45 | 39, 44 | eleq12d 2832 |
. . . . . . . 8
β’ (π = π β (((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))} β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) |
46 | 36, 45 | imbi12d 345 |
. . . . . . 7
β’ (π = π β (((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))}) β ((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))}))) |
47 | 46 | imbi2d 341 |
. . . . . 6
β’ (π = π β ((π β ((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β (π β ((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})))) |
48 | | sseq1 3974 |
. . . . . . . . 9
β’ (π = (π βͺ {π}) β (π β π΄ β (π βͺ {π}) β π΄)) |
49 | | reseq2 5937 |
. . . . . . . . . . 11
β’ (π = (π βͺ {π}) β (π βΎ π) = (π βΎ (π βͺ {π}))) |
50 | 49 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π = (π βͺ {π}) β (βfld
Ξ£g (π βΎ π)) = (βfld
Ξ£g (π βΎ (π βͺ {π})))) |
51 | 50 | breq2d 5122 |
. . . . . . . . 9
β’ (π = (π βͺ {π}) β (0 < (βfld
Ξ£g (π βΎ π)) β 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) |
52 | 48, 51 | anbi12d 632 |
. . . . . . . 8
β’ (π = (π βͺ {π}) β ((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π})))))) |
53 | | reseq2 5937 |
. . . . . . . . . . 11
β’ (π = (π βͺ {π}) β ((π βf Β· π) βΎ π) = ((π βf Β· π) βΎ (π βͺ {π}))) |
54 | 53 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π = (π βͺ {π}) β (βfld
Ξ£g ((π βf Β· π) βΎ π)) = (βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π})))) |
55 | 54, 50 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = (π βͺ {π}) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) = ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))) |
56 | | reseq2 5937 |
. . . . . . . . . . . . 13
β’ (π = (π βͺ {π}) β ((π βf Β· (πΉ β π)) βΎ π) = ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) |
57 | 56 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π = (π βͺ {π}) β (βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) = (βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π})))) |
58 | 57, 50 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = (π βͺ {π}) β ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π))) = ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))) |
59 | 58 | breq2d 5122 |
. . . . . . . . . 10
β’ (π = (π βͺ {π}) β ((πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))))) |
60 | 59 | rabbidv 3418 |
. . . . . . . . 9
β’ (π = (π βͺ {π}) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))} = {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))}) |
61 | 55, 60 | eleq12d 2832 |
. . . . . . . 8
β’ (π = (π βͺ {π}) β (((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))} β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))})) |
62 | 52, 61 | imbi12d 345 |
. . . . . . 7
β’ (π = (π βͺ {π}) β (((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))}) β (((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π})))) β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))}))) |
63 | 62 | imbi2d 341 |
. . . . . 6
β’ (π = (π βͺ {π}) β ((π β ((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β (π β (((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π})))) β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))})))) |
64 | | sseq1 3974 |
. . . . . . . . 9
β’ (π = π΄ β (π β π΄ β π΄ β π΄)) |
65 | | reseq2 5937 |
. . . . . . . . . . 11
β’ (π = π΄ β (π βΎ π) = (π βΎ π΄)) |
66 | 65 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π = π΄ β (βfld
Ξ£g (π βΎ π)) = (βfld
Ξ£g (π βΎ π΄))) |
67 | 66 | breq2d 5122 |
. . . . . . . . 9
β’ (π = π΄ β (0 < (βfld
Ξ£g (π βΎ π)) β 0 < (βfld
Ξ£g (π βΎ π΄)))) |
68 | 64, 67 | anbi12d 632 |
. . . . . . . 8
β’ (π = π΄ β ((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β (π΄ β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π΄))))) |
69 | | reseq2 5937 |
. . . . . . . . . . 11
β’ (π = π΄ β ((π βf Β· π) βΎ π) = ((π βf Β· π) βΎ π΄)) |
70 | 69 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π = π΄ β (βfld
Ξ£g ((π βf Β· π) βΎ π)) = (βfld
Ξ£g ((π βf Β· π) βΎ π΄))) |
71 | 70, 66 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = π΄ β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) = ((βfld
Ξ£g ((π βf Β· π) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄)))) |
72 | | reseq2 5937 |
. . . . . . . . . . . . 13
β’ (π = π΄ β ((π βf Β· (πΉ β π)) βΎ π) = ((π βf Β· (πΉ β π)) βΎ π΄)) |
73 | 72 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π = π΄ β (βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) = (βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΄))) |
74 | 73, 66 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = π΄ β ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π))) = ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄)))) |
75 | 74 | breq2d 5122 |
. . . . . . . . . 10
β’ (π = π΄ β ((πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄))))) |
76 | 75 | rabbidv 3418 |
. . . . . . . . 9
β’ (π = π΄ β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))} = {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄)))}) |
77 | 71, 76 | eleq12d 2832 |
. . . . . . . 8
β’ (π = π΄ β (((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))} β ((βfld
Ξ£g ((π βf Β· π) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄)))})) |
78 | 68, 77 | imbi12d 345 |
. . . . . . 7
β’ (π = π΄ β (((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))}) β ((π΄ β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π΄))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄)))}))) |
79 | 78 | imbi2d 341 |
. . . . . 6
β’ (π = π΄ β ((π β ((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β (π β ((π΄ β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π΄))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄)))})))) |
80 | | 0re 11164 |
. . . . . . . . . 10
β’ 0 β
β |
81 | 80 | ltnri 11271 |
. . . . . . . . 9
β’ Β¬ 0
< 0 |
82 | 81 | pm2.21i 119 |
. . . . . . . 8
β’ (0 < 0
β ((βfld Ξ£g ((π βf Β· π) βΎ β
)) / 0) β
{π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ β
)) / 0)}) |
83 | 82 | adantl 483 |
. . . . . . 7
β’ ((β
β π΄ β§ 0 < 0)
β ((βfld Ξ£g ((π βf Β· π) βΎ β
)) / 0) β
{π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ β
)) / 0)}) |
84 | 83 | a1i 11 |
. . . . . 6
β’ (π β ((β
β π΄ β§ 0 < 0) β
((βfld Ξ£g ((π βf Β· π) βΎ β
)) / 0) β
{π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ β
)) /
0)})) |
85 | | impexp 452 |
. . . . . . . . . . . 12
β’ (((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))}) β (π β π΄ β (0 < (βfld
Ξ£g (π βΎ π)) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))}))) |
86 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β (π βͺ {π}) β π΄) |
87 | 86 | unssad 4152 |
. . . . . . . . . . . . 13
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β π β π΄) |
88 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 < (βfld
Ξ£g (π βΎ π))) β 0 < (βfld
Ξ£g (π βΎ π))) |
89 | | jensen.1 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π· β β) |
90 | 89 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β π· β β) |
91 | | jensen.2 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΉ:π·βΆβ) |
92 | 91 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β πΉ:π·βΆβ) |
93 | | simplll 774 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β π) |
94 | | jensen.3 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β π· β§ π β π·)) β (π[,]π) β π·) |
95 | 93, 94 | sylan 581 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ Β¬
π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β§ (π β π· β§ π β π·)) β (π[,]π) β π·) |
96 | 93, 10 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β π΄ β Fin) |
97 | 93, 2 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β π:π΄βΆ(0[,)+β)) |
98 | | jensen.6 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π:π΄βΆπ·) |
99 | 93, 98 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β π:π΄βΆπ·) |
100 | 1 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β 0 < (βfld
Ξ£g π)) |
101 | | jensen.8 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π₯ β π· β§ π¦ β π· β§ π‘ β (0[,]1))) β (πΉβ((π‘ Β· π₯) + ((1 β π‘) Β· π¦))) β€ ((π‘ Β· (πΉβπ₯)) + ((1 β π‘) Β· (πΉβπ¦)))) |
102 | 93, 101 | sylan 581 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ Β¬
π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β§ (π₯ β π· β§ π¦ β π· β§ π‘ β (0[,]1))) β (πΉβ((π‘ Β· π₯) + ((1 β π‘) Β· π¦))) β€ ((π‘ Β· (πΉβπ₯)) + ((1 β π‘) Β· (πΉβπ¦)))) |
103 | | simpllr 775 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β Β¬ π β π) |
104 | 86 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β (π βͺ {π}) β π΄) |
105 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’
(βfld Ξ£g (π βΎ π)) = (βfld
Ξ£g (π βΎ π)) |
106 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’
(βfld Ξ£g (π βΎ (π βͺ {π}))) = (βfld
Ξ£g (π βΎ (π βͺ {π}))) |
107 | | cnring 20835 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
βfld β Ring |
108 | | ringcmn 20010 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(βfld β Ring β βfld β
CMnd) |
109 | 107, 108 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β βfld β
CMnd) |
110 | 10 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β π΄ β Fin) |
111 | 110, 87 | ssfid 9218 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β π β Fin) |
112 | | rege0subm 20869 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(0[,)+β) β
(SubMndββfld) |
113 | 112 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β (0[,)+β) β
(SubMndββfld)) |
114 | 2 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β π:π΄βΆ(0[,)+β)) |
115 | 114, 87 | fssresd 6714 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β (π βΎ π):πβΆ(0[,)+β)) |
116 | | c0ex 11156 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 0 β
V |
117 | 116 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β 0 β V) |
118 | 115, 111,
117 | fdmfifsupp 9322 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β (π βΎ π) finSupp 0) |
119 | 16, 109, 111, 113, 115, 118 | gsumsubmcl 19703 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β (βfld
Ξ£g (π βΎ π)) β (0[,)+β)) |
120 | | elrege0 13378 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((βfld Ξ£g (π βΎ π)) β (0[,)+β) β
((βfld Ξ£g (π βΎ π)) β β β§ 0 β€
(βfld Ξ£g (π βΎ π)))) |
121 | 120 | simplbi 499 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((βfld Ξ£g (π βΎ π)) β (0[,)+β) β
(βfld Ξ£g (π βΎ π)) β β) |
122 | 119, 121 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β (βfld
Ξ£g (π βΎ π)) β β) |
123 | 122 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β (βfld
Ξ£g (π βΎ π)) β β) |
124 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β 0 < (βfld
Ξ£g (π βΎ π))) |
125 | 123, 124 | elrpd 12961 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β (βfld
Ξ£g (π βΎ π)) β
β+) |
126 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))}) |
127 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π€ = ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β (πΉβπ€) = (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))))) |
128 | 127 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ = ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β ((πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π)))) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π))))) |
129 | 128 | elrab 3650 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((βfld Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))} β (((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β π· β§ (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π)))) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π))))) |
130 | 126, 129 | sylib 217 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β (((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β π· β§ (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π)))) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π))))) |
131 | 130 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β π·) |
132 | 130 | simprd 497 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π)))) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))) |
133 | 90, 92, 95, 96, 97, 99, 100, 102, 103, 104, 105, 106, 125, 131, 132 | jensenlem2 26353 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β (((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β π· β§ (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))))) |
134 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ = ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β (πΉβπ€) = (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))))) |
135 | 134 | breq1d 5120 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ = ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β ((πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))))) |
136 | 135 | elrab 3650 |
. . . . . . . . . . . . . . . . 17
β’
(((βfld Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))} β (((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β π· β§ (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))))) |
137 | 133, 136 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ (0 < (βfld
Ξ£g (π βΎ π)) β§ ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))}) |
138 | 137 | expr 458 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 < (βfld
Ξ£g (π βΎ π))) β (((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))} β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))})) |
139 | 88, 138 | embantd 59 |
. . . . . . . . . . . . . 14
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((0 < (βfld
Ξ£g (π βΎ π)) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))}) β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))})) |
140 | | cnfldbas 20816 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β =
(Baseββfld) |
141 | | ringmnd 19981 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(βfld β Ring β βfld β
Mnd) |
142 | 107, 141 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β βfld β
Mnd) |
143 | 110, 86 | ssfid 9218 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β (π βͺ {π}) β Fin) |
144 | 143 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (π βͺ {π}) β Fin) |
145 | | ssun2 4138 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ {π} β (π βͺ {π}) |
146 | | vsnid 4628 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ π β {π} |
147 | 145, 146 | sselii 3946 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π β (π βͺ {π}) |
148 | 147 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β π β (π βͺ {π})) |
149 | | remulcl 11143 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π₯ β β β§ π¦ β β) β (π₯ Β· π¦) β β) |
150 | 149 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (π₯ β β β§ π¦ β β)) β (π₯ Β· π¦) β β) |
151 | | rge0ssre 13380 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(0[,)+β) β β |
152 | | fss 6690 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π:π΄βΆ(0[,)+β) β§ (0[,)+β)
β β) β π:π΄βΆβ) |
153 | 2, 151, 152 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π:π΄βΆβ) |
154 | 98, 89 | fssd 6691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π:π΄βΆβ) |
155 | | inidm 4183 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π΄ β© π΄) = π΄ |
156 | 150, 153,
154, 10, 10, 155 | off 7640 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π βf Β· π):π΄βΆβ) |
157 | | ax-resscn 11115 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ β
β β |
158 | | fss 6690 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π βf Β·
π):π΄βΆβ β§ β β
β) β (π
βf Β· π):π΄βΆβ) |
159 | 156, 157,
158 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π βf Β· π):π΄βΆβ) |
160 | 159 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (π βf Β· π):π΄βΆβ) |
161 | 86 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (π βͺ {π}) β π΄) |
162 | 160, 161 | fssresd 6714 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((π βf Β· π) βΎ (π βͺ {π})):(π βͺ {π})βΆβ) |
163 | 2 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β π:π΄βΆ(0[,)+β)) |
164 | 110 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β π΄ β Fin) |
165 | 163, 164 | fexd 7182 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β π β V) |
166 | 98 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β π:π΄βΆπ·) |
167 | 166, 164 | fexd 7182 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β π β V) |
168 | | offres 7921 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β V β§ π β V) β ((π βf Β·
π) βΎ (π βͺ {π})) = ((π βΎ (π βͺ {π})) βf Β· (π βΎ (π βͺ {π})))) |
169 | 165, 167,
168 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((π βf Β· π) βΎ (π βͺ {π})) = ((π βΎ (π βͺ {π})) βf Β· (π βΎ (π βͺ {π})))) |
170 | 169 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (((π βf Β· π) βΎ (π βͺ {π})) supp 0) = (((π βΎ (π βͺ {π})) βf Β· (π βΎ (π βͺ {π}))) supp 0)) |
171 | 151, 157 | sstri 3958 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(0[,)+β) β β |
172 | | fss 6690 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π:π΄βΆ(0[,)+β) β§ (0[,)+β)
β β) β π:π΄βΆβ) |
173 | 163, 171,
172 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β π:π΄βΆβ) |
174 | 173, 161 | fssresd 6714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (π βΎ (π βͺ {π})):(π βͺ {π})βΆβ) |
175 | | eldifi 4091 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π₯ β ((π βͺ {π}) β {π}) β π₯ β (π βͺ {π})) |
176 | 175 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ Β¬
π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β§ π₯ β ((π βͺ {π}) β {π})) β π₯ β (π βͺ {π})) |
177 | 176 | fvresd 6867 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ Β¬
π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β§ π₯ β ((π βͺ {π}) β {π})) β ((π βΎ (π βͺ {π}))βπ₯) = (πβπ₯)) |
178 | | difun2 4445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π βͺ {π}) β {π}) = (π β {π}) |
179 | | difss 4096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β {π}) β π |
180 | 178, 179 | eqsstri 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π βͺ {π}) β {π}) β π |
181 | 180 | sseli 3945 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π₯ β ((π βͺ {π}) β {π}) β π₯ β π) |
182 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β 0 = (βfld
Ξ£g (π βΎ π))) |
183 | 87 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β π β π΄) |
184 | 163, 183 | feqresmpt 6916 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (π βΎ π) = (π₯ β π β¦ (πβπ₯))) |
185 | 184 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (βfld
Ξ£g (π βΎ π)) = (βfld
Ξ£g (π₯ β π β¦ (πβπ₯)))) |
186 | 111 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β π β Fin) |
187 | 183 | sselda 3949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((π β§ Β¬
π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β§ π₯ β π) β π₯ β π΄) |
188 | 163 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((π β§ Β¬
π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β§ π₯ β π΄) β (πβπ₯) β (0[,)+β)) |
189 | 187, 188 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(((((π β§ Β¬
π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β§ π₯ β π) β (πβπ₯) β (0[,)+β)) |
190 | 171, 189 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ Β¬
π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β§ π₯ β π) β (πβπ₯) β β) |
191 | 186, 190 | gsumfsum 20880 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (βfld
Ξ£g (π₯ β π β¦ (πβπ₯))) = Ξ£π₯ β π (πβπ₯)) |
192 | 182, 185,
191 | 3eqtrrd 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β Ξ£π₯ β π (πβπ₯) = 0) |
193 | | elrege0 13378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((πβπ₯) β (0[,)+β) β ((πβπ₯) β β β§ 0 β€ (πβπ₯))) |
194 | 189, 193 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ Β¬
π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β§ π₯ β π) β ((πβπ₯) β β β§ 0 β€ (πβπ₯))) |
195 | 194 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((((π β§ Β¬
π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β§ π₯ β π) β (πβπ₯) β β) |
196 | 194 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((((π β§ Β¬
π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β§ π₯ β π) β 0 β€ (πβπ₯)) |
197 | 186, 195,
196 | fsum00 15690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (Ξ£π₯ β π (πβπ₯) = 0 β βπ₯ β π (πβπ₯) = 0)) |
198 | 192, 197 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β βπ₯ β π (πβπ₯) = 0) |
199 | 198 | r19.21bi 3237 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ Β¬
π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β§ π₯ β π) β (πβπ₯) = 0) |
200 | 181, 199 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ Β¬
π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β§ π₯ β ((π βͺ {π}) β {π})) β (πβπ₯) = 0) |
201 | 177, 200 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ Β¬
π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β§ π₯ β ((π βͺ {π}) β {π})) β ((π βΎ (π βͺ {π}))βπ₯) = 0) |
202 | 174, 201 | suppss 8130 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((π βΎ (π βͺ {π})) supp 0) β {π}) |
203 | | mul02 11340 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ β β β (0
Β· π₯) =
0) |
204 | 203 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ Β¬
π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β§ π₯ β β) β (0 Β· π₯) = 0) |
205 | 89 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β π· β β) |
206 | 205, 157 | sstrdi 3961 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β π· β β) |
207 | 166, 206 | fssd 6691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β π:π΄βΆβ) |
208 | 207, 161 | fssresd 6714 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (π βΎ (π βͺ {π})):(π βͺ {π})βΆβ) |
209 | 116 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β 0 β V) |
210 | 202, 204,
174, 208, 144, 209 | suppssof1 8135 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (((π βΎ (π βͺ {π})) βf Β· (π βΎ (π βͺ {π}))) supp 0) β {π}) |
211 | 170, 210 | eqsstrd 3987 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (((π βf Β· π) βΎ (π βͺ {π})) supp 0) β {π}) |
212 | 140, 16, 142, 144, 148, 162, 211 | gsumpt 19746 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) = (((π βf Β· π) βΎ (π βͺ {π}))βπ)) |
213 | 148 | fvresd 6867 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (((π βf Β· π) βΎ (π βͺ {π}))βπ) = ((π βf Β· π)βπ)) |
214 | 163 | ffnd 6674 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β π Fn π΄) |
215 | 166 | ffnd 6674 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β π Fn π΄) |
216 | 161, 148 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β π β π΄) |
217 | | fnfvof 7639 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π Fn π΄ β§ π Fn π΄) β§ (π΄ β Fin β§ π β π΄)) β ((π βf Β· π)βπ) = ((πβπ) Β· (πβπ))) |
218 | 214, 215,
164, 216, 217 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((π βf Β· π)βπ) = ((πβπ) Β· (πβπ))) |
219 | 212, 213,
218 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) = ((πβπ) Β· (πβπ))) |
220 | 140, 16, 142, 144, 148, 174, 202 | gsumpt 19746 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (βfld
Ξ£g (π βΎ (π βͺ {π}))) = ((π βΎ (π βͺ {π}))βπ)) |
221 | 148 | fvresd 6867 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((π βΎ (π βͺ {π}))βπ) = (πβπ)) |
222 | 220, 221 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (βfld
Ξ£g (π βΎ (π βͺ {π}))) = (πβπ)) |
223 | 219, 222 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) = (((πβπ) Β· (πβπ)) / (πβπ))) |
224 | 207, 216 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (πβπ) β β) |
225 | 173, 216 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (πβπ) β β) |
226 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β 0 < (βfld
Ξ£g (π βΎ (π βͺ {π})))) |
227 | 226, 222 | breqtrd 5136 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β 0 < (πβπ)) |
228 | 227 | gt0ne0d 11726 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (πβπ) β 0) |
229 | 224, 225,
228 | divcan3d 11943 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (((πβπ) Β· (πβπ)) / (πβπ)) = (πβπ)) |
230 | 223, 229 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) = (πβπ)) |
231 | 166, 216 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (πβπ) β π·) |
232 | 230, 231 | eqeltrd 2838 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β π·) |
233 | 91 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β πΉ:π·βΆβ) |
234 | 233, 231 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (πΉβ(πβπ)) β β) |
235 | 234 | leidd 11728 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (πΉβ(πβπ)) β€ (πΉβ(πβπ))) |
236 | 230 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))) = (πΉβ(πβπ))) |
237 | | fco 6697 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΉ:π·βΆβ β§ π:π΄βΆπ·) β (πΉ β π):π΄βΆβ) |
238 | 91, 98, 237 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (πΉ β π):π΄βΆβ) |
239 | 150, 153,
238, 10, 10, 155 | off 7640 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π βf Β· (πΉ β π)):π΄βΆβ) |
240 | | fss 6690 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π βf Β·
(πΉ β π)):π΄βΆβ β§ β β
β) β (π
βf Β· (πΉ β π)):π΄βΆβ) |
241 | 239, 157,
240 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π βf Β· (πΉ β π)):π΄βΆβ) |
242 | 241 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (π βf Β· (πΉ β π)):π΄βΆβ) |
243 | 242, 161 | fssresd 6714 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((π βf Β· (πΉ β π)) βΎ (π βͺ {π})):(π βͺ {π})βΆβ) |
244 | 238 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (πΉ β π):π΄βΆβ) |
245 | 244, 164 | fexd 7182 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (πΉ β π) β V) |
246 | | offres 7921 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β V β§ (πΉ β π) β V) β ((π βf Β· (πΉ β π)) βΎ (π βͺ {π})) = ((π βΎ (π βͺ {π})) βf Β· ((πΉ β π) βΎ (π βͺ {π})))) |
247 | 165, 245,
246 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((π βf Β· (πΉ β π)) βΎ (π βͺ {π})) = ((π βΎ (π βͺ {π})) βf Β· ((πΉ β π) βΎ (π βͺ {π})))) |
248 | 247 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (((π βf Β· (πΉ β π)) βΎ (π βͺ {π})) supp 0) = (((π βΎ (π βͺ {π})) βf Β· ((πΉ β π) βΎ (π βͺ {π}))) supp 0)) |
249 | | fss 6690 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((πΉ β π):π΄βΆβ β§ β β
β) β (πΉ β
π):π΄βΆβ) |
250 | 244, 157,
249 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (πΉ β π):π΄βΆβ) |
251 | 250, 161 | fssresd 6714 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((πΉ β π) βΎ (π βͺ {π})):(π βͺ {π})βΆβ) |
252 | 202, 204,
174, 251, 144, 209 | suppssof1 8135 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (((π βΎ (π βͺ {π})) βf Β· ((πΉ β π) βΎ (π βͺ {π}))) supp 0) β {π}) |
253 | 248, 252 | eqsstrd 3987 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (((π βf Β· (πΉ β π)) βΎ (π βͺ {π})) supp 0) β {π}) |
254 | 140, 16, 142, 144, 148, 243, 253 | gsumpt 19746 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) = (((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))βπ)) |
255 | 148 | fvresd 6867 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))βπ) = ((π βf Β· (πΉ β π))βπ)) |
256 | 91 | ffnd 6674 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΉ Fn π·) |
257 | | fnfco 6712 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΉ Fn π· β§ π:π΄βΆπ·) β (πΉ β π) Fn π΄) |
258 | 256, 98, 257 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (πΉ β π) Fn π΄) |
259 | 258 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (πΉ β π) Fn π΄) |
260 | | fnfvof 7639 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π Fn π΄ β§ (πΉ β π) Fn π΄) β§ (π΄ β Fin β§ π β π΄)) β ((π βf Β· (πΉ β π))βπ) = ((πβπ) Β· ((πΉ β π)βπ))) |
261 | 214, 259,
164, 216, 260 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((π βf Β· (πΉ β π))βπ) = ((πβπ) Β· ((πΉ β π)βπ))) |
262 | | fvco3 6945 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π:π΄βΆπ· β§ π β π΄) β ((πΉ β π)βπ) = (πΉβ(πβπ))) |
263 | 166, 216,
262 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((πΉ β π)βπ) = (πΉβ(πβπ))) |
264 | 263 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((πβπ) Β· ((πΉ β π)βπ)) = ((πβπ) Β· (πΉβ(πβπ)))) |
265 | 261, 264 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((π βf Β· (πΉ β π))βπ) = ((πβπ) Β· (πΉβ(πβπ)))) |
266 | 254, 255,
265 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) = ((πβπ) Β· (πΉβ(πβπ)))) |
267 | 266, 222 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) = (((πβπ) Β· (πΉβ(πβπ))) / (πβπ))) |
268 | 234 | recnd 11190 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (πΉβ(πβπ)) β β) |
269 | 268, 225,
228 | divcan3d 11943 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (((πβπ) Β· (πΉβ(πβπ))) / (πβπ)) = (πΉβ(πβπ))) |
270 | 267, 269 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) = (πΉβ(πβπ))) |
271 | 235, 236,
270 | 3brtr4d 5142 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β (πΉβ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))) |
272 | 135, 232,
271 | elrabd 3652 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))}) |
273 | 272 | a1d 25 |
. . . . . . . . . . . . . 14
β’ ((((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β§ 0 = (βfld
Ξ£g (π βΎ π))) β ((0 < (βfld
Ξ£g (π βΎ π)) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))}) β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))})) |
274 | 120 | simprbi 498 |
. . . . . . . . . . . . . . . 16
β’
((βfld Ξ£g (π βΎ π)) β (0[,)+β) β 0 β€
(βfld Ξ£g (π βΎ π))) |
275 | 119, 274 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β 0 β€ (βfld
Ξ£g (π βΎ π))) |
276 | | leloe 11248 |
. . . . . . . . . . . . . . . 16
β’ ((0
β β β§ (βfld Ξ£g (π βΎ π)) β β) β (0 β€
(βfld Ξ£g (π βΎ π)) β (0 < (βfld
Ξ£g (π βΎ π)) β¨ 0 = (βfld
Ξ£g (π βΎ π))))) |
277 | 80, 122, 276 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β (0 β€ (βfld
Ξ£g (π βΎ π)) β (0 < (βfld
Ξ£g (π βΎ π)) β¨ 0 = (βfld
Ξ£g (π βΎ π))))) |
278 | 275, 277 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β (0 < (βfld
Ξ£g (π βΎ π)) β¨ 0 = (βfld
Ξ£g (π βΎ π)))) |
279 | 139, 273,
278 | mpjaodan 958 |
. . . . . . . . . . . . 13
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β ((0 < (βfld
Ξ£g (π βΎ π)) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))}) β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))})) |
280 | 87, 279 | embantd 59 |
. . . . . . . . . . . 12
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β ((π β π΄ β (0 < (βfld
Ξ£g (π βΎ π)) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))})) |
281 | 85, 280 | biimtrid 241 |
. . . . . . . . . . 11
β’ (((π β§ Β¬ π β π) β§ ((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π}))))) β (((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))}) β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))})) |
282 | 281 | ex 414 |
. . . . . . . . . 10
β’ ((π β§ Β¬ π β π) β (((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π})))) β (((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))}) β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))}))) |
283 | 282 | com23 86 |
. . . . . . . . 9
β’ ((π β§ Β¬ π β π) β (((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))}) β (((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π})))) β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))}))) |
284 | 283 | expcom 415 |
. . . . . . . 8
β’ (Β¬
π β π β (π β (((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))}) β (((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π})))) β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))})))) |
285 | 284 | adantl 483 |
. . . . . . 7
β’ ((π β Fin β§ Β¬ π β π) β (π β (((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))}) β (((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π})))) β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))})))) |
286 | 285 | a2d 29 |
. . . . . 6
β’ ((π β Fin β§ Β¬ π β π) β ((π β ((π β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π)) / (βfld
Ξ£g (π βΎ π))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π)) / (βfld
Ξ£g (π βΎ π)))})) β (π β (((π βͺ {π}) β π΄ β§ 0 < (βfld
Ξ£g (π βΎ (π βͺ {π})))) β ((βfld
Ξ£g ((π βf Β· π) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π})))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ (π βͺ {π}))) / (βfld
Ξ£g (π βΎ (π βͺ {π}))))})))) |
287 | 31, 47, 63, 79, 84, 286 | findcard2s 9116 |
. . . . 5
β’ (π΄ β Fin β (π β ((π΄ β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π΄))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄)))}))) |
288 | 10, 287 | mpcom 38 |
. . . 4
β’ (π β ((π΄ β π΄ β§ 0 < (βfld
Ξ£g (π βΎ π΄))) β ((βfld
Ξ£g ((π βf Β· π) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄)))})) |
289 | 9, 288 | mpd 15 |
. . 3
β’ (π β ((βfld
Ξ£g ((π βf Β· π) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄))) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄)))}) |
290 | 156 | ffnd 6674 |
. . . . . 6
β’ (π β (π βf Β· π) Fn π΄) |
291 | | fnresdm 6625 |
. . . . . 6
β’ ((π βf Β·
π) Fn π΄ β ((π βf Β· π) βΎ π΄) = (π βf Β· π)) |
292 | 290, 291 | syl 17 |
. . . . 5
β’ (π β ((π βf Β· π) βΎ π΄) = (π βf Β· π)) |
293 | 292 | oveq2d 7378 |
. . . 4
β’ (π β (βfld
Ξ£g ((π βf Β· π) βΎ π΄)) = (βfld
Ξ£g (π βf Β· π))) |
294 | 293, 6 | oveq12d 7380 |
. . 3
β’ (π β ((βfld
Ξ£g ((π βf Β· π) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄))) = ((βfld
Ξ£g (π βf Β· π)) / (βfld
Ξ£g π))) |
295 | 3, 258, 10, 10, 155 | offn 7635 |
. . . . . . . 8
β’ (π β (π βf Β· (πΉ β π)) Fn π΄) |
296 | | fnresdm 6625 |
. . . . . . . 8
β’ ((π βf Β·
(πΉ β π)) Fn π΄ β ((π βf Β· (πΉ β π)) βΎ π΄) = (π βf Β· (πΉ β π))) |
297 | 295, 296 | syl 17 |
. . . . . . 7
β’ (π β ((π βf Β· (πΉ β π)) βΎ π΄) = (π βf Β· (πΉ β π))) |
298 | 297 | oveq2d 7378 |
. . . . . 6
β’ (π β (βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΄)) = (βfld
Ξ£g (π βf Β· (πΉ β π)))) |
299 | 298, 6 | oveq12d 7380 |
. . . . 5
β’ (π β ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄))) = ((βfld
Ξ£g (π βf Β· (πΉ β π))) / (βfld
Ξ£g π))) |
300 | 299 | breq2d 5122 |
. . . 4
β’ (π β ((πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄))) β (πΉβπ€) β€ ((βfld
Ξ£g (π βf Β· (πΉ β π))) / (βfld
Ξ£g π)))) |
301 | 300 | rabbidv 3418 |
. . 3
β’ (π β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g ((π βf Β· (πΉ β π)) βΎ π΄)) / (βfld
Ξ£g (π βΎ π΄)))} = {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g (π βf Β· (πΉ β π))) / (βfld
Ξ£g π))}) |
302 | 289, 294,
301 | 3eltr3d 2852 |
. 2
β’ (π β ((βfld
Ξ£g (π βf Β· π)) / (βfld
Ξ£g π)) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g (π βf Β· (πΉ β π))) / (βfld
Ξ£g π))}) |
303 | | fveq2 6847 |
. . . 4
β’ (π€ = ((βfld
Ξ£g (π βf Β· π)) / (βfld
Ξ£g π)) β (πΉβπ€) = (πΉβ((βfld
Ξ£g (π βf Β· π)) / (βfld
Ξ£g π)))) |
304 | 303 | breq1d 5120 |
. . 3
β’ (π€ = ((βfld
Ξ£g (π βf Β· π)) / (βfld
Ξ£g π)) β ((πΉβπ€) β€ ((βfld
Ξ£g (π βf Β· (πΉ β π))) / (βfld
Ξ£g π)) β (πΉβ((βfld
Ξ£g (π βf Β· π)) / (βfld
Ξ£g π))) β€ ((βfld
Ξ£g (π βf Β· (πΉ β π))) / (βfld
Ξ£g π)))) |
305 | 304 | elrab 3650 |
. 2
β’
(((βfld Ξ£g (π βf Β· π)) / (βfld
Ξ£g π)) β {π€ β π· β£ (πΉβπ€) β€ ((βfld
Ξ£g (π βf Β· (πΉ β π))) / (βfld
Ξ£g π))} β (((βfld
Ξ£g (π βf Β· π)) / (βfld
Ξ£g π)) β π· β§ (πΉβ((βfld
Ξ£g (π βf Β· π)) / (βfld
Ξ£g π))) β€ ((βfld
Ξ£g (π βf Β· (πΉ β π))) / (βfld
Ξ£g π)))) |
306 | 302, 305 | sylib 217 |
1
β’ (π β (((βfld
Ξ£g (π βf Β· π)) / (βfld
Ξ£g π)) β π· β§ (πΉβ((βfld
Ξ£g (π βf Β· π)) / (βfld
Ξ£g π))) β€ ((βfld
Ξ£g (π βf Β· (πΉ β π))) / (βfld
Ξ£g π)))) |