Theorem ser1absdiflem 8181

Description: Lemma for ser1absdifi 8182. 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 4890	. . . . . . . 8 |- (y = 1 -> (A + y) = (A + 1))
2	1	fveq2d 4685	. . . . . . 7 |- (y = 1 -> (( + seq1 F)` (A + y)) = (( + seq1 F)` (A + 1)))
3	2	opreq1d 4897	. . . . . 6 |- (y = 1 -> ((( + seq1 F)` (A + y)) - (( + seq1 F)` A)) = ((( + seq1 F)` (A + 1)) - (( + seq1 F)` A)))
4	3	fveq2d 4685	. . . . 5 |- (y = 1 -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) = (abs` ((( + seq1 F)` (A + 1)) - (( + seq1 F)` A))))
5	1	fveq2d 4685	. . . . . 6 |- (y = 1 -> (( + seq1 G)` (A + y)) = (( + seq1 G)` (A + 1)))
6	5	opreq1d 4897	. . . . 5 |- (y = 1 -> ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) = ((( + seq1 G)` (A + 1)) - (( + seq1 G)` A)))
7	4, 6	breq12d 3351	. . . 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 674	. . 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 4890	. . . . . . . 8 |- (y = z -> (A + y) = (A + z))
10	9	fveq2d 4685	. . . . . . 7 |- (y = z -> (( + seq1 F)` (A + y)) = (( + seq1 F)` (A + z)))
11	10	opreq1d 4897	. . . . . 6 |- (y = z -> ((( + seq1 F)` (A + y)) - (( + seq1 F)` A)) = ((( + seq1 F)` (A + z)) - (( + seq1 F)` A)))
12	11	fveq2d 4685	. . . . 5 |- (y = z -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) = (abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))))
13	9	fveq2d 4685	. . . . . 6 |- (y = z -> (( + seq1 G)` (A + y)) = (( + seq1 G)` (A + z)))
14	13	opreq1d 4897	. . . . 5 |- (y = z -> ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) = ((( + seq1 G)` (A + z)) - (( + seq1 G)` A)))
15	12, 14	breq12d 3351	. . . 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 674	. . 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 4890	. . . . . . . 8 |- (y = (z + 1) -> (A + y) = (A + (z + 1)))
18	17	fveq2d 4685	. . . . . . 7 |- (y = (z + 1) -> (( + seq1 F)` (A + y)) = (( + seq1 F)` (A + (z + 1))))
19	18	opreq1d 4897	. . . . . 6 |- (y = (z + 1) -> ((( + seq1 F)` (A + y)) - (( + seq1 F)` A)) = ((( + seq1 F)` (A + (z + 1))) - (( + seq1 F)` A)))
20	19	fveq2d 4685	. . . . 5 |- (y = (z + 1) -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) = (abs` ((( + seq1 F)` (A + (z + 1))) - (( + seq1 F)` A))))
21	17	fveq2d 4685	. . . . . 6 |- (y = (z + 1) -> (( + seq1 G)` (A + y)) = (( + seq1 G)` (A + (z + 1))))
22	21	opreq1d 4897	. . . . 5 |- (y = (z + 1) -> ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) = ((( + seq1 G)` (A + (z + 1))) - (( + seq1 G)` A)))
23	20, 22	breq12d 3351	. . . 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 674	. . 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 4890	. . . . . . . 8 |- (y = B -> (A + y) = (A + B))
26	25	fveq2d 4685	. . . . . . 7 |- (y = B -> (( + seq1 F)` (A + y)) = (( + seq1 F)` (A + B)))
27	26	opreq1d 4897	. . . . . 6 |- (y = B -> ((( + seq1 F)` (A + y)) - (( + seq1 F)` A)) = ((( + seq1 F)` (A + B)) - (( + seq1 F)` A)))
28	27	fveq2d 4685	. . . . 5 |- (y = B -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) = (abs` ((( + seq1 F)` (A + B)) - (( + seq1 F)` A))))
29	25	fveq2d 4685	. . . . . 6 |- (y = B -> (( + seq1 G)` (A + y)) = (( + seq1 G)` (A + B)))
30	29	opreq1d 4897	. . . . 5 |- (y = B -> ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) = ((( + seq1 G)` (A + B)) - (( + seq1 G)` A)))
31	28, 30	breq12d 3351	. . . 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 674	. . 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 7118	. . . . . . 7 |- (A e. NN -> (A + 1) e. NN)
34		ser1absdif.1	. . . . . . . 8 |- F:NN-->CC
35	34	ffvelrni 4788	. . . . . . 7 |- ((A + 1) e. NN -> (F` (A + 1)) e. CC)
36	33, 35	syl 12	. . . . . 6 |- (A e. NN -> (F` (A + 1)) e. CC)
37		abscl 8084	. . . . . 6 |- ((F` (A + 1)) e. CC -> (abs` (F` (A + 1))) e. RR)
38	36, 37	syl 12	. . . . 5 |- (A e. NN -> (abs` (F` (A + 1))) e. RR)
39		leid 6701	. . . . 5 |- ((abs` (F` (A + 1))) e. RR -> (abs` (F` (A + 1))) <_ (abs` (F` (A + 1))))
40	38, 39	syl 12	. . . 4 |- (A e. NN -> (abs` (F` (A + 1))) <_ (abs` (F` (A + 1))))
41		addex 6470	. . . . . . . 8 |- + e. _V
42		nnex 7116	. . . . . . . . 9 |- NN e. _V
43		fex 4595	. . . . . . . . 9 |- ((F:NN-->CC /\ NN e. _V) -> F e. _V)
44	34, 42, 43	mp2an 761	. . . . . . . 8 |- F e. _V
45	41, 44	seq1p1 7731	. . . . . . 7 |- (A e. NN -> (( + seq1 F)` (A + 1)) = ((( + seq1 F)` A) + (F` (A + 1))))
46	45	opreq1d 4897	. . . . . 6 |- (A e. NN -> ((( + seq1 F)` (A + 1)) - (( + seq1 F)` A)) = (((( + seq1 F)` A) + (F` (A + 1))) - (( + seq1 F)` A)))
47	34	ser1cl1i 7743	. . . . . . 7 |- (A e. NN -> (( + seq1 F)` A) e. CC)
48		pncan2 6558	. . . . . . 7 |- (((( + seq1 F)` A) e. CC /\ (F` (A + 1)) e. CC) -> (((( + seq1 F)` A) + (F` (A + 1))) - (( + seq1 F)` A)) = (F` (A + 1)))
49	47, 36, 48	syl11anc 524	. . . . . 6 |- (A e. NN -> (((( + seq1 F)` A) + (F` (A + 1))) - (( + seq1 F)` A)) = (F` (A + 1)))
50	46, 49	eqtrd 1925	. . . . 5 |- (A e. NN -> ((( + seq1 F)` (A + 1)) - (( + seq1 F)` A)) = (F` (A + 1)))
51	50	fveq2d 4685	. . . 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 4535	. . . . . . . 8 |- ((G Fn NN /\ NN e. _V) -> G e. _V)
54	52, 42, 53	mp2an 761	. . . . . . 7 |- G e. _V
55	41, 54	seq1p1 7731	. . . . . 6 |- (A e. NN -> (( + seq1 G)` (A + 1)) = ((( + seq1 G)` A) + (G` (A + 1))))
56	55	opreq1d 4897	. . . . 5 |- (A e. NN -> ((( + seq1 G)` (A + 1)) - (( + seq1 G)` A)) = (((( + seq1 G)` A) + (G` (A + 1))) - (( + seq1 G)` A)))
57		ffnfv 4801	. . . . . . . . 9 |- (G:NN-->RR <-> (G Fn NN /\ A.x e. NN (G` x) e. RR))
58		ser1absdif.3	. . . . . . . . . . 11 |- (x e. NN -> (G` x) = (abs` (F` x)))
59	34	ffvelrni 4788	. . . . . . . . . . . 12 |- (x e. NN -> (F` x) e. CC)
60		abscl 8084	. . . . . . . . . . . 12 |- ((F` x) e. CC -> (abs` (F` x)) e. RR)
61	59, 60	syl 12	. . . . . . . . . . 11 |- (x e. NN -> (abs` (F` x)) e. RR)
62	58, 61	eqeltrd 1971	. . . . . . . . . 10 |- (x e. NN -> (G` x) e. RR)
63	62	rgen 2159	. . . . . . . . 9 |- A.x e. NN (G` x) e. RR
64	57, 52, 63	mpbir2an 800	. . . . . . . 8 |- G:NN-->RR
65		axresscn 6420	. . . . . . . 8 |- RR C_ CC
66		fss 4571	. . . . . . . 8 |- ((G:NN-->RR /\ RR C_ CC) -> G:NN-->CC)
67	64, 65, 66	mp2an 761	. . . . . . 7 |- G:NN-->CC
68	67	ser1cl1i 7743	. . . . . 6 |- (A e. NN -> (( + seq1 G)` A) e. CC)
69		fveq2 4681	. . . . . . . . . . 11 |- (x = (A + 1) -> (G` x) = (G` (A + 1)))
70		fveq2 4681	. . . . . . . . . . . 12 |- (x = (A + 1) -> (F` x) = (F` (A + 1)))
71	70	fveq2d 4685	. . . . . . . . . . 11 |- (x = (A + 1) -> (abs` (F` x)) = (abs` (F` (A + 1))))
72	69, 71	eqeq12d 1899	. . . . . . . . . 10 |- (x = (A + 1) -> ((G` x) = (abs` (F` x)) <-> (G` (A + 1)) = (abs` (F` (A + 1)))))
73	72, 58	vtoclga 2352	. . . . . . . . 9 |- ((A + 1) e. NN -> (G` (A + 1)) = (abs` (F` (A + 1))))
74	35, 37	syl 12	. . . . . . . . 9 |- ((A + 1) e. NN -> (abs` (F` (A + 1))) e. RR)
75	73, 74	eqeltrd 1971	. . . . . . . 8 |- ((A + 1) e. NN -> (G` (A + 1)) e. RR)
76	75	recnd 6468	. . . . . . 7 |- ((A + 1) e. NN -> (G` (A + 1)) e. CC)
77	33, 76	syl 12	. . . . . 6 |- (A e. NN -> (G` (A + 1)) e. CC)
78		pncan2 6558	. . . . . 6 |- (((( + seq1 G)` A) e. CC /\ (G` (A + 1)) e. CC) -> (((( + seq1 G)` A) + (G` (A + 1))) - (( + seq1 G)` A)) = (G` (A + 1)))
79	68, 77, 78	syl11anc 524	. . . . 5 |- (A e. NN -> (((( + seq1 G)` A) + (G` (A + 1))) - (( + seq1 G)` A)) = (G` (A + 1)))
80	33, 73	syl 12	. . . . 5 |- (A e. NN -> (G` (A + 1)) = (abs` (F` (A + 1))))
81	56, 79, 80	3eqtrd 1929	. . . 4 |- (A e. NN -> ((( + seq1 G)` (A + 1)) - (( + seq1 G)` A)) = (abs` (F` (A + 1))))
82	40, 51, 81	3brtr4d 3367	. . 3 |- (A e. NN -> (abs` ((( + seq1 F)` (A + 1)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + 1)) - (( + seq1 G)` A)))
83		nnaddcl 7123	. . . . . . . . . 10 |- ((A e. NN /\ z e. NN) -> (A + z) e. NN)
84	34	ser1cl1i 7743	. . . . . . . . . 10 |- ((A + z) e. NN -> (( + seq1 F)` (A + z)) e. CC)
85	83, 84	syl 12	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (( + seq1 F)` (A + z)) e. CC)
86	47	adantr 425	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (( + seq1 F)` A) e. CC)
87		subcl 6524	. . . . . . . . 9 |- (((( + seq1 F)` (A + z)) e. CC /\ (( + seq1 F)` A) e. CC) -> ((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) e. CC)
88	85, 86, 87	syl11anc 524	. . . . . . . 8 |- ((A e. NN /\ z e. NN) -> ((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) e. CC)
89		peano2nn 7118	. . . . . . . . . 10 |- ((A + z) e. NN -> ((A + z) + 1) e. NN)
90	83, 89	syl 12	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> ((A + z) + 1) e. NN)
91	34	ffvelrni 4788	. . . . . . . . 9 |- (((A + z) + 1) e. NN -> (F` ((A + z) + 1)) e. CC)
92	90, 91	syl 12	. . . . . . . 8 |- ((A e. NN /\ z e. NN) -> (F` ((A + z) + 1)) e. CC)
93		abstri 8150	. . . . . . . 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)))))
94	88, 92, 93	syl11anc 524	. . . . . . 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		addcl 6454	. . . . . . . . . 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)
96	88, 92, 95	syl11anc 524	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1))) e. CC)
97		abscl 8084	. . . . . . . . 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)
98	96, 97	syl 12	. . . . . . . 8 |- ((A e. NN /\ z e. NN) -> (abs` (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1)))) e. RR)
99		abscl 8084	. . . . . . . . . 10 |- (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) e. CC -> (abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) e. RR)
100	88, 99	syl 12	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) e. RR)
101		abscl 8084	. . . . . . . . . 10 |- ((F` ((A + z) + 1)) e. CC -> (abs` (F` ((A + z) + 1))) e. RR)
102	92, 101	syl 12	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (abs` (F` ((A + z) + 1))) e. RR)
103		readdcl 6455	. . . . . . . . 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)
104	100, 102, 103	syl11anc 524	. . . . . . . 8 |- ((A e. NN /\ z e. NN) -> ((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) + (abs` (F` ((A + z) + 1)))) e. RR)
105	64	ser1recli 7744	. . . . . . . . . . 11 |- ((A + z) e. NN -> (( + seq1 G)` (A + z)) e. RR)
106	83, 105	syl 12	. . . . . . . . . 10 |- ((A e. NN /\ z e. NN) -> (( + seq1 G)` (A + z)) e. RR)
107	64	ser1recli 7744	. . . . . . . . . . 11 |- (A e. NN -> (( + seq1 G)` A) e. RR)
108	107	adantr 425	. . . . . . . . . 10 |- ((A e. NN /\ z e. NN) -> (( + seq1 G)` A) e. RR)
109		resubcl 6601	. . . . . . . . . 10 |- (((( + seq1 G)` (A + z)) e. RR /\ (( + seq1 G)` A) e. RR) -> ((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) e. RR)
110	106, 108, 109	syl11anc 524	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> ((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) e. RR)
111		readdcl 6455	. . . . . . . . 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)
112	110, 102, 111	syl11anc 524	. . . . . . . 8 |- ((A e. NN /\ z e. NN) -> (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (abs` (F` ((A + z) + 1)))) e. RR)
113		letr 6695	. . . . . . . 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))))))
114	98, 104, 112, 113	syl111anc 1100	. . . . . . 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 765	. . . . . 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 6808	. . . . . . 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	100, 110, 102, 116	syl111anc 1100	. . . . . 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 6422	. . . . . . . . . . . . . 14 |- 1 e. CC
119		addass 6460	. . . . . . . . . . . . . 14 |- ((A e. CC /\ z e. CC /\ 1 e. CC) -> ((A + z) + 1) = (A + (z + 1)))
120	118, 119	mp3an3 1180	. . . . . . . . . . . . 13 |- ((A e. CC /\ z e. CC) -> ((A + z) + 1) = (A + (z + 1)))
121		nncn 7113	. . . . . . . . . . . . 13 |- (A e. NN -> A e. CC)
122		nncn 7113	. . . . . . . . . . . . 13 |- (z e. NN -> z e. CC)
123	120, 121, 122	syl2an 503	. . . . . . . . . . . 12 |- ((A e. NN /\ z e. NN) -> ((A + z) + 1) = (A + (z + 1)))
124	123	fveq2d 4685	. . . . . . . . . . 11 |- ((A e. NN /\ z e. NN) -> (( + seq1 F)` ((A + z) + 1)) = (( + seq1 F)` (A + (z + 1))))
125	41, 44	seq1p1 7731	. . . . . . . . . . . 12 |- ((A + z) e. NN -> (( + seq1 F)` ((A + z) + 1)) = ((( + seq1 F)` (A + z)) + (F` ((A + z) + 1))))
126	83, 125	syl 12	. . . . . . . . . . 11 |- ((A e. NN /\ z e. NN) -> (( + seq1 F)` ((A + z) + 1)) = ((( + seq1 F)` (A + z)) + (F` ((A + z) + 1))))
127	124, 126	eqtr3d 1927	. . . . . . . . . 10 |- ((A e. NN /\ z e. NN) -> (( + seq1 F)` (A + (z + 1))) = ((( + seq1 F)` (A + z)) + (F` ((A + z) + 1))))
128	127	opreq1d 4897	. . . . . . . . 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 6542	. . . . . . . . . 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	85, 92, 86, 129	syl111anc 1100	. . . . . . . . 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 1925	. . . . . . . 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 4685	. . . . . . 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 4685	. . . . . . . . . 10 |- ((A e. NN /\ z e. NN) -> (( + seq1 G)` ((A + z) + 1)) = (( + seq1 G)` (A + (z + 1))))
134	41, 54	seq1p1 7731	. . . . . . . . . . 11 |- ((A + z) e. NN -> (( + seq1 G)` ((A + z) + 1)) = ((( + seq1 G)` (A + z)) + (G` ((A + z) + 1))))
135	83, 134	syl 12	. . . . . . . . . 10 |- ((A e. NN /\ z e. NN) -> (( + seq1 G)` ((A + z) + 1)) = ((( + seq1 G)` (A + z)) + (G` ((A + z) + 1))))
136	133, 135	eqtr3d 1927	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (( + seq1 G)` (A + (z + 1))) = ((( + seq1 G)` (A + z)) + (G` ((A + z) + 1))))
137	136	opreq1d 4897	. . . . . . . 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	67	ser1cl1i 7743	. . . . . . . . . 10 |- ((A + z) e. NN -> (( + seq1 G)` (A + z)) e. CC)
139	83, 138	syl 12	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (( + seq1 G)` (A + z)) e. CC)
140		fveq2 4681	. . . . . . . . . . . . . 14 |- (x = ((A + z) + 1) -> (G` x) = (G` ((A + z) + 1)))
141		fveq2 4681	. . . . . . . . . . . . . . 15 |- (x = ((A + z) + 1) -> (F` x) = (F` ((A + z) + 1)))
142	141	fveq2d 4685	. . . . . . . . . . . . . 14 |- (x = ((A + z) + 1) -> (abs` (F` x)) = (abs` (F` ((A + z) + 1))))
143	140, 142	eqeq12d 1899	. . . . . . . . . . . . 13 |- (x = ((A + z) + 1) -> ((G` x) = (abs` (F` x)) <-> (G` ((A + z) + 1)) = (abs` (F` ((A + z) + 1)))))
144	143, 58	vtoclga 2352	. . . . . . . . . . . 12 |- (((A + z) + 1) e. NN -> (G` ((A + z) + 1)) = (abs` (F` ((A + z) + 1))))
145	91, 101	syl 12	. . . . . . . . . . . 12 |- (((A + z) + 1) e. NN -> (abs` (F` ((A + z) + 1))) e. RR)
146	144, 145	eqeltrd 1971	. . . . . . . . . . 11 |- (((A + z) + 1) e. NN -> (G` ((A + z) + 1)) e. RR)
147	146	recnd 6468	. . . . . . . . . 10 |- (((A + z) + 1) e. NN -> (G` ((A + z) + 1)) e. CC)
148	90, 147	syl 12	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (G` ((A + z) + 1)) e. CC)
149	68	adantr 425	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (( + seq1 G)` A) e. CC)
150		addsub 6542	. . . . . . . . 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))))
151	139, 148, 149, 150	syl111anc 1100	. . . . . . . 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	90, 144	syl 12	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (G` ((A + z) + 1)) = (abs` (F` ((A + z) + 1))))
153	152	opreq2d 4898	. . . . . . . 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 1929	. . . . . . 7 |- ((A e. NN /\ z e. NN) -> ((( + seq1 G)` (A + (z + 1))) - (( + seq1 G)` A)) = (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (abs` (F` ((A + z) + 1)))))
155	132, 154	breq12d 3351	. . . . . 6 |- ((A e. NN /\ z e. NN) -> ((abs` ((( + seq1 F)` (A + (z + 1))) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + (z + 1))) - (( + seq1 G)` A)) <-> (abs` (((( + seq1 F)` (A + z)) - (( + seq1 F)` A)) + (F` ((A + z) + 1)))) <_ (((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) + (abs` (F` ((A + z) + 1))))))
156	115, 117, 155	3imtr4d 602	. . . . 5 |- ((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 + 1))) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + (z + 1))) - (( + seq1 G)` A))))
157	156	expcom 403	. . . 4 |- (z e. NN -> (A e. NN -> ((abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + z)) - (( + seq1 G)` A)) -> (abs` ((( + seq1 F)` (A + (z + 1))) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + (z + 1))) - (( + seq1 G)` A)))))
158	157	a2d 16	. . 3 |- (z e. NN -> ((A e. NN -> (abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + z)) - (( + seq1 G)` A))) -> (A e. NN -> (abs` ((( + seq1 F)` (A + (z + 1))) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + (z + 1))) - (( + seq1 G)` A)))))
159	8, 16, 24, 32, 82, 158	nnind 7120	. 2 |- (B e. NN -> (A e. NN -> (abs` ((( + seq1 F)` (A + B)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + B)) - (( + seq1 G)` A))))
160	159	impcom 378	1 |- ((A e. NN /\ B e. NN) -> (abs` ((( + seq1 F)` (A + B)) - (( + seq1 F)` A))) <_ ((( + seq1 G)` (A + B)) - (( + seq1 G)` A)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  A.wral 2105  _Vcvv 2292   C_ wss 2593   class class class wbr 3338   Fn wfn 3993  -->wf 3994  ` cfv 3998  (class class class)co 4884  CCcc 6384  RRcr 6385  1c1 6387   + caddc 6389   - cmin 6445   <_ cle 6448  NNcn 6449   seq1 cseq1 7720  abscabs 8000

This theorem is referenced by:  ser1absdifi 8182

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-sup 5664  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-div 6892  df-n 7108  df-2 7154  df-n0 7309  df-z 7345  df-seq1 7721  df-exp 7812  df-sqr 7920  df-re 8001  df-im 8002  df-cj 8003  df-abs 8004

Copyright terms: Public domain