Metamath Proof Explorer

Theorem iseraltlem3

Description: Lemma for iseralt . From iseraltlem2 , we have ( -u 1 ^ n ) x. S ( n + 2 k ) <_ ( -u 1 ^ n ) x. S ( n ) and ( -u 1 ^ n ) x. S ( n + 1 ) <_ ( -u 1 ^ n ) x. S ( n + 2 k + 1 ) , and we also have ( -u 1 ^ n ) x. S ( n + 1 ) = ( -u 1 ^ n ) x. S ( n ) - G ( n + 1 ) for each n by the definition of the partial sum S , so combining the inequalities we get ( -u 1 ^ n ) x. S ( n ) - G ( n + 1 ) = ( -u 1 ^ n ) x. S ( n + 1 ) <_ ( -u 1 ^ n ) x. S ( n + 2 k + 1 ) = ( -u 1 ^ n ) x. S ( n + 2 k ) - G ( n + 2 k + 1 ) <_ ( -u 1 ^ n ) x. S ( n + 2 k ) <_ ( -u 1 ^ n ) x. S ( n ) <_ ( -u 1 ^ n ) x. S ( n ) + G ( n + 1 ) , so | ( -u 1 ^ n ) x. S ( n + 2 k + 1 ) - ( -u 1 ^ n ) x. S ( n ) | = | S ( n + 2 k + 1 ) - S ( n ) | <_ G ( n + 1 ) and | ( -u 1 ^ n ) x. S ( n + 2 k ) - ( -u 1 ^ n ) x. S ( n ) | = | S ( n + 2 k ) - S ( n ) | <_ G ( n + 1 ) . Thus, both even and odd partial sums are Cauchy if G converges to 0 . (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses iseralt.1 
|- Z = ( ZZ>= ` M )
iseralt.2 
|- ( ph -> M e. ZZ )
iseralt.3 
|- ( ph -> G : Z --> RR )
iseralt.4 
|- ( ( ph /\ k e. Z ) -> ( G ` ( k + 1 ) ) <_ ( G ` k ) )
iseralt.5 
|- ( ph -> G ~~> 0 )
iseralt.6 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( ( -u 1 ^ k ) x. ( G ` k ) ) )
Assertion iseraltlem3 
|- ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( abs ` ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) ) <_ ( G ` ( N + 1 ) ) /\ ( abs ` ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) ) <_ ( G ` ( N + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 iseralt.1 
 |-  Z = ( ZZ>= ` M )
2 iseralt.2 
 |-  ( ph -> M e. ZZ )
3 iseralt.3 
 |-  ( ph -> G : Z --> RR )
4 iseralt.4 
 |-  ( ( ph /\ k e. Z ) -> ( G ` ( k + 1 ) ) <_ ( G ` k ) )
5 iseralt.5 
 |-  ( ph -> G ~~> 0 )
6 iseralt.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( ( -u 1 ^ k ) x. ( G ` k ) ) )
7 neg1rr 
 |-  -u 1 e. RR
8 7 a1i 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> -u 1 e. RR )
9 neg1ne0 
 |-  -u 1 =/= 0
10 9 a1i 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> -u 1 =/= 0 )
11 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
12 1 11 eqsstri 
 |-  Z C_ ZZ
13 simp2 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> N e. Z )
14 12 13 sseldi 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> N e. ZZ )
15 8 10 14 reexpclzd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u 1 ^ N ) e. RR )
16 15 recnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u 1 ^ N ) e. CC )
17 7 a1i 
 |-  ( ( ph /\ k e. Z ) -> -u 1 e. RR )
18 9 a1i 
 |-  ( ( ph /\ k e. Z ) -> -u 1 =/= 0 )
19 simpr 
 |-  ( ( ph /\ k e. Z ) -> k e. Z )
20 12 19 sseldi 
 |-  ( ( ph /\ k e. Z ) -> k e. ZZ )
21 17 18 20 reexpclzd 
 |-  ( ( ph /\ k e. Z ) -> ( -u 1 ^ k ) e. RR )
