Theorem ser1absdiflem 7132

Description: Lemma for ser1absdifi 7133. Warning: The HTML proof page is 1/2 megabyte in size.

Hypotheses

Ref	Expression
ser1absdif.1	|- F:NN-->CC
ser1absdif.2	|- G Fn NN
ser1absdif.3	|- (x e. NN -> (G` x) = (abs` (F` x)))

Assertion

Ref	Expression
ser1absdiflem	|- ((A e. NN /\ B e. NN) -> (abs` ((( + seq1 F)` (A + B)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + B)) - (( + seq1 G)` A)))

Distinct variable groups:   x,A   x,F   x,G

Proof of Theorem ser1absdiflem

Step	Hyp	Ref	Expression
1		opreq2 4027	. . . . . . . 8 |- (y = 1 -> (A + y) = (A + 1))
2	1	fveq2d 3839	. . . . . . 7 |- (y = 1 -> (( + seq1 F)` (A + y)) = (( + seq1 F)` (A + 1)))
3	2	opreq1d 4033	. . . . . 6 |- (y = 1 -> ((( + seq1 F)` (A + y)) - (( + seq1 F)` A)) = ((( + seq1 F)` (A + 1)) - (( + seq1 F)` A)))
4	3	fveq2d 3839	. . . . 5 |- (y = 1 -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) = (abs` ((( + seq1 F)` (A + 1)) - (( + seq1 F)` A))))
5	1	fveq2d 3839	. . . . . 6 |- (y = 1 -> (( + seq1 G)` (A + y)) = (( + seq1 G)` (A + 1)))
6	5	opreq1d 4033	. . . . 5 |- (y = 1 -> ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) = ((( + seq1 G)` (A + 1)) - (( + seq1 G)` A)))
7	4, 6	breq12d 2704	. . . 4 |- (y = 1 -> ((abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) <-> (abs` ((( + seq1 F)` (A + 1)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + 1)) - (( + seq1 G)` A))))
8	7	imbi2d 615	. . 3 |- (y = 1 -> ((A e. NN -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + y)) - (( + seq1 G)` A))) <-> (A e. NN -> (abs` ((( + seq1 F)` (A + 1)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + 1)) - (( + seq1 G)` A)))))
9		opreq2 4027	. . . . . . . 8 |- (y = z -> (A + y) = (A + z))
10	9	fveq2d 3839	. . . . . . 7 |- (y = z -> (( + seq1 F)` (A + y)) = (( + seq1 F)` (A + z)))
11	10	opreq1d 4033	. . . . . 6 |- (y = z -> ((( + seq1 F)` (A + y)) - (( + seq1 F)` A)) = ((( + seq1 F)` (A + z)) - (( + seq1 F)` A)))
12	11	fveq2d 3839	. . . . 5 |- (y = z -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) = (abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))))
13	9	fveq2d 3839	. . . . . 6 |- (y = z -> (( + seq1 G)` (A + y)) = (( + seq1 G)` (A + z)))
14	13	opreq1d 4033	. . . . 5 |- (y = z -> ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) = ((( + seq1 G)` (A + z)) - (( + seq1 G)` A)))
15	12, 14	breq12d 2704	. . . 4 |- (y = z -> ((abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) <-> (abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + z)) - (( + seq1 G)` A))))
16	15	imbi2d 615	. . 3 |- (y = z -> ((A e. NN -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + y)) - (( + seq1 G)` A))) <-> (A e. NN -> (abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + z)) - (( + seq1 G)` A)))))
17		opreq2 4027	. . . . . . . 8 |- (y = (z + 1) -> (A + y) = (A + (z + 1)))
18	17	fveq2d 3839	. . . . . . 7 |- (y = (z + 1) -> (( + seq1 F)` (A + y)) = (( + seq1 F)` (A + (z + 1))))
19	18	opreq1d 4033	. . . . . 6 |- (y = (z + 1) -> ((( + seq1 F)` (A + y)) - (( + seq1 F)` A)) = ((( + seq1 F)` (A + (z + 1))) - (( + seq1 F)` A)))
20	19	fveq2d 3839	. . . . 5 |- (y = (z + 1) -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) = (abs` ((( + seq1 F)` (A + (z + 1))) - (( + seq1 F)` A))))
21	17	fveq2d 3839	. . . . . 6 |- (y = (z + 1) -> (( + seq1 G)` (A + y)) = (( + seq1 G)` (A + (z + 1))))
22	21	opreq1d 4033	. . . . 5 |- (y = (z + 1) -> ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) = ((( + seq1 G)` (A + (z + 1))) - (( + seq1 G)` A)))
23	20, 22	breq12d 2704	. . . 4 |- (y = (z + 1) -> ((abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) <-> (abs` ((( + seq1 F)` (A + (z + 1))) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + (z + 1))) - (( + seq1 G)` A))))
24	23	imbi2d 615	. . 3 |- (y = (z + 1) -> ((A e. NN -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + y)) - (( + seq1 G)` A))) <-> (A e. NN -> (abs` ((( + seq1 F)` (A + (z + 1))) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + (z + 1))) - (( + seq1 G)` A)))))
25		opreq2 4027	. . . . . . . 8 |- (y = B -> (A + y) = (A + B))
26	25	fveq2d 3839	. . . . . . 7 |- (y = B -> (( + seq1 F)` (A + y)) = (( + seq1 F)` (A + B)))
27	26	opreq1d 4033	. . . . . 6 |- (y = B -> ((( + seq1 F)` (A + y)) - (( + seq1 F)` A)) = ((( + seq1 F)` (A + B)) - (( + seq1 F)` A)))
28	27	fveq2d 3839	. . . . 5 |- (y = B -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) = (abs` ((( + seq1 F)` (A + B)) - (( + seq1 F)` A))))
29	25	fveq2d 3839	. . . . . 6 |- (y = B -> (( + seq1 G)` (A + y)) = (( + seq1 G)` (A + B)))
30	29	opreq1d 4033	. . . . 5 |- (y = B -> ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) = ((( + seq1 G)` (A + B)) - (( + seq1 G)` A)))
31	28, 30	breq12d 2704	. . . 4 |- (y = B -> ((abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) <-> (abs` ((( + seq1 F)` (A + B)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + B)) - (( + seq1 G)` A))))
32	31	imbi2d 615	. . 3 |- (y = B -> ((A e. NN -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + y)) - (( + seq1 G)` A))) <-> (A e. NN -> (abs` ((( + seq1 F)` (A + B)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + B)) - (( + seq1 G)` A)))))
33		peano2nn 6080	. . . . . . 7 |- (A e. NN -> (A + 1) e. NN)
34		ser1absdif.1	. . . . . . . 8 |- F:NN-->CC
35	34	ffvelrni 3929	. . . . . . 7 |- ((A + 1) e. NN -> (F` (A + 1)) e. CC)
36	33, 35	syl 10	. . . . . 6 |- (A e. NN -> (F` (A + 1)) e. CC)
37		abscl 7035	. . . . . 6 |- ((F` (A + 1)) e. CC -> (abs` (F` (A + 1))) e. RR)
38	36, 37	syl 10	. . . . 5 |- (A e. NN -> (abs` (F` (A + 1))) e. RR)
39		leid 5685	. . . . 5 |- ((abs` (F` (A + 1))) e. RR -> (abs` (F` (A + 1))) <_ (abs` (F` (A + 1))))
40	38, 39	syl 10	. . . 4 |- (A e. NN -> (abs` (F` (A + 1))) <_ (abs` (F` (A + 1))))
41		addex 5471	. . . . . . . 8 |- + e. V
42		nnex 6078	. . . . . . . . 9 |- NN e. V
43		fex 3759	. . . . . . . . 9 |- ((F:NN-->CC /\ NN e. V) -> F e. V)
44	34, 42, 43	mp2an 701	. . . . . . . 8 |- F e. V
45	41, 44	seq1p1 6683	. . . . . . 7 |- (A e. NN -> (( + seq1 F)` (A + 1)) = ((( + seq1 F)` A) + (F` (A + 1))))
46	45	opreq1d 4033	. . . . . 6 |- (A e. NN -> ((( + seq1 F)` (A + 1)) - (( + seq1 F)` A)) = (((( + seq1 F)` A) + (F` (A + 1))) - (( + seq1 F)` A)))
47		pncan2 5552	. . . . . . 7 |- (((( + seq1 F)` A) e. CC /\ (F` (A + 1)) e. CC) -> (((( + seq1 F)` A) + (F` (A + 1))) - (( + seq1 F)` A)) = (F` (A + 1)))
48	34	ser1cl1i 6695	. . . . . . 7 |- (A e. NN -> (( + seq1 F)` A) e. CC)
49	47, 48, 36	sylanc 473	. . . . . 6 |- (A e. NN -> (((( + seq1 F)` A) + (F` (A + 1))) - (( + seq1 F)` A)) = (F` (A + 1)))
50	46, 49	eqtrd 1550	. . . . 5 |- (A e. NN -> ((( + seq1 F)` (A + 1)) - (( + seq1 F)` A)) = (F` (A + 1)))
51	50	fveq2d 3839	. . . 4 |- (A e. NN -> (abs` ((( + seq1 F)` (A + 1)) - (( + seq1 F)` A))) = (abs` (F` (A + 1))))
52		ser1absdif.2	. . . . . . . 8 |- G Fn NN
53		fnex 3713	. . . . . . . 8 |- ((G Fn NN /\ NN e. V) -> G e. V)
54	52, 42, 53	mp2an 701	. . . . . . 7 |- G e. V
55	41, 54	seq1p1 6683	. . . . . 6 |- (A e. NN -> (( + seq1 G)` (A + 1)) = ((( + seq1 G)` A) + (G` (A + 1))))
56	55	opreq1d 4033	. . . . 5 |- (A e. NN -> ((( + seq1 G)` (A + 1)) - (( + seq1 G)` A)) = (((( + seq1 G)` A) + (G` (A + 1))) - (( + seq1 G)` A)))
57		pncan2 5552	. . . . . 6 |- (((( + seq1 G)` A) e. CC /\ (G` (A + 1)) e. CC) -> (((( + seq1 G)` A) + (G` (A + 1))) - (( + seq1 G)` A)) = (G` (A + 1)))
58		ffnfv 3942	. . . . . . . . 9 |- (G:NN-->RR <-> (G Fn NN /\ A.x e. NN (G` x) e. RR))
59		ser1absdif.3	. . . . . . . . . . 11 |- (x e. NN -> (G` x) = (abs` (F` x)))
60	34	ffvelrni 3929	. . . . . . . . . . . 12 |- (x e. NN -> (F` x) e. CC)
61		abscl 7035	. . . . . . . . . . . 12 |- ((F` x) e. CC -> (abs` (F` x)) e. RR)
62	60, 61	syl 10	. . . . . . . . . . 11 |- (x e. NN -> (abs` (F` x)) e. RR)
63	59, 62	eqeltrd 1591	. . . . . . . . . 10 |- (x e. NN -> (G` x) e. RR)
64	63	rgen 1744	. . . . . . . . 9 |- A.x e. NN (G` x) e. RR
65	58, 52, 64	mpbir2an 735	. . . . . . . 8 |- G:NN-->RR
66		axresscn 5422	. . . . . . . 8 |- RR (_ CC
67		fss 3742	. . . . . . . 8 |- ((G:NN-->RR /\ RR (_ CC) -> G:NN-->CC)
68	65, 66, 67	mp2an 701	. . . . . . 7 |- G:NN-->CC
69	68	ser1cl1i 6695	. . . . . 6 |- (A e. NN -> (( + seq1 G)` A) e. CC)
70		fveq2 3835	. . . . . . . . . . 11 |- (x = (A + 1) -> (G` x) = (G` (A + 1)))
71		fveq2 3835	. . . . . . . . . . . 12 |- (x = (A + 1) -> (F` x) = (F` (A + 1)))
72	71	fveq2d 3839	. . . . . . . . . . 11 |- (x = (A + 1) -> (abs` (F` x)) = (abs` (F` (A + 1))))
73	70, 72	eqeq12d 1532	. . . . . . . . . 10 |- (x = (A + 1) -> ((G` x) = (abs` (F` x)) <-> (G` (A + 1)) = (abs` (F` (A + 1)))))
74	73, 59	vtoclga 1898	. . . . . . . . 9 |- ((A + 1) e. NN -> (G` (A + 1)) = (abs` (F` (A + 1))))
75	35, 37	syl 10	. . . . . . . . 9 |- ((A + 1) e. NN -> (abs` (F` (A + 1))) e. RR)
76	74, 75	eqeltrd 1591	. . . . . . . 8 |- ((A + 1) e. NN -> (G` (A + 1)) e. RR)
77	76	recnd 5469	. . . . . . 7 |- ((A + 1) e. NN -> (G` (A + 1)) e. CC)
78	33, 77	syl 10	. . . . . 6 |- (A e. NN -> (G` (A + 1)) e. CC)
79	57, 69, 78	sylanc 473	. . . . 5 |- (A e. NN -> (((( + seq1 G)` A) + (G` (A + 1))) - (( + seq1 G)` A)) = (G` (A + 1)))
80	33, 74	syl 10	. . . . 5 |- (A e. NN -> (G` (A + 1)) = (abs` (F` (A + 1))))
81	56, 79, 80	3eqtrd 1554	. . . 4 |- (A e. NN -> ((( + seq1 G)` (A + 1)) - (( + seq1 G)` A)) = (abs` (F` (A + 1))))
82	40, 51, 81	3brtr4d 2718	. . 3 |- (A e. NN -> (abs` ((( + seq1 F)` (A + 1)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + 1)) - (( + seq1 G)` A)))
83		abstri 7101	. . . . . . . 8 |- ((((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) e. CC /\ (F` ((A + z) + 1)) e. CC) -> (abs` (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1)))) <_ ((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) + (abs` (F` ((A + z) + 1)))))
84		subcl 5521	. . . . . . . . 9 |- (((( + seq1 F)` (A + z)) e. CC /\ (( + seq1 F)` A) e. CC) -> ((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) e. CC)
85		nnaddcl 6085	. . . . . . . . . 10 |- ((A e. NN /\ z e. NN) -> (A + z) e. NN)
86	34	ser1cl1i 6695	. . . . . . . . . 10 |- ((A + z) e. NN -> (( + seq1 F)` (A + z)) e. CC)
87	85, 86	syl 10	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (( + seq1 F)` (A + z)) e. CC)
88	48	adantr 389	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (( + seq1 F)` A) e. CC)
89	84, 87, 88	sylanc 473	. . . . . . . 8 |- ((A e. NN /\ z e. NN) -> ((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) e. CC)
90		peano2nn 6080	. . . . . . . . . 10 |- ((A + z) e. NN -> ((A + z) + 1) e. NN)
91	85, 90	syl 10	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> ((A + z) + 1) e. NN)
92	34	ffvelrni 3929	. . . . . . . . 9 |- (((A + z) + 1) e. NN -> (F` ((A + z) + 1)) e. CC)
93	91, 92	syl 10	. . . . . . . 8 |- ((A e. NN /\ z e. NN) -> (F` ((A + z) + 1)) e. CC)
94	83, 89, 93	sylanc 473	. . . . . . 7 |- ((A e. NN /\ z e. NN) -> (abs` (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1)))) <_ ((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) + (abs` (F` ((A + z) + 1)))))
95		letr 5679	. . . . . . . 8 |- (((abs` (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1)))) e. RR /\ ((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) + (abs` (F` ((A + z) + 1)))) e. RR /\ (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (abs` (F` ((A + z) + 1)))) e. RR) -> (((abs` (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1)))) <_ ((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) + (abs` (F` ((A + z) + 1)))) /\ ((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) + (abs` (F` ((A + z) + 1)))) <_ (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (abs` (F` ((A + z) + 1))))) -> (abs` (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1)))) <_ (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (abs` (F` ((A + z) + 1))))))
96		addcl 5455	. . . . . . . . . 10 |- ((((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) e. CC /\ (F` ((A + z) + 1)) e. CC) -> (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1))) e. CC)
97	96, 89, 93	sylanc 473	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1))) e. CC)
98		abscl 7035	. . . . . . . . 9 |- ((((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1))) e. CC -> (abs` (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1)))) e. RR)
99	97, 98	syl 10	. . . . . . . 8 |- ((A e. NN /\ z e. NN) -> (abs` (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1)))) e. RR)
100		readdcl 5456	. . . . . . . . 9 |- (((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) e. RR /\ (abs` (F` ((A + z) + 1))) e. RR) -> ((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) + (abs` (F` ((A + z) + 1)))) e. RR)
101		abscl 7035	. . . . . . . . . 10 |- (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) e. CC -> (abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) e. RR)
102	89, 101	syl 10	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) e. RR)
103		abscl 7035	. . . . . . . . . 10 |- ((F` ((A + z) + 1)) e. CC -> (abs` (F` ((A + z) + 1))) e. RR)
104	93, 103	syl 10	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (abs` (F` ((A + z) + 1))) e. RR)
105	100, 102, 104	sylanc 473	. . . . . . . 8 |- ((A e. NN /\ z e. NN) -> ((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) + (abs` (F` ((A + z) + 1)))) e. RR)
106		readdcl 5456	. . . . . . . . 9 |- ((((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) e. RR /\ (abs` (F` ((A + z) + 1))) e. RR) -> (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (abs` (F` ((A + z) + 1)))) e. RR)
107		resubcl 5592	. . . . . . . . . 10 |- (((( + seq1 G)` (A + z)) e. RR /\ (( + seq1 G)` A) e. RR) -> ((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) e. RR)
108	65	ser1recli 6696	. . . . . . . . . . 11 |- ((A + z) e. NN -> (( + seq1 G)` (A + z)) e. RR)
109	85, 108	syl 10	. . . . . . . . . 10 |- ((A e. NN /\ z e. NN) -> (( + seq1 G)` (A + z)) e. RR)
110	65	ser1recli 6696	. . . . . . . . . . 11 |- (A e. NN -> (( + seq1 G)` A) e. RR)
111	110	adantr 389	. . . . . . . . . 10 |- ((A e. NN /\ z e. NN) -> (( + seq1 G)` A) e. RR)
112	107, 109, 111	sylanc 473	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> ((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) e. RR)
113	106, 112, 104	sylanc 473	. . . . . . . 8 |- ((A e. NN /\ z e. NN) -> (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (abs` (F` ((A + z) + 1)))) e. RR)
114	95, 99, 105, 113	syl3anc 864	. . . . . . 7 |- ((A e. NN /\ z e. NN) -> (((abs` (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1)))) <_ ((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) + (abs` (F` ((A + z) + 1)))) /\ ((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) + (abs` (F` ((A + z) + 1)))) <_ (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (abs` (F` ((A + z) + 1))))) -> (abs` (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1)))) <_ (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (abs` (F` ((A + z) + 1))))))
115	94, 114	mpand 705	. . . . . 6 |- ((A e. NN /\ z e. NN) -> (((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) + (abs` (F` ((A + z) + 1)))) <_ (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (abs` (F` ((A + z) + 1)))) -> (abs` (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1)))) <_ (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (abs` (F` ((A + z) + 1))))))
116		leadd1 5779	. . . . . . 7 |- (((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) e. RR /\ ((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) e. RR /\ (abs` (F` ((A + z) + 1))) e. RR) -> ((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) <-> ((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) + (abs` (F` ((A + z) + 1)))) <_ (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (abs` (F` ((A + z) + 1))))))
117	116, 102, 112, 104	syl3anc 864	. . . . . 6 |- ((A e. NN /\ z e. NN) -> ((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) <-> ((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) + (abs` (F` ((A + z) + 1)))) <_ (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (abs` (F` ((A + z) + 1))))))
118		ax1cn 5423	. . . . . . . . . . . . . 14 |- 1 e. CC
119		addass 5461	. . . . . . . . . . . . . 14 |- ((A e. CC /\ z e. CC /\ 1 e. CC) -> ((A + z) + 1) = (A + (z + 1)))
120	118, 119	mp3an3 911	. . . . . . . . . . . . 13 |- ((A e. CC /\ z e. CC) -> ((A + z) + 1) = (A + (z + 1)))
121		nncn 6075	. . . . . . . . . . . . 13 |- (A e. NN -> A e. CC)
122		nncn 6075	. . . . . . . . . . . . 13 |- (z e. NN -> z e. CC)
123	120, 121, 122	syl2an 456	. . . . . . . . . . . 12 |- ((A e. NN /\ z e. NN) -> ((A + z) + 1) = (A + (z + 1)))
124	123	fveq2d 3839	. . . . . . . . . . 11 |- ((A e. NN /\ z e. NN) -> (( + seq1 F)` ((A + z) + 1)) = (( + seq1 F)` (A + (z + 1))))
125	41, 44	seq1p1 6683	. . . . . . . . . . . 12 |- ((A + z) e. NN -> (( + seq1 F)` ((A + z) + 1)) = ((( + seq1 F)` (A + z)) + (F` ((A + z) + 1))))
126	85, 125	syl 10	. . . . . . . . . . 11 |- ((A e. NN /\ z e. NN) -> (( + seq1 F)` ((A + z) + 1)) = ((( + seq1 F)` (A + z)) + (F` ((A + z) + 1))))
127	124, 126	eqtr3d 1552	. . . . . . . . . 10 |- ((A e. NN /\ z e. NN) -> (( + seq1 F)` (A + (z + 1))) = ((( + seq1 F)` (A + z)) + (F` ((A + z) + 1))))
128	127	opreq1d 4033	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> ((( + seq1 F)` (A + (z + 1))) - (( + seq1 F)` A)) = (((( + seq1 F)` (A + z)) + (F` ((A + z) + 1))) - (( + seq1 F)` A)))
129		addsub 5538	. . . . . . . . . 10 |- (((( + seq1 F)` (A + z)) e. CC /\ (F` ((A + z) + 1)) e. CC /\ (( + seq1 F)` A) e. CC) -> (((( + seq1 F)` (A + z)) + (F` ((A + z) + 1))) - (( + seq1 F)` A)) = (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1))))
130	129, 87, 93, 88	syl3anc 864	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (((( + seq1 F)` (A + z)) + (F` ((A + z) + 1))) - (( + seq1 F)` A)) = (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1))))
131	128, 130	eqtrd 1550	. . . . . . . 8 |- ((A e. NN /\ z e. NN) -> ((( + seq1 F)` (A + (z + 1))) - (( + seq1 F)` A)) = (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1))))
132	131	fveq2d 3839	. . . . . . 7 |- ((A e. NN /\ z e. NN) -> (abs` ((( + seq1 F)` (A + (z + 1))) - (( + seq1 F)` A))) = (abs` (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1)))))
133	123	fveq2d 3839	. . . . . . . . . 10 |- ((A e. NN /\ z e. NN) -> (( + seq1 G)` ((A + z) + 1)) = (( + seq1 G)` (A + (z + 1))))
134	41, 54	seq1p1 6683	. . . . . . . . . . 11 |- ((A + z) e. NN -> (( + seq1 G)` ((A + z) + 1)) = ((( + seq1 G)` (A + z)) + (G` ((A + z) + 1))))
135	85, 134	syl 10	. . . . . . . . . 10 |- ((A e. NN /\ z e. NN) -> (( + seq1 G)` ((A + z) + 1)) = ((( + seq1 G)` (A + z)) + (G` ((A + z) + 1))))
136	133, 135	eqtr3d 1552	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (( + seq1 G)` (A + (z + 1))) = ((( + seq1 G)` (A + z)) + (G` ((A + z) + 1))))
137	136	opreq1d 4033	. . . . . . . 8 |- ((A e. NN /\ z e. NN) -> ((( + seq1 G)` (A + (z + 1))) - (( + seq1 G)` A)) = (((( + seq1 G)` (A + z)) + (G` ((A + z) + 1))) - (( + seq1 G)` A)))
138		addsub 5538	. . . . . . . . 9 |- (((( + seq1 G)` (A + z)) e. CC /\ (G` ((A + z) + 1)) e. CC /\ (( + seq1 G)` A) e. CC) -> (((( + seq1 G)` (A + z)) + (G` ((A + z) + 1))) - (( + seq1 G)` A)) = (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (G` ((A + z) + 1))))
139	68	ser1cl1i 6695	. . . . . . . . . 10 |- ((A + z) e. NN -> (( + seq1 G)` (A + z)) e. CC)
140	85, 139	syl 10	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (( + seq1 G)` (A + z)) e. CC)
141		fveq2 3835	. . . . . . . . . . . . . 14 |- (x = ((A + z) + 1) -> (G` x) = (G` ((A + z) + 1)))
142		fveq2 3835	. . . . . . . . . . . . . . 15 |- (x = ((A + z) + 1) -> (F` x) = (F` ((A + z) + 1)))
143	142	fveq2d 3839	. . . . . . . . . . . . . 14 |- (x = ((A + z) + 1) -> (abs` (F` x)) = (abs` (F` ((A + z) + 1))))
144	141, 143	eqeq12d 1532	. . . . . . . . . . . . 13 |- (x = ((A + z) + 1) -> ((G` x) = (abs` (F` x)) <-> (G` ((A + z) + 1)) = (abs` (F` ((A + z) + 1)))))
145	144, 59	vtoclga 1898	. . . . . . . . . . . 12 |- (((A + z) + 1) e. NN -> (G` ((A + z) + 1)) = (abs` (F` ((A + z) + 1))))
146	92, 103	syl 10	. . . . . . . . . . . 12 |- (((A + z) + 1) e. NN -> (abs` (F` ((A + z) + 1))) e. RR)
147	145, 146	eqeltrd 1591	. . . . . . . . . . 11 |- (((A + z) + 1) e. NN -> (G` ((A + z) + 1)) e. RR)
148	147	recnd 5469	. . . . . . . . . 10 |- (((A + z) + 1) e. NN -> (G` ((A + z) + 1)) e. CC)
149	91, 148	syl 10	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (G` ((A + z) + 1)) e. CC)
150	69	adantr 389	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (( + seq1 G)` A) e. CC)
151	138, 140, 149, 150	syl3anc 864	. . . . . . . 8 |- ((A e. NN /\ z e. NN) -> (((( + seq1 G)` (A + z)) + (G` ((A + z) + 1))) - (( + seq1 G)` A)) = (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (G` ((A + z) + 1))))
152	91, 145	syl 10	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (G` ((A + z) + 1)) = (abs` (F` ((A + z) + 1))))
153	152	opreq2d 4034	. . . . . . . 8 |- ((A e. NN /\ z e. NN) -> (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (G` ((A + z) + 1))) = (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (abs` (F` ((A + z) + 1)))))
154	137, 151, 153	3eqtrd 1554	. . . . . . 7 |- ((A e. NN /\ z e. NN) -> ((( + seq1 G)` (A + (z + 1))) - (( + seq1 G)` A)) = (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (abs` (F` (