Step | Hyp | Ref
| Expression |
1 | | fvex 6856 |
. . . . . . . . . 10
β’ (πΉβπ₯) β V |
2 | | c0ex 11150 |
. . . . . . . . . 10
β’ 0 β
V |
3 | 1, 2 | ifex 4537 |
. . . . . . . . 9
β’ if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β V |
4 | | eqid 2737 |
. . . . . . . . . 10
β’ (π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) = (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) |
5 | 4 | fvmpt2 6960 |
. . . . . . . . 9
β’ ((π₯ β β β§ if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β V) β ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ₯) = if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) |
6 | 3, 5 | mpan2 690 |
. . . . . . . 8
β’ (π₯ β β β ((π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ₯) = if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) |
7 | 6 | mpteq2dv 5208 |
. . . . . . 7
β’ (π₯ β β β (π β β β¦ ((π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ₯)) = (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) |
8 | 7 | rneqd 5894 |
. . . . . 6
β’ (π₯ β β β ran
(π β β β¦
((π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ₯)) = ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) |
9 | 8 | supeq1d 9383 |
. . . . 5
β’ (π₯ β β β sup(ran
(π β β β¦
((π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ₯)), β, < ) = sup(ran (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)), β, < )) |
10 | 9 | mpteq2ia 5209 |
. . . 4
β’ (π₯ β β β¦ sup(ran
(π β β β¦
((π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ₯)), β, < )) = (π₯ β β β¦ sup(ran (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)), β, < )) |
11 | | nfcv 2908 |
. . . . 5
β’
β²π¦sup(ran (π β β β¦ ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ₯)), β, < ) |
12 | | nfcv 2908 |
. . . . . . . 8
β’
β²π₯β |
13 | | nfmpt1 5214 |
. . . . . . . . . . 11
β’
β²π₯(π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) |
14 | 12, 13 | nfmpt 5213 |
. . . . . . . . . 10
β’
β²π₯(π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) |
15 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²π₯π |
16 | 14, 15 | nffv 6853 |
. . . . . . . . 9
β’
β²π₯((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ) |
17 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π₯π¦ |
18 | 16, 17 | nffv 6853 |
. . . . . . . 8
β’
β²π₯(((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦) |
19 | 12, 18 | nfmpt 5213 |
. . . . . . 7
β’
β²π₯(π β β β¦ (((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦)) |
20 | 19 | nfrn 5908 |
. . . . . 6
β’
β²π₯ran
(π β β β¦
(((π β β β¦
(π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦)) |
21 | | nfcv 2908 |
. . . . . 6
β’
β²π₯β |
22 | | nfcv 2908 |
. . . . . 6
β’
β²π₯
< |
23 | 20, 21, 22 | nfsup 9388 |
. . . . 5
β’
β²π₯sup(ran (π β β β¦ (((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦)), β, < ) |
24 | | fveq2 6843 |
. . . . . . . . 9
β’ (π₯ = π¦ β ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ₯) = ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ¦)) |
25 | 24 | mpteq2dv 5208 |
. . . . . . . 8
β’ (π₯ = π¦ β (π β β β¦ ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ₯)) = (π β β β¦ ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ¦))) |
26 | | breq2 5110 |
. . . . . . . . . . . . 13
β’ (π = π β ((πΉβπ₯) β€ π β (πΉβπ₯) β€ π)) |
27 | 26 | ifbid 4510 |
. . . . . . . . . . . 12
β’ (π = π β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) = if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) |
28 | 27 | mpteq2dv 5208 |
. . . . . . . . . . 11
β’ (π = π β (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) = (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) |
29 | 28 | fveq1d 6845 |
. . . . . . . . . 10
β’ (π = π β ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ¦) = ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ¦)) |
30 | 29 | cbvmptv 5219 |
. . . . . . . . 9
β’ (π β β β¦ ((π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ¦)) = (π β β β¦ ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ¦)) |
31 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π β β β¦ (π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) = (π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) |
32 | | reex 11143 |
. . . . . . . . . . . . 13
β’ β
β V |
33 | 32 | mptex 7174 |
. . . . . . . . . . . 12
β’ (π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) β V |
34 | 28, 31, 33 | fvmpt 6949 |
. . . . . . . . . . 11
β’ (π β β β ((π β β β¦ (π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ) = (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) |
35 | 34 | fveq1d 6845 |
. . . . . . . . . 10
β’ (π β β β (((π β β β¦ (π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦) = ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ¦)) |
36 | 35 | mpteq2ia 5209 |
. . . . . . . . 9
β’ (π β β β¦ (((π β β β¦ (π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦)) = (π β β β¦ ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ¦)) |
37 | 30, 36 | eqtr4i 2768 |
. . . . . . . 8
β’ (π β β β¦ ((π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ¦)) = (π β β β¦ (((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦)) |
38 | 25, 37 | eqtrdi 2793 |
. . . . . . 7
β’ (π₯ = π¦ β (π β β β¦ ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ₯)) = (π β β β¦ (((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦))) |
39 | 38 | rneqd 5894 |
. . . . . 6
β’ (π₯ = π¦ β ran (π β β β¦ ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ₯)) = ran (π β β β¦ (((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦))) |
40 | 39 | supeq1d 9383 |
. . . . 5
β’ (π₯ = π¦ β sup(ran (π β β β¦ ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ₯)), β, < ) = sup(ran (π β β β¦ (((π β β β¦ (π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦)), β, < )) |
41 | 11, 23, 40 | cbvmpt 5217 |
. . . 4
β’ (π₯ β β β¦ sup(ran
(π β β β¦
((π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ₯)), β, < )) = (π¦ β β β¦ sup(ran (π β β β¦ (((π β β β¦ (π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦)), β, < )) |
42 | 10, 41 | eqtr3i 2767 |
. . 3
β’ (π₯ β β β¦ sup(ran
(π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)), β, < )) = (π¦ β β β¦ sup(ran
(π β β β¦
(((π β β β¦
(π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦)), β, < )) |
43 | | fveq2 6843 |
. . . . . . . 8
β’ (π₯ = π¦ β (πΉβπ₯) = (πΉβπ¦)) |
44 | 43 | breq1d 5116 |
. . . . . . 7
β’ (π₯ = π¦ β ((πΉβπ₯) β€ π β (πΉβπ¦) β€ π)) |
45 | 44, 43 | ifbieq1d 4511 |
. . . . . 6
β’ (π₯ = π¦ β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) = if((πΉβπ¦) β€ π, (πΉβπ¦), 0)) |
46 | 45 | cbvmptv 5219 |
. . . . 5
β’ (π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) = (π¦ β β β¦ if((πΉβπ¦) β€ π, (πΉβπ¦), 0)) |
47 | 34 | adantl 483 |
. . . . 5
β’ ((π β§ π β β) β ((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ) = (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) |
48 | | nnre 12161 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β) |
49 | 48 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π¦ β β) β π β β) |
50 | 49 | rexrd 11206 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π¦ β β) β π β β*) |
51 | | elioopnf 13361 |
. . . . . . . . . . 11
β’ (π β β*
β ((πΉβπ¦) β (π(,)+β) β ((πΉβπ¦) β β β§ π < (πΉβπ¦)))) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π¦ β β) β ((πΉβπ¦) β (π(,)+β) β ((πΉβπ¦) β β β§ π < (πΉβπ¦)))) |
53 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π¦ β β) β π¦ β β) |
54 | | itg2cn.1 |
. . . . . . . . . . . . . 14
β’ (π β πΉ:ββΆ(0[,)+β)) |
55 | 54 | ffnd 6670 |
. . . . . . . . . . . . 13
β’ (π β πΉ Fn β) |
56 | 55 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π¦ β β) β πΉ Fn β) |
57 | | elpreima 7009 |
. . . . . . . . . . . 12
β’ (πΉ Fn β β (π¦ β (β‘πΉ β (π(,)+β)) β (π¦ β β β§ (πΉβπ¦) β (π(,)+β)))) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π¦ β β) β (π¦ β (β‘πΉ β (π(,)+β)) β (π¦ β β β§ (πΉβπ¦) β (π(,)+β)))) |
59 | 53, 58 | mpbirand 706 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π¦ β β) β (π¦ β (β‘πΉ β (π(,)+β)) β (πΉβπ¦) β (π(,)+β))) |
60 | | rge0ssre 13374 |
. . . . . . . . . . . . . 14
β’
(0[,)+β) β β |
61 | | fss 6686 |
. . . . . . . . . . . . . 14
β’ ((πΉ:ββΆ(0[,)+β)
β§ (0[,)+β) β β) β πΉ:ββΆβ) |
62 | 54, 60, 61 | sylancl 587 |
. . . . . . . . . . . . 13
β’ (π β πΉ:ββΆβ) |
63 | 62 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β πΉ:ββΆβ) |
64 | 63 | ffvelcdmda 7036 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π¦ β β) β (πΉβπ¦) β β) |
65 | 64 | biantrurd 534 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π¦ β β) β (π < (πΉβπ¦) β ((πΉβπ¦) β β β§ π < (πΉβπ¦)))) |
66 | 52, 59, 65 | 3bitr4d 311 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π¦ β β) β (π¦ β (β‘πΉ β (π(,)+β)) β π < (πΉβπ¦))) |
67 | 66 | notbid 318 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π¦ β β) β (Β¬ π¦ β (β‘πΉ β (π(,)+β)) β Β¬ π < (πΉβπ¦))) |
68 | | eldif 3921 |
. . . . . . . . . 10
β’ (π¦ β (β β (β‘πΉ β (π(,)+β))) β (π¦ β β β§ Β¬ π¦ β (β‘πΉ β (π(,)+β)))) |
69 | 68 | baib 537 |
. . . . . . . . 9
β’ (π¦ β β β (π¦ β (β β (β‘πΉ β (π(,)+β))) β Β¬ π¦ β (β‘πΉ β (π(,)+β)))) |
70 | 69 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π¦ β β) β (π¦ β (β β (β‘πΉ β (π(,)+β))) β Β¬ π¦ β (β‘πΉ β (π(,)+β)))) |
71 | 64, 49 | lenltd 11302 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π¦ β β) β ((πΉβπ¦) β€ π β Β¬ π < (πΉβπ¦))) |
72 | 67, 70, 71 | 3bitr4d 311 |
. . . . . . 7
β’ (((π β§ π β β) β§ π¦ β β) β (π¦ β (β β (β‘πΉ β (π(,)+β))) β (πΉβπ¦) β€ π)) |
73 | 72 | ifbid 4510 |
. . . . . 6
β’ (((π β§ π β β) β§ π¦ β β) β if(π¦ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ¦), 0) = if((πΉβπ¦) β€ π, (πΉβπ¦), 0)) |
74 | 73 | mpteq2dva 5206 |
. . . . 5
β’ ((π β§ π β β) β (π¦ β β β¦ if(π¦ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ¦), 0)) = (π¦ β β β¦ if((πΉβπ¦) β€ π, (πΉβπ¦), 0))) |
75 | 46, 47, 74 | 3eqtr4a 2803 |
. . . 4
β’ ((π β§ π β β) β ((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ) = (π¦ β β β¦ if(π¦ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ¦), 0))) |
76 | | difss 4092 |
. . . . . 6
β’ (β
β (β‘πΉ β (π(,)+β))) β
β |
77 | 76 | a1i 11 |
. . . . 5
β’ ((π β§ π β β) β (β β
(β‘πΉ β (π(,)+β))) β
β) |
78 | | rembl 24907 |
. . . . . 6
β’ β
β dom vol |
79 | 78 | a1i 11 |
. . . . 5
β’ ((π β§ π β β) β β β dom
vol) |
80 | | fvex 6856 |
. . . . . . 7
β’ (πΉβπ¦) β V |
81 | 80, 2 | ifex 4537 |
. . . . . 6
β’ if(π¦ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ¦), 0) β V |
82 | 81 | a1i 11 |
. . . . 5
β’ (((π β§ π β β) β§ π¦ β (β β (β‘πΉ β (π(,)+β)))) β if(π¦ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ¦), 0) β V) |
83 | | eldifn 4088 |
. . . . . . 7
β’ (π¦ β (β β
(β β (β‘πΉ β (π(,)+β)))) β Β¬ π¦ β (β β (β‘πΉ β (π(,)+β)))) |
84 | 83 | adantl 483 |
. . . . . 6
β’ (((π β§ π β β) β§ π¦ β (β β (β β
(β‘πΉ β (π(,)+β))))) β Β¬ π¦ β (β β (β‘πΉ β (π(,)+β)))) |
85 | 84 | iffalsed 4498 |
. . . . 5
β’ (((π β§ π β β) β§ π¦ β (β β (β β
(β‘πΉ β (π(,)+β))))) β if(π¦ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ¦), 0) = 0) |
86 | | iftrue 4493 |
. . . . . . . . 9
β’ (π¦ β (β β (β‘πΉ β (π(,)+β))) β if(π¦ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ¦), 0) = (πΉβπ¦)) |
87 | 86 | mpteq2ia 5209 |
. . . . . . . 8
β’ (π¦ β (β β (β‘πΉ β (π(,)+β))) β¦ if(π¦ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ¦), 0)) = (π¦ β (β β (β‘πΉ β (π(,)+β))) β¦ (πΉβπ¦)) |
88 | | resmpt 5992 |
. . . . . . . . 9
β’ ((β
β (β‘πΉ β (π(,)+β))) β β β ((π¦ β β β¦ (πΉβπ¦)) βΎ (β β (β‘πΉ β (π(,)+β)))) = (π¦ β (β β (β‘πΉ β (π(,)+β))) β¦ (πΉβπ¦))) |
89 | 76, 88 | ax-mp 5 |
. . . . . . . 8
β’ ((π¦ β β β¦ (πΉβπ¦)) βΎ (β β (β‘πΉ β (π(,)+β)))) = (π¦ β (β β (β‘πΉ β (π(,)+β))) β¦ (πΉβπ¦)) |
90 | 87, 89 | eqtr4i 2768 |
. . . . . . 7
β’ (π¦ β (β β (β‘πΉ β (π(,)+β))) β¦ if(π¦ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ¦), 0)) = ((π¦ β β β¦ (πΉβπ¦)) βΎ (β β (β‘πΉ β (π(,)+β)))) |
91 | 54 | feqmptd 6911 |
. . . . . . . . 9
β’ (π β πΉ = (π¦ β β β¦ (πΉβπ¦))) |
92 | | itg2cn.2 |
. . . . . . . . 9
β’ (π β πΉ β MblFn) |
93 | 91, 92 | eqeltrrd 2839 |
. . . . . . . 8
β’ (π β (π¦ β β β¦ (πΉβπ¦)) β MblFn) |
94 | | mbfima 24997 |
. . . . . . . . . 10
β’ ((πΉ β MblFn β§ πΉ:ββΆβ) β
(β‘πΉ β (π(,)+β)) β dom
vol) |
95 | 92, 62, 94 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (β‘πΉ β (π(,)+β)) β dom
vol) |
96 | | cmmbl 24901 |
. . . . . . . . 9
β’ ((β‘πΉ β (π(,)+β)) β dom vol β (β
β (β‘πΉ β (π(,)+β))) β dom
vol) |
97 | 95, 96 | syl 17 |
. . . . . . . 8
β’ (π β (β β (β‘πΉ β (π(,)+β))) β dom
vol) |
98 | | mbfres 25011 |
. . . . . . . 8
β’ (((π¦ β β β¦ (πΉβπ¦)) β MblFn β§ (β β (β‘πΉ β (π(,)+β))) β dom vol) β ((π¦ β β β¦ (πΉβπ¦)) βΎ (β β (β‘πΉ β (π(,)+β)))) β
MblFn) |
99 | 93, 97, 98 | syl2anc 585 |
. . . . . . 7
β’ (π β ((π¦ β β β¦ (πΉβπ¦)) βΎ (β β (β‘πΉ β (π(,)+β)))) β
MblFn) |
100 | 90, 99 | eqeltrid 2842 |
. . . . . 6
β’ (π β (π¦ β (β β (β‘πΉ β (π(,)+β))) β¦ if(π¦ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ¦), 0)) β MblFn) |
101 | 100 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β (π¦ β (β β (β‘πΉ β (π(,)+β))) β¦ if(π¦ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ¦), 0)) β MblFn) |
102 | 77, 79, 82, 85, 101 | mbfss 25013 |
. . . 4
β’ ((π β§ π β β) β (π¦ β β β¦ if(π¦ β (β β (β‘πΉ β (π(,)+β))), (πΉβπ¦), 0)) β MblFn) |
103 | 75, 102 | eqeltrd 2838 |
. . 3
β’ ((π β§ π β β) β ((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ) β MblFn) |
104 | 54 | ffvelcdmda 7036 |
. . . . . 6
β’ ((π β§ π₯ β β) β (πΉβπ₯) β (0[,)+β)) |
105 | | 0e0icopnf 13376 |
. . . . . 6
β’ 0 β
(0[,)+β) |
106 | | ifcl 4532 |
. . . . . 6
β’ (((πΉβπ₯) β (0[,)+β) β§ 0 β
(0[,)+β)) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β (0[,)+β)) |
107 | 104, 105,
106 | sylancl 587 |
. . . . 5
β’ ((π β§ π₯ β β) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β (0[,)+β)) |
108 | 107 | adantlr 714 |
. . . 4
β’ (((π β§ π β β) β§ π₯ β β) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β (0[,)+β)) |
109 | 47, 108 | fmpt3d 7065 |
. . 3
β’ ((π β§ π β β) β ((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ):ββΆ(0[,)+β)) |
110 | | elrege0 13372 |
. . . . . . . . . . . . 13
β’ ((πΉβπ₯) β (0[,)+β) β ((πΉβπ₯) β β β§ 0 β€ (πΉβπ₯))) |
111 | 104, 110 | sylib 217 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β ((πΉβπ₯) β β β§ 0 β€ (πΉβπ₯))) |
112 | 111 | simpld 496 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β (πΉβπ₯) β β) |
113 | 112 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β β) β (πΉβπ₯) β β) |
114 | 113 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π β β) β§ π₯ β β) β§ (πΉβπ₯) β€ π) β (πΉβπ₯) β β) |
115 | 114 | leidd 11722 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ π₯ β β) β§ (πΉβπ₯) β€ π) β (πΉβπ₯) β€ (πΉβπ₯)) |
116 | | iftrue 4493 |
. . . . . . . . 9
β’ ((πΉβπ₯) β€ π β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) = (πΉβπ₯)) |
117 | 116 | adantl 483 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ π₯ β β) β§ (πΉβπ₯) β€ π) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) = (πΉβπ₯)) |
118 | 48 | ad3antlr 730 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ π₯ β β) β§ (πΉβπ₯) β€ π) β π β β) |
119 | | peano2re 11329 |
. . . . . . . . . . 11
β’ (π β β β (π + 1) β
β) |
120 | 118, 119 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ π₯ β β) β§ (πΉβπ₯) β€ π) β (π + 1) β β) |
121 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ π₯ β β) β§ (πΉβπ₯) β€ π) β (πΉβπ₯) β€ π) |
122 | 118 | lep1d 12087 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ π₯ β β) β§ (πΉβπ₯) β€ π) β π β€ (π + 1)) |
123 | 114, 118,
120, 121, 122 | letrd 11313 |
. . . . . . . . 9
β’ ((((π β§ π β β) β§ π₯ β β) β§ (πΉβπ₯) β€ π) β (πΉβπ₯) β€ (π + 1)) |
124 | 123 | iftrued 4495 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ π₯ β β) β§ (πΉβπ₯) β€ π) β if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0) = (πΉβπ₯)) |
125 | 115, 117,
124 | 3brtr4d 5138 |
. . . . . . 7
β’ ((((π β§ π β β) β§ π₯ β β) β§ (πΉβπ₯) β€ π) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β€ if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0)) |
126 | | iffalse 4496 |
. . . . . . . . 9
β’ (Β¬
(πΉβπ₯) β€ π β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) = 0) |
127 | 126 | adantl 483 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ π₯ β β) β§ Β¬ (πΉβπ₯) β€ π) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) = 0) |
128 | 111 | simprd 497 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β) β 0 β€ (πΉβπ₯)) |
129 | | 0le0 12255 |
. . . . . . . . . . 11
β’ 0 β€
0 |
130 | | breq2 5110 |
. . . . . . . . . . . 12
β’ ((πΉβπ₯) = if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0) β (0 β€ (πΉβπ₯) β 0 β€ if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0))) |
131 | | breq2 5110 |
. . . . . . . . . . . 12
β’ (0 =
if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0) β (0 β€ 0 β 0 β€
if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0))) |
132 | 130, 131 | ifboth 4526 |
. . . . . . . . . . 11
β’ ((0 β€
(πΉβπ₯) β§ 0 β€ 0) β 0 β€ if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0)) |
133 | 128, 129,
132 | sylancl 587 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β 0 β€ if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0)) |
134 | 133 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π₯ β β) β 0 β€ if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0)) |
135 | 134 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ π₯ β β) β§ Β¬ (πΉβπ₯) β€ π) β 0 β€ if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0)) |
136 | 127, 135 | eqbrtrd 5128 |
. . . . . . 7
β’ ((((π β§ π β β) β§ π₯ β β) β§ Β¬ (πΉβπ₯) β€ π) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β€ if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0)) |
137 | 125, 136 | pm2.61dan 812 |
. . . . . 6
β’ (((π β§ π β β) β§ π₯ β β) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β€ if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0)) |
138 | 137 | ralrimiva 3144 |
. . . . 5
β’ ((π β§ π β β) β βπ₯ β β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β€ if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0)) |
139 | 1, 2 | ifex 4537 |
. . . . . . 7
β’ if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0) β V |
140 | 139 | a1i 11 |
. . . . . 6
β’ (((π β§ π β β) β§ π₯ β β) β if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0) β V) |
141 | | eqidd 2738 |
. . . . . 6
β’ ((π β§ π β β) β (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) = (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) |
142 | | eqidd 2738 |
. . . . . 6
β’ ((π β§ π β β) β (π₯ β β β¦ if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0)) = (π₯ β β β¦ if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0))) |
143 | 79, 108, 140, 141, 142 | ofrfval2 7639 |
. . . . 5
β’ ((π β§ π β β) β ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) βr β€ (π₯ β β β¦
if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0)) β βπ₯ β β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β€ if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0))) |
144 | 138, 143 | mpbird 257 |
. . . 4
β’ ((π β§ π β β) β (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) βr β€ (π₯ β β β¦
if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0))) |
145 | | peano2nn 12166 |
. . . . . 6
β’ (π β β β (π + 1) β
β) |
146 | 145 | adantl 483 |
. . . . 5
β’ ((π β§ π β β) β (π + 1) β β) |
147 | | breq2 5110 |
. . . . . . . 8
β’ (π = (π + 1) β ((πΉβπ₯) β€ π β (πΉβπ₯) β€ (π + 1))) |
148 | 147 | ifbid 4510 |
. . . . . . 7
β’ (π = (π + 1) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) = if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0)) |
149 | 148 | mpteq2dv 5208 |
. . . . . 6
β’ (π = (π + 1) β (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) = (π₯ β β β¦ if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0))) |
150 | 32 | mptex 7174 |
. . . . . 6
β’ (π₯ β β β¦
if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0)) β V |
151 | 149, 31, 150 | fvmpt 6949 |
. . . . 5
β’ ((π + 1) β β β
((π β β β¦
(π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))β(π + 1)) = (π₯ β β β¦ if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0))) |
152 | 146, 151 | syl 17 |
. . . 4
β’ ((π β§ π β β) β ((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))β(π + 1)) = (π₯ β β β¦ if((πΉβπ₯) β€ (π + 1), (πΉβπ₯), 0))) |
153 | 144, 47, 152 | 3brtr4d 5138 |
. . 3
β’ ((π β§ π β β) β ((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ) βr β€ ((π β β β¦ (π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))β(π + 1))) |
154 | 62 | ffvelcdmda 7036 |
. . . 4
β’ ((π β§ π¦ β β) β (πΉβπ¦) β β) |
155 | 34 | adantl 483 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ π β β) β ((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ) = (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) |
156 | 155 | fveq1d 6845 |
. . . . . 6
β’ (((π β§ π¦ β β) β§ π β β) β (((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦) = ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ¦)) |
157 | 112 | leidd 11722 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β) β (πΉβπ₯) β€ (πΉβπ₯)) |
158 | | breq1 5109 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ₯) = if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β ((πΉβπ₯) β€ (πΉβπ₯) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β€ (πΉβπ₯))) |
159 | | breq1 5109 |
. . . . . . . . . . . . . 14
β’ (0 =
if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β (0 β€ (πΉβπ₯) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β€ (πΉβπ₯))) |
160 | 158, 159 | ifboth 4526 |
. . . . . . . . . . . . 13
β’ (((πΉβπ₯) β€ (πΉβπ₯) β§ 0 β€ (πΉβπ₯)) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β€ (πΉβπ₯)) |
161 | 157, 128,
160 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β€ (πΉβπ₯)) |
162 | 161 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β€ (πΉβπ₯)) |
163 | 162 | ralrimiva 3144 |
. . . . . . . . . 10
β’ ((π β§ π β β) β βπ₯ β β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β€ (πΉβπ₯)) |
164 | 32 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β β β
V) |
165 | 1, 2 | ifex 4537 |
. . . . . . . . . . . 12
β’ if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β V |
166 | 165 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β V) |
167 | 54 | feqmptd 6911 |
. . . . . . . . . . . 12
β’ (π β πΉ = (π₯ β β β¦ (πΉβπ₯))) |
168 | 167 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β πΉ = (π₯ β β β¦ (πΉβπ₯))) |
169 | 164, 166,
113, 141, 168 | ofrfval2 7639 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) βr β€ πΉ β βπ₯ β β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β€ (πΉβπ₯))) |
170 | 163, 169 | mpbird 257 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) βr β€ πΉ) |
171 | 166 | fmpttd 7064 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)):ββΆV) |
172 | 171 | ffnd 6670 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) Fn β) |
173 | 55 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β πΉ Fn β) |
174 | | inidm 4179 |
. . . . . . . . . 10
β’ (β
β© β) = β |
175 | | eqidd 2738 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π¦ β β) β ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ¦) = ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ¦)) |
176 | | eqidd 2738 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π¦ β β) β (πΉβπ¦) = (πΉβπ¦)) |
177 | 172, 173,
164, 164, 174, 175, 176 | ofrfval 7628 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) βr β€ πΉ β βπ¦ β β ((π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ¦) β€ (πΉβπ¦))) |
178 | 170, 177 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π β β) β βπ¦ β β ((π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ¦) β€ (πΉβπ¦)) |
179 | 178 | r19.21bi 3235 |
. . . . . . 7
β’ (((π β§ π β β) β§ π¦ β β) β ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ¦) β€ (πΉβπ¦)) |
180 | 179 | an32s 651 |
. . . . . 6
β’ (((π β§ π¦ β β) β§ π β β) β ((π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ¦) β€ (πΉβπ¦)) |
181 | 156, 180 | eqbrtrd 5128 |
. . . . 5
β’ (((π β§ π¦ β β) β§ π β β) β (((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦) β€ (πΉβπ¦)) |
182 | 181 | ralrimiva 3144 |
. . . 4
β’ ((π β§ π¦ β β) β βπ β β (((π β β β¦ (π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦) β€ (πΉβπ¦)) |
183 | | brralrspcev 5166 |
. . . 4
β’ (((πΉβπ¦) β β β§ βπ β β (((π β β β¦ (π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦) β€ (πΉβπ¦)) β βπ§ β β βπ β β (((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦) β€ π§) |
184 | 154, 182,
183 | syl2anc 585 |
. . 3
β’ ((π β§ π¦ β β) β βπ§ β β βπ β β (((π β β β¦ (π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)βπ¦) β€ π§) |
185 | 28 | fveq2d 6847 |
. . . . . . 7
β’ (π = π β (β«2β(π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) = (β«2β(π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) |
186 | 185 | cbvmptv 5219 |
. . . . . 6
β’ (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) = (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) |
187 | 34 | fveq2d 6847 |
. . . . . . 7
β’ (π β β β
(β«2β((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ)) = (β«2β(π₯ β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) |
188 | 187 | mpteq2ia 5209 |
. . . . . 6
β’ (π β β β¦
(β«2β((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ))) = (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) |
189 | 186, 188 | eqtr4i 2768 |
. . . . 5
β’ (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) = (π β β β¦
(β«2β((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ))) |
190 | 189 | rneqi 5893 |
. . . 4
β’ ran
(π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))) = ran (π β β β¦
(β«2β((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ))) |
191 | 190 | supeq1i 9384 |
. . 3
β’ sup(ran
(π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))), β*, < ) =
sup(ran (π β β
β¦ (β«2β((π β β β¦ (π₯ β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))βπ))), β*, <
) |
192 | 42, 103, 109, 153, 184, 191 | itg2mono 25121 |
. 2
β’ (π β
(β«2β(π₯
β β β¦ sup(ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)), β, < ))) = sup(ran (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))), β*, <
)) |
193 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) = (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) |
194 | 27, 193, 165 | fvmpt 6949 |
. . . . . . . . . . 11
β’ (π β β β ((π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ) = if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) |
195 | 194 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π β β) β ((π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ) = if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) |
196 | 161 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π β β) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β€ (πΉβπ₯)) |
197 | 195, 196 | eqbrtrd 5128 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ π β β) β ((π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ) β€ (πΉβπ₯)) |
198 | 197 | ralrimiva 3144 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β βπ β β ((π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ) β€ (πΉβπ₯)) |
199 | 3 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ π β β) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β V) |
200 | 199 | fmpttd 7064 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)):ββΆV) |
201 | 200 | ffnd 6670 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) Fn β) |
202 | | breq1 5109 |
. . . . . . . . . 10
β’ (π€ = ((π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ) β (π€ β€ (πΉβπ₯) β ((π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ) β€ (πΉβπ₯))) |
203 | 202 | ralrn 7039 |
. . . . . . . . 9
β’ ((π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) Fn β β (βπ€ β ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))π€ β€ (πΉβπ₯) β βπ β β ((π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ) β€ (πΉβπ₯))) |
204 | 201, 203 | syl 17 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (βπ€ β ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))π€ β€ (πΉβπ₯) β βπ β β ((π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ) β€ (πΉβπ₯))) |
205 | 198, 204 | mpbird 257 |
. . . . . . 7
β’ ((π β§ π₯ β β) β βπ€ β ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))π€ β€ (πΉβπ₯)) |
206 | 112 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ π β β) β (πΉβπ₯) β β) |
207 | | 0re 11158 |
. . . . . . . . . . 11
β’ 0 β
β |
208 | | ifcl 4532 |
. . . . . . . . . . 11
β’ (((πΉβπ₯) β β β§ 0 β β)
β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β β) |
209 | 206, 207,
208 | sylancl 587 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π β β) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) β β) |
210 | 209 | fmpttd 7064 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯),
0)):ββΆβ) |
211 | 210 | frnd 6677 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β ran (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) β β) |
212 | | 1nn 12165 |
. . . . . . . . . 10
β’ 1 β
β |
213 | 193, 209 | dmmptd 6647 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β dom (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) = β) |
214 | 212, 213 | eleqtrrid 2845 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β 1 β dom (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) |
215 | | n0i 4294 |
. . . . . . . . . 10
β’ (1 β
dom (π β β
β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) β Β¬ dom (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) = β
) |
216 | | dm0rn0 5881 |
. . . . . . . . . . 11
β’ (dom
(π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) = β
β ran (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) = β
) |
217 | 216 | necon3bbii 2992 |
. . . . . . . . . 10
β’ (Β¬
dom (π β β
β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) = β
β ran (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) β β
) |
218 | 215, 217 | sylib 217 |
. . . . . . . . 9
β’ (1 β
dom (π β β
β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) β ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) β β
) |
219 | 214, 218 | syl 17 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β ran (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) β β
) |
220 | | brralrspcev 5166 |
. . . . . . . . 9
β’ (((πΉβπ₯) β β β§ βπ€ β ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))π€ β€ (πΉβπ₯)) β βπ§ β β βπ€ β ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))π€ β€ π§) |
221 | 112, 205,
220 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β βπ§ β β βπ€ β ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))π€ β€ π§) |
222 | | suprleub 12122 |
. . . . . . . 8
β’ (((ran
(π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) β β β§ ran (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) β β
β§ βπ§ β β βπ€ β ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))π€ β€ π§) β§ (πΉβπ₯) β β) β (sup(ran (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)), β, < ) β€ (πΉβπ₯) β βπ€ β ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))π€ β€ (πΉβπ₯))) |
223 | 211, 219,
221, 112, 222 | syl31anc 1374 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (sup(ran (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)), β, < ) β€ (πΉβπ₯) β βπ€ β ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))π€ β€ (πΉβπ₯))) |
224 | 205, 223 | mpbird 257 |
. . . . . 6
β’ ((π β§ π₯ β β) β sup(ran (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)), β, < ) β€ (πΉβπ₯)) |
225 | | arch 12411 |
. . . . . . . . 9
β’ ((πΉβπ₯) β β β βπ β β (πΉβπ₯) < π) |
226 | 112, 225 | syl 17 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β βπ β β (πΉβπ₯) < π) |
227 | 194 | ad2antrl 727 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ (π β β β§ (πΉβπ₯) < π)) β ((π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ) = if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) |
228 | | ltle 11244 |
. . . . . . . . . . . . 13
β’ (((πΉβπ₯) β β β§ π β β) β ((πΉβπ₯) < π β (πΉβπ₯) β€ π)) |
229 | 112, 48, 228 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β) β§ π β β) β ((πΉβπ₯) < π β (πΉβπ₯) β€ π)) |
230 | 229 | impr 456 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ (π β β β§ (πΉβπ₯) < π)) β (πΉβπ₯) β€ π) |
231 | 230 | iftrued 4495 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ (π β β β§ (πΉβπ₯) < π)) β if((πΉβπ₯) β€ π, (πΉβπ₯), 0) = (πΉβπ₯)) |
232 | 227, 231 | eqtrd 2777 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ (π β β β§ (πΉβπ₯) < π)) β ((π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ) = (πΉβπ₯)) |
233 | 201 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ (π β β β§ (πΉβπ₯) < π)) β (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) Fn β) |
234 | | simprl 770 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ (π β β β§ (πΉβπ₯) < π)) β π β β) |
235 | | fnfvelrn 7032 |
. . . . . . . . . 10
β’ (((π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)) Fn β β§ π β β) β ((π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ) β ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) |
236 | 233, 234,
235 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ (π β β β§ (πΉβπ₯) < π)) β ((π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))βπ) β ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) |
237 | 232, 236 | eqeltrrd 2839 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ (π β β β§ (πΉβπ₯) < π)) β (πΉβπ₯) β ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) |
238 | 226, 237 | rexlimddv 3159 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (πΉβπ₯) β ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0))) |
239 | 211, 219,
221, 238 | suprubd 12118 |
. . . . . 6
β’ ((π β§ π₯ β β) β (πΉβπ₯) β€ sup(ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)), β, < )) |
240 | 211, 219,
221 | suprcld 12119 |
. . . . . . 7
β’ ((π β§ π₯ β β) β sup(ran (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)), β, < ) β
β) |
241 | 240, 112 | letri3d 11298 |
. . . . . 6
β’ ((π β§ π₯ β β) β (sup(ran (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)), β, < ) = (πΉβπ₯) β (sup(ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)), β, < ) β€ (πΉβπ₯) β§ (πΉβπ₯) β€ sup(ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)), β, < )))) |
242 | 224, 239,
241 | mpbir2and 712 |
. . . . 5
β’ ((π β§ π₯ β β) β sup(ran (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)), β, < ) = (πΉβπ₯)) |
243 | 242 | mpteq2dva 5206 |
. . . 4
β’ (π β (π₯ β β β¦ sup(ran (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)), β, < )) = (π₯ β β β¦ (πΉβπ₯))) |
244 | 243, 167 | eqtr4d 2780 |
. . 3
β’ (π β (π₯ β β β¦ sup(ran (π β β β¦
if((πΉβπ₯) β€ π, (πΉβπ₯), 0)), β, < )) = πΉ) |
245 | 244 | fveq2d 6847 |
. 2
β’ (π β
(β«2β(π₯
β β β¦ sup(ran (π β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)), β, < ))) =
(β«2βπΉ)) |
246 | 192, 245 | eqtr3d 2779 |
1
β’ (π β sup(ran (π β β β¦
(β«2β(π₯
β β β¦ if((πΉβπ₯) β€ π, (πΉβπ₯), 0)))), β*, < ) =
(β«2βπΉ)) |