22 3 ffvelrnda 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )
23 21 22 remulcld 
 |-  ( ( ph /\ k e. Z ) -> ( ( -u 1 ^ k ) x. ( G ` k ) ) e. RR )
24 6 23 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
25 1 2 24 serfre 
 |-  ( ph -> seq M ( + , F ) : Z --> RR )
26 25 3ad2ant1 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> seq M ( + , F ) : Z --> RR )
27 13 1 eleqtrdi 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> N e. ( ZZ>= ` M ) )
28 2nn0 
 |-  2 e. NN0
29 simp3 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> K e. NN0 )
30 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ K e. NN0 ) -> ( 2 x. K ) e. NN0 )
31 28 29 30 sylancr 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( 2 x. K ) e. NN0 )
32 uzaddcl 
 |-  ( ( N e. ( ZZ>= ` M ) /\ ( 2 x. K ) e. NN0 ) -> ( N + ( 2 x. K ) ) e. ( ZZ>= ` M ) )
33 27 31 32 syl2anc 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( N + ( 2 x. K ) ) e. ( ZZ>= ` M ) )
34 33 1 eleqtrrdi 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( N + ( 2 x. K ) ) e. Z )
35 26 34 ffvelrnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) e. RR )
36 35 recnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) e. CC )
37 26 13 ffvelrnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( seq M ( + , F ) ` N ) e. RR )
38 37 recnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( seq M ( + , F ) ` N ) e. CC )
39 16 36 38 subdid 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) ) = ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) - ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) )
40 39 fveq2d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( ( -u 1 ^ N ) x. ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) ) ) = ( abs ` ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) - ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) ) )
41 35 37 resubcld 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) e. RR )
42 41 recnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) e. CC )
43 16 42 absmuld 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( ( -u 1 ^ N ) x. ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) ) ) = ( ( abs ` ( -u 1 ^ N ) ) x. ( abs ` ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) ) ) )
44 40 43 eqtr3d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) - ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) ) = ( ( abs ` ( -u 1 ^ N ) ) x. ( abs ` ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) ) ) )
45 8 recnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> -u 1 e. CC )
46 absexpz 
 |-  ( ( -u 1 e. CC /\ -u 1 =/= 0 /\ N e. ZZ ) -> ( abs ` ( -u 1 ^ N ) ) = ( ( abs ` -u 1 ) ^ N ) )
47 45 10 14 46 syl3anc 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( -u 1 ^ N ) ) = ( ( abs ` -u 1 ) ^ N ) )
48 ax-1cn 
 |-  1 e. CC
49 48 absnegi 
 |-  ( abs ` -u 1 ) = ( abs ` 1 )
50 abs1 
 |-  ( abs ` 1 ) = 1
51 49 50 eqtri 
 |-  ( abs ` -u 1 ) = 1
52 51 oveq1i 
 |-  ( ( abs ` -u 1 ) ^ N ) = ( 1 ^ N )
53 1exp 
 |-  ( N e. ZZ -> ( 1 ^ N ) = 1 )
54 14 53 syl 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( 1 ^ N ) = 1 )
55 52 54 syl5eq 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( abs ` -u 1 ) ^ N ) = 1 )
56 47 55 eqtrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( -u 1 ^ N ) ) = 1 )
57 56 oveq1d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( abs ` ( -u 1 ^ N ) ) x. ( abs ` ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) ) ) = ( 1 x. ( abs ` ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) ) ) )
58 42 abscld 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) ) e. RR )
59 58 recnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) ) e. CC )
60 59 mulid2d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( 1 x. ( abs ` ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) ) ) = ( abs ` ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) ) )
61 44 57 60 3eqtrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) - ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) ) = ( abs ` ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) ) )
62 15 37 remulcld 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) e. RR )
63 3 3ad2ant1 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> G : Z --> RR )
64 1 peano2uzs 
 |-  ( N e. Z -> ( N + 1 ) e. Z )
65 64 3ad2ant2 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( N + 1 ) e. Z )
66 63 65 ffvelrnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( G ` ( N + 1 ) ) e. RR )
67 62 66 resubcld 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) - ( G ` ( N + 1 ) ) ) e. RR )
68 1 peano2uzs 
 |-  ( ( N + ( 2 x. K ) ) e. Z -> ( ( N + ( 2 x. K ) ) + 1 ) e. Z )
69 34 68 syl 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( N + ( 2 x. K ) ) + 1 ) e. Z )
70 26 69 ffvelrnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) e. RR )
71 15 70 remulcld 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) e. RR )
72 15 35 remulcld 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) e. RR )
73 seqp1 
 |-  ( N e. ( ZZ>= ` M ) -> ( seq M ( + , F ) ` ( N + 1 ) ) = ( ( seq M ( + , F ) ` N ) + ( F ` ( N + 1 ) ) ) )
74 27 73 syl 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( seq M ( + , F ) ` ( N + 1 ) ) = ( ( seq M ( + , F ) ` N ) + ( F ` ( N + 1 ) ) ) )
75 fveq2 
 |-  ( k = ( N + 1 ) -> ( F ` k ) = ( F ` ( N + 1 ) ) )
