Metamath Proof Explorer

Theorem iseraltlem2

Description: Lemma for iseralt . The terms of an alternating series form a chain of inequalities in alternate terms, so that for example S ( 1 ) <_ S ( 3 ) <_ S ( 5 ) <_ ... and ... <_ S ( 4 ) <_ S ( 2 ) <_ S ( 0 ) (assuming M = 0 so that these terms are defined). (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 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 ) ) )

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 oveq2 
 |-  ( x = 0 -> ( 2 x. x ) = ( 2 x. 0 ) )
8 2t0e0 
 |-  ( 2 x. 0 ) = 0
9 7 8 eqtrdi 
 |-  ( x = 0 -> ( 2 x. x ) = 0 )
10 9 oveq2d 
 |-  ( x = 0 -> ( N + ( 2 x. x ) ) = ( N + 0 ) )
11 10 fveq2d 
 |-  ( x = 0 -> ( seq M ( + , F ) ` ( N + ( 2 x. x ) ) ) = ( seq M ( + , F ) ` ( N + 0 ) ) )
12 11 oveq2d 
 |-  ( x = 0 -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. x ) ) ) ) = ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + 0 ) ) ) )
13 12 breq1d 
 |-  ( x = 0 -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. x ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) <-> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + 0 ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) )
14 13 imbi2d 
 |-  ( x = 0 -> ( ( ( ph /\ N e. Z ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. x ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) <-> ( ( ph /\ N e. Z ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + 0 ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) ) )
15 oveq2 
 |-  ( x = n -> ( 2 x. x ) = ( 2 x. n ) )
16 15 oveq2d 
 |-  ( x = n -> ( N + ( 2 x. x ) ) = ( N + ( 2 x. n ) ) )
17 16 fveq2d 
 |-  ( x = n -> ( seq M ( + , F ) ` ( N + ( 2 x. x ) ) ) = ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) )
18 17 oveq2d 
 |-  ( x = n -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. x ) ) ) ) = ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) )
19 18 breq1d 
 |-  ( x = n -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. x ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) <-> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) )
20 19 imbi2d 
 |-  ( x = n -> ( ( ( ph /\ N e. Z ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. x ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) <-> ( ( ph /\ N e. Z ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) ) )
21 oveq2 
 |-  ( x = ( n + 1 ) -> ( 2 x. x ) = ( 2 x. ( n + 1 ) ) )
22 21 oveq2d 
 |-  ( x = ( n + 1 ) -> ( N + ( 2 x. x ) ) = ( N + ( 2 x. ( n + 1 ) ) ) )
23 22 fveq2d 
 |-  ( x = ( n + 1 ) -> ( seq M ( + , F ) ` ( N + ( 2 x. x ) ) ) = ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) )
24 23 oveq2d 
 |-  ( x = ( n + 1 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. x ) ) ) ) = ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) ) )
25 24 breq1d 
 |-  ( x = ( n + 1 ) -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. x ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) <-> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) )
