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+1B
Assertion fseq1p1m1 N0F:1NABAG=FHG:1N+1AGN+1=BF=G1N

Proof

Step Hyp Ref Expression
1 fseq1p1m1.1 H=N+1B
2 simpr1 N0F:1NABAG=FHF:1NA
3 nn0p1nn N0N+1
4 3 adantr N0F:1NABAG=FHN+1
5 simpr2 N0F:1NABAG=FHBA
6 fsng N+1BAH:N+1BH=N+1B
7 1 6 mpbiri N+1BAH:N+1B
8 4 5 7 syl2anc N0F:1NABAG=FHH:N+1B
9 5 snssd N0F:1NABAG=FHBA
10 8 9 fssd N0F:1NABAG=FHH:N+1A
11 fzp1disj 1NN+1=
12 11 a1i N0F:1NABAG=FH1NN+1=
13 2 10 12 fun2d N0F:1NABAG=FHFH:1NN+1A
14 1z 1
15 simpl N0F:1NABAG=FHN0
16 nn0uz 0=0
17 1m1e0 11=0
18 17 fveq2i 11=0
19 16 18 eqtr4i 0=11
20 15 19 eleqtrdi N0F:1NABAG=FHN11
21 fzsuc2 1N111N+1=1NN+1
22 14 20 21 sylancr N0F:1NABAG=FH1N+1=1NN+1
23 22 eqcomd N0F:1NABAG=FH1NN+1=1N+1
24 23 feq2d N0F:1NABAG=FHFH:1NN+1AFH:1N+1A
25 13 24 mpbid N0F:1NABAG=FHFH:1N+1A
26 simpr3 N0F:1NABAG=FHG=FH
27 26 feq1d N0F:1NABAG=FHG:1N+1AFH:1N+1A
28 25 27 mpbird N0F:1NABAG=FHG:1N+1A
29 ovex N+1V
30 29 snid N+1N+1
31 fvres N+1N+1GN+1N+1=GN+1
32 30 31 ax-mp GN+1N+1=GN+1
33 26 reseq1d N0F:1NABAG=FHGN+1=FHN+1
34 ffn F:1NAFFn1N
35 fnresdisj FFn1N1NN+1=FN+1=
36 2 34 35 3syl N0F:1NABAG=FH1NN+1=FN+1=
37 12 36 mpbid N0F:1NABAG=FHFN+1=
38 37 uneq1d N0F:1NABAG=FHFN+1HN+1=HN+1
39 resundir FHN+1=FN+1HN+1
40 uncom HN+1=HN+1
41 un0 HN+1=HN+1
42 40 41 eqtr2i HN+1=HN+1
43 38 39 42 3eqtr4g N0F:1NABAG=FHFHN+1=HN+1
44 ffn H:N+1AHFnN+1
45 fnresdm HFnN+1HN+1=H
46 10 44 45 3syl N0F:1NABAG=FHHN+1=H
47 33 43 46 3eqtrd N0F:1NABAG=FHGN+1=H
48 47 fveq1d N0F:1NABAG=FHGN+1N+1=HN+1
49 1 fveq1i HN+1=N+1BN+1
50 fvsng N+1BAN+1BN+1=B
51 49 50 eqtrid N+1BAHN+1=B
52 4 5 51 syl2anc N0F:1NABAG=FHHN+1=B
53 48 52 eqtrd N0F:1NABAG=FHGN+1N+1=B
54 32 53 eqtr3id N0F:1NABAG=FHGN+1=B
55 26 reseq1d N0F:1NABAG=FHG1N=FH1N
56 incom N+11N=1NN+1
57 56 12 eqtrid N0F:1NABAG=FHN+11N=
58 ffn H:N+1BHFnN+1
59 fnresdisj HFnN+1N+11N=H1N=
60 8 58 59 3syl N0F:1NABAG=FHN+11N=H1N=
61 57 60 mpbid N0F:1NABAG=FHH1N=
62 61 uneq2d N0F:1NABAG=FHF1NH1N=F1N
63 resundir FH1N=F1NH1N
64 un0 F1N=F1N
65 64 eqcomi F1N=F1N
66 62 63 65 3eqtr4g N0F:1NABAG=FHFH1N=F1N
67 fnresdm FFn1NF1N=F
68 2 34 67 3syl N0F:1NABAG=FHF1N=F
69 55 66 68 3eqtrrd N0F:1NABAG=FHF=G1N
70 28 54 69 3jca N0F:1NABAG=FHG:1N+1AGN+1=BF=G1N
71 simpr1 N0G:1N+1AGN+1=BF=G1NG:1N+1A
72 fzssp1 1N1N+1
73 fssres G:1N+1A1N1N+1G1N:1NA
74 71 72 73 sylancl N0G:1N+1AGN+1=BF=G1NG1N:1NA
75 simpr3 N0G:1N+1AGN+1=BF=G1NF=G1N
76 75 feq1d N0G:1N+1AGN+1=BF=G1NF:1NAG1N:1NA
77 74 76 mpbird N0G:1N+1AGN+1=BF=G1NF:1NA
78 simpr2 N0G:1N+1AGN+1=BF=G1NGN+1=B
79 3 adantr N0G:1N+1AGN+1=BF=G1NN+1
80 nnuz =1
81 79 80 eleqtrdi N0G:1N+1AGN+1=BF=G1NN+11
82 eluzfz2 N+11N+11N+1
83 81 82 syl N0G:1N+1AGN+1=BF=G1NN+11N+1
84 71 83 ffvelrnd N0G:1N+1AGN+1=BF=G1NGN+1A
85 78 84 eqeltrrd N0G:1N+1AGN+1=BF=G1NBA
86 ffn G:1N+1AGFn1N+1
87 71 86 syl N0G:1N+1AGN+1=BF=G1NGFn1N+1
88 fnressn GFn1N+1N+11N+1GN+1=N+1GN+1
89 87 83 88 syl2anc N0G:1N+1AGN+1=BF=G1NGN+1=N+1GN+1
90 opeq2 GN+1=BN+1GN+1=N+1B
91 90 sneqd GN+1=BN+1GN+1=N+1B
92 78 91 syl N0G:1N+1AGN+1=BF=G1NN+1GN+1=N+1B
93 89 92 eqtrd N0G:1N+1AGN+1=BF=G1NGN+1=N+1B
94 1 93 eqtr4id N0G:1N+1AGN+1=BF=G1NH=GN+1
95 75 94 uneq12d N0G:1N+1AGN+1=BF=G1NFH=G1NGN+1
96 simpl N0G:1N+1AGN+1=BF=G1NN0
97 96 19 eleqtrdi N0G:1N+1AGN+1=BF=G1NN11
98 14 97 21 sylancr N0G:1N+1AGN+1=BF=G1N1N+1=1NN+1
99 98 reseq2d N0G:1N+1AGN+1=BF=G1NG1N+1=G1NN+1
100 resundi G1NN+1=G1NGN+1
101 99 100 eqtr2di N0G:1N+1AGN+1=BF=G1NG1NGN+1=G1N+1
102 fnresdm GFn1N+1G1N+1=G
103 71 86 102 3syl N0G:1N+1AGN+1=BF=G1NG1N+1=G
104 95 101 103 3eqtrrd N0G:1N+1AGN+1=BF=G1NG=FH
105 77 85 104 3jca N0G:1N+1AGN+1=BF=G1NF:1NABAG=FH
106 70 105 impbida N0F:1NABAG=FHG:1N+1AGN+1=BF=G1N