76 oveq2 
 |-  ( k = ( N + 1 ) -> ( -u 1 ^ k ) = ( -u 1 ^ ( N + 1 ) ) )
77 fveq2 
 |-  ( k = ( N + 1 ) -> ( G ` k ) = ( G ` ( N + 1 ) ) )
78 76 77 oveq12d 
 |-  ( k = ( N + 1 ) -> ( ( -u 1 ^ k ) x. ( G ` k ) ) = ( ( -u 1 ^ ( N + 1 ) ) x. ( G ` ( N + 1 ) ) ) )
79 75 78 eqeq12d 
 |-  ( k = ( N + 1 ) -> ( ( F ` k ) = ( ( -u 1 ^ k ) x. ( G ` k ) ) <-> ( F ` ( N + 1 ) ) = ( ( -u 1 ^ ( N + 1 ) ) x. ( G ` ( N + 1 ) ) ) ) )
80 6 ralrimiva 
 |-  ( ph -> A. k e. Z ( F ` k ) = ( ( -u 1 ^ k ) x. ( G ` k ) ) )
81 80 3ad2ant1 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> A. k e. Z ( F ` k ) = ( ( -u 1 ^ k ) x. ( G ` k ) ) )
82 79 81 65 rspcdva 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( F ` ( N + 1 ) ) = ( ( -u 1 ^ ( N + 1 ) ) x. ( G ` ( N + 1 ) ) ) )
83 82 oveq2d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( seq M ( + , F ) ` N ) + ( F ` ( N + 1 ) ) ) = ( ( seq M ( + , F ) ` N ) + ( ( -u 1 ^ ( N + 1 ) ) x. ( G ` ( N + 1 ) ) ) ) )
84 45 10 14 expp1zd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u 1 ^ ( N + 1 ) ) = ( ( -u 1 ^ N ) x. -u 1 ) )
85 neg1cn 
 |-  -u 1 e. CC
86 mulcom 
 |-  ( ( ( -u 1 ^ N ) e. CC /\ -u 1 e. CC ) -> ( ( -u 1 ^ N ) x. -u 1 ) = ( -u 1 x. ( -u 1 ^ N ) ) )