26 25 imbi2d 
 |-  ( x = ( n + 1 ) -> ( ( ( ph /\ N e. Z ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. x ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) <-> ( ( ph /\ N e. Z ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) ) )
27 oveq2 
 |-  ( x = K -> ( 2 x. x ) = ( 2 x. K ) )
28 27 oveq2d 
 |-  ( x = K -> ( N + ( 2 x. x ) ) = ( N + ( 2 x. K ) ) )
29 28 fveq2d 
 |-  ( x = K -> ( seq M ( + , F ) ` ( N + ( 2 x. x ) ) ) = ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) )
30 29 oveq2d 
 |-  ( x = K -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. x ) ) ) ) = ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) )
31 30 breq1d 
 |-  ( x = K -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. x ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) <-> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) )
32 31 imbi2d 
 |-  ( x = K -> ( ( ( ph /\ N e. Z ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. x ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) <-> ( ( ph /\ N e. Z ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) ) )
33 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
34 1 33 eqsstri 
 |-  Z C_ ZZ
35 34 a1i 
 |-  ( ph -> Z C_ ZZ )
36 35 sselda 
 |-  ( ( ph /\ N e. Z ) -> N e. ZZ )
37 36 zcnd 
 |-  ( ( ph /\ N e. Z ) -> N e. CC )
38 37 addid1d 
 |-  ( ( ph /\ N e. Z ) -> ( N + 0 ) = N )
39 38 fveq2d 
 |-  ( ( ph /\ N e. Z ) -> ( seq M ( + , F ) ` ( N + 0 ) ) = ( seq M ( + , F ) ` N ) )
40 39 oveq2d 
 |-  ( ( ph /\ N e. Z ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + 0 ) ) ) = ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) )
41 neg1rr 
 |-  -u 1 e. RR
42 neg1ne0 
 |-  -u 1 =/= 0
43 reexpclz 
 |-  ( ( -u 1 e. RR /\ -u 1 =/= 0 /\ N e. ZZ ) -> ( -u 1 ^ N ) e. RR )
44 41 42 36 43 mp3an12i 
 |-  ( ( ph /\ N e. Z ) -> ( -u 1 ^ N ) e. RR )
45 35 sselda 
 |-  ( ( ph /\ k e. Z ) -> k e. ZZ )
46 reexpclz 
 |-  ( ( -u 1 e. RR /\ -u 1 =/= 0 /\ k e. ZZ ) -> ( -u 1 ^ k ) e. RR )
47 41 42 45 46 mp3an12i 
 |-  ( ( ph /\ k e. Z ) -> ( -u 1 ^ k ) e. RR )
48 3 ffvelrnda 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )
49 47 48 remulcld 
 |-  ( ( ph /\ k e. Z ) -> ( ( -u 1 ^ k ) x. ( G ` k ) ) e. RR )
50 6 49 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
51 1 2 50 serfre 
 |-  ( ph -> seq M ( + , F ) : Z --> RR )
52 51 ffvelrnda 
 |-  ( ( ph /\ N e. Z ) -> ( seq M ( + , F ) ` N ) e. RR )
53 44 52 remulcld 
 |-  ( ( ph /\ N e. Z ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) e. RR )
54 53 leidd 
 |-  ( ( ph /\ N e. Z ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) )
55 40 54 eqbrtrd 
 |-  ( ( ph /\ N e. Z ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + 0 ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) )
56 3 ad2antrr 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> G : Z --> RR )
57 ax-1cn 
 |-  1 e. CC
58 57 2timesi 
 |-  ( 2 x. 1 ) = ( 1 + 1 )
59 58 oveq2i 
 |-  ( ( N + ( 2 x. n ) ) + ( 2 x. 1 ) ) = ( ( N + ( 2 x. n ) ) + ( 1 + 1 ) )
60 simpr 
 |-  ( ( ph /\ N e. Z ) -> N e. Z )
61 60 1 eleqtrdi 
 |-  ( ( ph /\ N e. Z ) -> N e. ( ZZ>= ` M ) )
62 61 adantr 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> N e. ( ZZ>= ` M ) )
63 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
64 62 63 syl 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> N e. ZZ )
65 64 zcnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> N e. CC )
66 2cn 
 |-  2 e. CC
67 nn0cn 
 |-  ( n e. NN0 -> n e. CC )
68 67 adantl 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> n e. CC )
69 mulcl 
 |-  ( ( 2 e. CC /\ n e. CC ) -> ( 2 x. n ) e. CC )
70 66 68 69 sylancr 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( 2 x. n ) e. CC )
71 66 57 mulcli 
 |-  ( 2 x. 1 ) e. CC
72 71 a1i 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( 2 x. 1 ) e. CC )
73 65 70 72 addassd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( N + ( 2 x. n ) ) + ( 2 x. 1 ) ) = ( N + ( ( 2 x. n ) + ( 2 x. 1 ) ) ) )
74 59 73 eqtr3id 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( N + ( 2 x. n ) ) + ( 1 + 1 ) ) = ( N + ( ( 2 x. n ) + ( 2 x. 1 ) ) ) )
75 2nn0 
 |-  2 e. NN0
76 simpr 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> n e. NN0 )
77 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ n e. NN0 ) -> ( 2 x. n ) e. NN0 )
78 75 76 77 sylancr 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( 2 x. n ) e. NN0 )
79 uzaddcl 
 |-  ( ( N e. ( ZZ>= ` M ) /\ ( 2 x. n ) e. NN0 ) -> ( N + ( 2 x. n ) ) e. ( ZZ>= ` M ) )
80 62 78 79 syl2anc 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( N + ( 2 x. n ) ) e. ( ZZ>= ` M ) )
81 33 80 sselid 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( N + ( 2 x. n ) ) e. ZZ )
82 81 zcnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( N + ( 2 x. n ) ) e. CC )
83 1cnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> 1 e. CC )
84 82 83 83 addassd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) = ( ( N + ( 2 x. n ) ) + ( 1 + 1 ) ) )
85 2cnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> 2 e. CC )
86 85 68 83 adddid 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( 2 x. ( n + 1 ) ) = ( ( 2 x. n ) + ( 2 x. 1 ) ) )
87 86 oveq2d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( N + ( 2 x. ( n + 1 ) ) ) = ( N + ( ( 2 x. n ) + ( 2 x. 1 ) ) ) )
88 74 84 87 3eqtr4d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) = ( N + ( 2 x. ( n + 1 ) ) ) )
89 peano2nn0 
 |-  ( n e. NN0 -> ( n + 1 ) e. NN0 )
