Theorem ser1absdiflem 6929

Description: Lemma for ser1absdif 6930. 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 3969	. . . . . . . 8 |- (y = 1 -> (A + y) = (A + 1))
2	1	fveq2d 3728	. . . . . . 7 |- (y = 1 -> (( + seq1 F)` (A + y)) = (( + seq1 F)` (A + 1)))
3	2	opreq1d 3975	. . . . . 6 |- (y = 1 -> ((( + seq1 F)` (A + y)) - (( + seq1 F)` A)) = ((( + seq1 F)` (A + 1)) - (( + seq1 F)` A)))
4	3	fveq2d 3728	. . . . 5 |- (y = 1 -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) = (abs` ((( + seq1 F)` (A + 1)) - (( + seq1 F)` A))))
5	1	fveq2d 3728	. . . . . 6 |- (y = 1 -> (( + seq1 G)` (A + y)) = (( + seq1 G)` (A + 1)))
6	5	opreq1d 3975	. . . . 5 |- (y = 1 -> ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) = ((( + seq1 G)` (A + 1)) - (( + seq1 G)` A)))
7	4, 6	breq12d 2631	. . . 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 612	. . 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 3969	. . . . . . . 8 |- (y = z -> (A + y) = (A + z))
10	9	fveq2d 3728	. . . . . . 7 |- (y = z -> (( + seq1 F)` (A + y)) = (( + seq1 F)` (A + z)))
11	10	opreq1d 3975	. . . . . 6 |- (y = z -> ((( + seq1 F)` (A + y)) - (( + seq1 F)` A)) = ((( + seq1 F)` (A + z)) - (( + seq1 F)` A)))
12	11	fveq2d 3728	. . . . 5 |- (y = z -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) = (abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))))
13	9	fveq2d 3728	. . . . . 6 |- (y = z -> (( + seq1 G)` (A + y)) = (( + seq1 G)` (A + z)))
14	13	opreq1d 3975	. . . . 5 |- (y = z -> ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) = ((( + seq1 G)` (A + z)) - (( + seq1 G)` A)))
15	12, 14	breq12d 2631	. . . 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 612	. . 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 3969	. . . . . . . 8 |- (y = (z + 1) -> (A + y) = (A + (z + 1)))
18	17	fveq2d 3728	. . . . . . 7 |- (y = (z + 1) -> (( + seq1 F)` (A + y)) = (( + seq1 F)` (A + (z + 1))))
19	18	opreq1d 3975	. . . . . 6 |- (y = (z + 1) -> ((( + seq1 F)` (A + y)) - (( + seq1 F)` A)) = ((( + seq1 F)` (A + (z + 1))) - (( + seq1 F)` A)))
20	19	fveq2d 3728	. . . . 5 |- (y = (z + 1) -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) = (abs` ((( + seq1 F)` (A + (z + 1))) - (( + seq1 F)` A))))
21	17	fveq2d 3728	. . . . . 6 |- (y = (z + 1) -> (( + seq1 G)` (A + y)) = (( + seq1 G)` (A + (z + 1))))
22	21	opreq1d 3975	. . . . 5 |- (y = (z + 1) -> ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) = ((( + seq1 G)` (A + (z + 1))) - (( + seq1 G)` A)))
23	20, 22	breq12d 2631	. . . 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 612	. . 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 3969	. . . . . . . 8 |- (y = B -> (A + y) = (A + B))
26	25	fveq2d 3728	. . . . . . 7 |- (y = B -> (( + seq1 F)` (A + y)) = (( + seq1 F)` (A + B)))
27	26	opreq1d 3975	. . . . . 6 |- (y = B -> ((( + seq1 F)` (A + y)) - (( + seq1 F)` A)) = ((( + seq1 F)` (A + B)) - (( + seq1 F)` A)))
28	27	fveq2d 3728	. . . . 5 |- (y = B -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) = (abs` ((( + seq1 F)` (A + B)) - (( + seq1 F)` A))))
29	25	fveq2d 3728	. . . . . 6 |- (y = B -> (( + seq1 G)` (A + y)) = (( + seq1 G)` (A + B)))
30	29	opreq1d 3975	. . . . 5 |- (y = B -> ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) = ((( + seq1 G)` (A + B)) - (( + seq1 G)` A)))
31	28, 30	breq12d 2631	. . . 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 612	. . 3 |- (y = B -> ((A e. NN ->