87 16 85 86 sylancl 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. -u 1 ) = ( -u 1 x. ( -u 1 ^ N ) ) )
88 16 mulm1d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u 1 x. ( -u 1 ^ N ) ) = -u ( -u 1 ^ N ) )
89 84 87 88 3eqtrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u 1 ^ ( N + 1 ) ) = -u ( -u 1 ^ N ) )
90 89 oveq1d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ ( N + 1 ) ) x. ( G ` ( N + 1 ) ) ) = ( -u ( -u 1 ^ N ) x. ( G ` ( N + 1 ) ) ) )
91 66 recnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( G ` ( N + 1 ) ) e. CC )
92 16 91 mulneg1d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u ( -u 1 ^ N ) x. ( G ` ( N + 1 ) ) ) = -u ( ( -u 1 ^ N ) x. ( G ` ( N + 1 ) ) ) )
93 90 92 eqtrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ ( N + 1 ) ) x. ( G ` ( N + 1 ) ) ) = -u ( ( -u 1 ^ N ) x. ( G ` ( N + 1 ) ) ) )
94 93 oveq2d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( seq M ( + , F ) ` N ) + ( ( -u 1 ^ ( N + 1 ) ) x. ( G ` ( N + 1 ) ) ) ) = ( ( seq M ( + , F ) ` N ) + -u ( ( -u 1 ^ N ) x. ( G ` ( N + 1 ) ) ) ) )
95 74 83 94 3eqtrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( seq M ( + , F ) ` ( N + 1 ) ) = ( ( seq M ( + , F ) ` N ) + -u ( ( -u 1 ^ N ) x. ( G ` ( N + 1 ) ) ) ) )
96 15 66 remulcld 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( G ` ( N + 1 ) ) ) e. RR )
97 96 recnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( G ` ( N + 1 ) ) ) e. CC )
98 38 97 negsubd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( seq M ( + , F ) ` N ) + -u ( ( -u 1 ^ N ) x. ( G ` ( N + 1 ) ) ) ) = ( ( seq M ( + , F ) ` N ) - ( ( -u 1 ^ N ) x. ( G ` ( N + 1 ) ) ) ) )
99 95 98 eqtrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( seq M ( + , F ) ` ( N + 1 ) ) = ( ( seq M ( + , F ) ` N ) - ( ( -u 1 ^ N ) x. ( G ` ( N + 1 ) ) ) ) )
100 99 oveq2d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + 1 ) ) ) = ( ( -u 1 ^ N ) x. ( ( seq M ( + , F ) ` N ) - ( ( -u 1 ^ N ) x. ( G ` ( N + 1 ) ) ) ) ) )
101 16 38 97 subdid 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( ( seq M ( + , F ) ` N ) - ( ( -u 1 ^ N ) x. ( G ` ( N + 1 ) ) ) ) ) = ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) - ( ( -u 1 ^ N ) x. ( ( -u 1 ^ N ) x. ( G ` ( N + 1 ) ) ) ) ) )
102 14 zcnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> N e. CC )
103 102 2timesd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( 2 x. N ) = ( N + N ) )
104 103 oveq2d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u 1 ^ ( 2 x. N ) ) = ( -u 1 ^ ( N + N ) ) )
105 2z 
 |-  2 e. ZZ
106 105 a1i 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> 2 e. ZZ )
107 expmulz 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( 2 e. ZZ /\ N e. ZZ ) ) -> ( -u 1 ^ ( 2 x. N ) ) = ( ( -u 1 ^ 2 ) ^ N ) )
108 45 10 106 14 107 syl22anc 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u 1 ^ ( 2 x. N ) ) = ( ( -u 1 ^ 2 ) ^ N ) )
109 104 108 eqtr3d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u 1 ^ ( N + N ) ) = ( ( -u 1 ^ 2 ) ^ N ) )
110 neg1sqe1 
 |-  ( -u 1 ^ 2 ) = 1
111 110 oveq1i 
 |-  ( ( -u 1 ^ 2 ) ^ N ) = ( 1 ^ N )