90 89 adantl 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( n + 1 ) e. NN0 )
91 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ ( n + 1 ) e. NN0 ) -> ( 2 x. ( n + 1 ) ) e. NN0 )
92 75 90 91 sylancr 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( 2 x. ( n + 1 ) ) e. NN0 )
93 uzaddcl 
 |-  ( ( N e. ( ZZ>= ` M ) /\ ( 2 x. ( n + 1 ) ) e. NN0 ) -> ( N + ( 2 x. ( n + 1 ) ) ) e. ( ZZ>= ` M ) )
94 62 92 93 syl2anc 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( N + ( 2 x. ( n + 1 ) ) ) e. ( ZZ>= ` M ) )
95 94 1 eleqtrrdi 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( N + ( 2 x. ( n + 1 ) ) ) e. Z )
96 88 95 eqeltrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) e. Z )
97 56 96 ffvelrnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) e. RR )
98 peano2uz 
 |-  ( ( N + ( 2 x. n ) ) e. ( ZZ>= ` M ) -> ( ( N + ( 2 x. n ) ) + 1 ) e. ( ZZ>= ` M ) )
99 80 98 syl 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( N + ( 2 x. n ) ) + 1 ) e. ( ZZ>= ` M ) )
100 99 1 eleqtrrdi 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( N + ( 2 x. n ) ) + 1 ) e. Z )
101 56 100 ffvelrnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) e. RR )
102 97 101 resubcld 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) - ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) e. RR )
103 0red 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> 0 e. RR )
104 44 adantr 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u 1 ^ N ) e. RR )
105 51 ad2antrr 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> seq M ( + , F ) : Z --> RR )
106 80 1 eleqtrrdi 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( N + ( 2 x. n ) ) e. Z )
107 105 106 ffvelrnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) e. RR )
108 104 107 remulcld 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) e. RR )
109 fvoveq1 
 |-  ( k = ( ( N + ( 2 x. n ) ) + 1 ) -> ( G ` ( k + 1 ) ) = ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) )
110 fveq2 
 |-  ( k = ( ( N + ( 2 x. n ) ) + 1 ) -> ( G ` k ) = ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) )
