Step | Hyp | Ref
| Expression |
1 | | mbfpos.1 |
. . 3
β’ ((π β§ π₯ β π΄) β π΅ β β) |
2 | 1 | fmpttd 7068 |
. 2
β’ (π β (π₯ β π΄ β¦ π΅):π΄βΆβ) |
3 | | mbfposr.2 |
. . 3
β’ (π β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn) |
4 | | 0re 11164 |
. . . 4
β’ 0 β
β |
5 | | ifcl 4536 |
. . . 4
β’ ((π΅ β β β§ 0 β
β) β if(0 β€ π΅, π΅, 0) β β) |
6 | 1, 4, 5 | sylancl 587 |
. . 3
β’ ((π β§ π₯ β π΄) β if(0 β€ π΅, π΅, 0) β β) |
7 | 3, 6 | mbfdm2 25017 |
. 2
β’ (π β π΄ β dom vol) |
8 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β π¦ < 0) |
9 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β π¦ β β) |
10 | 9 | lt0neg1d 11731 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β (π¦ < 0 β 0 < -π¦)) |
11 | 8, 10 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β 0 < -π¦) |
12 | 11 | biantrurd 534 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β (-π΅ < -π¦ β (0 < -π¦ β§ -π΅ < -π¦))) |
13 | 1 | ad4ant14 751 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β π΅ β β) |
14 | 9, 13 | ltnegd 11740 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β (π¦ < π΅ β -π΅ < -π¦)) |
15 | | 0red 11165 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β 0 β β) |
16 | 13 | renegcld 11589 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β -π΅ β β) |
17 | 9 | renegcld 11589 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β -π¦ β β) |
18 | | maxlt 13119 |
. . . . . . . . . . . . 13
β’ ((0
β β β§ -π΅
β β β§ -π¦
β β) β (if(0 β€ -π΅, -π΅, 0) < -π¦ β (0 < -π¦ β§ -π΅ < -π¦))) |
19 | 15, 16, 17, 18 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β (if(0 β€ -π΅, -π΅, 0) < -π¦ β (0 < -π¦ β§ -π΅ < -π¦))) |
20 | 12, 14, 19 | 3bitr4rd 312 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β (if(0 β€ -π΅, -π΅, 0) < -π¦ β π¦ < π΅)) |
21 | 1 | renegcld 11589 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π΄) β -π΅ β β) |
22 | | ifcl 4536 |
. . . . . . . . . . . . . 14
β’ ((-π΅ β β β§ 0 β
β) β if(0 β€ -π΅, -π΅, 0) β β) |
23 | 21, 4, 22 | sylancl 587 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β if(0 β€ -π΅, -π΅, 0) β β) |
24 | 23 | ad4ant14 751 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β if(0 β€ -π΅, -π΅, 0) β β) |
25 | 24 | biantrurd 534 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β (if(0 β€ -π΅, -π΅, 0) < -π¦ β (if(0 β€ -π΅, -π΅, 0) β β β§ if(0 β€ -π΅, -π΅, 0) < -π¦))) |
26 | 13 | biantrurd 534 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β (π¦ < π΅ β (π΅ β β β§ π¦ < π΅))) |
27 | 20, 25, 26 | 3bitr3d 309 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β ((if(0 β€ -π΅, -π΅, 0) β β β§ if(0 β€ -π΅, -π΅, 0) < -π¦) β (π΅ β β β§ π¦ < π΅))) |
28 | 17 | rexrd 11212 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β -π¦ β β*) |
29 | | elioomnf 13368 |
. . . . . . . . . . 11
β’ (-π¦ β β*
β (if(0 β€ -π΅,
-π΅, 0) β
(-β(,)-π¦) β
(if(0 β€ -π΅, -π΅, 0) β β β§ if(0
β€ -π΅, -π΅, 0) < -π¦))) |
30 | 28, 29 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β (if(0 β€ -π΅, -π΅, 0) β (-β(,)-π¦) β (if(0 β€ -π΅, -π΅, 0) β β β§ if(0 β€ -π΅, -π΅, 0) < -π¦))) |
31 | 9 | rexrd 11212 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β π¦ β β*) |
32 | | elioopnf 13367 |
. . . . . . . . . . 11
β’ (π¦ β β*
β (π΅ β (π¦(,)+β) β (π΅ β β β§ π¦ < π΅))) |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β (π΅ β (π¦(,)+β) β (π΅ β β β§ π¦ < π΅))) |
34 | 27, 30, 33 | 3bitr4d 311 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β (if(0 β€ -π΅, -π΅, 0) β (-β(,)-π¦) β π΅ β (π¦(,)+β))) |
35 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β π₯ β π΄) |
36 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) = (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) |
37 | 36 | fvmpt2 6964 |
. . . . . . . . . . . 12
β’ ((π₯ β π΄ β§ if(0 β€ -π΅, -π΅, 0) β β) β ((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))βπ₯) = if(0 β€ -π΅, -π΅, 0)) |
38 | 35, 23, 37 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β ((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))βπ₯) = if(0 β€ -π΅, -π΅, 0)) |
39 | 38 | eleq1d 2823 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))βπ₯) β (-β(,)-π¦) β if(0 β€ -π΅, -π΅, 0) β (-β(,)-π¦))) |
40 | 39 | ad4ant14 751 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β (((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))βπ₯) β (-β(,)-π¦) β if(0 β€ -π΅, -π΅, 0) β (-β(,)-π¦))) |
41 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π₯ β π΄ β¦ π΅) = (π₯ β π΄ β¦ π΅) |
42 | 41 | fvmpt2 6964 |
. . . . . . . . . . . 12
β’ ((π₯ β π΄ β§ π΅ β β) β ((π₯ β π΄ β¦ π΅)βπ₯) = π΅) |
43 | 35, 1, 42 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β ((π₯ β π΄ β¦ π΅)βπ₯) = π΅) |
44 | 43 | eleq1d 2823 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (((π₯ β π΄ β¦ π΅)βπ₯) β (π¦(,)+β) β π΅ β (π¦(,)+β))) |
45 | 44 | ad4ant14 751 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β (((π₯ β π΄ β¦ π΅)βπ₯) β (π¦(,)+β) β π΅ β (π¦(,)+β))) |
46 | 34, 40, 45 | 3bitr4d 311 |
. . . . . . . 8
β’ ((((π β§ π¦ β β) β§ π¦ < 0) β§ π₯ β π΄) β (((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))βπ₯) β (-β(,)-π¦) β ((π₯ β π΄ β¦ π΅)βπ₯) β (π¦(,)+β))) |
47 | 46 | pm5.32da 580 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ π¦ < 0) β ((π₯ β π΄ β§ ((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))βπ₯) β (-β(,)-π¦)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ π΅)βπ₯) β (π¦(,)+β)))) |
48 | 23 | fmpttd 7068 |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)):π΄βΆβ) |
49 | | ffn 6673 |
. . . . . . . . 9
β’ ((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)):π΄βΆβ β (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) Fn π΄) |
50 | | elpreima 7013 |
. . . . . . . . 9
β’ ((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) Fn π΄ β (π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-β(,)-π¦)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))βπ₯) β (-β(,)-π¦)))) |
51 | 48, 49, 50 | 3syl 18 |
. . . . . . . 8
β’ (π β (π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-β(,)-π¦)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))βπ₯) β (-β(,)-π¦)))) |
52 | 51 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ π¦ < 0) β (π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-β(,)-π¦)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))βπ₯) β (-β(,)-π¦)))) |
53 | | ffn 6673 |
. . . . . . . . 9
β’ ((π₯ β π΄ β¦ π΅):π΄βΆβ β (π₯ β π΄ β¦ π΅) Fn π΄) |
54 | | elpreima 7013 |
. . . . . . . . 9
β’ ((π₯ β π΄ β¦ π΅) Fn π΄ β (π₯ β (β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ π΅)βπ₯) β (π¦(,)+β)))) |
55 | 2, 53, 54 | 3syl 18 |
. . . . . . . 8
β’ (π β (π₯ β (β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ π΅)βπ₯) β (π¦(,)+β)))) |
56 | 55 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ π¦ < 0) β (π₯ β (β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ π΅)βπ₯) β (π¦(,)+β)))) |
57 | 47, 52, 56 | 3bitr4d 311 |
. . . . . 6
β’ (((π β§ π¦ β β) β§ π¦ < 0) β (π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-β(,)-π¦)) β π₯ β (β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β)))) |
58 | 57 | alrimiv 1931 |
. . . . 5
β’ (((π β§ π¦ β β) β§ π¦ < 0) β βπ₯(π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-β(,)-π¦)) β π₯ β (β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β)))) |
59 | | nfmpt1 5218 |
. . . . . . . 8
β’
β²π₯(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) |
60 | 59 | nfcnv 5839 |
. . . . . . 7
β’
β²π₯β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) |
61 | | nfcv 2908 |
. . . . . . 7
β’
β²π₯(-β(,)-π¦) |
62 | 60, 61 | nfima 6026 |
. . . . . 6
β’
β²π₯(β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-β(,)-π¦)) |
63 | | nfmpt1 5218 |
. . . . . . . 8
β’
β²π₯(π₯ β π΄ β¦ π΅) |
64 | 63 | nfcnv 5839 |
. . . . . . 7
β’
β²π₯β‘(π₯ β π΄ β¦ π΅) |
65 | | nfcv 2908 |
. . . . . . 7
β’
β²π₯(π¦(,)+β) |
66 | 64, 65 | nfima 6026 |
. . . . . 6
β’
β²π₯(β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β)) |
67 | 62, 66 | cleqf 2939 |
. . . . 5
β’ ((β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-β(,)-π¦)) = (β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β)) β βπ₯(π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-β(,)-π¦)) β π₯ β (β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β)))) |
68 | 58, 67 | sylibr 233 |
. . . 4
β’ (((π β§ π¦ β β) β§ π¦ < 0) β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-β(,)-π¦)) = (β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β))) |
69 | | mbfposr.3 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn) |
70 | | mbfima 25010 |
. . . . . 6
β’ (((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn β§ (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)):π΄βΆβ) β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-β(,)-π¦)) β dom
vol) |
71 | 69, 48, 70 | syl2anc 585 |
. . . . 5
β’ (π β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-β(,)-π¦)) β dom
vol) |
72 | 71 | ad2antrr 725 |
. . . 4
β’ (((π β§ π¦ β β) β§ π¦ < 0) β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-β(,)-π¦)) β dom
vol) |
73 | 68, 72 | eqeltrrd 2839 |
. . 3
β’ (((π β§ π¦ β β) β§ π¦ < 0) β (β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β)) β dom
vol) |
74 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β 0 β€ π¦) |
75 | | 0red 11165 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β 0 β β) |
76 | 1 | ad4ant14 751 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β π΅ β β) |
77 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β π¦ β β) |
78 | | maxle 13117 |
. . . . . . . . . . . . . . 15
β’ ((0
β β β§ π΅
β β β§ π¦
β β) β (if(0 β€ π΅, π΅, 0) β€ π¦ β (0 β€ π¦ β§ π΅ β€ π¦))) |
79 | 75, 76, 77, 78 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β (if(0 β€ π΅, π΅, 0) β€ π¦ β (0 β€ π¦ β§ π΅ β€ π¦))) |
80 | 74, 79 | mpbirand 706 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β (if(0 β€ π΅, π΅, 0) β€ π¦ β π΅ β€ π¦)) |
81 | 80 | notbid 318 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β (Β¬ if(0 β€ π΅, π΅, 0) β€ π¦ β Β¬ π΅ β€ π¦)) |
82 | 76, 4, 5 | sylancl 587 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β if(0 β€ π΅, π΅, 0) β β) |
83 | 77, 82 | ltnled 11309 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β (π¦ < if(0 β€ π΅, π΅, 0) β Β¬ if(0 β€ π΅, π΅, 0) β€ π¦)) |
84 | 77, 76 | ltnled 11309 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β (π¦ < π΅ β Β¬ π΅ β€ π¦)) |
85 | 81, 83, 84 | 3bitr4d 311 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β (π¦ < if(0 β€ π΅, π΅, 0) β π¦ < π΅)) |
86 | 82 | biantrurd 534 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β (π¦ < if(0 β€ π΅, π΅, 0) β (if(0 β€ π΅, π΅, 0) β β β§ π¦ < if(0 β€ π΅, π΅, 0)))) |
87 | 76 | biantrurd 534 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β (π¦ < π΅ β (π΅ β β β§ π¦ < π΅))) |
88 | 85, 86, 87 | 3bitr3d 309 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β ((if(0 β€ π΅, π΅, 0) β β β§ π¦ < if(0 β€ π΅, π΅, 0)) β (π΅ β β β§ π¦ < π΅))) |
89 | 77 | rexrd 11212 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β π¦ β β*) |
90 | | elioopnf 13367 |
. . . . . . . . . . 11
β’ (π¦ β β*
β (if(0 β€ π΅, π΅, 0) β (π¦(,)+β) β (if(0 β€ π΅, π΅, 0) β β β§ π¦ < if(0 β€ π΅, π΅, 0)))) |
91 | 89, 90 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β (if(0 β€ π΅, π΅, 0) β (π¦(,)+β) β (if(0 β€ π΅, π΅, 0) β β β§ π¦ < if(0 β€ π΅, π΅, 0)))) |
92 | 89, 32 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β (π΅ β (π¦(,)+β) β (π΅ β β β§ π¦ < π΅))) |
93 | 88, 91, 92 | 3bitr4d 311 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β (if(0 β€ π΅, π΅, 0) β (π¦(,)+β) β π΅ β (π¦(,)+β))) |
94 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) = (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) |
95 | 94 | fvmpt2 6964 |
. . . . . . . . . . . 12
β’ ((π₯ β π΄ β§ if(0 β€ π΅, π΅, 0) β β) β ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))βπ₯) = if(0 β€ π΅, π΅, 0)) |
96 | 35, 6, 95 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))βπ₯) = if(0 β€ π΅, π΅, 0)) |
97 | 96 | eleq1d 2823 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))βπ₯) β (π¦(,)+β) β if(0 β€ π΅, π΅, 0) β (π¦(,)+β))) |
98 | 97 | ad4ant14 751 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β (((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))βπ₯) β (π¦(,)+β) β if(0 β€ π΅, π΅, 0) β (π¦(,)+β))) |
99 | 44 | ad4ant14 751 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β (((π₯ β π΄ β¦ π΅)βπ₯) β (π¦(,)+β) β π΅ β (π¦(,)+β))) |
100 | 93, 98, 99 | 3bitr4d 311 |
. . . . . . . 8
β’ ((((π β§ π¦ β β) β§ 0 β€ π¦) β§ π₯ β π΄) β (((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))βπ₯) β (π¦(,)+β) β ((π₯ β π΄ β¦ π΅)βπ₯) β (π¦(,)+β))) |
101 | 100 | pm5.32da 580 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ 0 β€ π¦) β ((π₯ β π΄ β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))βπ₯) β (π¦(,)+β)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ π΅)βπ₯) β (π¦(,)+β)))) |
102 | 6 | fmpttd 7068 |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)):π΄βΆβ) |
103 | | ffn 6673 |
. . . . . . . . 9
β’ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)):π΄βΆβ β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) Fn π΄) |
104 | | elpreima 7013 |
. . . . . . . . 9
β’ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) Fn π΄ β (π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (π¦(,)+β)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))βπ₯) β (π¦(,)+β)))) |
105 | 102, 103,
104 | 3syl 18 |
. . . . . . . 8
β’ (π β (π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (π¦(,)+β)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))βπ₯) β (π¦(,)+β)))) |
106 | 105 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ 0 β€ π¦) β (π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (π¦(,)+β)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))βπ₯) β (π¦(,)+β)))) |
107 | 55 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ 0 β€ π¦) β (π₯ β (β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ π΅)βπ₯) β (π¦(,)+β)))) |
108 | 101, 106,
107 | 3bitr4d 311 |
. . . . . 6
β’ (((π β§ π¦ β β) β§ 0 β€ π¦) β (π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (π¦(,)+β)) β π₯ β (β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β)))) |
109 | 108 | alrimiv 1931 |
. . . . 5
β’ (((π β§ π¦ β β) β§ 0 β€ π¦) β βπ₯(π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (π¦(,)+β)) β π₯ β (β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β)))) |
110 | | nfmpt1 5218 |
. . . . . . . 8
β’
β²π₯(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) |
111 | 110 | nfcnv 5839 |
. . . . . . 7
β’
β²π₯β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) |
112 | 111, 65 | nfima 6026 |
. . . . . 6
β’
β²π₯(β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (π¦(,)+β)) |
113 | 112, 66 | cleqf 2939 |
. . . . 5
β’ ((β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (π¦(,)+β)) = (β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β)) β βπ₯(π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (π¦(,)+β)) β π₯ β (β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β)))) |
114 | 109, 113 | sylibr 233 |
. . . 4
β’ (((π β§ π¦ β β) β§ 0 β€ π¦) β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (π¦(,)+β)) = (β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β))) |
115 | | mbfima 25010 |
. . . . . 6
β’ (((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn β§ (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)):π΄βΆβ) β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (π¦(,)+β)) β dom
vol) |
116 | 3, 102, 115 | syl2anc 585 |
. . . . 5
β’ (π β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (π¦(,)+β)) β dom
vol) |
117 | 116 | ad2antrr 725 |
. . . 4
β’ (((π β§ π¦ β β) β§ 0 β€ π¦) β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (π¦(,)+β)) β dom
vol) |
118 | 114, 117 | eqeltrrd 2839 |
. . 3
β’ (((π β§ π¦ β β) β§ 0 β€ π¦) β (β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β)) β dom
vol) |
119 | | simpr 486 |
. . 3
β’ ((π β§ π¦ β β) β π¦ β β) |
120 | | 0red 11165 |
. . 3
β’ ((π β§ π¦ β β) β 0 β
β) |
121 | 73, 118, 119, 120 | ltlecasei 11270 |
. 2
β’ ((π β§ π¦ β β) β (β‘(π₯ β π΄ β¦ π΅) β (π¦(,)+β)) β dom
vol) |
122 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ 0 < π¦) β§ π₯ β π΄) β 0 < π¦) |
123 | | 0red 11165 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β β) β§ 0 < π¦) β§ π₯ β π΄) β 0 β β) |
124 | 1 | ad4ant14 751 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β β) β§ 0 < π¦) β§ π₯ β π΄) β π΅ β β) |
125 | | simpllr 775 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β β) β§ 0 < π¦) β§ π₯ β π΄) β π¦ β β) |
126 | | maxlt 13119 |
. . . . . . . . . . . . 13
β’ ((0
β β β§ π΅
β β β§ π¦
β β) β (if(0 β€ π΅, π΅, 0) < π¦ β (0 < π¦ β§ π΅ < π¦))) |
127 | 123, 124,
125, 126 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ 0 < π¦) β§ π₯ β π΄) β (if(0 β€ π΅, π΅, 0) < π¦ β (0 < π¦ β§ π΅ < π¦))) |
128 | 122, 127 | mpbirand 706 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ 0 < π¦) β§ π₯ β π΄) β (if(0 β€ π΅, π΅, 0) < π¦ β π΅ < π¦)) |
129 | 6 | ad4ant14 751 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ 0 < π¦) β§ π₯ β π΄) β if(0 β€ π΅, π΅, 0) β β) |
130 | 129 | biantrurd 534 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ 0 < π¦) β§ π₯ β π΄) β (if(0 β€ π΅, π΅, 0) < π¦ β (if(0 β€ π΅, π΅, 0) β β β§ if(0 β€ π΅, π΅, 0) < π¦))) |
131 | 124 | biantrurd 534 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ 0 < π¦) β§ π₯ β π΄) β (π΅ < π¦ β (π΅ β β β§ π΅ < π¦))) |
132 | 128, 130,
131 | 3bitr3d 309 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β β) β§ 0 < π¦) β§ π₯ β π΄) β ((if(0 β€ π΅, π΅, 0) β β β§ if(0 β€ π΅, π΅, 0) < π¦) β (π΅ β β β§ π΅ < π¦))) |
133 | 125 | rexrd 11212 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ 0 < π¦) β§ π₯ β π΄) β π¦ β β*) |
134 | | elioomnf 13368 |
. . . . . . . . . . 11
β’ (π¦ β β*
β (if(0 β€ π΅, π΅, 0) β (-β(,)π¦) β (if(0 β€ π΅, π΅, 0) β β β§ if(0 β€ π΅, π΅, 0) < π¦))) |
135 | 133, 134 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β β) β§ 0 < π¦) β§ π₯ β π΄) β (if(0 β€ π΅, π΅, 0) β (-β(,)π¦) β (if(0 β€ π΅, π΅, 0) β β β§ if(0 β€ π΅, π΅, 0) < π¦))) |
136 | | elioomnf 13368 |
. . . . . . . . . . 11
β’ (π¦ β β*
β (π΅ β
(-β(,)π¦) β
(π΅ β β β§
π΅ < π¦))) |
137 | 133, 136 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β β) β§ 0 < π¦) β§ π₯ β π΄) β (π΅ β (-β(,)π¦) β (π΅ β β β§ π΅ < π¦))) |
138 | 132, 135,
137 | 3bitr4d 311 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ 0 < π¦) β§ π₯ β π΄) β (if(0 β€ π΅, π΅, 0) β (-β(,)π¦) β π΅ β (-β(,)π¦))) |
139 | 96 | eleq1d 2823 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))βπ₯) β (-β(,)π¦) β if(0 β€ π΅, π΅, 0) β (-β(,)π¦))) |
140 | 139 | ad4ant14 751 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ 0 < π¦) β§ π₯ β π΄) β (((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))βπ₯) β (-β(,)π¦) β if(0 β€ π΅, π΅, 0) β (-β(,)π¦))) |
141 | 43 | eleq1d 2823 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (((π₯ β π΄ β¦ π΅)βπ₯) β (-β(,)π¦) β π΅ β (-β(,)π¦))) |
142 | 141 | ad4ant14 751 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ 0 < π¦) β§ π₯ β π΄) β (((π₯ β π΄ β¦ π΅)βπ₯) β (-β(,)π¦) β π΅ β (-β(,)π¦))) |
143 | 138, 140,
142 | 3bitr4d 311 |
. . . . . . . 8
β’ ((((π β§ π¦ β β) β§ 0 < π¦) β§ π₯ β π΄) β (((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))βπ₯) β (-β(,)π¦) β ((π₯ β π΄ β¦ π΅)βπ₯) β (-β(,)π¦))) |
144 | 143 | pm5.32da 580 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ 0 < π¦) β ((π₯ β π΄ β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))βπ₯) β (-β(,)π¦)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ π΅)βπ₯) β (-β(,)π¦)))) |
145 | | elpreima 7013 |
. . . . . . . . 9
β’ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) Fn π΄ β (π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (-β(,)π¦)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))βπ₯) β (-β(,)π¦)))) |
146 | 102, 103,
145 | 3syl 18 |
. . . . . . . 8
β’ (π β (π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (-β(,)π¦)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))βπ₯) β (-β(,)π¦)))) |
147 | 146 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ 0 < π¦) β (π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (-β(,)π¦)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))βπ₯) β (-β(,)π¦)))) |
148 | | elpreima 7013 |
. . . . . . . . 9
β’ ((π₯ β π΄ β¦ π΅) Fn π΄ β (π₯ β (β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ π΅)βπ₯) β (-β(,)π¦)))) |
149 | 2, 53, 148 | 3syl 18 |
. . . . . . . 8
β’ (π β (π₯ β (β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ π΅)βπ₯) β (-β(,)π¦)))) |
150 | 149 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ 0 < π¦) β (π₯ β (β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ π΅)βπ₯) β (-β(,)π¦)))) |
151 | 144, 147,
150 | 3bitr4d 311 |
. . . . . 6
β’ (((π β§ π¦ β β) β§ 0 < π¦) β (π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (-β(,)π¦)) β π₯ β (β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦)))) |
152 | 151 | alrimiv 1931 |
. . . . 5
β’ (((π β§ π¦ β β) β§ 0 < π¦) β βπ₯(π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (-β(,)π¦)) β π₯ β (β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦)))) |
153 | | nfcv 2908 |
. . . . . . 7
β’
β²π₯(-β(,)π¦) |
154 | 111, 153 | nfima 6026 |
. . . . . 6
β’
β²π₯(β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (-β(,)π¦)) |
155 | 64, 153 | nfima 6026 |
. . . . . 6
β’
β²π₯(β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦)) |
156 | 154, 155 | cleqf 2939 |
. . . . 5
β’ ((β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (-β(,)π¦)) = (β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦)) β βπ₯(π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (-β(,)π¦)) β π₯ β (β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦)))) |
157 | 152, 156 | sylibr 233 |
. . . 4
β’ (((π β§ π¦ β β) β§ 0 < π¦) β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (-β(,)π¦)) = (β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦))) |
158 | | mbfima 25010 |
. . . . . 6
β’ (((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn β§ (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)):π΄βΆβ) β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (-β(,)π¦)) β dom vol) |
159 | 3, 102, 158 | syl2anc 585 |
. . . . 5
β’ (π β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (-β(,)π¦)) β dom vol) |
160 | 159 | ad2antrr 725 |
. . . 4
β’ (((π β§ π¦ β β) β§ 0 < π¦) β (β‘(π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β (-β(,)π¦)) β dom vol) |
161 | 157, 160 | eqeltrrd 2839 |
. . 3
β’ (((π β§ π¦ β β) β§ 0 < π¦) β (β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦)) β dom vol) |
162 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β π¦ β€ 0) |
163 | | simpllr 775 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β π¦ β β) |
164 | 163 | le0neg1d 11733 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β (π¦ β€ 0 β 0 β€ -π¦)) |
165 | 162, 164 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β 0 β€ -π¦) |
166 | 165 | biantrurd 534 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β (-π΅ β€ -π¦ β (0 β€ -π¦ β§ -π΅ β€ -π¦))) |
167 | 1 | ad4ant14 751 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β π΅ β β) |
168 | 163, 167 | lenegd 11741 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β (π¦ β€ π΅ β -π΅ β€ -π¦)) |
169 | | 0red 11165 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β 0 β β) |
170 | 167 | renegcld 11589 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β -π΅ β β) |
171 | 163 | renegcld 11589 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β -π¦ β β) |
172 | | maxle 13117 |
. . . . . . . . . . . . . . 15
β’ ((0
β β β§ -π΅
β β β§ -π¦
β β) β (if(0 β€ -π΅, -π΅, 0) β€ -π¦ β (0 β€ -π¦ β§ -π΅ β€ -π¦))) |
173 | 169, 170,
171, 172 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β (if(0 β€ -π΅, -π΅, 0) β€ -π¦ β (0 β€ -π¦ β§ -π΅ β€ -π¦))) |
174 | 166, 168,
173 | 3bitr4rd 312 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β (if(0 β€ -π΅, -π΅, 0) β€ -π¦ β π¦ β€ π΅)) |
175 | 174 | notbid 318 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β (Β¬ if(0 β€ -π΅, -π΅, 0) β€ -π¦ β Β¬ π¦ β€ π΅)) |
176 | 23 | ad4ant14 751 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β if(0 β€ -π΅, -π΅, 0) β β) |
177 | 171, 176 | ltnled 11309 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β (-π¦ < if(0 β€ -π΅, -π΅, 0) β Β¬ if(0 β€ -π΅, -π΅, 0) β€ -π¦)) |
178 | 167, 163 | ltnled 11309 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β (π΅ < π¦ β Β¬ π¦ β€ π΅)) |
179 | 175, 177,
178 | 3bitr4d 311 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β (-π¦ < if(0 β€ -π΅, -π΅, 0) β π΅ < π¦)) |
180 | 176 | biantrurd 534 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β (-π¦ < if(0 β€ -π΅, -π΅, 0) β (if(0 β€ -π΅, -π΅, 0) β β β§ -π¦ < if(0 β€ -π΅, -π΅, 0)))) |
181 | 167 | biantrurd 534 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β (π΅ < π¦ β (π΅ β β β§ π΅ < π¦))) |
182 | 179, 180,
181 | 3bitr3d 309 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β ((if(0 β€ -π΅, -π΅, 0) β β β§ -π¦ < if(0 β€ -π΅, -π΅, 0)) β (π΅ β β β§ π΅ < π¦))) |
183 | 171 | rexrd 11212 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β -π¦ β β*) |
184 | | elioopnf 13367 |
. . . . . . . . . . 11
β’ (-π¦ β β*
β (if(0 β€ -π΅,
-π΅, 0) β (-π¦(,)+β) β (if(0 β€
-π΅, -π΅, 0) β β β§ -π¦ < if(0 β€ -π΅, -π΅, 0)))) |
185 | 183, 184 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β (if(0 β€ -π΅, -π΅, 0) β (-π¦(,)+β) β (if(0 β€ -π΅, -π΅, 0) β β β§ -π¦ < if(0 β€ -π΅, -π΅, 0)))) |
186 | 163 | rexrd 11212 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β π¦ β β*) |
187 | 186, 136 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β (π΅ β (-β(,)π¦) β (π΅ β β β§ π΅ < π¦))) |
188 | 182, 185,
187 | 3bitr4d 311 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β (if(0 β€ -π΅, -π΅, 0) β (-π¦(,)+β) β π΅ β (-β(,)π¦))) |
189 | 38 | eleq1d 2823 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))βπ₯) β (-π¦(,)+β) β if(0 β€ -π΅, -π΅, 0) β (-π¦(,)+β))) |
190 | 189 | ad4ant14 751 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β (((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))βπ₯) β (-π¦(,)+β) β if(0 β€ -π΅, -π΅, 0) β (-π¦(,)+β))) |
191 | 141 | ad4ant14 751 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β (((π₯ β π΄ β¦ π΅)βπ₯) β (-β(,)π¦) β π΅ β (-β(,)π¦))) |
192 | 188, 190,
191 | 3bitr4d 311 |
. . . . . . . 8
β’ ((((π β§ π¦ β β) β§ π¦ β€ 0) β§ π₯ β π΄) β (((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))βπ₯) β (-π¦(,)+β) β ((π₯ β π΄ β¦ π΅)βπ₯) β (-β(,)π¦))) |
193 | 192 | pm5.32da 580 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ π¦ β€ 0) β ((π₯ β π΄ β§ ((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))βπ₯) β (-π¦(,)+β)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ π΅)βπ₯) β (-β(,)π¦)))) |
194 | | elpreima 7013 |
. . . . . . . . 9
β’ ((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) Fn π΄ β (π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-π¦(,)+β)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))βπ₯) β (-π¦(,)+β)))) |
195 | 48, 49, 194 | 3syl 18 |
. . . . . . . 8
β’ (π β (π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-π¦(,)+β)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))βπ₯) β (-π¦(,)+β)))) |
196 | 195 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ π¦ β€ 0) β (π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-π¦(,)+β)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))βπ₯) β (-π¦(,)+β)))) |
197 | 149 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ π¦ β€ 0) β (π₯ β (β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦)) β (π₯ β π΄ β§ ((π₯ β π΄ β¦ π΅)βπ₯) β (-β(,)π¦)))) |
198 | 193, 196,
197 | 3bitr4d 311 |
. . . . . 6
β’ (((π β§ π¦ β β) β§ π¦ β€ 0) β (π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-π¦(,)+β)) β π₯ β (β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦)))) |
199 | 198 | alrimiv 1931 |
. . . . 5
β’ (((π β§ π¦ β β) β§ π¦ β€ 0) β βπ₯(π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-π¦(,)+β)) β π₯ β (β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦)))) |
200 | | nfcv 2908 |
. . . . . . 7
β’
β²π₯(-π¦(,)+β) |
201 | 60, 200 | nfima 6026 |
. . . . . 6
β’
β²π₯(β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-π¦(,)+β)) |
202 | 201, 155 | cleqf 2939 |
. . . . 5
β’ ((β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-π¦(,)+β)) = (β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦)) β βπ₯(π₯ β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-π¦(,)+β)) β π₯ β (β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦)))) |
203 | 199, 202 | sylibr 233 |
. . . 4
β’ (((π β§ π¦ β β) β§ π¦ β€ 0) β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-π¦(,)+β)) = (β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦))) |
204 | | mbfima 25010 |
. . . . . 6
β’ (((π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn β§ (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)):π΄βΆβ) β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-π¦(,)+β)) β dom
vol) |
205 | 69, 48, 204 | syl2anc 585 |
. . . . 5
β’ (π β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-π¦(,)+β)) β dom
vol) |
206 | 205 | ad2antrr 725 |
. . . 4
β’ (((π β§ π¦ β β) β§ π¦ β€ 0) β (β‘(π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β (-π¦(,)+β)) β dom
vol) |
207 | 203, 206 | eqeltrrd 2839 |
. . 3
β’ (((π β§ π¦ β β) β§ π¦ β€ 0) β (β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦)) β dom vol) |
208 | 161, 207,
120, 119 | ltlecasei 11270 |
. 2
β’ ((π β§ π¦ β β) β (β‘(π₯ β π΄ β¦ π΅) β (-β(,)π¦)) β dom vol) |
209 | 2, 7, 121, 208 | ismbf2d 25020 |
1
β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) |