HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem ser1absdiflem 6866
Description: Lemma for ser1absdif 6867. 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
StepHypRef Expression
1 opreq2 3954 . . . . . . . 8 |- (y = 1 -> (A + y) = (A + 1))
21fveq2d 3713 . . . . . . 7 |- (y = 1 -> (( + seq1 F)` (A + y)) = (( + seq1 F)` (A + 1)))
32opreq1d 3960 . . . . . 6 |- (y = 1 -> ((( + seq1 F)` (A + y)) - (( + seq1 F)` A)) = ((( + seq1 F)` (A + 1)) - (( + seq1 F)` A)))
43fveq2d 3713 . . . . 5 |- (y = 1 -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) = (abs` ((( + seq1 F)` (A + 1)) - (( + seq1 F)` A))))
51fveq2d 3713 . . . . . 6 |- (y = 1 -> (( + seq1 G)` (A + y)) = (( + seq1 G)` (A + 1)))
65opreq1d 3960 . . . . 5 |- (y = 1 -> ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) = ((( + seq1 G)` (A + 1)) - (( + seq1 G)` A)))
74, 6breq12d 2621 . . . 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))))
87imbi2d 610 . . 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 3954 . . . . . . . 8 |- (y = z -> (A + y) = (A + z))
109fveq2d 3713 . . . . . . 7 |- (y = z -> (( + seq1 F)` (A + y)) = (( + seq1 F)` (A + z)))
1110opreq1d 3960 . . . . . 6 |- (y = z -> ((( + seq1 F)` (A + y)) - (( + seq1 F)` A)) = ((( + seq1 F)` (A + z)) - (( + seq1 F)` A)))
1211fveq2d 3713 . . . . 5 |- (y = z -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) = (abs` ((( + seq1 F)` (A + z)) - (( + seq1 F)` A))))
139fveq2d 3713 . . . . . 6 |- (y = z -> (( + seq1 G)` (A + y)) = (( + seq1 G)` (A + z)))
1413opreq1d 3960 . . . . 5 |- (y = z -> ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) = ((( + seq1 G)` (A + z)) - (( + seq1 G)` A)))
1512, 14breq12d 2621 . . . 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))))
1615imbi2d 610 . . 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 3954 . . . . . . . 8 |- (y = (z + 1) -> (A + y) = (A + (z + 1)))
1817fveq2d 3713 . . . . . . 7 |- (y = (z + 1) -> (( + seq1 F)` (A + y)) = (( + seq1 F)` (A + (z + 1))))
1918opreq1d 3960 . . . . . 6 |- (y = (z + 1) -> ((( + seq1 F)` (A + y)) - (( + seq1 F)` A)) = ((( + seq1 F)` (A + (z + 1))) - (( + seq1 F)` A)))
2019fveq2d 3713 . . . . 5 |- (y = (z + 1) -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) = (abs` ((( + seq1 F)` (A + (z + 1))) - (( + seq1 F)` A))))
2117fveq2d 3713 . . . . . 6 |- (y = (z + 1) -> (( + seq1 G)` (A + y)) = (( + seq1 G)` (A + (z + 1))))
2221opreq1d 3960 . . . . 5 |- (y = (z + 1) -> ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) = ((( + seq1 G)` (A + (z + 1))) - (( + seq1 G)` A)))
2320, 22breq12d 2621 . . . 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))))
2423imbi2d 610 . . 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 3954 . . . . . . . 8 |- (y = B -> (A + y) = (A + B))
2625fveq2d 3713 . . . . . . 7 |- (y = B -> (( + seq1 F)` (A + y)) = (( + seq1 F)` (A + B)))
2726opreq1d 3960 . . . . . 6 |- (y = B -> ((( + seq1 F)` (A + y)) - (( + seq1 F)` A)) = ((( + seq1 F)` (A + B)) - (( + seq1 F)` A)))
2827fveq2d 3713 . . . . 5 |- (y = B -> (abs` ((( + seq1 F)` (A + y)) - (( + seq1 F)` A))) = (abs` ((( + seq1 F)` (A + B)) - (( + seq1 F)` A))))
2925fveq2d 3713 . . . . . 6 |- (y = B -> (( + seq1 G)` (A + y)) = (( + seq1 G)` (A + B)))
3029opreq1d 3960 . . . . 5 |- (y = B -> ((( + seq1 G)` (A + y)) - (( + seq1 G)` A)) = ((( + seq1 G)` (A + B)) - (( + seq1 G)` A)))
3128, 30breq12d 2621 . . . 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))))
3231imbi2d 610 . . 3 |- (y = B -> ((A e. NN -> (