Metamath Proof Explorer


Theorem fseq1p1m1

Description: Add/remove an item to/from the end of a finite sequence. (Contributed by Paul Chapman, 17-Nov-2012) (Revised by Mario Carneiro, 7-Mar-2014)

Ref Expression
Hypothesis fseq1p1m1.1 H = N + 1 B
Assertion fseq1p1m1 N 0 F : 1 N A B A G = F H G : 1 N + 1 A G N + 1 = B F = G 1 N

Proof

Step Hyp Ref Expression
1 fseq1p1m1.1 H = N + 1 B
2 simpr1 N 0 F : 1 N A B A G = F H F : 1 N A
3 nn0p1nn N 0 N + 1
4 3 adantr N 0 F : 1 N A B A G = F H N + 1
5 simpr2 N 0 F : 1 N A B A G = F H B A
6 fsng N + 1 B A H : N + 1 B H = N + 1 B
7 1 6 mpbiri N + 1 B A H : N + 1 B
8 4 5 7 syl2anc N 0 F : 1 N A B A G = F H H : N + 1 B
9 5 snssd N 0 F : 1 N A B A G = F H B A
10 8 9 fssd N 0 F : 1 N A B A G = F H H : N + 1 A
11 fzp1disj 1 N N + 1 =
12 11 a1i N 0 F : 1 N A B A G = F H 1 N N + 1 =
13 2 10 12 fun2d N 0 F : 1 N A B A G = F H F H : 1 N N + 1 A
14 1z 1
15 simpl N 0 F : 1 N A B A G = F H N 0
16 nn0uz 0 = 0
17 1m1e0 1 1 = 0
18 17 fveq2i 1 1 = 0
19 16 18 eqtr4i 0 = 1 1
20 15 19 eleqtrdi N 0 F : 1 N A B A G = F H N 1 1
21 fzsuc2 1 N 1 1 1 N + 1 = 1 N N + 1
22 14 20 21 sylancr N 0 F : 1 N A B A G = F H 1 N + 1 = 1 N N + 1
23 22 eqcomd N 0 F : 1 N A B A G = F H 1 N N + 1 = 1 N + 1
24 23 feq2d N 0 F : 1 N A B A G = F H F H : 1 N N + 1 A F H : 1 N + 1 A
25 13 24 mpbid N 0 F : 1 N A B A G = F H F H : 1 N + 1 A
26 simpr3 N 0 F : 1 N A B A G = F H G = F H
27 26 feq1d N 0 F : 1 N A B A G = F H G : 1 N + 1 A F H : 1 N + 1 A
28 25 27 mpbird N 0 F : 1 N A B A G = F H G : 1 N + 1 A
29 ovex N + 1 V
30 29 snid N + 1 N + 1
31 fvres N + 1 N + 1 G N + 1 N + 1 = G N + 1
32 30 31 ax-mp G N + 1 N + 1 = G N + 1
33 26 reseq1d N 0 F : 1 N A B A G = F H G N + 1 = F H N + 1
34 ffn F : 1 N A F Fn 1 N
35 fnresdisj F Fn 1 N 1 N N + 1 = F N + 1 =
36 2 34 35 3syl N 0 F : 1 N A B A G = F H 1 N N + 1 = F N + 1 =
37 12 36 mpbid N 0 F : 1 N A B A G = F H F N + 1 =
38 37 uneq1d N 0 F : 1 N A B A G = F H F N + 1 H N + 1 = H N + 1
39 resundir F H N + 1 = F N + 1 H N + 1
40 uncom H N + 1 = H N + 1
41 un0 H N + 1 = H N + 1
42 40 41 eqtr2i H N + 1 = H N + 1
43 38 39 42 3eqtr4g N 0 F : 1 N A B A G = F H F H N + 1 = H N + 1
44 ffn H : N + 1 A H Fn N + 1
45 fnresdm H Fn N + 1 H N + 1 = H
46 10 44 45 3syl N 0 F : 1 N A B A G = F H H N + 1 = H
47 33 43 46 3eqtrd N 0 F : 1 N A B A G = F H G N + 1 = H
48 47 fveq1d N 0 F : 1 N A B A G = F H G N + 1 N + 1 = H N + 1
49 1 fveq1i H N + 1 = N + 1 B N + 1
50 fvsng N + 1 B A N + 1 B N + 1 = B
51 49 50 syl5eq N + 1 B A H N + 1 = B
52 4 5 51 syl2anc N 0 F : 1 N A B A G = F H H N + 1 = B
53 48 52 eqtrd N 0 F : 1 N A B A G = F H G N + 1 N + 1 = B
54 32 53 eqtr3id N 0 F : 1 N A B A G = F H G N + 1 = B
55 26 reseq1d N 0 F : 1 N A B A G = F H G 1 N = F H 1 N
56 incom N + 1 1 N = 1 N N + 1
57 56 12 syl5eq N 0 F : 1 N A B A G = F H N + 1 1 N =
58 ffn H : N + 1 B H Fn N + 1
59 fnresdisj H Fn N + 1 N + 1 1 N = H 1 N =
60 8 58 59 3syl N 0 F : 1 N A B A G = F H N + 1 1 N = H 1 N =
61 57 60 mpbid N 0 F : 1 N A B A G = F H H 1 N =
62 61 uneq2d N 0 F : 1 N A B A G = F H F 1 N H 1 N = F 1 N
63 resundir F H 1 N = F 1 N H 1 N
64 un0 F 1 N = F 1 N
65 64 eqcomi F 1 N = F 1 N
66 62 63 65 3eqtr4g N 0 F : 1 N A B A G = F H F H 1 N = F 1 N
67 fnresdm F Fn 1 N F 1 N = F
68 2 34 67 3syl N 0 F : 1 N A B A G = F H F 1 N = F
69 55 66 68 3eqtrrd N 0 F : 1 N A B A G = F H F = G 1 N
70 28 54 69 3jca N 0 F : 1 N A B A G = F H G : 1 N + 1 A G N + 1 = B F = G 1 N
71 simpr1 N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N G : 1 N + 1 A
72 fzssp1 1 N 1 N + 1
73 fssres G : 1 N + 1 A 1 N 1 N + 1 G 1 N : 1 N A
74 71 72 73 sylancl N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N G 1 N : 1 N A
75 simpr3 N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N F = G 1 N
76 75 feq1d N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N F : 1 N A G 1 N : 1 N A
77 74 76 mpbird N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N F : 1 N A
78 simpr2 N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N G N + 1 = B
79 3 adantr N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N N + 1
80 nnuz = 1
81 79 80 eleqtrdi N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N N + 1 1
82 eluzfz2 N + 1 1 N + 1 1 N + 1
83 81 82 syl N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N N + 1 1 N + 1
84 71 83 ffvelrnd N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N G N + 1 A
85 78 84 eqeltrrd N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N B A
86 ffn G : 1 N + 1 A G Fn 1 N + 1
87 71 86 syl N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N G Fn 1 N + 1
88 fnressn G Fn 1 N + 1 N + 1 1 N + 1 G N + 1 = N + 1 G N + 1
89 87 83 88 syl2anc N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N G N + 1 = N + 1 G N + 1
90 opeq2 G N + 1 = B N + 1 G N + 1 = N + 1 B
91 90 sneqd G N + 1 = B N + 1 G N + 1 = N + 1 B
92 78 91 syl N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N N + 1 G N + 1 = N + 1 B
93 89 92 eqtrd N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N G N + 1 = N + 1 B
94 1 93 eqtr4id N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N H = G N + 1
95 75 94 uneq12d N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N F H = G 1 N G N + 1
96 simpl N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N N 0
97 96 19 eleqtrdi N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N N 1 1
98 14 97 21 sylancr N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N 1 N + 1 = 1 N N + 1
99 98 reseq2d N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N G 1 N + 1 = G 1 N N + 1
100 resundi G 1 N N + 1 = G 1 N G N + 1
101 99 100 eqtr2di N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N G 1 N G N + 1 = G 1 N + 1
102 fnresdm G Fn 1 N + 1 G 1 N + 1 = G
103 71 86 102 3syl N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N G 1 N + 1 = G
104 95 101 103 3eqtrrd N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N G = F H
105 77 85 104 3jca N 0 G : 1 N + 1 A G N + 1 = B F = G 1 N F : 1 N A B A G = F H
106 70 105 impbida N 0 F : 1 N A B A G = F H G : 1 N + 1 A G N + 1 = B F = G 1 N