112 109 111 eqtrdi 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u 1 ^ ( N + N ) ) = ( 1 ^ N ) )
113 expaddz 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( N e. ZZ /\ N e. ZZ ) ) -> ( -u 1 ^ ( N + N ) ) = ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) )
114 45 10 14 14 113 syl22anc 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u 1 ^ ( N + N ) ) = ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) )
115 112 114 54 3eqtr3d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = 1 )
116 115 oveq1d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) x. ( G ` ( N + 1 ) ) ) = ( 1 x. ( G ` ( N + 1 ) ) ) )
117 16 16 91 mulassd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) x. ( G ` ( N + 1 ) ) ) = ( ( -u 1 ^ N ) x. ( ( -u 1 ^ N ) x. ( G ` ( N + 1 ) ) ) ) )
118 91 mulid2d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( 1 x. ( G ` ( N + 1 ) ) ) = ( G ` ( N + 1 ) ) )
119 116 117 118 3eqtr3d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( ( -u 1 ^ N ) x. ( G ` ( N + 1 ) ) ) ) = ( G ` ( N + 1 ) ) )
120 119 oveq2d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) - ( ( -u 1 ^ N ) x. ( ( -u 1 ^ N ) x. ( G ` ( N + 1 ) ) ) ) ) = ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) - ( G ` ( N + 1 ) ) ) )
121 100 101 120 3eqtrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + 1 ) ) ) = ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) - ( G ` ( N + 1 ) ) ) )
122 1 2 3 4 5 6 iseraltlem2 
 |-  ( ( ph /\ ( N + 1 ) e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ ( N + 1 ) ) x. ( seq M ( + , F ) ` ( ( N + 1 ) + ( 2 x. K ) ) ) ) <_ ( ( -u 1 ^ ( N + 1 ) ) x. ( seq M ( + , F ) ` ( N + 1 ) ) ) )
123 64 122 syl3an2 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ ( N + 1 ) ) x. ( seq M ( + , F ) ` ( ( N + 1 ) + ( 2 x. K ) ) ) ) <_ ( ( -u 1 ^ ( N + 1 ) ) x. ( seq M ( + , F ) ` ( N + 1 ) ) ) )
124 1cnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> 1 e. CC )
125 31 nn0cnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( 2 x. K ) e. CC )
126 102 124 125 add32d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( N + 1 ) + ( 2 x. K ) ) = ( ( N + ( 2 x. K ) ) + 1 ) )
127 126 fveq2d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( seq M ( + , F ) ` ( ( N + 1 ) + ( 2 x. K ) ) ) = ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) )
128 89 127 oveq12d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ ( N + 1 ) ) x. ( seq M ( + , F ) ` ( ( N + 1 ) + ( 2 x. K ) ) ) ) = ( -u ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) )
129 89 oveq1d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ ( N + 1 ) ) x. ( seq M ( + , F ) ` ( N + 1 ) ) ) = ( -u ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + 1 ) ) ) )
130 123 128 129 3brtr3d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) <_ ( -u ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + 1 ) ) ) )
131 70 recnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) e. CC )
132 16 131 mulneg1d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) = -u ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) )
133 26 65 ffvelrnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( seq M ( + , F ) ` ( N + 1 ) ) e. RR )
134 133 recnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( seq M ( + , F ) ` ( N + 1 ) ) e. CC )
135 16 134 mulneg1d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + 1 ) ) ) = -u ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + 1 ) ) ) )
136 130 132 135 3brtr3d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> -u ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) <_ -u ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + 1 ) ) ) )
137 15 133 remulcld 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + 1 ) ) ) e. RR )
138 137 71 lenegd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + 1 ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) <-> -u ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) <_ -u ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + 1 ) ) ) ) )
139 136 138 mpbird 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + 1 ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) )
140 121 139 eqbrtrrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) - ( G ` ( N + 1 ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) )
141 seqp1 
 |-  ( ( N + ( 2 x. K ) ) e. ( ZZ>= ` M ) -> ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) = ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) + ( F ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) )
142 33 141 syl 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) = ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) + ( F ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) )
143 fveq2 
 |-  ( k = ( ( N + ( 2 x. K ) ) + 1 ) -> ( F ` k ) = ( F ` ( ( N + ( 2 x. K ) ) + 1 ) ) )
144 oveq2 
 |-  ( k = ( ( N + ( 2 x. K ) ) + 1 ) -> ( -u 1 ^ k ) = ( -u 1 ^ ( ( N + ( 2 x. K ) ) + 1 ) ) )
145 fveq2 
 |-  ( k = ( ( N + ( 2 x. K ) ) + 1 ) -> ( G ` k ) = ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) )
146 144 145 oveq12d 
 |-  ( k = ( ( N + ( 2 x. K ) ) + 1 ) -> ( ( -u 1 ^ k ) x. ( G ` k ) ) = ( ( -u 1 ^ ( ( N + ( 2 x. K ) ) + 1 ) ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) )
