Step | Hyp | Ref
| Expression |
1 | | ismbf3d.1 |
. 2
β’ (π β πΉ:π΄βΆβ) |
2 | | fimacnv 6737 |
. . . 4
β’ (πΉ:π΄βΆβ β (β‘πΉ β β) = π΄) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β (β‘πΉ β β) = π΄) |
4 | | imaiun 7241 |
. . . . 5
β’ (β‘πΉ β βͺ
π¦ β β (-π¦(,)+β)) = βͺ π¦ β β (β‘πΉ β (-π¦(,)+β)) |
5 | | ioossre 13382 |
. . . . . . . . 9
β’ (-π¦(,)+β) β
β |
6 | 5 | rgenw 3066 |
. . . . . . . 8
β’
βπ¦ β
β (-π¦(,)+β)
β β |
7 | | iunss 5048 |
. . . . . . . 8
β’ (βͺ π¦ β β (-π¦(,)+β) β β β
βπ¦ β β
(-π¦(,)+β) β
β) |
8 | 6, 7 | mpbir 230 |
. . . . . . 7
β’ βͺ π¦ β β (-π¦(,)+β) β β |
9 | | renegcl 11520 |
. . . . . . . . . . 11
β’ (π§ β β β -π§ β
β) |
10 | | arch 12466 |
. . . . . . . . . . 11
β’ (-π§ β β β
βπ¦ β β
-π§ < π¦) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
β’ (π§ β β β
βπ¦ β β
-π§ < π¦) |
12 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π§ β β β§ π¦ β β) β π§ β
β) |
13 | 12 | biantrurd 534 |
. . . . . . . . . . . 12
β’ ((π§ β β β§ π¦ β β) β (-π¦ < π§ β (π§ β β β§ -π¦ < π§))) |
14 | | nnre 12216 |
. . . . . . . . . . . . 13
β’ (π¦ β β β π¦ β
β) |
15 | | ltnegcon1 11712 |
. . . . . . . . . . . . 13
β’ ((π§ β β β§ π¦ β β) β (-π§ < π¦ β -π¦ < π§)) |
16 | 14, 15 | sylan2 594 |
. . . . . . . . . . . 12
β’ ((π§ β β β§ π¦ β β) β (-π§ < π¦ β -π¦ < π§)) |
17 | 14 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π§ β β β§ π¦ β β) β π¦ β
β) |
18 | 17 | renegcld 11638 |
. . . . . . . . . . . . . 14
β’ ((π§ β β β§ π¦ β β) β -π¦ β
β) |
19 | 18 | rexrd 11261 |
. . . . . . . . . . . . 13
β’ ((π§ β β β§ π¦ β β) β -π¦ β
β*) |
20 | | elioopnf 13417 |
. . . . . . . . . . . . 13
β’ (-π¦ β β*
β (π§ β (-π¦(,)+β) β (π§ β β β§ -π¦ < π§))) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . 12
β’ ((π§ β β β§ π¦ β β) β (π§ β (-π¦(,)+β) β (π§ β β β§ -π¦ < π§))) |
22 | 13, 16, 21 | 3bitr4d 311 |
. . . . . . . . . . 11
β’ ((π§ β β β§ π¦ β β) β (-π§ < π¦ β π§ β (-π¦(,)+β))) |
23 | 22 | rexbidva 3177 |
. . . . . . . . . 10
β’ (π§ β β β
(βπ¦ β β
-π§ < π¦ β βπ¦ β β π§ β (-π¦(,)+β))) |
24 | 11, 23 | mpbid 231 |
. . . . . . . . 9
β’ (π§ β β β
βπ¦ β β
π§ β (-π¦(,)+β)) |
25 | | eliun 5001 |
. . . . . . . . 9
β’ (π§ β βͺ π¦ β β (-π¦(,)+β) β βπ¦ β β π§ β (-π¦(,)+β)) |
26 | 24, 25 | sylibr 233 |
. . . . . . . 8
β’ (π§ β β β π§ β βͺ π¦ β β (-π¦(,)+β)) |
27 | 26 | ssriv 3986 |
. . . . . . 7
β’ β
β βͺ π¦ β β (-π¦(,)+β) |
28 | 8, 27 | eqssi 3998 |
. . . . . 6
β’ βͺ π¦ β β (-π¦(,)+β) = β |
29 | 28 | imaeq2i 6056 |
. . . . 5
β’ (β‘πΉ β βͺ
π¦ β β (-π¦(,)+β)) = (β‘πΉ β β) |
30 | 4, 29 | eqtr3i 2763 |
. . . 4
β’ βͺ π¦ β β (β‘πΉ β (-π¦(,)+β)) = (β‘πΉ β β) |
31 | | ismbf3d.2 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (β‘πΉ β (π₯(,)+β)) β dom
vol) |
32 | 31 | ralrimiva 3147 |
. . . . . . 7
β’ (π β βπ₯ β β (β‘πΉ β (π₯(,)+β)) β dom
vol) |
33 | 14 | renegcld 11638 |
. . . . . . 7
β’ (π¦ β β β -π¦ β
β) |
34 | | oveq1 7413 |
. . . . . . . . . 10
β’ (π₯ = -π¦ β (π₯(,)+β) = (-π¦(,)+β)) |
35 | 34 | imaeq2d 6058 |
. . . . . . . . 9
β’ (π₯ = -π¦ β (β‘πΉ β (π₯(,)+β)) = (β‘πΉ β (-π¦(,)+β))) |
36 | 35 | eleq1d 2819 |
. . . . . . . 8
β’ (π₯ = -π¦ β ((β‘πΉ β (π₯(,)+β)) β dom vol β (β‘πΉ β (-π¦(,)+β)) β dom
vol)) |
37 | 36 | rspccva 3612 |
. . . . . . 7
β’
((βπ₯ β
β (β‘πΉ β (π₯(,)+β)) β dom vol β§ -π¦ β β) β (β‘πΉ β (-π¦(,)+β)) β dom
vol) |
38 | 32, 33, 37 | syl2an 597 |
. . . . . 6
β’ ((π β§ π¦ β β) β (β‘πΉ β (-π¦(,)+β)) β dom
vol) |
39 | 38 | ralrimiva 3147 |
. . . . 5
β’ (π β βπ¦ β β (β‘πΉ β (-π¦(,)+β)) β dom
vol) |
40 | | iunmbl 25062 |
. . . . 5
β’
(βπ¦ β
β (β‘πΉ β (-π¦(,)+β)) β dom vol β βͺ π¦ β β (β‘πΉ β (-π¦(,)+β)) β dom
vol) |
41 | 39, 40 | syl 17 |
. . . 4
β’ (π β βͺ π¦ β β (β‘πΉ β (-π¦(,)+β)) β dom
vol) |
42 | 30, 41 | eqeltrrid 2839 |
. . 3
β’ (π β (β‘πΉ β β) β dom
vol) |
43 | 3, 42 | eqeltrrd 2835 |
. 2
β’ (π β π΄ β dom vol) |
44 | | imaiun 7241 |
. . . . . . 7
β’ (β‘πΉ β βͺ
π¦ β β
(-β(,](π§ β (1 /
π¦)))) = βͺ π¦ β β (β‘πΉ β (-β(,](π§ β (1 / π¦)))) |
45 | | eliun 5001 |
. . . . . . . . . 10
β’ (π₯ β βͺ π¦ β β (-β(,](π§ β (1 / π¦))) β βπ¦ β β π₯ β (-β(,](π§ β (1 / π¦)))) |
46 | | 3simpb 1150 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ -β
< π₯ β§ π₯ β€ (π§ β (1 / π¦))) β (π₯ β β β§ π₯ β€ (π§ β (1 / π¦)))) |
47 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π§ β β) β§ (π¦ β β β§ π₯ β β)) β π§ β β) |
48 | | nnrp 12982 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ β β β π¦ β
β+) |
49 | 48 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π§ β β) β§ (π¦ β β β§ π₯ β β)) β π¦ β β+) |
50 | 49 | rpreccld 13023 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π§ β β) β§ (π¦ β β β§ π₯ β β)) β (1 / π¦) β
β+) |
51 | 47, 50 | ltsubrpd 13045 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π§ β β) β§ (π¦ β β β§ π₯ β β)) β (π§ β (1 / π¦)) < π§) |
52 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π§ β β) β§ (π¦ β β β§ π₯ β β)) β π₯ β β) |
53 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π§ β β) β π§ β β) |
54 | | nnrecre 12251 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ β β β (1 /
π¦) β
β) |
55 | | resubcl 11521 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π§ β β β§ (1 / π¦) β β) β (π§ β (1 / π¦)) β β) |
56 | 53, 54, 55 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π§ β β) β§ π¦ β β) β (π§ β (1 / π¦)) β β) |
57 | 56 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π§ β β) β§ (π¦ β β β§ π₯ β β)) β (π§ β (1 / π¦)) β β) |
58 | | lelttr 11301 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β β β§ (π§ β (1 / π¦)) β β β§ π§ β β) β ((π₯ β€ (π§ β (1 / π¦)) β§ (π§ β (1 / π¦)) < π§) β π₯ < π§)) |
59 | 52, 57, 47, 58 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π§ β β) β§ (π¦ β β β§ π₯ β β)) β ((π₯ β€ (π§ β (1 / π¦)) β§ (π§ β (1 / π¦)) < π§) β π₯ < π§)) |
60 | 51, 59 | mpan2d 693 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π§ β β) β§ (π¦ β β β§ π₯ β β)) β (π₯ β€ (π§ β (1 / π¦)) β π₯ < π§)) |
61 | 60 | anassrs 469 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π§ β β) β§ π¦ β β) β§ π₯ β β) β (π₯ β€ (π§ β (1 / π¦)) β π₯ < π§)) |
62 | 61 | imdistanda 573 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β β) β§ π¦ β β) β ((π₯ β β β§ π₯ β€ (π§ β (1 / π¦))) β (π₯ β β β§ π₯ < π§))) |
63 | 46, 62 | syl5 34 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β β) β§ π¦ β β) β ((π₯ β β β§ -β < π₯ β§ π₯ β€ (π§ β (1 / π¦))) β (π₯ β β β§ π₯ < π§))) |
64 | | mnfxr 11268 |
. . . . . . . . . . . . . . . 16
β’ -β
β β* |
65 | | elioc2 13384 |
. . . . . . . . . . . . . . . 16
β’
((-β β β* β§ (π§ β (1 / π¦)) β β) β (π₯ β (-β(,](π§ β (1 / π¦))) β (π₯ β β β§ -β < π₯ β§ π₯ β€ (π§ β (1 / π¦))))) |
66 | 64, 56, 65 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β β) β§ π¦ β β) β (π₯ β (-β(,](π§ β (1 / π¦))) β (π₯ β β β§ -β < π₯ β§ π₯ β€ (π§ β (1 / π¦))))) |
67 | | rexr 11257 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β β β π§ β
β*) |
68 | 67 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β β) β π§ β β*) |
69 | | elioomnf 13418 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β β*
β (π₯ β
(-β(,)π§) β
(π₯ β β β§
π₯ < π§))) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π§ β β) β (π₯ β (-β(,)π§) β (π₯ β β β§ π₯ < π§))) |
71 | 70 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β β) β§ π¦ β β) β (π₯ β (-β(,)π§) β (π₯ β β β§ π₯ < π§))) |
72 | 63, 66, 71 | 3imtr4d 294 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β β) β§ π¦ β β) β (π₯ β (-β(,](π§ β (1 / π¦))) β π₯ β (-β(,)π§))) |
73 | 72 | rexlimdva 3156 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β β) β (βπ¦ β β π₯ β (-β(,](π§ β (1 / π¦))) β π₯ β (-β(,)π§))) |
74 | 73, 70 | sylibd 238 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β β) β (βπ¦ β β π₯ β (-β(,](π§ β (1 / π¦))) β (π₯ β β β§ π₯ < π§))) |
75 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β π₯ β β) |
76 | 75 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β§ (π¦ β β β§ (1 / π¦) < (π§ β π₯))) β π₯ β β) |
77 | 76 | mnfltd 13101 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β§ (π¦ β β β§ (1 / π¦) < (π§ β π₯))) β -β < π₯) |
78 | 56 | ad2ant2r 746 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β§ (π¦ β β β§ (1 / π¦) < (π§ β π₯))) β (π§ β (1 / π¦)) β β) |
79 | 54 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β§ (π¦ β β β§ (1 / π¦) < (π§ β π₯))) β (1 / π¦) β β) |
80 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β π§ β β) |
81 | 80 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β§ (π¦ β β β§ (1 / π¦) < (π§ β π₯))) β π§ β β) |
82 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β§ (π¦ β β β§ (1 / π¦) < (π§ β π₯))) β (1 / π¦) < (π§ β π₯)) |
83 | 79, 81, 76, 82 | ltsub13d 11817 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β§ (π¦ β β β§ (1 / π¦) < (π§ β π₯))) β π₯ < (π§ β (1 / π¦))) |
84 | 76, 78, 83 | ltled 11359 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β§ (π¦ β β β§ (1 / π¦) < (π§ β π₯))) β π₯ β€ (π§ β (1 / π¦))) |
85 | 66 | ad2ant2r 746 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β§ (π¦ β β β§ (1 / π¦) < (π§ β π₯))) β (π₯ β (-β(,](π§ β (1 / π¦))) β (π₯ β β β§ -β < π₯ β§ π₯ β€ (π§ β (1 / π¦))))) |
86 | 76, 77, 84, 85 | mpbir3and 1343 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β§ (π¦ β β β§ (1 / π¦) < (π§ β π₯))) β π₯ β (-β(,](π§ β (1 / π¦)))) |
87 | 80, 75 | resubcld 11639 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β (π§ β π₯) β β) |
88 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β π₯ < π§) |
89 | 75, 80 | posdifd 11798 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β (π₯ < π§ β 0 < (π§ β π₯))) |
90 | 88, 89 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β 0 < (π§ β π₯)) |
91 | | nnrecl 12467 |
. . . . . . . . . . . . . . 15
β’ (((π§ β π₯) β β β§ 0 < (π§ β π₯)) β βπ¦ β β (1 / π¦) < (π§ β π₯)) |
92 | 87, 90, 91 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β βπ¦ β β (1 / π¦) < (π§ β π₯)) |
93 | 86, 92 | reximddv 3172 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β β) β§ (π₯ β β β§ π₯ < π§)) β βπ¦ β β π₯ β (-β(,](π§ β (1 / π¦)))) |
94 | 93 | ex 414 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β β) β ((π₯ β β β§ π₯ < π§) β βπ¦ β β π₯ β (-β(,](π§ β (1 / π¦))))) |
95 | 74, 94 | impbid 211 |
. . . . . . . . . . 11
β’ ((π β§ π§ β β) β (βπ¦ β β π₯ β (-β(,](π§ β (1 / π¦))) β (π₯ β β β§ π₯ < π§))) |
96 | 95, 70 | bitr4d 282 |
. . . . . . . . . 10
β’ ((π β§ π§ β β) β (βπ¦ β β π₯ β (-β(,](π§ β (1 / π¦))) β π₯ β (-β(,)π§))) |
97 | 45, 96 | bitrid 283 |
. . . . . . . . 9
β’ ((π β§ π§ β β) β (π₯ β βͺ
π¦ β β
(-β(,](π§ β (1 /
π¦))) β π₯ β (-β(,)π§))) |
98 | 97 | eqrdv 2731 |
. . . . . . . 8
β’ ((π β§ π§ β β) β βͺ π¦ β β (-β(,](π§ β (1 / π¦))) = (-β(,)π§)) |
99 | 98 | imaeq2d 6058 |
. . . . . . 7
β’ ((π β§ π§ β β) β (β‘πΉ β βͺ
π¦ β β
(-β(,](π§ β (1 /
π¦)))) = (β‘πΉ β (-β(,)π§))) |
100 | 44, 99 | eqtr3id 2787 |
. . . . . 6
β’ ((π β§ π§ β β) β βͺ π¦ β β (β‘πΉ β (-β(,](π§ β (1 / π¦)))) = (β‘πΉ β (-β(,)π§))) |
101 | 1 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π¦ β β) β πΉ:π΄βΆβ) |
102 | | ffun 6718 |
. . . . . . . . . . 11
β’ (πΉ:π΄βΆβ β Fun πΉ) |
103 | | funcnvcnv 6613 |
. . . . . . . . . . 11
β’ (Fun
πΉ β Fun β‘β‘πΉ) |
104 | | imadif 6630 |
. . . . . . . . . . 11
β’ (Fun
β‘β‘πΉ β (β‘πΉ β (β β ((π§ β (1 / π¦))(,)+β))) = ((β‘πΉ β β) β (β‘πΉ β ((π§ β (1 / π¦))(,)+β)))) |
105 | 101, 102,
103, 104 | 4syl 19 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π¦ β β) β (β‘πΉ β (β β ((π§ β (1 / π¦))(,)+β))) = ((β‘πΉ β β) β (β‘πΉ β ((π§ β (1 / π¦))(,)+β)))) |
106 | 64 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β β) β§ π¦ β β) β -β β
β*) |
107 | 56 | rexrd 11261 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β β) β§ π¦ β β) β (π§ β (1 / π¦)) β
β*) |
108 | | pnfxr 11265 |
. . . . . . . . . . . . . . 15
β’ +β
β β* |
109 | 108 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β β) β§ π¦ β β) β +β β
β*) |
110 | 56 | mnfltd 13101 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β β) β§ π¦ β β) β -β < (π§ β (1 / π¦))) |
111 | 56 | ltpnfd 13098 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β β) β§ π¦ β β) β (π§ β (1 / π¦)) < +β) |
112 | | df-ioc 13326 |
. . . . . . . . . . . . . . 15
β’ (,] =
(π’ β
β*, π£
β β* β¦ {π€ β β* β£ (π’ < π€ β§ π€ β€ π£)}) |
113 | | df-ioo 13325 |
. . . . . . . . . . . . . . 15
β’ (,) =
(π’ β
β*, π£
β β* β¦ {π€ β β* β£ (π’ < π€ β§ π€ < π£)}) |
114 | | xrltnle 11278 |
. . . . . . . . . . . . . . 15
β’ (((π§ β (1 / π¦)) β β* β§ π₯ β β*)
β ((π§ β (1 /
π¦)) < π₯ β Β¬ π₯ β€ (π§ β (1 / π¦)))) |
115 | | xrlelttr 13132 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β*
β§ (π§ β (1 / π¦)) β β*
β§ +β β β*) β ((π₯ β€ (π§ β (1 / π¦)) β§ (π§ β (1 / π¦)) < +β) β π₯ < +β)) |
116 | | xrlttr 13116 |
. . . . . . . . . . . . . . 15
β’
((-β β β* β§ (π§ β (1 / π¦)) β β* β§ π₯ β β*)
β ((-β < (π§
β (1 / π¦)) β§
(π§ β (1 / π¦)) < π₯) β -β < π₯)) |
117 | 112, 113,
114, 113, 115, 116 | ixxun 13337 |
. . . . . . . . . . . . . 14
β’
(((-β β β* β§ (π§ β (1 / π¦)) β β* β§ +β
β β*) β§ (-β < (π§ β (1 / π¦)) β§ (π§ β (1 / π¦)) < +β)) β ((-β(,](π§ β (1 / π¦))) βͺ ((π§ β (1 / π¦))(,)+β)) =
(-β(,)+β)) |
118 | 106, 107,
109, 110, 111, 117 | syl32anc 1379 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β β) β§ π¦ β β) β ((-β(,](π§ β (1 / π¦))) βͺ ((π§ β (1 / π¦))(,)+β)) =
(-β(,)+β)) |
119 | | uncom 4153 |
. . . . . . . . . . . . 13
β’
((-β(,](π§
β (1 / π¦))) βͺ
((π§ β (1 / π¦))(,)+β)) = (((π§ β (1 / π¦))(,)+β) βͺ (-β(,](π§ β (1 / π¦)))) |
120 | | ioomax 13396 |
. . . . . . . . . . . . 13
β’
(-β(,)+β) = β |
121 | 118, 119,
120 | 3eqtr3g 2796 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β β) β§ π¦ β β) β (((π§ β (1 / π¦))(,)+β) βͺ (-β(,](π§ β (1 / π¦)))) = β) |
122 | | ioossre 13382 |
. . . . . . . . . . . . 13
β’ ((π§ β (1 / π¦))(,)+β) β
β |
123 | | incom 4201 |
. . . . . . . . . . . . . 14
β’ (((π§ β (1 / π¦))(,)+β) β© (-β(,](π§ β (1 / π¦)))) = ((-β(,](π§ β (1 / π¦))) β© ((π§ β (1 / π¦))(,)+β)) |
124 | 112, 113,
114 | ixxdisj 13336 |
. . . . . . . . . . . . . . . 16
β’
((-β β β* β§ (π§ β (1 / π¦)) β β* β§ +β
β β*) β ((-β(,](π§ β (1 / π¦))) β© ((π§ β (1 / π¦))(,)+β)) = β
) |
125 | 64, 108, 124 | mp3an13 1453 |
. . . . . . . . . . . . . . 15
β’ ((π§ β (1 / π¦)) β β* β
((-β(,](π§ β (1
/ π¦))) β© ((π§ β (1 / π¦))(,)+β)) = β
) |
126 | 107, 125 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β β) β§ π¦ β β) β ((-β(,](π§ β (1 / π¦))) β© ((π§ β (1 / π¦))(,)+β)) = β
) |
127 | 123, 126 | eqtrid 2785 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β β) β§ π¦ β β) β (((π§ β (1 / π¦))(,)+β) β© (-β(,](π§ β (1 / π¦)))) = β
) |
128 | | uneqdifeq 4492 |
. . . . . . . . . . . . 13
β’ ((((π§ β (1 / π¦))(,)+β) β β β§ (((π§ β (1 / π¦))(,)+β) β© (-β(,](π§ β (1 / π¦)))) = β
) β ((((π§ β (1 / π¦))(,)+β) βͺ (-β(,](π§ β (1 / π¦)))) = β β (β β
((π§ β (1 / π¦))(,)+β)) =
(-β(,](π§ β (1 /
π¦))))) |
129 | 122, 127,
128 | sylancr 588 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β β) β§ π¦ β β) β ((((π§ β (1 / π¦))(,)+β) βͺ (-β(,](π§ β (1 / π¦)))) = β β (β β
((π§ β (1 / π¦))(,)+β)) =
(-β(,](π§ β (1 /
π¦))))) |
130 | 121, 129 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π¦ β β) β (β β
((π§ β (1 / π¦))(,)+β)) =
(-β(,](π§ β (1 /
π¦)))) |
131 | 130 | imaeq2d 6058 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π¦ β β) β (β‘πΉ β (β β ((π§ β (1 / π¦))(,)+β))) = (β‘πΉ β (-β(,](π§ β (1 / π¦))))) |
132 | 105, 131 | eqtr3d 2775 |
. . . . . . . . 9
β’ (((π β§ π§ β β) β§ π¦ β β) β ((β‘πΉ β β) β (β‘πΉ β ((π§ β (1 / π¦))(,)+β))) = (β‘πΉ β (-β(,](π§ β (1 / π¦))))) |
133 | 42 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π¦ β β) β (β‘πΉ β β) β dom
vol) |
134 | | oveq1 7413 |
. . . . . . . . . . . . 13
β’ (π₯ = (π§ β (1 / π¦)) β (π₯(,)+β) = ((π§ β (1 / π¦))(,)+β)) |
135 | 134 | imaeq2d 6058 |
. . . . . . . . . . . 12
β’ (π₯ = (π§ β (1 / π¦)) β (β‘πΉ β (π₯(,)+β)) = (β‘πΉ β ((π§ β (1 / π¦))(,)+β))) |
136 | 135 | eleq1d 2819 |
. . . . . . . . . . 11
β’ (π₯ = (π§ β (1 / π¦)) β ((β‘πΉ β (π₯(,)+β)) β dom vol β (β‘πΉ β ((π§ β (1 / π¦))(,)+β)) β dom
vol)) |
137 | 32 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π¦ β β) β βπ₯ β β (β‘πΉ β (π₯(,)+β)) β dom
vol) |
138 | 136, 137,
56 | rspcdva 3614 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π¦ β β) β (β‘πΉ β ((π§ β (1 / π¦))(,)+β)) β dom
vol) |
139 | | difmbl 25052 |
. . . . . . . . . 10
β’ (((β‘πΉ β β) β dom vol β§
(β‘πΉ β ((π§ β (1 / π¦))(,)+β)) β dom vol) β
((β‘πΉ β β) β (β‘πΉ β ((π§ β (1 / π¦))(,)+β))) β dom
vol) |
140 | 133, 138,
139 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π§ β β) β§ π¦ β β) β ((β‘πΉ β β) β (β‘πΉ β ((π§ β (1 / π¦))(,)+β))) β dom
vol) |
141 | 132, 140 | eqeltrrd 2835 |
. . . . . . . 8
β’ (((π β§ π§ β β) β§ π¦ β β) β (β‘πΉ β (-β(,](π§ β (1 / π¦)))) β dom vol) |
142 | 141 | ralrimiva 3147 |
. . . . . . 7
β’ ((π β§ π§ β β) β βπ¦ β β (β‘πΉ β (-β(,](π§ β (1 / π¦)))) β dom vol) |
143 | | iunmbl 25062 |
. . . . . . 7
β’
(βπ¦ β
β (β‘πΉ β (-β(,](π§ β (1 / π¦)))) β dom vol β βͺ π¦ β β (β‘πΉ β (-β(,](π§ β (1 / π¦)))) β dom vol) |
144 | 142, 143 | syl 17 |
. . . . . 6
β’ ((π β§ π§ β β) β βͺ π¦ β β (β‘πΉ β (-β(,](π§ β (1 / π¦)))) β dom vol) |
145 | 100, 144 | eqeltrrd 2835 |
. . . . 5
β’ ((π β§ π§ β β) β (β‘πΉ β (-β(,)π§)) β dom vol) |
146 | 145 | ralrimiva 3147 |
. . . 4
β’ (π β βπ§ β β (β‘πΉ β (-β(,)π§)) β dom vol) |
147 | | oveq2 7414 |
. . . . . . 7
β’ (π§ = π₯ β (-β(,)π§) = (-β(,)π₯)) |
148 | 147 | imaeq2d 6058 |
. . . . . 6
β’ (π§ = π₯ β (β‘πΉ β (-β(,)π§)) = (β‘πΉ β (-β(,)π₯))) |
149 | 148 | eleq1d 2819 |
. . . . 5
β’ (π§ = π₯ β ((β‘πΉ β (-β(,)π§)) β dom vol β (β‘πΉ β (-β(,)π₯)) β dom vol)) |
150 | 149 | cbvralvw 3235 |
. . . 4
β’
(βπ§ β
β (β‘πΉ β (-β(,)π§)) β dom vol β βπ₯ β β (β‘πΉ β (-β(,)π₯)) β dom vol) |
151 | 146, 150 | sylib 217 |
. . 3
β’ (π β βπ₯ β β (β‘πΉ β (-β(,)π₯)) β dom vol) |
152 | 151 | r19.21bi 3249 |
. 2
β’ ((π β§ π₯ β β) β (β‘πΉ β (-β(,)π₯)) β dom vol) |
153 | 1, 43, 31, 152 | ismbf2d 25149 |
1
β’ (π β πΉ β MblFn) |