Step | Hyp | Ref
| Expression |
1 | | remulcl 11143 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β) β (π₯ Β· π¦) β β) |
2 | 1 | adantl 483 |
. . . . 5
β’ ((π β§ (π₯ β β β§ π¦ β β)) β (π₯ Β· π¦) β β) |
3 | | mbfmulc2re.2 |
. . . . . 6
β’ (π β π΅ β β) |
4 | | fconst6g 6736 |
. . . . . 6
β’ (π΅ β β β (π΄ Γ {π΅}):π΄βΆβ) |
5 | 3, 4 | syl 17 |
. . . . 5
β’ (π β (π΄ Γ {π΅}):π΄βΆβ) |
6 | | mbfmulc2lem.3 |
. . . . 5
β’ (π β πΉ:π΄βΆβ) |
7 | 6 | fdmd 6684 |
. . . . . 6
β’ (π β dom πΉ = π΄) |
8 | | mbfmulc2re.1 |
. . . . . . 7
β’ (π β πΉ β MblFn) |
9 | | mbfdm 25006 |
. . . . . . 7
β’ (πΉ β MblFn β dom πΉ β dom
vol) |
10 | 8, 9 | syl 17 |
. . . . . 6
β’ (π β dom πΉ β dom vol) |
11 | 7, 10 | eqeltrrd 2839 |
. . . . 5
β’ (π β π΄ β dom vol) |
12 | | inidm 4183 |
. . . . 5
β’ (π΄ β© π΄) = π΄ |
13 | 2, 5, 6, 11, 11, 12 | off 7640 |
. . . 4
β’ (π β ((π΄ Γ {π΅}) βf Β· πΉ):π΄βΆβ) |
14 | 13 | adantr 482 |
. . 3
β’ ((π β§ π΅ < 0) β ((π΄ Γ {π΅}) βf Β· πΉ):π΄βΆβ) |
15 | 11 | adantr 482 |
. . 3
β’ ((π β§ π΅ < 0) β π΄ β dom vol) |
16 | | simprl 770 |
. . . . . . . . . . 11
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β π¦ β β) |
17 | 16 | rexrd 11212 |
. . . . . . . . . 10
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β π¦ β β*) |
18 | | elioopnf 13367 |
. . . . . . . . . 10
β’ (π¦ β β*
β ((((π΄ Γ {π΅}) βf Β·
πΉ)βπ§) β (π¦(,)+β) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β β β§ π¦ < (((π΄ Γ {π΅}) βf Β· πΉ)βπ§)))) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (π¦(,)+β) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β β β§ π¦ < (((π΄ Γ {π΅}) βf Β· πΉ)βπ§)))) |
20 | 13 | ffvelcdmda 7040 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π΄) β (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β β) |
21 | 20 | ad2ant2rl 748 |
. . . . . . . . . 10
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β β) |
22 | 21 | biantrurd 534 |
. . . . . . . . 9
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β (π¦ < (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β β β§ π¦ < (((π΄ Γ {π΅}) βf Β· πΉ)βπ§)))) |
23 | 6 | ffvelcdmda 7040 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π΄) β (πΉβπ§) β β) |
24 | 23 | ad2ant2rl 748 |
. . . . . . . . . . 11
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β (πΉβπ§) β β) |
25 | 24 | biantrurd 534 |
. . . . . . . . . 10
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((πΉβπ§) < (π¦ / π΅) β ((πΉβπ§) β β β§ (πΉβπ§) < (π¦ / π΅)))) |
26 | | simprr 772 |
. . . . . . . . . . . . 13
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β π§ β π΄) |
27 | 11 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β π΄ β dom vol) |
28 | 3 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β π΅ β β) |
29 | 6 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β πΉ:π΄βΆβ) |
30 | 29 | ffnd 6674 |
. . . . . . . . . . . . . 14
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β πΉ Fn π΄) |
31 | | eqidd 2738 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β§ π§ β π΄) β (πΉβπ§) = (πΉβπ§)) |
32 | 27, 28, 30, 31 | ofc1 7648 |
. . . . . . . . . . . . 13
β’ ((((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β§ π§ β π΄) β (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) = (π΅ Β· (πΉβπ§))) |
33 | 26, 32 | mpdan 686 |
. . . . . . . . . . . 12
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) = (π΅ Β· (πΉβπ§))) |
34 | 33 | breq2d 5122 |
. . . . . . . . . . 11
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β (π¦ < (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β π¦ < (π΅ Β· (πΉβπ§)))) |
35 | 33, 21 | eqeltrrd 2839 |
. . . . . . . . . . . . 13
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β (π΅ Β· (πΉβπ§)) β β) |
36 | 16, 35 | ltnegd 11740 |
. . . . . . . . . . . 12
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β (π¦ < (π΅ Β· (πΉβπ§)) β -(π΅ Β· (πΉβπ§)) < -π¦)) |
37 | 28 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β π΅ β β) |
38 | 24 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β (πΉβπ§) β β) |
39 | 37, 38 | mulneg1d 11615 |
. . . . . . . . . . . . 13
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β (-π΅ Β· (πΉβπ§)) = -(π΅ Β· (πΉβπ§))) |
40 | 39 | breq1d 5120 |
. . . . . . . . . . . 12
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((-π΅ Β· (πΉβπ§)) < -π¦ β -(π΅ Β· (πΉβπ§)) < -π¦)) |
41 | 16 | renegcld 11589 |
. . . . . . . . . . . . 13
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β -π¦ β β) |
42 | 28 | renegcld 11589 |
. . . . . . . . . . . . 13
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β -π΅ β β) |
43 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β π΅ < 0) |
44 | 28 | lt0neg1d 11731 |
. . . . . . . . . . . . . 14
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β (π΅ < 0 β 0 < -π΅)) |
45 | 43, 44 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β 0 < -π΅) |
46 | | ltmuldiv2 12036 |
. . . . . . . . . . . . 13
β’ (((πΉβπ§) β β β§ -π¦ β β β§ (-π΅ β β β§ 0 < -π΅)) β ((-π΅ Β· (πΉβπ§)) < -π¦ β (πΉβπ§) < (-π¦ / -π΅))) |
47 | 24, 41, 42, 45, 46 | syl112anc 1375 |
. . . . . . . . . . . 12
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((-π΅ Β· (πΉβπ§)) < -π¦ β (πΉβπ§) < (-π¦ / -π΅))) |
48 | 36, 40, 47 | 3bitr2rd 308 |
. . . . . . . . . . 11
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((πΉβπ§) < (-π¦ / -π΅) β π¦ < (π΅ Β· (πΉβπ§)))) |
49 | 16 | recnd 11190 |
. . . . . . . . . . . . 13
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β π¦ β β) |
50 | 43 | lt0ne0d 11727 |
. . . . . . . . . . . . 13
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β π΅ β 0) |
51 | 49, 37, 50 | div2negd 11953 |
. . . . . . . . . . . 12
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β (-π¦ / -π΅) = (π¦ / π΅)) |
52 | 51 | breq2d 5122 |
. . . . . . . . . . 11
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((πΉβπ§) < (-π¦ / -π΅) β (πΉβπ§) < (π¦ / π΅))) |
53 | 34, 48, 52 | 3bitr2d 307 |
. . . . . . . . . 10
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β (π¦ < (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (πΉβπ§) < (π¦ / π΅))) |
54 | 16, 28, 50 | redivcld 11990 |
. . . . . . . . . . . 12
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β (π¦ / π΅) β β) |
55 | 54 | rexrd 11212 |
. . . . . . . . . . 11
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β (π¦ / π΅) β
β*) |
56 | | elioomnf 13368 |
. . . . . . . . . . 11
β’ ((π¦ / π΅) β β* β ((πΉβπ§) β (-β(,)(π¦ / π΅)) β ((πΉβπ§) β β β§ (πΉβπ§) < (π¦ / π΅)))) |
57 | 55, 56 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((πΉβπ§) β (-β(,)(π¦ / π΅)) β ((πΉβπ§) β β β§ (πΉβπ§) < (π¦ / π΅)))) |
58 | 25, 53, 57 | 3bitr4d 311 |
. . . . . . . . 9
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β (π¦ < (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (πΉβπ§) β (-β(,)(π¦ / π΅)))) |
59 | 19, 22, 58 | 3bitr2d 307 |
. . . . . . . 8
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (π¦(,)+β) β (πΉβπ§) β (-β(,)(π¦ / π΅)))) |
60 | 59 | anassrs 469 |
. . . . . . 7
β’ ((((π β§ π΅ < 0) β§ π¦ β β) β§ π§ β π΄) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (π¦(,)+β) β (πΉβπ§) β (-β(,)(π¦ / π΅)))) |
61 | 60 | pm5.32da 580 |
. . . . . 6
β’ (((π β§ π΅ < 0) β§ π¦ β β) β ((π§ β π΄ β§ (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (π¦(,)+β)) β (π§ β π΄ β§ (πΉβπ§) β (-β(,)(π¦ / π΅))))) |
62 | 13 | ffnd 6674 |
. . . . . . . 8
β’ (π β ((π΄ Γ {π΅}) βf Β· πΉ) Fn π΄) |
63 | 62 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π΅ < 0) β§ π¦ β β) β ((π΄ Γ {π΅}) βf Β· πΉ) Fn π΄) |
64 | | elpreima 7013 |
. . . . . . 7
β’ (((π΄ Γ {π΅}) βf Β· πΉ) Fn π΄ β (π§ β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (π¦(,)+β)) β (π§ β π΄ β§ (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (π¦(,)+β)))) |
65 | 63, 64 | syl 17 |
. . . . . 6
β’ (((π β§ π΅ < 0) β§ π¦ β β) β (π§ β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (π¦(,)+β)) β (π§ β π΄ β§ (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (π¦(,)+β)))) |
66 | 6 | ffnd 6674 |
. . . . . . . 8
β’ (π β πΉ Fn π΄) |
67 | 66 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π΅ < 0) β§ π¦ β β) β πΉ Fn π΄) |
68 | | elpreima 7013 |
. . . . . . 7
β’ (πΉ Fn π΄ β (π§ β (β‘πΉ β (-β(,)(π¦ / π΅))) β (π§ β π΄ β§ (πΉβπ§) β (-β(,)(π¦ / π΅))))) |
69 | 67, 68 | syl 17 |
. . . . . 6
β’ (((π β§ π΅ < 0) β§ π¦ β β) β (π§ β (β‘πΉ β (-β(,)(π¦ / π΅))) β (π§ β π΄ β§ (πΉβπ§) β (-β(,)(π¦ / π΅))))) |
70 | 61, 65, 69 | 3bitr4d 311 |
. . . . 5
β’ (((π β§ π΅ < 0) β§ π¦ β β) β (π§ β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (π¦(,)+β)) β π§ β (β‘πΉ β (-β(,)(π¦ / π΅))))) |
71 | 70 | eqrdv 2735 |
. . . 4
β’ (((π β§ π΅ < 0) β§ π¦ β β) β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (π¦(,)+β)) = (β‘πΉ β (-β(,)(π¦ / π΅)))) |
72 | | mbfima 25010 |
. . . . . 6
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β (β‘πΉ β (-β(,)(π¦ / π΅))) β dom vol) |
73 | 8, 6, 72 | syl2anc 585 |
. . . . 5
β’ (π β (β‘πΉ β (-β(,)(π¦ / π΅))) β dom vol) |
74 | 73 | ad2antrr 725 |
. . . 4
β’ (((π β§ π΅ < 0) β§ π¦ β β) β (β‘πΉ β (-β(,)(π¦ / π΅))) β dom vol) |
75 | 71, 74 | eqeltrd 2838 |
. . 3
β’ (((π β§ π΅ < 0) β§ π¦ β β) β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (π¦(,)+β)) β dom
vol) |
76 | | elioomnf 13368 |
. . . . . . . . . 10
β’ (π¦ β β*
β ((((π΄ Γ {π΅}) βf Β·
πΉ)βπ§) β (-β(,)π¦) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β β β§ (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) < π¦))) |
77 | 17, 76 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (-β(,)π¦) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β β β§ (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) < π¦))) |
78 | 21 | biantrurd 534 |
. . . . . . . . 9
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) < π¦ β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β β β§ (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) < π¦))) |
79 | 24 | biantrurd 534 |
. . . . . . . . . 10
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((π¦ / π΅) < (πΉβπ§) β ((πΉβπ§) β β β§ (π¦ / π΅) < (πΉβπ§)))) |
80 | 33 | breq1d 5120 |
. . . . . . . . . . 11
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) < π¦ β (π΅ Β· (πΉβπ§)) < π¦)) |
81 | 39 | breq2d 5122 |
. . . . . . . . . . . 12
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β (-π¦ < (-π΅ Β· (πΉβπ§)) β -π¦ < -(π΅ Β· (πΉβπ§)))) |
82 | 51 | breq1d 5120 |
. . . . . . . . . . . . 13
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((-π¦ / -π΅) < (πΉβπ§) β (π¦ / π΅) < (πΉβπ§))) |
83 | | ltdivmul 12037 |
. . . . . . . . . . . . . 14
β’ ((-π¦ β β β§ (πΉβπ§) β β β§ (-π΅ β β β§ 0 < -π΅)) β ((-π¦ / -π΅) < (πΉβπ§) β -π¦ < (-π΅ Β· (πΉβπ§)))) |
84 | 41, 24, 42, 45, 83 | syl112anc 1375 |
. . . . . . . . . . . . 13
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((-π¦ / -π΅) < (πΉβπ§) β -π¦ < (-π΅ Β· (πΉβπ§)))) |
85 | 82, 84 | bitr3d 281 |
. . . . . . . . . . . 12
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((π¦ / π΅) < (πΉβπ§) β -π¦ < (-π΅ Β· (πΉβπ§)))) |
86 | 35, 16 | ltnegd 11740 |
. . . . . . . . . . . 12
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((π΅ Β· (πΉβπ§)) < π¦ β -π¦ < -(π΅ Β· (πΉβπ§)))) |
87 | 81, 85, 86 | 3bitr4d 311 |
. . . . . . . . . . 11
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((π¦ / π΅) < (πΉβπ§) β (π΅ Β· (πΉβπ§)) < π¦)) |
88 | 80, 87 | bitr4d 282 |
. . . . . . . . . 10
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) < π¦ β (π¦ / π΅) < (πΉβπ§))) |
89 | | elioopnf 13367 |
. . . . . . . . . . 11
β’ ((π¦ / π΅) β β* β ((πΉβπ§) β ((π¦ / π΅)(,)+β) β ((πΉβπ§) β β β§ (π¦ / π΅) < (πΉβπ§)))) |
90 | 55, 89 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((πΉβπ§) β ((π¦ / π΅)(,)+β) β ((πΉβπ§) β β β§ (π¦ / π΅) < (πΉβπ§)))) |
91 | 79, 88, 90 | 3bitr4d 311 |
. . . . . . . . 9
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) < π¦ β (πΉβπ§) β ((π¦ / π΅)(,)+β))) |
92 | 77, 78, 91 | 3bitr2d 307 |
. . . . . . . 8
β’ (((π β§ π΅ < 0) β§ (π¦ β β β§ π§ β π΄)) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (-β(,)π¦) β (πΉβπ§) β ((π¦ / π΅)(,)+β))) |
93 | 92 | anassrs 469 |
. . . . . . 7
β’ ((((π β§ π΅ < 0) β§ π¦ β β) β§ π§ β π΄) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (-β(,)π¦) β (πΉβπ§) β ((π¦ / π΅)(,)+β))) |
94 | 93 | pm5.32da 580 |
. . . . . 6
β’ (((π β§ π΅ < 0) β§ π¦ β β) β ((π§ β π΄ β§ (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (-β(,)π¦)) β (π§ β π΄ β§ (πΉβπ§) β ((π¦ / π΅)(,)+β)))) |
95 | | elpreima 7013 |
. . . . . . 7
β’ (((π΄ Γ {π΅}) βf Β· πΉ) Fn π΄ β (π§ β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (-β(,)π¦)) β (π§ β π΄ β§ (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (-β(,)π¦)))) |
96 | 63, 95 | syl 17 |
. . . . . 6
β’ (((π β§ π΅ < 0) β§ π¦ β β) β (π§ β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (-β(,)π¦)) β (π§ β π΄ β§ (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (-β(,)π¦)))) |
97 | | elpreima 7013 |
. . . . . . 7
β’ (πΉ Fn π΄ β (π§ β (β‘πΉ β ((π¦ / π΅)(,)+β)) β (π§ β π΄ β§ (πΉβπ§) β ((π¦ / π΅)(,)+β)))) |
98 | 67, 97 | syl 17 |
. . . . . 6
β’ (((π β§ π΅ < 0) β§ π¦ β β) β (π§ β (β‘πΉ β ((π¦ / π΅)(,)+β)) β (π§ β π΄ β§ (πΉβπ§) β ((π¦ / π΅)(,)+β)))) |
99 | 94, 96, 98 | 3bitr4d 311 |
. . . . 5
β’ (((π β§ π΅ < 0) β§ π¦ β β) β (π§ β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (-β(,)π¦)) β π§ β (β‘πΉ β ((π¦ / π΅)(,)+β)))) |
100 | 99 | eqrdv 2735 |
. . . 4
β’ (((π β§ π΅ < 0) β§ π¦ β β) β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (-β(,)π¦)) = (β‘πΉ β ((π¦ / π΅)(,)+β))) |
101 | | mbfima 25010 |
. . . . . 6
β’ ((πΉ β MblFn β§ πΉ:π΄βΆβ) β (β‘πΉ β ((π¦ / π΅)(,)+β)) β dom
vol) |
102 | 8, 6, 101 | syl2anc 585 |
. . . . 5
β’ (π β (β‘πΉ β ((π¦ / π΅)(,)+β)) β dom
vol) |
103 | 102 | ad2antrr 725 |
. . . 4
β’ (((π β§ π΅ < 0) β§ π¦ β β) β (β‘πΉ β ((π¦ / π΅)(,)+β)) β dom
vol) |
104 | 100, 103 | eqeltrd 2838 |
. . 3
β’ (((π β§ π΅ < 0) β§ π¦ β β) β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (-β(,)π¦)) β dom
vol) |
105 | 14, 15, 75, 104 | ismbf2d 25020 |
. 2
β’ ((π β§ π΅ < 0) β ((π΄ Γ {π΅}) βf Β· πΉ) β MblFn) |
106 | 11 | adantr 482 |
. . . 4
β’ ((π β§ π΅ = 0) β π΄ β dom vol) |
107 | 6 | adantr 482 |
. . . 4
β’ ((π β§ π΅ = 0) β πΉ:π΄βΆβ) |
108 | | simpr 486 |
. . . . 5
β’ ((π β§ π΅ = 0) β π΅ = 0) |
109 | | 0cn 11154 |
. . . . 5
β’ 0 β
β |
110 | 108, 109 | eqeltrdi 2846 |
. . . 4
β’ ((π β§ π΅ = 0) β π΅ β β) |
111 | | 0cnd 11155 |
. . . 4
β’ ((π β§ π΅ = 0) β 0 β
β) |
112 | | simplr 768 |
. . . . . 6
β’ (((π β§ π΅ = 0) β§ π₯ β β) β π΅ = 0) |
113 | 112 | oveq1d 7377 |
. . . . 5
β’ (((π β§ π΅ = 0) β§ π₯ β β) β (π΅ Β· π₯) = (0 Β· π₯)) |
114 | | mul02lem2 11339 |
. . . . . 6
β’ (π₯ β β β (0
Β· π₯) =
0) |
115 | 114 | adantl 483 |
. . . . 5
β’ (((π β§ π΅ = 0) β§ π₯ β β) β (0 Β· π₯) = 0) |
116 | 113, 115 | eqtrd 2777 |
. . . 4
β’ (((π β§ π΅ = 0) β§ π₯ β β) β (π΅ Β· π₯) = 0) |
117 | 106, 107,
110, 111, 116 | caofid2 7656 |
. . 3
β’ ((π β§ π΅ = 0) β ((π΄ Γ {π΅}) βf Β· πΉ) = (π΄ Γ {0})) |
118 | | mbfconst 25013 |
. . . 4
β’ ((π΄ β dom vol β§ 0 β
β) β (π΄ Γ
{0}) β MblFn) |
119 | 106, 109,
118 | sylancl 587 |
. . 3
β’ ((π β§ π΅ = 0) β (π΄ Γ {0}) β MblFn) |
120 | 117, 119 | eqeltrd 2838 |
. 2
β’ ((π β§ π΅ = 0) β ((π΄ Γ {π΅}) βf Β· πΉ) β MblFn) |
121 | 13 | adantr 482 |
. . 3
β’ ((π β§ 0 < π΅) β ((π΄ Γ {π΅}) βf Β· πΉ):π΄βΆβ) |
122 | 11 | adantr 482 |
. . 3
β’ ((π β§ 0 < π΅) β π΄ β dom vol) |
123 | | simprl 770 |
. . . . . . . . . . 11
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β π¦ β β) |
124 | 123 | rexrd 11212 |
. . . . . . . . . 10
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β π¦ β β*) |
125 | 124, 18 | syl 17 |
. . . . . . . . 9
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (π¦(,)+β) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β β β§ π¦ < (((π΄ Γ {π΅}) βf Β· πΉ)βπ§)))) |
126 | 20 | ad2ant2rl 748 |
. . . . . . . . . 10
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β β) |
127 | 126 | biantrurd 534 |
. . . . . . . . 9
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β (π¦ < (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β β β§ π¦ < (((π΄ Γ {π΅}) βf Β· πΉ)βπ§)))) |
128 | 23 | ad2ant2rl 748 |
. . . . . . . . . . 11
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β (πΉβπ§) β β) |
129 | 128 | biantrurd 534 |
. . . . . . . . . 10
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β ((π¦ / π΅) < (πΉβπ§) β ((πΉβπ§) β β β§ (π¦ / π΅) < (πΉβπ§)))) |
130 | | eqidd 2738 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π΄) β (πΉβπ§) = (πΉβπ§)) |
131 | 11, 3, 66, 130 | ofc1 7648 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π΄) β (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) = (π΅ Β· (πΉβπ§))) |
132 | 131 | ad2ant2rl 748 |
. . . . . . . . . . . 12
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) = (π΅ Β· (πΉβπ§))) |
133 | 132 | breq2d 5122 |
. . . . . . . . . . 11
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β (π¦ < (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β π¦ < (π΅ Β· (πΉβπ§)))) |
134 | 3 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β π΅ β β) |
135 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β 0 < π΅) |
136 | | ltdivmul 12037 |
. . . . . . . . . . . 12
β’ ((π¦ β β β§ (πΉβπ§) β β β§ (π΅ β β β§ 0 < π΅)) β ((π¦ / π΅) < (πΉβπ§) β π¦ < (π΅ Β· (πΉβπ§)))) |
137 | 123, 128,
134, 135, 136 | syl112anc 1375 |
. . . . . . . . . . 11
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β ((π¦ / π΅) < (πΉβπ§) β π¦ < (π΅ Β· (πΉβπ§)))) |
138 | 133, 137 | bitr4d 282 |
. . . . . . . . . 10
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β (π¦ < (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (π¦ / π΅) < (πΉβπ§))) |
139 | 134, 135 | elrpd 12961 |
. . . . . . . . . . . . 13
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β π΅ β
β+) |
140 | 123, 139 | rerpdivcld 12995 |
. . . . . . . . . . . 12
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β (π¦ / π΅) β β) |
141 | 140 | rexrd 11212 |
. . . . . . . . . . 11
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β (π¦ / π΅) β
β*) |
142 | 141, 89 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β ((πΉβπ§) β ((π¦ / π΅)(,)+β) β ((πΉβπ§) β β β§ (π¦ / π΅) < (πΉβπ§)))) |
143 | 129, 138,
142 | 3bitr4d 311 |
. . . . . . . . 9
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β (π¦ < (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (πΉβπ§) β ((π¦ / π΅)(,)+β))) |
144 | 125, 127,
143 | 3bitr2d 307 |
. . . . . . . 8
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (π¦(,)+β) β (πΉβπ§) β ((π¦ / π΅)(,)+β))) |
145 | 144 | anassrs 469 |
. . . . . . 7
β’ ((((π β§ 0 < π΅) β§ π¦ β β) β§ π§ β π΄) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (π¦(,)+β) β (πΉβπ§) β ((π¦ / π΅)(,)+β))) |
146 | 145 | pm5.32da 580 |
. . . . . 6
β’ (((π β§ 0 < π΅) β§ π¦ β β) β ((π§ β π΄ β§ (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (π¦(,)+β)) β (π§ β π΄ β§ (πΉβπ§) β ((π¦ / π΅)(,)+β)))) |
147 | 62 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ 0 < π΅) β§ π¦ β β) β ((π΄ Γ {π΅}) βf Β· πΉ) Fn π΄) |
148 | 147, 64 | syl 17 |
. . . . . 6
β’ (((π β§ 0 < π΅) β§ π¦ β β) β (π§ β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (π¦(,)+β)) β (π§ β π΄ β§ (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (π¦(,)+β)))) |
149 | 66 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ 0 < π΅) β§ π¦ β β) β πΉ Fn π΄) |
150 | 149, 97 | syl 17 |
. . . . . 6
β’ (((π β§ 0 < π΅) β§ π¦ β β) β (π§ β (β‘πΉ β ((π¦ / π΅)(,)+β)) β (π§ β π΄ β§ (πΉβπ§) β ((π¦ / π΅)(,)+β)))) |
151 | 146, 148,
150 | 3bitr4d 311 |
. . . . 5
β’ (((π β§ 0 < π΅) β§ π¦ β β) β (π§ β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (π¦(,)+β)) β π§ β (β‘πΉ β ((π¦ / π΅)(,)+β)))) |
152 | 151 | eqrdv 2735 |
. . . 4
β’ (((π β§ 0 < π΅) β§ π¦ β β) β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (π¦(,)+β)) = (β‘πΉ β ((π¦ / π΅)(,)+β))) |
153 | 102 | ad2antrr 725 |
. . . 4
β’ (((π β§ 0 < π΅) β§ π¦ β β) β (β‘πΉ β ((π¦ / π΅)(,)+β)) β dom
vol) |
154 | 152, 153 | eqeltrd 2838 |
. . 3
β’ (((π β§ 0 < π΅) β§ π¦ β β) β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (π¦(,)+β)) β dom
vol) |
155 | 124, 76 | syl 17 |
. . . . . . . . 9
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (-β(,)π¦) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β β β§ (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) < π¦))) |
156 | 126 | biantrurd 534 |
. . . . . . . . 9
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) < π¦ β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β β β§ (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) < π¦))) |
157 | | ltmuldiv2 12036 |
. . . . . . . . . . 11
β’ (((πΉβπ§) β β β§ π¦ β β β§ (π΅ β β β§ 0 < π΅)) β ((π΅ Β· (πΉβπ§)) < π¦ β (πΉβπ§) < (π¦ / π΅))) |
158 | 128, 123,
134, 135, 157 | syl112anc 1375 |
. . . . . . . . . 10
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β ((π΅ Β· (πΉβπ§)) < π¦ β (πΉβπ§) < (π¦ / π΅))) |
159 | 132 | breq1d 5120 |
. . . . . . . . . 10
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) < π¦ β (π΅ Β· (πΉβπ§)) < π¦)) |
160 | 141, 56 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β ((πΉβπ§) β (-β(,)(π¦ / π΅)) β ((πΉβπ§) β β β§ (πΉβπ§) < (π¦ / π΅)))) |
161 | 128, 160 | mpbirand 706 |
. . . . . . . . . 10
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β ((πΉβπ§) β (-β(,)(π¦ / π΅)) β (πΉβπ§) < (π¦ / π΅))) |
162 | 158, 159,
161 | 3bitr4d 311 |
. . . . . . . . 9
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) < π¦ β (πΉβπ§) β (-β(,)(π¦ / π΅)))) |
163 | 155, 156,
162 | 3bitr2d 307 |
. . . . . . . 8
β’ (((π β§ 0 < π΅) β§ (π¦ β β β§ π§ β π΄)) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (-β(,)π¦) β (πΉβπ§) β (-β(,)(π¦ / π΅)))) |
164 | 163 | anassrs 469 |
. . . . . . 7
β’ ((((π β§ 0 < π΅) β§ π¦ β β) β§ π§ β π΄) β ((((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (-β(,)π¦) β (πΉβπ§) β (-β(,)(π¦ / π΅)))) |
165 | 164 | pm5.32da 580 |
. . . . . 6
β’ (((π β§ 0 < π΅) β§ π¦ β β) β ((π§ β π΄ β§ (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (-β(,)π¦)) β (π§ β π΄ β§ (πΉβπ§) β (-β(,)(π¦ / π΅))))) |
166 | 147, 95 | syl 17 |
. . . . . 6
β’ (((π β§ 0 < π΅) β§ π¦ β β) β (π§ β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (-β(,)π¦)) β (π§ β π΄ β§ (((π΄ Γ {π΅}) βf Β· πΉ)βπ§) β (-β(,)π¦)))) |
167 | 149, 68 | syl 17 |
. . . . . 6
β’ (((π β§ 0 < π΅) β§ π¦ β β) β (π§ β (β‘πΉ β (-β(,)(π¦ / π΅))) β (π§ β π΄ β§ (πΉβπ§) β (-β(,)(π¦ / π΅))))) |
168 | 165, 166,
167 | 3bitr4d 311 |
. . . . 5
β’ (((π β§ 0 < π΅) β§ π¦ β β) β (π§ β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (-β(,)π¦)) β π§ β (β‘πΉ β (-β(,)(π¦ / π΅))))) |
169 | 168 | eqrdv 2735 |
. . . 4
β’ (((π β§ 0 < π΅) β§ π¦ β β) β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (-β(,)π¦)) = (β‘πΉ β (-β(,)(π¦ / π΅)))) |
170 | 73 | ad2antrr 725 |
. . . 4
β’ (((π β§ 0 < π΅) β§ π¦ β β) β (β‘πΉ β (-β(,)(π¦ / π΅))) β dom vol) |
171 | 169, 170 | eqeltrd 2838 |
. . 3
β’ (((π β§ 0 < π΅) β§ π¦ β β) β (β‘((π΄ Γ {π΅}) βf Β· πΉ) β (-β(,)π¦)) β dom
vol) |
172 | 121, 122,
154, 171 | ismbf2d 25020 |
. 2
β’ ((π β§ 0 < π΅) β ((π΄ Γ {π΅}) βf Β· πΉ) β MblFn) |
173 | | 0re 11164 |
. . 3
β’ 0 β
β |
174 | | lttri4 11246 |
. . 3
β’ ((π΅ β β β§ 0 β
β) β (π΅ < 0
β¨ π΅ = 0 β¨ 0 <
π΅)) |
175 | 3, 173, 174 | sylancl 587 |
. 2
β’ (π β (π΅ < 0 β¨ π΅ = 0 β¨ 0 < π΅)) |
176 | 105, 120,
172, 175 | mpjao3dan 1432 |
1
β’ (π β ((π΄ Γ {π΅}) βf Β· πΉ) β MblFn) |