Step | Hyp | Ref
| Expression |
1 | | mbfi1flimlem.2 |
. . . . 5
β’ (π β πΉ:ββΆβ) |
2 | 1 | ffvelcdmda 7039 |
. . . 4
β’ ((π β§ π¦ β β) β (πΉβπ¦) β β) |
3 | 1 | feqmptd 6914 |
. . . . 5
β’ (π β πΉ = (π¦ β β β¦ (πΉβπ¦))) |
4 | | mbfi1flim.1 |
. . . . 5
β’ (π β πΉ β MblFn) |
5 | 3, 4 | eqeltrrd 2835 |
. . . 4
β’ (π β (π¦ β β β¦ (πΉβπ¦)) β MblFn) |
6 | 2, 5 | mbfpos 25038 |
. . 3
β’ (π β (π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0)) β MblFn) |
7 | | 0re 11165 |
. . . . . 6
β’ 0 β
β |
8 | | ifcl 4535 |
. . . . . 6
β’ (((πΉβπ¦) β β β§ 0 β β)
β if(0 β€ (πΉβπ¦), (πΉβπ¦), 0) β β) |
9 | 2, 7, 8 | sylancl 587 |
. . . . 5
β’ ((π β§ π¦ β β) β if(0 β€ (πΉβπ¦), (πΉβπ¦), 0) β β) |
10 | | max1 13113 |
. . . . . 6
β’ ((0
β β β§ (πΉβπ¦) β β) β 0 β€ if(0 β€
(πΉβπ¦), (πΉβπ¦), 0)) |
11 | 7, 2, 10 | sylancr 588 |
. . . . 5
β’ ((π β§ π¦ β β) β 0 β€ if(0 β€
(πΉβπ¦), (πΉβπ¦), 0)) |
12 | | elrege0 13380 |
. . . . 5
β’ (if(0
β€ (πΉβπ¦), (πΉβπ¦), 0) β (0[,)+β) β (if(0 β€
(πΉβπ¦), (πΉβπ¦), 0) β β β§ 0 β€ if(0 β€
(πΉβπ¦), (πΉβπ¦), 0))) |
13 | 9, 11, 12 | sylanbrc 584 |
. . . 4
β’ ((π β§ π¦ β β) β if(0 β€ (πΉβπ¦), (πΉβπ¦), 0) β (0[,)+β)) |
14 | 13 | fmpttd 7067 |
. . 3
β’ (π β (π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦),
0)):ββΆ(0[,)+β)) |
15 | 6, 14 | mbfi1fseq 25109 |
. 2
β’ (π β βπ(π:ββΆdom β«1 β§
βπ β β
(0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))) β§ βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯))) |
16 | 2 | renegcld 11590 |
. . . 4
β’ ((π β§ π¦ β β) β -(πΉβπ¦) β β) |
17 | 2, 5 | mbfneg 25037 |
. . . 4
β’ (π β (π¦ β β β¦ -(πΉβπ¦)) β MblFn) |
18 | 16, 17 | mbfpos 25038 |
. . 3
β’ (π β (π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0)) β MblFn) |
19 | | ifcl 4535 |
. . . . . 6
β’ ((-(πΉβπ¦) β β β§ 0 β β)
β if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0) β β) |
20 | 16, 7, 19 | sylancl 587 |
. . . . 5
β’ ((π β§ π¦ β β) β if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0) β β) |
21 | | max1 13113 |
. . . . . 6
β’ ((0
β β β§ -(πΉβπ¦) β β) β 0 β€ if(0 β€
-(πΉβπ¦), -(πΉβπ¦), 0)) |
22 | 7, 16, 21 | sylancr 588 |
. . . . 5
β’ ((π β§ π¦ β β) β 0 β€ if(0 β€
-(πΉβπ¦), -(πΉβπ¦), 0)) |
23 | | elrege0 13380 |
. . . . 5
β’ (if(0
β€ -(πΉβπ¦), -(πΉβπ¦), 0) β (0[,)+β) β (if(0 β€
-(πΉβπ¦), -(πΉβπ¦), 0) β β β§ 0 β€ if(0 β€
-(πΉβπ¦), -(πΉβπ¦), 0))) |
24 | 20, 22, 23 | sylanbrc 584 |
. . . 4
β’ ((π β§ π¦ β β) β if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0) β (0[,)+β)) |
25 | 24 | fmpttd 7067 |
. . 3
β’ (π β (π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦),
0)):ββΆ(0[,)+β)) |
26 | 18, 25 | mbfi1fseq 25109 |
. 2
β’ (π β ββ(β:ββΆdom β«1 β§
βπ β β
(0π βr β€ (ββπ) β§ (ββπ) βr β€ (ββ(π + 1))) β§ βπ₯ β β (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯))) |
27 | | exdistrv 1960 |
. . 3
β’
(βπββ((π:ββΆdom β«1 β§
βπ β β
(0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))) β§ βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯)) β§ (β:ββΆdom β«1 β§
βπ β β
(0π βr β€ (ββπ) β§ (ββπ) βr β€ (ββ(π + 1))) β§ βπ₯ β β (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯))) β (βπ(π:ββΆdom β«1 β§
βπ β β
(0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))) β§ βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯)) β§ ββ(β:ββΆdom β«1 β§
βπ β β
(0π βr β€ (ββπ) β§ (ββπ) βr β€ (ββ(π + 1))) β§ βπ₯ β β (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯)))) |
28 | | 3simpb 1150 |
. . . . . . 7
β’ ((π:ββΆdom
β«1 β§ βπ β β (0π
βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))) β§ βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯)) β (π:ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯))) |
29 | | 3simpb 1150 |
. . . . . . 7
β’ ((β:ββΆdom
β«1 β§ βπ β β (0π
βr β€ (ββπ) β§ (ββπ) βr β€ (ββ(π + 1))) β§ βπ₯ β β (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯)) β (β:ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯))) |
30 | 28, 29 | anim12i 614 |
. . . . . 6
β’ (((π:ββΆdom
β«1 β§ βπ β β (0π
βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))) β§ βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯)) β§ (β:ββΆdom β«1 β§
βπ β β
(0π βr β€ (ββπ) β§ (ββπ) βr β€ (ββ(π + 1))) β§ βπ₯ β β (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯))) β ((π:ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯)) β§ (β:ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯)))) |
31 | | an4 655 |
. . . . . 6
β’ (((π:ββΆdom
β«1 β§ βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯)) β§ (β:ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯))) β ((π:ββΆdom β«1 β§
β:ββΆdom
β«1) β§ (βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯) β§ βπ₯ β β (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯)))) |
32 | 30, 31 | sylib 217 |
. . . . 5
β’ (((π:ββΆdom
β«1 β§ βπ β β (0π
βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))) β§ βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯)) β§ (β:ββΆdom β«1 β§
βπ β β
(0π βr β€ (ββπ) β§ (ββπ) βr β€ (ββ(π + 1))) β§ βπ₯ β β (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯))) β ((π:ββΆdom β«1 β§
β:ββΆdom
β«1) β§ (βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯) β§ βπ₯ β β (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯)))) |
33 | | r19.26 3111 |
. . . . . . 7
β’
(βπ₯ β
β ((π β β
β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯) β§ (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯)) β (βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯) β§ βπ₯ β β (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯))) |
34 | | i1fsub 25096 |
. . . . . . . . . 10
β’ ((π₯ β dom β«1
β§ π¦ β dom
β«1) β (π₯ βf β π¦) β dom
β«1) |
35 | 34 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ (π₯ β dom β«1 β§ π¦ β dom β«1))
β (π₯
βf β π¦) β dom
β«1) |
36 | | simprl 770 |
. . . . . . . . 9
β’ ((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β π:ββΆdom
β«1) |
37 | | simprr 772 |
. . . . . . . . 9
β’ ((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β β:ββΆdom
β«1) |
38 | | nnex 12167 |
. . . . . . . . . 10
β’ β
β V |
39 | 38 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β β β V) |
40 | | inidm 4182 |
. . . . . . . . 9
β’ (β
β© β) = β |
41 | 35, 36, 37, 39, 39, 40 | off 7639 |
. . . . . . . 8
β’ ((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β (π βf βf
β β):ββΆdom
β«1) |
42 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π₯ β (πΉβπ¦) = (πΉβπ₯)) |
43 | 42 | breq2d 5121 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π₯ β (0 β€ (πΉβπ¦) β 0 β€ (πΉβπ₯))) |
44 | 43, 42 | ifbieq1d 4514 |
. . . . . . . . . . . . . 14
β’ (π¦ = π₯ β if(0 β€ (πΉβπ¦), (πΉβπ¦), 0) = if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) |
45 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β¦ if(0
β€ (πΉβπ¦), (πΉβπ¦), 0)) = (π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0)) |
46 | | fvex 6859 |
. . . . . . . . . . . . . . 15
β’ (πΉβπ₯) β V |
47 | | c0ex 11157 |
. . . . . . . . . . . . . . 15
β’ 0 β
V |
48 | 46, 47 | ifex 4540 |
. . . . . . . . . . . . . 14
β’ if(0 β€
(πΉβπ₯), (πΉβπ₯), 0) β V |
49 | 44, 45, 48 | fvmpt 6952 |
. . . . . . . . . . . . 13
β’ (π₯ β β β ((π¦ β β β¦ if(0
β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯) = if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) |
50 | 49 | breq2d 5121 |
. . . . . . . . . . . 12
β’ (π₯ β β β ((π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯) β (π β β β¦ ((πβπ)βπ₯)) β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0))) |
51 | 42 | negeqd 11403 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π₯ β -(πΉβπ¦) = -(πΉβπ₯)) |
52 | 51 | breq2d 5121 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π₯ β (0 β€ -(πΉβπ¦) β 0 β€ -(πΉβπ₯))) |
53 | 52, 51 | ifbieq1d 4514 |
. . . . . . . . . . . . . 14
β’ (π¦ = π₯ β if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0) = if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) |
54 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β¦ if(0
β€ -(πΉβπ¦), -(πΉβπ¦), 0)) = (π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0)) |
55 | | negex 11407 |
. . . . . . . . . . . . . . 15
β’ -(πΉβπ₯) β V |
56 | 55, 47 | ifex 4540 |
. . . . . . . . . . . . . 14
β’ if(0 β€
-(πΉβπ₯), -(πΉβπ₯), 0) β V |
57 | 53, 54, 56 | fvmpt 6952 |
. . . . . . . . . . . . 13
β’ (π₯ β β β ((π¦ β β β¦ if(0
β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯) = if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) |
58 | 57 | breq2d 5121 |
. . . . . . . . . . . 12
β’ (π₯ β β β ((π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯) β (π β β β¦ ((ββπ)βπ₯)) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) |
59 | 50, 58 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π₯ β β β (((π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯) β§ (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯)) β ((π β β β¦ ((πβπ)βπ₯)) β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β§ (π β β β¦ ((ββπ)βπ₯)) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)))) |
60 | 59 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β (((π
β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯) β§ (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯)) β ((π β β β¦ ((πβπ)βπ₯)) β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β§ (π β β β¦ ((ββπ)βπ₯)) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)))) |
61 | | nnuz 12814 |
. . . . . . . . . . . . 13
β’ β =
(β€β₯β1) |
62 | | 1zzd 12542 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β§ ((π
β β β¦ ((πβπ)βπ₯)) β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β§ (π β β β¦ ((ββπ)βπ₯)) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) β 1 β
β€) |
63 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β§ ((π
β β β¦ ((πβπ)βπ₯)) β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β§ (π β β β¦ ((ββπ)βπ₯)) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) β (π β β β¦ ((πβπ)βπ₯)) β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) |
64 | 38 | mptex 7177 |
. . . . . . . . . . . . . 14
β’ (π β β β¦ (((π βf
βf β β)βπ)βπ₯)) β V |
65 | 64 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β§ ((π
β β β¦ ((πβπ)βπ₯)) β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β§ (π β β β¦ ((ββπ)βπ₯)) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) β (π β β β¦ (((π βf βf
β β)βπ)βπ₯)) β V) |
66 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β§ ((π
β β β¦ ((πβπ)βπ₯)) β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β§ (π β β β¦ ((ββπ)βπ₯)) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) β (π β β β¦ ((ββπ)βπ₯)) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) |
67 | 36 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β (πβπ) β dom
β«1) |
68 | | i1ff 25063 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πβπ) β dom β«1 β (πβπ):ββΆβ) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β (πβπ):ββΆβ) |
70 | 69 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β§ π₯
β β) β ((πβπ)βπ₯) β β) |
71 | 70 | an32s 651 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β§ π
β β) β ((πβπ)βπ₯) β β) |
72 | 71 | recnd 11191 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β§ π
β β) β ((πβπ)βπ₯) β β) |
73 | 72 | fmpttd 7067 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β (π
β β β¦ ((πβπ)βπ₯)):ββΆβ) |
74 | 73 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β§ ((π
β β β¦ ((πβπ)βπ₯)) β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β§ (π β β β¦ ((ββπ)βπ₯)) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) β (π β β β¦ ((πβπ)βπ₯)):ββΆβ) |
75 | 74 | ffvelcdmda 7039 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π:ββΆdom
β«1 β§ β:ββΆdom β«1)) β§
π₯ β β) β§
((π β β β¦
((πβπ)βπ₯)) β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β§ (π β β β¦ ((ββπ)βπ₯)) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) β§ π β β) β ((π β β β¦ ((πβπ)βπ₯))βπ) β β) |
76 | 37 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β (ββπ) β dom
β«1) |
77 | | i1ff 25063 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((ββπ) β dom β«1 β (ββπ):ββΆβ) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β (ββπ):ββΆβ) |
79 | 78 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β§ π₯
β β) β ((ββπ)βπ₯) β β) |
80 | 79 | an32s 651 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β§ π
β β) β ((ββπ)βπ₯) β β) |
81 | 80 | recnd 11191 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β§ π
β β) β ((ββπ)βπ₯) β β) |
82 | 81 | fmpttd 7067 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β (π
β β β¦ ((ββπ)βπ₯)):ββΆβ) |
83 | 82 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β§ ((π
β β β¦ ((πβπ)βπ₯)) β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β§ (π β β β¦ ((ββπ)βπ₯)) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) β (π β β β¦ ((ββπ)βπ₯)):ββΆβ) |
84 | 83 | ffvelcdmda 7039 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π:ββΆdom
β«1 β§ β:ββΆdom β«1)) β§
π₯ β β) β§
((π β β β¦
((πβπ)βπ₯)) β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β§ (π β β β¦ ((ββπ)βπ₯)) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) β§ π β β) β ((π β β β¦ ((ββπ)βπ₯))βπ) β β) |
85 | 36 | ffnd 6673 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β π Fn β) |
86 | 37 | ffnd 6673 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β β
Fn β) |
87 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β (πβπ) = (πβπ)) |
88 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β (ββπ) = (ββπ)) |
89 | 85, 86, 39, 39, 40, 87, 88 | ofval 7632 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β ((π
βf βf β β)βπ) = ((πβπ) βf β (ββπ))) |
90 | 89 | fveq1d 6848 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β (((π
βf βf β β)βπ)βπ₯) = (((πβπ) βf β (ββπ))βπ₯)) |
91 | 90 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β§ π₯
β β) β (((π
βf βf β β)βπ)βπ₯) = (((πβπ) βf β (ββπ))βπ₯)) |
92 | 36 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β (πβπ) β dom
β«1) |
93 | | i1ff 25063 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πβπ) β dom β«1 β (πβπ):ββΆβ) |
94 | | ffn 6672 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πβπ):ββΆβ β (πβπ) Fn β) |
95 | 92, 93, 94 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β (πβπ) Fn β) |
96 | 37 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β (ββπ) β dom
β«1) |
97 | | i1ff 25063 |
. . . . . . . . . . . . . . . . . . 19
β’ ((ββπ) β dom β«1 β (ββπ):ββΆβ) |
98 | | ffn 6672 |
. . . . . . . . . . . . . . . . . . 19
β’ ((ββπ):ββΆβ β (ββπ) Fn β) |
99 | 96, 97, 98 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β (ββπ) Fn β) |
100 | | reex 11150 |
. . . . . . . . . . . . . . . . . . 19
β’ β
β V |
101 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β β β V) |
102 | | inidm 4182 |
. . . . . . . . . . . . . . . . . 18
β’ (β
β© β) = β |
103 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β§ π₯
β β) β ((πβπ)βπ₯) = ((πβπ)βπ₯)) |
104 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β§ π₯
β β) β ((ββπ)βπ₯) = ((ββπ)βπ₯)) |
105 | 95, 99, 101, 101, 102, 103, 104 | ofval 7632 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β§ π₯
β β) β (((πβπ) βf β (ββπ))βπ₯) = (((πβπ)βπ₯) β ((ββπ)βπ₯))) |
106 | 91, 105 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π
β β) β§ π₯
β β) β (((π
βf βf β β)βπ)βπ₯) = (((πβπ)βπ₯) β ((ββπ)βπ₯))) |
107 | 106 | an32s 651 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β§ π
β β) β (((π
βf βf β β)βπ)βπ₯) = (((πβπ)βπ₯) β ((ββπ)βπ₯))) |
108 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((π βf βf
β β)βπ) = ((π βf βf
β β)βπ)) |
109 | 108 | fveq1d 6848 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (((π βf βf
β β)βπ)βπ₯) = (((π βf βf
β β)βπ)βπ₯)) |
110 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β¦ (((π βf
βf β β)βπ)βπ₯)) = (π β β β¦ (((π βf βf
β β)βπ)βπ₯)) |
111 | | fvex 6859 |
. . . . . . . . . . . . . . . . 17
β’ (((π βf
βf β β)βπ)βπ₯) β V |
112 | 109, 110,
111 | fvmpt 6952 |
. . . . . . . . . . . . . . . 16
β’ (π β β β ((π β β β¦ (((π βf
βf β β)βπ)βπ₯))βπ) = (((π βf βf
β β)βπ)βπ₯)) |
113 | 112 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β§ π
β β) β ((π
β β β¦ (((π
βf βf β β)βπ)βπ₯))βπ) = (((π βf βf
β β)βπ)βπ₯)) |
114 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (πβπ) = (πβπ)) |
115 | 114 | fveq1d 6848 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((πβπ)βπ₯) = ((πβπ)βπ₯)) |
116 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β¦ ((πβπ)βπ₯)) = (π β β β¦ ((πβπ)βπ₯)) |
117 | | fvex 6859 |
. . . . . . . . . . . . . . . . . 18
β’ ((πβπ)βπ₯) β V |
118 | 115, 116,
117 | fvmpt 6952 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β ((π β β β¦ ((πβπ)βπ₯))βπ) = ((πβπ)βπ₯)) |
119 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (ββπ) = (ββπ)) |
120 | 119 | fveq1d 6848 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((ββπ)βπ₯) = ((ββπ)βπ₯)) |
121 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β¦ ((ββπ)βπ₯)) = (π β β β¦ ((ββπ)βπ₯)) |
122 | | fvex 6859 |
. . . . . . . . . . . . . . . . . 18
β’ ((ββπ)βπ₯) β V |
123 | 120, 121,
122 | fvmpt 6952 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β ((π β β β¦ ((ββπ)βπ₯))βπ) = ((ββπ)βπ₯)) |
124 | 118, 123 | oveq12d 7379 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (((π β β β¦ ((πβπ)βπ₯))βπ) β ((π β β β¦ ((ββπ)βπ₯))βπ)) = (((πβπ)βπ₯) β ((ββπ)βπ₯))) |
125 | 124 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β§ π
β β) β (((π
β β β¦ ((πβπ)βπ₯))βπ) β ((π β β β¦ ((ββπ)βπ₯))βπ)) = (((πβπ)βπ₯) β ((ββπ)βπ₯))) |
126 | 107, 113,
125 | 3eqtr4d 2783 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β§ π
β β) β ((π
β β β¦ (((π
βf βf β β)βπ)βπ₯))βπ) = (((π β β β¦ ((πβπ)βπ₯))βπ) β ((π β β β¦ ((ββπ)βπ₯))βπ))) |
127 | 126 | adantlr 714 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π:ββΆdom
β«1 β§ β:ββΆdom β«1)) β§
π₯ β β) β§
((π β β β¦
((πβπ)βπ₯)) β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β§ (π β β β¦ ((ββπ)βπ₯)) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) β§ π β β) β ((π β β β¦ (((π βf βf
β β)βπ)βπ₯))βπ) = (((π β β β¦ ((πβπ)βπ₯))βπ) β ((π β β β¦ ((ββπ)βπ₯))βπ))) |
128 | 61, 62, 63, 65, 66, 75, 84, 127 | climsub 15525 |
. . . . . . . . . . . 12
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β§ ((π
β β β¦ ((πβπ)βπ₯)) β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β§ (π β β β¦ ((ββπ)βπ₯)) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) β (π β β β¦ (((π βf βf
β β)βπ)βπ₯)) β (if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) |
129 | 1 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β πΉ:ββΆβ) |
130 | 129 | ffvelcdmda 7039 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β (πΉβπ₯) β β) |
131 | | max0sub 13124 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ₯) β β β (if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) = (πΉβπ₯)) |
132 | 130, 131 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β (if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) = (πΉβπ₯)) |
133 | 132 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β§ ((π
β β β¦ ((πβπ)βπ₯)) β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β§ (π β β β¦ ((ββπ)βπ₯)) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) β (if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) = (πΉβπ₯)) |
134 | 128, 133 | breqtrd 5135 |
. . . . . . . . . . 11
β’ ((((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β§ ((π
β β β¦ ((πβπ)βπ₯)) β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β§ (π β β β¦ ((ββπ)βπ₯)) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) β (π β β β¦ (((π βf βf
β β)βπ)βπ₯)) β (πΉβπ₯)) |
135 | 134 | ex 414 |
. . . . . . . . . 10
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β (((π
β β β¦ ((πβπ)βπ₯)) β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β§ (π β β β¦ ((ββπ)βπ₯)) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) β (π β β β¦ (((π βf βf
β β)βπ)βπ₯)) β (πΉβπ₯))) |
136 | 60, 135 | sylbid 239 |
. . . . . . . . 9
β’ (((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β§ π₯
β β) β (((π
β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯) β§ (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯)) β (π β β β¦ (((π βf βf
β β)βπ)βπ₯)) β (πΉβπ₯))) |
137 | 136 | ralimdva 3161 |
. . . . . . . 8
β’ ((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β (βπ₯ β β ((π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯) β§ (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯)) β βπ₯ β β (π β β β¦ (((π βf βf
β β)βπ)βπ₯)) β (πΉβπ₯))) |
138 | | ovex 7394 |
. . . . . . . . 9
β’ (π βf
βf β β) β V |
139 | | feq1 6653 |
. . . . . . . . . 10
β’ (π = (π βf βf
β β) β (π:ββΆdom
β«1 β (π
βf βf β β):ββΆdom
β«1)) |
140 | | fveq1 6845 |
. . . . . . . . . . . . . 14
β’ (π = (π βf βf
β β) β (πβπ) = ((π βf βf
β β)βπ)) |
141 | 140 | fveq1d 6848 |
. . . . . . . . . . . . 13
β’ (π = (π βf βf
β β) β ((πβπ)βπ₯) = (((π βf βf
β β)βπ)βπ₯)) |
142 | 141 | mpteq2dv 5211 |
. . . . . . . . . . . 12
β’ (π = (π βf βf
β β) β (π β β β¦ ((πβπ)βπ₯)) = (π β β β¦ (((π βf βf
β β)βπ)βπ₯))) |
143 | 142 | breq1d 5119 |
. . . . . . . . . . 11
β’ (π = (π βf βf
β β) β ((π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯) β (π β β β¦ (((π βf βf
β β)βπ)βπ₯)) β (πΉβπ₯))) |
144 | 143 | ralbidv 3171 |
. . . . . . . . . 10
β’ (π = (π βf βf
β β) β
(βπ₯ β β
(π β β β¦
((πβπ)βπ₯)) β (πΉβπ₯) β βπ₯ β β (π β β β¦ (((π βf βf
β β)βπ)βπ₯)) β (πΉβπ₯))) |
145 | 139, 144 | anbi12d 632 |
. . . . . . . . 9
β’ (π = (π βf βf
β β) β ((π:ββΆdom
β«1 β§ βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯)) β ((π βf βf
β β):ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
(((π βf
βf β β)βπ)βπ₯)) β (πΉβπ₯)))) |
146 | 138, 145 | spcev 3567 |
. . . . . . . 8
β’ (((π βf
βf β β):ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
(((π βf
βf β β)βπ)βπ₯)) β (πΉβπ₯)) β βπ(π:ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
((πβπ)βπ₯)) β (πΉβπ₯))) |
147 | 41, 137, 146 | syl6an 683 |
. . . . . . 7
β’ ((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β (βπ₯ β β ((π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯) β§ (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯)) β βπ(π:ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
((πβπ)βπ₯)) β (πΉβπ₯)))) |
148 | 33, 147 | biimtrrid 242 |
. . . . . 6
β’ ((π β§ (π:ββΆdom β«1 β§
β:ββΆdom
β«1)) β ((βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯) β§ βπ₯ β β (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯)) β βπ(π:ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
((πβπ)βπ₯)) β (πΉβπ₯)))) |
149 | 148 | expimpd 455 |
. . . . 5
β’ (π β (((π:ββΆdom β«1 β§
β:ββΆdom
β«1) β§ (βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯) β§ βπ₯ β β (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯))) β βπ(π:ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
((πβπ)βπ₯)) β (πΉβπ₯)))) |
150 | 32, 149 | syl5 34 |
. . . 4
β’ (π β (((π:ββΆdom β«1 β§
βπ β β
(0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))) β§ βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯)) β§ (β:ββΆdom β«1 β§
βπ β β
(0π βr β€ (ββπ) β§ (ββπ) βr β€ (ββ(π + 1))) β§ βπ₯ β β (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯))) β βπ(π:ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
((πβπ)βπ₯)) β (πΉβπ₯)))) |
151 | 150 | exlimdvv 1938 |
. . 3
β’ (π β (βπββ((π:ββΆdom β«1 β§
βπ β β
(0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))) β§ βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯)) β§ (β:ββΆdom β«1 β§
βπ β β
(0π βr β€ (ββπ) β§ (ββπ) βr β€ (ββ(π + 1))) β§ βπ₯ β β (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯))) β βπ(π:ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
((πβπ)βπ₯)) β (πΉβπ₯)))) |
152 | 27, 151 | biimtrrid 242 |
. 2
β’ (π β ((βπ(π:ββΆdom β«1 β§
βπ β β
(0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))) β§ βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ (πΉβπ¦), (πΉβπ¦), 0))βπ₯)) β§ ββ(β:ββΆdom β«1 β§
βπ β β
(0π βr β€ (ββπ) β§ (ββπ) βr β€ (ββ(π + 1))) β§ βπ₯ β β (π β β β¦ ((ββπ)βπ₯)) β ((π¦ β β β¦ if(0 β€ -(πΉβπ¦), -(πΉβπ¦), 0))βπ₯))) β βπ(π:ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
((πβπ)βπ₯)) β (πΉβπ₯)))) |
153 | 15, 26, 152 | mp2and 698 |
1
β’ (π β βπ(π:ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
((πβπ)βπ₯)) β (πΉβπ₯))) |