111 109 110 breq12d 
 |-  ( k = ( ( N + ( 2 x. n ) ) + 1 ) -> ( ( G ` ( k + 1 ) ) <_ ( G ` k ) <-> ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) <_ ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) )
112 4 ralrimiva 
 |-  ( ph -> A. k e. Z ( G ` ( k + 1 ) ) <_ ( G ` k ) )
113 112 ad2antrr 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> A. k e. Z ( G ` ( k + 1 ) ) <_ ( G ` k ) )
114 111 113 100 rspcdva 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) <_ ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) )
115 97 101 suble0d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) - ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) <_ 0 <-> ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) <_ ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) )
116 114 115 mpbird 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) - ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) <_ 0 )
117 102 103 108 116 leadd2dd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) + ( ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) - ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) ) <_ ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) + 0 ) )
118 seqp1 
 |-  ( ( ( N + ( 2 x. n ) ) + 1 ) e. ( ZZ>= ` M ) -> ( seq M ( + , F ) ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) = ( ( seq M ( + , F ) ` ( ( N + ( 2 x. n ) ) + 1 ) ) + ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) )
119 99 118 syl 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( seq M ( + , F ) ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) = ( ( seq M ( + , F ) ` ( ( N + ( 2 x. n ) ) + 1 ) ) + ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) )
120 seqp1 
 |-  ( ( N + ( 2 x. n ) ) e. ( ZZ>= ` M ) -> ( seq M ( + , F ) ` ( ( N + ( 2 x. n ) ) + 1 ) ) = ( ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) + ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) )
121 80 120 syl 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( seq M ( + , F ) ` ( ( N + ( 2 x. n ) ) + 1 ) ) = ( ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) + ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) )
122 121 oveq1d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( seq M ( + , F ) ` ( ( N + ( 2 x. n ) ) + 1 ) ) + ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) = ( ( ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) + ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) + ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) )
123 119 122 eqtrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( seq M ( + , F ) ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) = ( ( ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) + ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) + ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) )
124 88 fveq2d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( seq M ( + , F ) ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) = ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) )
125 107 recnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) e. CC )
126 fveq2 
 |-  ( k = ( ( N + ( 2 x. n ) ) + 1 ) -> ( F ` k ) = ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) )
127 oveq2 
 |-  ( k = ( ( N + ( 2 x. n ) ) + 1 ) -> ( -u 1 ^ k ) = ( -u 1 ^ ( ( N + ( 2 x. n ) ) + 1 ) ) )