147 143 146 eqeq12d 
 |-  ( k = ( ( N + ( 2 x. K ) ) + 1 ) -> ( ( F ` k ) = ( ( -u 1 ^ k ) x. ( G ` k ) ) <-> ( F ` ( ( N + ( 2 x. K ) ) + 1 ) ) = ( ( -u 1 ^ ( ( N + ( 2 x. K ) ) + 1 ) ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) ) )
148 147 81 69 rspcdva 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( F ` ( ( N + ( 2 x. K ) ) + 1 ) ) = ( ( -u 1 ^ ( ( N + ( 2 x. K ) ) + 1 ) ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) )
149 12 65 sseldi 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( N + 1 ) e. ZZ )
150 31 nn0zd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( 2 x. K ) e. ZZ )
151 expaddz 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( ( N + 1 ) e. ZZ /\ ( 2 x. K ) e. ZZ ) ) -> ( -u 1 ^ ( ( N + 1 ) + ( 2 x. K ) ) ) = ( ( -u 1 ^ ( N + 1 ) ) x. ( -u 1 ^ ( 2 x. K ) ) ) )
152 45 10 149 150 151 syl22anc 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u 1 ^ ( ( N + 1 ) + ( 2 x. K ) ) ) = ( ( -u 1 ^ ( N + 1 ) ) x. ( -u 1 ^ ( 2 x. K ) ) ) )
153 29 nn0zd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> K e. ZZ )
154 expmulz 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( 2 e. ZZ /\ K e. ZZ ) ) -> ( -u 1 ^ ( 2 x. K ) ) = ( ( -u 1 ^ 2 ) ^ K ) )
155 45 10 106 153 154 syl22anc 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u 1 ^ ( 2 x. K ) ) = ( ( -u 1 ^ 2 ) ^ K ) )
156 110 oveq1i 
 |-  ( ( -u 1 ^ 2 ) ^ K ) = ( 1 ^ K )
157 1exp 
 |-  ( K e. ZZ -> ( 1 ^ K ) = 1 )
158 153 157 syl 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( 1 ^ K ) = 1 )
159 156 158 syl5eq 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ 2 ) ^ K ) = 1 )
160 155 159 eqtrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u 1 ^ ( 2 x. K ) ) = 1 )
161 89 160 oveq12d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ ( N + 1 ) ) x. ( -u 1 ^ ( 2 x. K ) ) ) = ( -u ( -u 1 ^ N ) x. 1 ) )
162 152 161 eqtrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u 1 ^ ( ( N + 1 ) + ( 2 x. K ) ) ) = ( -u ( -u 1 ^ N ) x. 1 ) )
163 126 oveq2d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u 1 ^ ( ( N + 1 ) + ( 2 x. K ) ) ) = ( -u 1 ^ ( ( N + ( 2 x. K ) ) + 1 ) ) )
164 16 negcld 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> -u ( -u 1 ^ N ) e. CC )
165 164 mulid1d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u ( -u 1 ^ N ) x. 1 ) = -u ( -u 1 ^ N ) )
166 162 163 165 3eqtr3d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u 1 ^ ( ( N + ( 2 x. K ) ) + 1 ) ) = -u ( -u 1 ^ N ) )
167 166 oveq1d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ ( ( N + ( 2 x. K ) ) + 1 ) ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) = ( -u ( -u 1 ^ N ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) )
168 63 69 ffvelrnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) e. RR )
169 168 recnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) e. CC )
170 16 169 mulneg1d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( -u ( -u 1 ^ N ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) = -u ( ( -u 1 ^ N ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) )
171 148 167 170 3eqtrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( F ` ( ( N + ( 2 x. K ) ) + 1 ) ) = -u ( ( -u 1 ^ N ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) )
172 171 oveq2d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) + ( F ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) = ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) + -u ( ( -u 1 ^ N ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) ) )
173 15 168 remulcld 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) e. RR )
174 173 recnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) e. CC )
175 36 174 negsubd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) + -u ( ( -u 1 ^ N ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) ) = ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( ( -u 1 ^ N ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) ) )
176 142 172 175 3eqtrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) = ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( ( -u 1 ^ N ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) ) )
177 176 oveq2d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) = ( ( -u 1 ^ N ) x. ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( ( -u 1 ^ N ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) ) ) )
178 16 36 174 subdid 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( ( -u 1 ^ N ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) ) ) = ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) - ( ( -u 1 ^ N ) x. ( ( -u 1 ^ N ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) ) ) )
179 115 oveq1d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) = ( 1 x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) )
180 16 16 169 mulassd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) = ( ( -u 1 ^ N ) x. ( ( -u 1 ^ N ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) ) )
181 169 mulid2d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( 1 x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) = ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) )
182 179 180 181 3eqtr3d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( ( -u 1 ^ N ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) ) = ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) )
183 182 oveq2d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) - ( ( -u 1 ^ N ) x. ( ( -u 1 ^ N ) x. ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) ) ) = ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) - ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) )
184 177 178 183 3eqtrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) = ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) - ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) )
185 simp1 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ph )
186 1 2 3 4 5 iseraltlem1 
 |-  ( ( ph /\ ( ( N + ( 2 x. K ) ) + 1 ) e. Z ) -> 0 <_ ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) )
187 185 69 186 syl2anc 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> 0 <_ ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) )
188 72 168 subge02d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( 0 <_ ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) <-> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) - ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) ) )
189 187 188 mpbid 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) - ( G ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) )
190 184 189 eqbrtrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) )
191 67 71 72 140 190 letrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) - ( G ` ( N + 1 ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) )
192 62 66 readdcld 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) + ( G ` ( N + 1 ) ) ) e. RR )
193 1 2 3 4 5 6 iseraltlem2 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) )
194 1 2 3 4 5 iseraltlem1 
 |-  ( ( ph /\ ( N + 1 ) e. Z ) -> 0 <_ ( G ` ( N + 1 ) ) )
