Metamath Proof Explorer


Theorem fseq1m1p1

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

Ref Expression
Hypothesis fseq1m1p1.1 H = N B
Assertion fseq1m1p1 N F : 1 N 1 A B A G = F H G : 1 N A G N = B F = G 1 N 1

Proof

Step Hyp Ref Expression
1 fseq1m1p1.1 H = N B
2 nnm1nn0 N N 1 0
3 eqid N - 1 + 1 B = N - 1 + 1 B
4 3 fseq1p1m1 N 1 0 F : 1 N 1 A B A G = F N - 1 + 1 B G : 1 N - 1 + 1 A G N - 1 + 1 = B F = G 1 N 1
5 2 4 syl N F : 1 N 1 A B A G = F N - 1 + 1 B G : 1 N - 1 + 1 A G N - 1 + 1 = B F = G 1 N 1
6 nncn N N
7 ax-1cn 1
8 npcan N 1 N - 1 + 1 = N
9 6 7 8 sylancl N N - 1 + 1 = N
10 9 opeq1d N N - 1 + 1 B = N B
11 10 sneqd N N - 1 + 1 B = N B
12 11 1 eqtr4di N N - 1 + 1 B = H
13 12 uneq2d N F N - 1 + 1 B = F H
14 13 eqeq2d N G = F N - 1 + 1 B G = F H
15 14 3anbi3d N F : 1 N 1 A B A G = F N - 1 + 1 B F : 1 N 1 A B A G = F H
16 9 oveq2d N 1 N - 1 + 1 = 1 N
17 16 feq2d N G : 1 N - 1 + 1 A G : 1 N A
18 9 fveqeq2d N G N - 1 + 1 = B G N = B
19 17 18 3anbi12d N G : 1 N - 1 + 1 A G N - 1 + 1 = B F = G 1 N 1 G : 1 N A G N = B F = G 1 N 1
20 5 15 19 3bitr3d N F : 1 N 1 A B A G = F H G : 1 N A G N = B F = G 1 N 1