128 127 110 oveq12d 
 |-  ( k = ( ( N + ( 2 x. n ) ) + 1 ) -> ( ( -u 1 ^ k ) x. ( G ` k ) ) = ( ( -u 1 ^ ( ( N + ( 2 x. n ) ) + 1 ) ) x. ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) )
129 126 128 eqeq12d 
 |-  ( k = ( ( N + ( 2 x. n ) ) + 1 ) -> ( ( F ` k ) = ( ( -u 1 ^ k ) x. ( G ` k ) ) <-> ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) = ( ( -u 1 ^ ( ( N + ( 2 x. n ) ) + 1 ) ) x. ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) ) )
130 6 ralrimiva 
 |-  ( ph -> A. k e. Z ( F ` k ) = ( ( -u 1 ^ k ) x. ( G ` k ) ) )
131 130 ad2antrr 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> A. k e. Z ( F ` k ) = ( ( -u 1 ^ k ) x. ( G ` k ) ) )
132 129 131 100 rspcdva 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) = ( ( -u 1 ^ ( ( N + ( 2 x. n ) ) + 1 ) ) x. ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) )
133 neg1cn 
 |-  -u 1 e. CC
134 133 a1i 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> -u 1 e. CC )
135 42 a1i 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> -u 1 =/= 0 )
136 134 135 81 expp1zd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u 1 ^ ( ( N + ( 2 x. n ) ) + 1 ) ) = ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. -u 1 ) )
137 41 a1i 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> -u 1 e. RR )
138 137 135 81 reexpclzd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u 1 ^ ( N + ( 2 x. n ) ) ) e. RR )
139 138 recnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u 1 ^ ( N + ( 2 x. n ) ) ) e. CC )
140 mulcom 
 |-  ( ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) e. CC /\ -u 1 e. CC ) -> ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. -u 1 ) = ( -u 1 x. ( -u 1 ^ ( N + ( 2 x. n ) ) ) ) )
141 139 133 140 sylancl 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. -u 1 ) = ( -u 1 x. ( -u 1 ^ ( N + ( 2 x. n ) ) ) ) )
142 139 mulm1d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u 1 x. ( -u 1 ^ ( N + ( 2 x. n ) ) ) ) = -u ( -u 1 ^ ( N + ( 2 x. n ) ) ) )
143 136 141 142 3eqtrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u 1 ^ ( ( N + ( 2 x. n ) ) + 1 ) ) = -u ( -u 1 ^ ( N + ( 2 x. n ) ) ) )
144 143 oveq1d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ ( ( N + ( 2 x. n ) ) + 1 ) ) x. ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) = ( -u ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) )
145 101 recnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) e. CC )
146 mulneg12 
 |-  ( ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) e. CC /\ ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) e. CC ) -> ( -u ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) = ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) )
147 139 145 146 syl2anc 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) = ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) )
148 132 144 147 3eqtrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) = ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) )
149 101 renegcld 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) e. RR )
150 138 149 remulcld 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) e. RR )
151 148 150 eqeltrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) e. RR )
152 151 recnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) e. CC )
153 fveq2 
 |-  ( k = ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) -> ( F ` k ) = ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) )
154 oveq2 
 |-  ( k = ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) -> ( -u 1 ^ k ) = ( -u 1 ^ ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) )
155 fveq2 
 |-  ( k = ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) -> ( G ` k ) = ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) )
156 154 155 oveq12d 
 |-  ( k = ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) -> ( ( -u 1 ^ k ) x. ( G ` k ) ) = ( ( -u 1 ^ ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) x. ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) )
157 153 156 eqeq12d 
 |-  ( k = ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) -> ( ( F ` k ) = ( ( -u 1 ^ k ) x. ( G ` k ) ) <-> ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) = ( ( -u 1 ^ ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) x. ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) ) )
158 157 131 96 rspcdva 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) = ( ( -u 1 ^ ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) x. ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) )
159 81 peano2zd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( N + ( 2 x. n ) ) + 1 ) e. ZZ )
160 134 135 159 expp1zd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u 1 ^ ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) = ( ( -u 1 ^ ( ( N + ( 2 x. n ) ) + 1 ) ) x. -u 1 ) )
161 143 oveq1d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ ( ( N + ( 2 x. n ) ) + 1 ) ) x. -u 1 ) = ( -u ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. -u 1 ) )
162 mul2neg 
 |-  ( ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) e. CC /\ 1 e. CC ) -> ( -u ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. -u 1 ) = ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. 1 ) )