195 185 65 194 syl2anc 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> 0 <_ ( G ` ( N + 1 ) ) )
196 62 66 addge01d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( 0 <_ ( G ` ( N + 1 ) ) <-> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) <_ ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) + ( G ` ( N + 1 ) ) ) ) )
197 195 196 mpbid 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) <_ ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) + ( G ` ( N + 1 ) ) ) )
198 72 62 192 193 197 letrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) <_ ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) + ( G ` ( N + 1 ) ) ) )
199 72 62 66 absdifled 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( abs ` ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) - ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) ) <_ ( G ` ( N + 1 ) ) <-> ( ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) - ( G ` ( N + 1 ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) /\ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) <_ ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) + ( G ` ( N + 1 ) ) ) ) ) )
200 191 198 199 mpbir2and 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) - ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) ) <_ ( G ` ( N + 1 ) ) )
201 61 200 eqbrtrrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) ) <_ ( G ` ( N + 1 ) ) )
202 16 131 38 subdid 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) ) = ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) - ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) )
203 202 fveq2d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( ( -u 1 ^ N ) x. ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) ) ) = ( abs ` ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) - ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) ) )
204 70 37 resubcld 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) e. RR )
205 204 recnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) e. CC )
206 16 205 absmuld 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( ( -u 1 ^ N ) x. ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) ) ) = ( ( abs ` ( -u 1 ^ N ) ) x. ( abs ` ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) ) ) )
207 203 206 eqtr3d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) - ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) ) = ( ( abs ` ( -u 1 ^ N ) ) x. ( abs ` ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) ) ) )
208 56 oveq1d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( abs ` ( -u 1 ^ N ) ) x. ( abs ` ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) ) ) = ( 1 x. ( abs ` ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) ) ) )
209 205 abscld 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) ) e. RR )
210 209 recnd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) ) e. CC )
211 210 mulid2d 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( 1 x. ( abs ` ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) ) ) = ( abs ` ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) ) )
212 207 208 211 3eqtrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) - ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) ) = ( abs ` ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) ) )
213 71 72 192 190 198 letrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) <_ ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) + ( G ` ( N + 1 ) ) ) )
214 71 62 66 absdifled 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( abs ` ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) - ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) ) <_ ( G ` ( N + 1 ) ) <-> ( ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) - ( G ` ( N + 1 ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) /\ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) <_ ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) + ( G ` ( N + 1 ) ) ) ) ) )
215 140 213 214 mpbir2and 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) ) - ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) ) <_ ( G ` ( N + 1 ) ) )
216 212 215 eqbrtrrd 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( abs ` ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) ) <_ ( G ` ( N + 1 ) ) )
217 201 216 jca 
 |-  ( ( ph /\ N e. Z /\ K e. NN0 ) -> ( ( abs ` ( ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) - ( seq M ( + , F ) ` N ) ) ) <_ ( G ` ( N + 1 ) ) /\ ( abs ` ( ( seq M ( + , F ) ` ( ( N + ( 2 x. K ) ) + 1 ) ) - ( seq M ( + , F ) ` N ) ) ) <_ ( G ` ( N + 1 ) ) ) )