Step | Hyp | Ref
| Expression |
1 | | isercoll2.z |
. . 3
β’ π =
(β€β₯βπ) |
2 | | isercoll2.m |
. . 3
β’ (π β π β β€) |
3 | | 1z 12589 |
. . . 4
β’ 1 β
β€ |
4 | | zsubcl 12601 |
. . . 4
β’ ((1
β β€ β§ π
β β€) β (1 β π) β β€) |
5 | 3, 2, 4 | sylancr 588 |
. . 3
β’ (π β (1 β π) β
β€) |
6 | | seqex 13965 |
. . . 4
β’ seqπ( + , π») β V |
7 | 6 | a1i 11 |
. . 3
β’ (π β seqπ( + , π») β V) |
8 | | seqex 13965 |
. . . 4
β’ seq1( + ,
(π₯ β β β¦
(π»β(π + (π₯ β 1))))) β V |
9 | 8 | a1i 11 |
. . 3
β’ (π β seq1( + , (π₯ β β β¦ (π»β(π + (π₯ β 1))))) β V) |
10 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β π) β π β π) |
11 | 10, 1 | eleqtrdi 2844 |
. . . . 5
β’ ((π β§ π β π) β π β (β€β₯βπ)) |
12 | 5 | adantr 482 |
. . . . 5
β’ ((π β§ π β π) β (1 β π) β β€) |
13 | | simpl 484 |
. . . . . 6
β’ ((π β§ π β π) β π) |
14 | | elfzuz 13494 |
. . . . . . 7
β’ (π β (π...π) β π β (β€β₯βπ)) |
15 | 14, 1 | eleqtrrdi 2845 |
. . . . . 6
β’ (π β (π...π) β π β π) |
16 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β π) |
17 | 16, 1 | eleqtrdi 2844 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β π β (β€β₯βπ)) |
18 | | eluzelz 12829 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯βπ) β π β β€) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β π β β€) |
20 | 19 | zcnd 12664 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β β) |
21 | 2 | zcnd 12664 |
. . . . . . . . . . 11
β’ (π β π β β) |
22 | 21 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β β) |
23 | | 1cnd 11206 |
. . . . . . . . . 10
β’ ((π β§ π β π) β 1 β β) |
24 | 20, 22, 23 | subadd23d 11590 |
. . . . . . . . 9
β’ ((π β§ π β π) β ((π β π) + 1) = (π + (1 β π))) |
25 | | uznn0sub 12858 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ) β (π β π) β
β0) |
26 | 17, 25 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (π β π) β
β0) |
27 | | nn0p1nn 12508 |
. . . . . . . . . 10
β’ ((π β π) β β0 β ((π β π) + 1) β β) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β π) β ((π β π) + 1) β β) |
29 | 24, 28 | eqeltrrd 2835 |
. . . . . . . 8
β’ ((π β§ π β π) β (π + (1 β π)) β β) |
30 | | oveq1 7413 |
. . . . . . . . . . 11
β’ (π₯ = (π + (1 β π)) β (π₯ β 1) = ((π + (1 β π)) β 1)) |
31 | 30 | oveq2d 7422 |
. . . . . . . . . 10
β’ (π₯ = (π + (1 β π)) β (π + (π₯ β 1)) = (π + ((π + (1 β π)) β 1))) |
32 | 31 | fveq2d 6893 |
. . . . . . . . 9
β’ (π₯ = (π + (1 β π)) β (π»β(π + (π₯ β 1))) = (π»β(π + ((π + (1 β π)) β 1)))) |
33 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β β β¦ (π»β(π + (π₯ β 1)))) = (π₯ β β β¦ (π»β(π + (π₯ β 1)))) |
34 | | fvex 6902 |
. . . . . . . . 9
β’ (π»β(π + ((π + (1 β π)) β 1))) β V |
35 | 32, 33, 34 | fvmpt 6996 |
. . . . . . . 8
β’ ((π + (1 β π)) β β β ((π₯ β β β¦ (π»β(π + (π₯ β 1))))β(π + (1 β π))) = (π»β(π + ((π + (1 β π)) β 1)))) |
36 | 29, 35 | syl 17 |
. . . . . . 7
β’ ((π β§ π β π) β ((π₯ β β β¦ (π»β(π + (π₯ β 1))))β(π + (1 β π))) = (π»β(π + ((π + (1 β π)) β 1)))) |
37 | 24 | oveq1d 7421 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (((π β π) + 1) β 1) = ((π + (1 β π)) β 1)) |
38 | 26 | nn0cnd 12531 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (π β π) β β) |
39 | | ax-1cn 11165 |
. . . . . . . . . . . 12
β’ 1 β
β |
40 | | pncan 11463 |
. . . . . . . . . . . 12
β’ (((π β π) β β β§ 1 β β)
β (((π β π) + 1) β 1) = (π β π)) |
41 | 38, 39, 40 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (((π β π) + 1) β 1) = (π β π)) |
42 | 37, 41 | eqtr3d 2775 |
. . . . . . . . . 10
β’ ((π β§ π β π) β ((π + (1 β π)) β 1) = (π β π)) |
43 | 42 | oveq2d 7422 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π + ((π + (1 β π)) β 1)) = (π + (π β π))) |
44 | 22, 20 | pncan3d 11571 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π + (π β π)) = π) |
45 | 43, 44 | eqtrd 2773 |
. . . . . . . 8
β’ ((π β§ π β π) β (π + ((π + (1 β π)) β 1)) = π) |
46 | 45 | fveq2d 6893 |
. . . . . . 7
β’ ((π β§ π β π) β (π»β(π + ((π + (1 β π)) β 1))) = (π»βπ)) |
47 | 36, 46 | eqtr2d 2774 |
. . . . . 6
β’ ((π β§ π β π) β (π»βπ) = ((π₯ β β β¦ (π»β(π + (π₯ β 1))))β(π + (1 β π)))) |
48 | 13, 15, 47 | syl2an 597 |
. . . . 5
β’ (((π β§ π β π) β§ π β (π...π)) β (π»βπ) = ((π₯ β β β¦ (π»β(π + (π₯ β 1))))β(π + (1 β π)))) |
49 | 11, 12, 48 | seqshft2 13991 |
. . . 4
β’ ((π β§ π β π) β (seqπ( + , π»)βπ) = (seq(π + (1 β π))( + , (π₯ β β β¦ (π»β(π + (π₯ β 1)))))β(π + (1 β π)))) |
50 | 21 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π) β π β β) |
51 | | pncan3 11465 |
. . . . . . 7
β’ ((π β β β§ 1 β
β) β (π + (1
β π)) =
1) |
52 | 50, 39, 51 | sylancl 587 |
. . . . . 6
β’ ((π β§ π β π) β (π + (1 β π)) = 1) |
53 | 52 | seqeq1d 13969 |
. . . . 5
β’ ((π β§ π β π) β seq(π + (1 β π))( + , (π₯ β β β¦ (π»β(π + (π₯ β 1))))) = seq1( + , (π₯ β β β¦ (π»β(π + (π₯ β 1)))))) |
54 | 53 | fveq1d 6891 |
. . . 4
β’ ((π β§ π β π) β (seq(π + (1 β π))( + , (π₯ β β β¦ (π»β(π + (π₯ β 1)))))β(π + (1 β π))) = (seq1( + , (π₯ β β β¦ (π»β(π + (π₯ β 1)))))β(π + (1 β π)))) |
55 | 49, 54 | eqtr2d 2774 |
. . 3
β’ ((π β§ π β π) β (seq1( + , (π₯ β β β¦ (π»β(π + (π₯ β 1)))))β(π + (1 β π))) = (seqπ( + , π»)βπ)) |
56 | 1, 2, 5, 7, 9, 55 | climshft2 15523 |
. 2
β’ (π β (seqπ( + , π») β π΄ β seq1( + , (π₯ β β β¦ (π»β(π + (π₯ β 1))))) β π΄)) |
57 | | isercoll2.w |
. . 3
β’ π =
(β€β₯βπ) |
58 | | isercoll2.n |
. . 3
β’ (π β π β β€) |
59 | | isercoll2.g |
. . . . . 6
β’ (π β πΊ:πβΆπ) |
60 | 59 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β β) β πΊ:πβΆπ) |
61 | | uzid 12834 |
. . . . . . . 8
β’ (π β β€ β π β
(β€β₯βπ)) |
62 | 2, 61 | syl 17 |
. . . . . . 7
β’ (π β π β (β€β₯βπ)) |
63 | | nnm1nn0 12510 |
. . . . . . 7
β’ (π₯ β β β (π₯ β 1) β
β0) |
64 | | uzaddcl 12885 |
. . . . . . 7
β’ ((π β
(β€β₯βπ) β§ (π₯ β 1) β β0)
β (π + (π₯ β 1)) β
(β€β₯βπ)) |
65 | 62, 63, 64 | syl2an 597 |
. . . . . 6
β’ ((π β§ π₯ β β) β (π + (π₯ β 1)) β
(β€β₯βπ)) |
66 | 65, 1 | eleqtrrdi 2845 |
. . . . 5
β’ ((π β§ π₯ β β) β (π + (π₯ β 1)) β π) |
67 | 60, 66 | ffvelcdmd 7085 |
. . . 4
β’ ((π β§ π₯ β β) β (πΊβ(π + (π₯ β 1))) β π) |
68 | 67 | fmpttd 7112 |
. . 3
β’ (π β (π₯ β β β¦ (πΊβ(π + (π₯ β 1)))):ββΆπ) |
69 | | fveq2 6889 |
. . . . . . 7
β’ (π = (π + (π β 1)) β (πΊβπ) = (πΊβ(π + (π β 1)))) |
70 | | fvoveq1 7429 |
. . . . . . 7
β’ (π = (π + (π β 1)) β (πΊβ(π + 1)) = (πΊβ((π + (π β 1)) + 1))) |
71 | 69, 70 | breq12d 5161 |
. . . . . 6
β’ (π = (π + (π β 1)) β ((πΊβπ) < (πΊβ(π + 1)) β (πΊβ(π + (π β 1))) < (πΊβ((π + (π β 1)) + 1)))) |
72 | | isercoll2.i |
. . . . . . . 8
β’ ((π β§ π β π) β (πΊβπ) < (πΊβ(π + 1))) |
73 | 72 | ralrimiva 3147 |
. . . . . . 7
β’ (π β βπ β π (πΊβπ) < (πΊβ(π + 1))) |
74 | 73 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β βπ β π (πΊβπ) < (πΊβ(π + 1))) |
75 | | nnm1nn0 12510 |
. . . . . . . 8
β’ (π β β β (π β 1) β
β0) |
76 | | uzaddcl 12885 |
. . . . . . . 8
β’ ((π β
(β€β₯βπ) β§ (π β 1) β β0)
β (π + (π β 1)) β
(β€β₯βπ)) |
77 | 62, 75, 76 | syl2an 597 |
. . . . . . 7
β’ ((π β§ π β β) β (π + (π β 1)) β
(β€β₯βπ)) |
78 | 77, 1 | eleqtrrdi 2845 |
. . . . . 6
β’ ((π β§ π β β) β (π + (π β 1)) β π) |
79 | 71, 74, 78 | rspcdva 3614 |
. . . . 5
β’ ((π β§ π β β) β (πΊβ(π + (π β 1))) < (πΊβ((π + (π β 1)) + 1))) |
80 | | nncn 12217 |
. . . . . . . . . 10
β’ (π β β β π β
β) |
81 | 80 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β β) |
82 | | 1cnd 11206 |
. . . . . . . . 9
β’ ((π β§ π β β) β 1 β
β) |
83 | 81, 82, 82 | addsubd 11589 |
. . . . . . . 8
β’ ((π β§ π β β) β ((π + 1) β 1) = ((π β 1) + 1)) |
84 | 83 | oveq2d 7422 |
. . . . . . 7
β’ ((π β§ π β β) β (π + ((π + 1) β 1)) = (π + ((π β 1) + 1))) |
85 | 21 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β) |
86 | 75 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π β 1) β
β0) |
87 | 86 | nn0cnd 12531 |
. . . . . . . 8
β’ ((π β§ π β β) β (π β 1) β β) |
88 | 85, 87, 82 | addassd 11233 |
. . . . . . 7
β’ ((π β§ π β β) β ((π + (π β 1)) + 1) = (π + ((π β 1) + 1))) |
89 | 84, 88 | eqtr4d 2776 |
. . . . . 6
β’ ((π β§ π β β) β (π + ((π + 1) β 1)) = ((π + (π β 1)) + 1)) |
90 | 89 | fveq2d 6893 |
. . . . 5
β’ ((π β§ π β β) β (πΊβ(π + ((π + 1) β 1))) = (πΊβ((π + (π β 1)) + 1))) |
91 | 79, 90 | breqtrrd 5176 |
. . . 4
β’ ((π β§ π β β) β (πΊβ(π + (π β 1))) < (πΊβ(π + ((π + 1) β 1)))) |
92 | | oveq1 7413 |
. . . . . . . 8
β’ (π₯ = π β (π₯ β 1) = (π β 1)) |
93 | 92 | oveq2d 7422 |
. . . . . . 7
β’ (π₯ = π β (π + (π₯ β 1)) = (π + (π β 1))) |
94 | 93 | fveq2d 6893 |
. . . . . 6
β’ (π₯ = π β (πΊβ(π + (π₯ β 1))) = (πΊβ(π + (π β 1)))) |
95 | | eqid 2733 |
. . . . . 6
β’ (π₯ β β β¦ (πΊβ(π + (π₯ β 1)))) = (π₯ β β β¦ (πΊβ(π + (π₯ β 1)))) |
96 | | fvex 6902 |
. . . . . 6
β’ (πΊβ(π + (π β 1))) β V |
97 | 94, 95, 96 | fvmpt 6996 |
. . . . 5
β’ (π β β β ((π₯ β β β¦ (πΊβ(π + (π₯ β 1))))βπ) = (πΊβ(π + (π β 1)))) |
98 | 97 | adantl 483 |
. . . 4
β’ ((π β§ π β β) β ((π₯ β β β¦ (πΊβ(π + (π₯ β 1))))βπ) = (πΊβ(π + (π β 1)))) |
99 | | peano2nn 12221 |
. . . . . 6
β’ (π β β β (π + 1) β
β) |
100 | 99 | adantl 483 |
. . . . 5
β’ ((π β§ π β β) β (π + 1) β β) |
101 | | oveq1 7413 |
. . . . . . . 8
β’ (π₯ = (π + 1) β (π₯ β 1) = ((π + 1) β 1)) |
102 | 101 | oveq2d 7422 |
. . . . . . 7
β’ (π₯ = (π + 1) β (π + (π₯ β 1)) = (π + ((π + 1) β 1))) |
103 | 102 | fveq2d 6893 |
. . . . . 6
β’ (π₯ = (π + 1) β (πΊβ(π + (π₯ β 1))) = (πΊβ(π + ((π + 1) β 1)))) |
104 | | fvex 6902 |
. . . . . 6
β’ (πΊβ(π + ((π + 1) β 1))) β V |
105 | 103, 95, 104 | fvmpt 6996 |
. . . . 5
β’ ((π + 1) β β β
((π₯ β β β¦
(πΊβ(π + (π₯ β 1))))β(π + 1)) = (πΊβ(π + ((π + 1) β 1)))) |
106 | 100, 105 | syl 17 |
. . . 4
β’ ((π β§ π β β) β ((π₯ β β β¦ (πΊβ(π + (π₯ β 1))))β(π + 1)) = (πΊβ(π + ((π + 1) β 1)))) |
107 | 91, 98, 106 | 3brtr4d 5180 |
. . 3
β’ ((π β§ π β β) β ((π₯ β β β¦ (πΊβ(π + (π₯ β 1))))βπ) < ((π₯ β β β¦ (πΊβ(π + (π₯ β 1))))β(π + 1))) |
108 | 59 | ffnd 6716 |
. . . . . . . 8
β’ (π β πΊ Fn π) |
109 | | uznn0sub 12858 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯βπ) β (π β π) β
β0) |
110 | 11, 109 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (π β π) β
β0) |
111 | | nn0p1nn 12508 |
. . . . . . . . . . . 12
β’ ((π β π) β β0 β ((π β π) + 1) β β) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β ((π β π) + 1) β β) |
113 | 110 | nn0cnd 12531 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β (π β π) β β) |
114 | | pncan 11463 |
. . . . . . . . . . . . . . 15
β’ (((π β π) β β β§ 1 β β)
β (((π β π) + 1) β 1) = (π β π)) |
115 | 113, 39, 114 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β (((π β π) + 1) β 1) = (π β π)) |
116 | 115 | oveq2d 7422 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (π + (((π β π) + 1) β 1)) = (π + (π β π))) |
117 | | eluzelz 12829 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯βπ) β π β β€) |
118 | 117, 1 | eleq2s 2852 |
. . . . . . . . . . . . . . 15
β’ (π β π β π β β€) |
119 | 118 | zcnd 12664 |
. . . . . . . . . . . . . 14
β’ (π β π β π β β) |
120 | | pncan3 11465 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β) β (π + (π β π)) = π) |
121 | 21, 119, 120 | syl2an 597 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (π + (π β π)) = π) |
122 | 116, 121 | eqtr2d 2774 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β π = (π + (((π β π) + 1) β 1))) |
123 | 122 | fveq2d 6893 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΊβπ) = (πΊβ(π + (((π β π) + 1) β 1)))) |
124 | | oveq1 7413 |
. . . . . . . . . . . . . 14
β’ (π₯ = ((π β π) + 1) β (π₯ β 1) = (((π β π) + 1) β 1)) |
125 | 124 | oveq2d 7422 |
. . . . . . . . . . . . 13
β’ (π₯ = ((π β π) + 1) β (π + (π₯ β 1)) = (π + (((π β π) + 1) β 1))) |
126 | 125 | fveq2d 6893 |
. . . . . . . . . . . 12
β’ (π₯ = ((π β π) + 1) β (πΊβ(π + (π₯ β 1))) = (πΊβ(π + (((π β π) + 1) β 1)))) |
127 | 126 | rspceeqv 3633 |
. . . . . . . . . . 11
β’ ((((π β π) + 1) β β β§ (πΊβπ) = (πΊβ(π + (((π β π) + 1) β 1)))) β βπ₯ β β (πΊβπ) = (πΊβ(π + (π₯ β 1)))) |
128 | 112, 123,
127 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π β π) β βπ₯ β β (πΊβπ) = (πΊβ(π + (π₯ β 1)))) |
129 | | fvex 6902 |
. . . . . . . . . . 11
β’ (πΊβπ) β V |
130 | 95 | elrnmpt 5954 |
. . . . . . . . . . 11
β’ ((πΊβπ) β V β ((πΊβπ) β ran (π₯ β β β¦ (πΊβ(π + (π₯ β 1)))) β βπ₯ β β (πΊβπ) = (πΊβ(π + (π₯ β 1))))) |
131 | 129, 130 | ax-mp 5 |
. . . . . . . . . 10
β’ ((πΊβπ) β ran (π₯ β β β¦ (πΊβ(π + (π₯ β 1)))) β βπ₯ β β (πΊβπ) = (πΊβ(π + (π₯ β 1)))) |
132 | 128, 131 | sylibr 233 |
. . . . . . . . 9
β’ ((π β§ π β π) β (πΊβπ) β ran (π₯ β β β¦ (πΊβ(π + (π₯ β 1))))) |
133 | 132 | ralrimiva 3147 |
. . . . . . . 8
β’ (π β βπ β π (πΊβπ) β ran (π₯ β β β¦ (πΊβ(π + (π₯ β 1))))) |
134 | | ffnfv 7115 |
. . . . . . . 8
β’ (πΊ:πβΆran (π₯ β β β¦ (πΊβ(π + (π₯ β 1)))) β (πΊ Fn π β§ βπ β π (πΊβπ) β ran (π₯ β β β¦ (πΊβ(π + (π₯ β 1)))))) |
135 | 108, 133,
134 | sylanbrc 584 |
. . . . . . 7
β’ (π β πΊ:πβΆran (π₯ β β β¦ (πΊβ(π + (π₯ β 1))))) |
136 | 135 | frnd 6723 |
. . . . . 6
β’ (π β ran πΊ β ran (π₯ β β β¦ (πΊβ(π + (π₯ β 1))))) |
137 | 136 | sscond 4141 |
. . . . 5
β’ (π β (π β ran (π₯ β β β¦ (πΊβ(π + (π₯ β 1))))) β (π β ran πΊ)) |
138 | 137 | sselda 3982 |
. . . 4
β’ ((π β§ π β (π β ran (π₯ β β β¦ (πΊβ(π + (π₯ β 1)))))) β π β (π β ran πΊ)) |
139 | | isercoll2.0 |
. . . 4
β’ ((π β§ π β (π β ran πΊ)) β (πΉβπ) = 0) |
140 | 138, 139 | syldan 592 |
. . 3
β’ ((π β§ π β (π β ran (π₯ β β β¦ (πΊβ(π + (π₯ β 1)))))) β (πΉβπ) = 0) |
141 | | isercoll2.f |
. . 3
β’ ((π β§ π β π) β (πΉβπ) β β) |
142 | | fveq2 6889 |
. . . . . 6
β’ (π = (π + (π β 1)) β (π»βπ) = (π»β(π + (π β 1)))) |
143 | 69 | fveq2d 6893 |
. . . . . 6
β’ (π = (π + (π β 1)) β (πΉβ(πΊβπ)) = (πΉβ(πΊβ(π + (π β 1))))) |
144 | 142, 143 | eqeq12d 2749 |
. . . . 5
β’ (π = (π + (π β 1)) β ((π»βπ) = (πΉβ(πΊβπ)) β (π»β(π + (π β 1))) = (πΉβ(πΊβ(π + (π β 1)))))) |
145 | | isercoll2.h |
. . . . . . 7
β’ ((π β§ π β π) β (π»βπ) = (πΉβ(πΊβπ))) |
146 | 145 | ralrimiva 3147 |
. . . . . 6
β’ (π β βπ β π (π»βπ) = (πΉβ(πΊβπ))) |
147 | 146 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β βπ β π (π»βπ) = (πΉβ(πΊβπ))) |
148 | 144, 147,
78 | rspcdva 3614 |
. . . 4
β’ ((π β§ π β β) β (π»β(π + (π β 1))) = (πΉβ(πΊβ(π + (π β 1))))) |
149 | 93 | fveq2d 6893 |
. . . . . 6
β’ (π₯ = π β (π»β(π + (π₯ β 1))) = (π»β(π + (π β 1)))) |
150 | | fvex 6902 |
. . . . . 6
β’ (π»β(π + (π β 1))) β V |
151 | 149, 33, 150 | fvmpt 6996 |
. . . . 5
β’ (π β β β ((π₯ β β β¦ (π»β(π + (π₯ β 1))))βπ) = (π»β(π + (π β 1)))) |
152 | 151 | adantl 483 |
. . . 4
β’ ((π β§ π β β) β ((π₯ β β β¦ (π»β(π + (π₯ β 1))))βπ) = (π»β(π + (π β 1)))) |
153 | 98 | fveq2d 6893 |
. . . 4
β’ ((π β§ π β β) β (πΉβ((π₯ β β β¦ (πΊβ(π + (π₯ β 1))))βπ)) = (πΉβ(πΊβ(π + (π β 1))))) |
154 | 148, 152,
153 | 3eqtr4d 2783 |
. . 3
β’ ((π β§ π β β) β ((π₯ β β β¦ (π»β(π + (π₯ β 1))))βπ) = (πΉβ((π₯ β β β¦ (πΊβ(π + (π₯ β 1))))βπ))) |
155 | 57, 58, 68, 107, 140, 141, 154 | isercoll 15611 |
. 2
β’ (π β (seq1( + , (π₯ β β β¦ (π»β(π + (π₯ β 1))))) β π΄ β seqπ( + , πΉ) β π΄)) |
156 | 56, 155 | bitrd 279 |
1
β’ (π β (seqπ( + , π») β π΄ β seqπ( + , πΉ) β π΄)) |