163 139 57 162 sylancl 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. -u 1 ) = ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. 1 ) )
164 139 mulid1d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. 1 ) = ( -u 1 ^ ( N + ( 2 x. n ) ) ) )
165 163 164 eqtrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. -u 1 ) = ( -u 1 ^ ( N + ( 2 x. n ) ) ) )
166 160 161 165 3eqtrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u 1 ^ ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) = ( -u 1 ^ ( N + ( 2 x. n ) ) ) )
167 166 oveq1d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) x. ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) = ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) )
168 158 167 eqtrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) = ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) )
169 138 97 remulcld 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) e. RR )
170 168 169 eqeltrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) e. RR )
171 170 recnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) e. CC )
172 125 152 171 addassd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) + ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) + ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) = ( ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) + ( ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) + ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) ) )
173 123 124 172 3eqtr3d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) = ( ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) + ( ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) + ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) ) )
174 173 oveq2d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) ) = ( ( -u 1 ^ N ) x. ( ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) + ( ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) + ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) ) ) )
175 104 recnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u 1 ^ N ) e. CC )
176 151 170 readdcld 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) + ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) e. RR )
177 176 recnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) + ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) e. CC )
178 175 125 177 adddid 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ N ) x. ( ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) + ( ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) + ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) ) ) = ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) + ( ( -u 1 ^ N ) x. ( ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) + ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) ) ) )
179 175 152 171 adddid 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ N ) x. ( ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) + ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) ) = ( ( ( -u 1 ^ N ) x. ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) + ( ( -u 1 ^ N ) x. ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) ) )
180 148 oveq2d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ N ) x. ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) = ( ( -u 1 ^ N ) x. ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) ) )
181 149 recnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) e. CC )
182 175 139 181 mulassd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( -u 1 ^ ( N + ( 2 x. n ) ) ) ) x. -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) = ( ( -u 1 ^ N ) x. ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) ) )
183 180 182 eqtr4d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ N ) x. ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) = ( ( ( -u 1 ^ N ) x. ( -u 1 ^ ( N + ( 2 x. n ) ) ) ) x. -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) )
184 85 65 68 adddid 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( 2 x. ( N + n ) ) = ( ( 2 x. N ) + ( 2 x. n ) ) )
185 65 2timesd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( 2 x. N ) = ( N + N ) )
186 185 oveq1d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( 2 x. N ) + ( 2 x. n ) ) = ( ( N + N ) + ( 2 x. n ) ) )
187 65 65 70 addassd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( N + N ) + ( 2 x. n ) ) = ( N + ( N + ( 2 x. n ) ) ) )
188 184 186 187 3eqtrrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( N + ( N + ( 2 x. n ) ) ) = ( 2 x. ( N + n ) ) )
189 188 oveq2d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u 1 ^ ( N + ( N + ( 2 x. n ) ) ) ) = ( -u 1 ^ ( 2 x. ( N + n ) ) ) )
190 expaddz 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( N e. ZZ /\ ( N + ( 2 x. n ) ) e. ZZ ) ) -> ( -u 1 ^ ( N + ( N + ( 2 x. n ) ) ) ) = ( ( -u 1 ^ N ) x. ( -u 1 ^ ( N + ( 2 x. n ) ) ) ) )
191 134 135 64 81 190 syl22anc 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u 1 ^ ( N + ( N + ( 2 x. n ) ) ) ) = ( ( -u 1 ^ N ) x. ( -u 1 ^ ( N + ( 2 x. n ) ) ) ) )
192 2z 
 |-  2 e. ZZ
193 192 a1i 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> 2 e. ZZ )
194 nn0z 
 |-  ( n e. NN0 -> n e. ZZ )
195 zaddcl 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> ( N + n ) e. ZZ )
196 36 194 195 syl2an 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( N + n ) e. ZZ )
197 expmulz 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( 2 e. ZZ /\ ( N + n ) e. ZZ ) ) -> ( -u 1 ^ ( 2 x. ( N + n ) ) ) = ( ( -u 1 ^ 2 ) ^ ( N + n ) ) )
198 134 135 193 196 197 syl22anc 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u 1 ^ ( 2 x. ( N + n ) ) ) = ( ( -u 1 ^ 2 ) ^ ( N + n ) ) )
199 neg1sqe1 
 |-  ( -u 1 ^ 2 ) = 1
200 199 oveq1i 
 |-  ( ( -u 1 ^ 2 ) ^ ( N + n ) ) = ( 1 ^ ( N + n ) )
201 1exp 
 |-  ( ( N + n ) e. ZZ -> ( 1 ^ ( N + n ) ) = 1 )
202 196 201 syl 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( 1 ^ ( N + n ) ) = 1 )
203 200 202 eqtrid 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ 2 ) ^ ( N + n ) ) = 1 )
204 198 203 eqtrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u 1 ^ ( 2 x. ( N + n ) ) ) = 1 )
205 189 191 204 3eqtr3d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ N ) x. ( -u 1 ^ ( N + ( 2 x. n ) ) ) ) = 1 )
206 205 oveq1d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( -u 1 ^ ( N + ( 2 x. n ) ) ) ) x. -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) = ( 1 x. -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) )
207 181 mulid2d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( 1 x. -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) = -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) )
208 183 206 207 3eqtrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ N ) x. ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) = -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) )
209 168 oveq2d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ N ) x. ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) = ( ( -u 1 ^ N ) x. ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) ) )
210 97 recnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) e. CC )
211 175 139 210 mulassd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( -u 1 ^ ( N + ( 2 x. n ) ) ) ) x. ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) = ( ( -u 1 ^ N ) x. ( ( -u 1 ^ ( N + ( 2 x. n ) ) ) x. ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) ) )
212 209 211 eqtr4d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ N ) x. ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) = ( ( ( -u 1 ^ N ) x. ( -u 1 ^ ( N + ( 2 x. n ) ) ) ) x. ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) )
213 205 oveq1d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( -u 1 ^ ( N + ( 2 x. n ) ) ) ) x. ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) = ( 1 x. ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) )
214 210 mulid2d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( 1 x. ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) = ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) )
215 212 213 214 3eqtrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ N ) x. ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) = ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) )
216 208 215 oveq12d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) + ( ( -u 1 ^ N ) x. ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) ) = ( -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) + ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) )
217 145 negcld 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) e. CC )
218 217 210 addcomd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) + ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) = ( ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) + -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) )
219 210 145 negsubd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) + -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) = ( ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) - ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) )
220 218 219 eqtrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( -u ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) + ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) = ( ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) - ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) )
221 179 216 220 3eqtrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ N ) x. ( ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) + ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) ) = ( ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) - ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) )
222 221 oveq2d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) + ( ( -u 1 ^ N ) x. ( ( F ` ( ( N + ( 2 x. n ) ) + 1 ) ) + ( F ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) ) ) ) = ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) + ( ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) - ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) ) )
223 174 178 222 3eqtrrd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) + ( ( G ` ( ( ( N + ( 2 x. n ) ) + 1 ) + 1 ) ) - ( G ` ( ( N + ( 2 x. n ) ) + 1 ) ) ) ) = ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) ) )
224 108 recnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) e. CC )
225 224 addid1d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) + 0 ) = ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) )
226 117 223 225 3brtr3d 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) )
227 105 95 ffvelrnd 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) e. RR )
228 104 227 remulcld 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) ) e. RR )
229 53 adantr 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) e. RR )
230 letr 
 |-  ( ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) ) e. RR /\ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) e. RR /\ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) e. RR ) -> ( ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) /\ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) )
231 228 108 229 230 syl3anc 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) /\ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) )
232 226 231 mpand 
 |-  ( ( ( ph /\ N e. Z ) /\ n e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) )
233 232 expcom 
 |-  ( n e. NN0 -> ( ( ph /\ N e. Z ) -> ( ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) ) )
234 233 a2d 
 |-  ( n e. NN0 -> ( ( ( ph /\ N e. Z ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. n ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) -> ( ( ph /\ N e. Z ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. ( n + 1 ) ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) ) )
235 14 20 26 32 55 234 nn0ind 
 |-  ( K e. NN0 -> ( ( ph /\ N e. Z ) -> ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` ( N + ( 2 x. K ) ) ) ) <_ ( ( -u 1 ^ N ) x. ( seq M ( + , F ) ` N ) ) ) )
236 235 com12 
 |-  ( ( 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 ) ) ) )
237 236 3impia 
 |-  ( ( 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 ) ) )