Metamath Proof Explorer

Theorem isercoll

Description: Rearrange an infinite series by spacing out the terms using an order isomorphism. (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses isercoll.z 
|- Z = ( ZZ>= ` M )
isercoll.m 
|- ( ph -> M e. ZZ )
isercoll.g 
|- ( ph -> G : NN --> Z )
isercoll.i 
|- ( ( ph /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )
isercoll.0 
|- ( ( ph /\ n e. ( Z \ ran G ) ) -> ( F ` n ) = 0 )
isercoll.f 
|- ( ( ph /\ n e. Z ) -> ( F ` n ) e. CC )
isercoll.h 
|- ( ( ph /\ k e. NN ) -> ( H ` k ) = ( F ` ( G ` k ) ) )
Assertion isercoll 
|- ( ph -> ( seq 1 ( + , H ) ~~> A <-> seq M ( + , F ) ~~> A ) )

Proof

Step Hyp Ref Expression
1 isercoll.z 
 |-  Z = ( ZZ>= ` M )
2 isercoll.m 
 |-  ( ph -> M e. ZZ )
3 isercoll.g 
 |-  ( ph -> G : NN --> Z )
4 isercoll.i 
 |-  ( ( ph /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )
5 isercoll.0 
 |-  ( ( ph /\ n e. ( Z \ ran G ) ) -> ( F ` n ) = 0 )
6 isercoll.f 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. CC )
7 isercoll.h 
 |-  ( ( ph /\ k e. NN ) -> ( H ` k ) = ( F ` ( G ` k ) ) )
8 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
9 1 8 eqsstri 
 |-  Z C_ ZZ
10 3 ffvelrnda 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) e. Z )
11 9 10 sselid 
 |-  ( ( ph /\ n e. NN ) -> ( G ` n ) e. ZZ )
12 nnz 
 |-  ( n e. NN -> n e. ZZ )
13 12 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> n e. ZZ )
14 fzfid 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( M ... m ) e. Fin )
15 ffun 
 |-  ( G : NN --> Z -> Fun G )
16 funimacnv 
 |-  ( Fun G -> ( G " ( `' G " ( M ... m ) ) ) = ( ( M ... m ) i^i ran G ) )
17 3 15 16 3syl 
 |-  ( ph -> ( G " ( `' G " ( M ... m ) ) ) = ( ( M ... m ) i^i ran G ) )
18 inss1 
 |-  ( ( M ... m ) i^i ran G ) C_ ( M ... m )
19 17 18 eqsstrdi 
 |-  ( ph -> ( G " ( `' G " ( M ... m ) ) ) C_ ( M ... m ) )
20 19 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( G " ( `' G " ( M ... m ) ) ) C_ ( M ... m ) )
21 14 20 ssfid 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( G " ( `' G " ( M ... m ) ) ) e. Fin )
22 hashcl 
 |-  ( ( G " ( `' G " ( M ... m ) ) ) e. Fin -> ( # ` ( G " ( `' G " ( M ... m ) ) ) ) e. NN0 )
23 nn0z 
 |-  ( ( # ` ( G " ( `' G " ( M ... m ) ) ) ) e. NN0 -> ( # ` ( G " ( `' G " ( M ... m ) ) ) ) e. ZZ )
24 21 22 23 3syl 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( # ` ( G " ( `' G " ( M ... m ) ) ) ) e. ZZ )
25 ssid 
 |-  NN C_ NN
26 1 2 3 4 isercolllem1 
 |-  ( ( ph /\ NN C_ NN ) -> ( G |` NN ) Isom < , < ( NN , ( G " NN ) ) )
27 25 26 mpan2 
 |-  ( ph -> ( G |` NN ) Isom < , < ( NN , ( G " NN ) ) )
28 ffn 
 |-  ( G : NN --> Z -> G Fn NN )
29 fnresdm 
 |-  ( G Fn NN -> ( G |` NN ) = G )
30 isoeq1 
 |-  ( ( G |` NN ) = G -> ( ( G |` NN ) Isom < , < ( NN , ( G " NN ) ) <-> G Isom < , < ( NN , ( G " NN ) ) ) )
31 3 28 29 30 4syl 
 |-  ( ph -> ( ( G |` NN ) Isom < , < ( NN , ( G " NN ) ) <-> G Isom < , < ( NN , ( G " NN ) ) ) )
32 27 31 mpbid 
 |-  ( ph -> G Isom < , < ( NN , ( G " NN ) ) )
33 isof1o 
 |-  ( G Isom < , < ( NN , ( G " NN ) ) -> G : NN -1-1-onto-> ( G " NN ) )
34 f1ocnv 
 |-  ( G : NN -1-1-onto-> ( G " NN ) -> `' G : ( G " NN ) -1-1-onto-> NN )
35 f1ofun 
 |-  ( `' G : ( G " NN ) -1-1-onto-> NN -> Fun `' G )
36 32 33 34 35 4syl 
 |-  ( ph -> Fun `' G )
37 df-f1 
 |-  ( G : NN -1-1-> Z <-> ( G : NN --> Z /\ Fun `' G ) )
38 3 36 37 sylanbrc 
 |-  ( ph -> G : NN -1-1-> Z )
39 38 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> G : NN -1-1-> Z )
40 fz1ssnn 
 |-  ( 1 ... n ) C_ NN
41 ovex 
 |-  ( 1 ... n ) e. _V
42 41 f1imaen 
 |-  ( ( G : NN -1-1-> Z /\ ( 1 ... n ) C_ NN ) -> ( G " ( 1 ... n ) ) ~~ ( 1 ... n ) )
43 39 40 42 sylancl 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( G " ( 1 ... n ) ) ~~ ( 1 ... n ) )
44 fzfid 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( 1 ... n ) e. Fin )
45 enfii 
 |-  ( ( ( 1 ... n ) e. Fin /\ ( G " ( 1 ... n ) ) ~~ ( 1 ... n ) ) -> ( G " ( 1 ... n ) ) e. Fin )
46 44 43 45 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( G " ( 1 ... n ) ) e. Fin )
47 hashen 
 |-  ( ( ( G " ( 1 ... n ) ) e. Fin /\ ( 1 ... n ) e. Fin ) -> ( ( # ` ( G " ( 1 ... n ) ) ) = ( # ` ( 1 ... n ) ) <-> ( G " ( 1 ... n ) ) ~~ ( 1 ... n ) ) )
48 46 44 47 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( ( # ` ( G " ( 1 ... n ) ) ) = ( # ` ( 1 ... n ) ) <-> ( G " ( 1 ... n ) ) ~~ ( 1 ... n ) ) )
49 43 48 mpbird 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( # ` ( G " ( 1 ... n ) ) ) = ( # ` ( 1 ... n ) ) )
50 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
51 50 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> n e. NN0 )
52 hashfz1 
 |-  ( n e. NN0 -> ( # ` ( 1 ... n ) ) = n )
53 51 52 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( # ` ( 1 ... n ) ) = n )
54 49 53 eqtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( # ` ( G " ( 1 ... n ) ) ) = n )
55 elfznn 
 |-  ( y e. ( 1 ... n ) -> y e. NN )
56 55 adantl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> y e. NN )
57 zssre 
 |-  ZZ C_ RR
58 9 57 sstri 
 |-  Z C_ RR
59 3 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> G : NN --> Z )
60 ffvelrn 
 |-  ( ( G : NN --> Z /\ y e. NN ) -> ( G ` y ) e. Z )
61 59 55 60 syl2an 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> ( G ` y ) e. Z )
62 58 61 sselid 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> ( G ` y ) e. RR )
63 10 ad2antrr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> ( G ` n ) e. Z )
64 58 63 sselid 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> ( G ` n ) e. RR )
65 eluzelz 
 |-  ( m e. ( ZZ>= ` ( G ` n ) ) -> m e. ZZ )
66 65 ad2antlr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> m e. ZZ )
67 66 zred 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> m e. RR )
68 elfzle2 
 |-  ( y e. ( 1 ... n ) -> y <_ n )
69 68 adantl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> y <_ n )
70 32 ad3antrrr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> G Isom < , < ( NN , ( G " NN ) ) )
71 simpllr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> n e. NN )
72 isorel 
 |-  ( ( G Isom < , < ( NN , ( G " NN ) ) /\ ( n e. NN /\ y e. NN ) ) -> ( n < y <-> ( G ` n ) < ( G ` y ) ) )
73 70 71 56 72 syl12anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> ( n < y <-> ( G ` n ) < ( G ` y ) ) )
74 73 notbid 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> ( -. n < y <-> -. ( G ` n ) < ( G ` y ) ) )
75 56 nnred 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> y e. RR )
76 71 nnred 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> n e. RR )
77 75 76 lenltd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> ( y <_ n <-> -. n < y ) )
78 62 64 lenltd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> ( ( G ` y ) <_ ( G ` n ) <-> -. ( G ` n ) < ( G ` y ) ) )
79 74 77 78 3bitr4d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> ( y <_ n <-> ( G ` y ) <_ ( G ` n ) ) )
80 69 79 mpbid 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> ( G ` y ) <_ ( G ` n ) )
81 eluzle 
 |-  ( m e. ( ZZ>= ` ( G ` n ) ) -> ( G ` n ) <_ m )
82 81 ad2antlr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> ( G ` n ) <_ m )
83 62 64 67 80 82 letrd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> ( G ` y ) <_ m )
84 61 1 eleqtrdi 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> ( G ` y ) e. ( ZZ>= ` M ) )
85 elfz5 
 |-  ( ( ( G ` y ) e. ( ZZ>= ` M ) /\ m e. ZZ ) -> ( ( G ` y ) e. ( M ... m ) <-> ( G ` y ) <_ m ) )
86 84 66 85 syl2anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> ( ( G ` y ) e. ( M ... m ) <-> ( G ` y ) <_ m ) )
87 83 86 mpbird 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> ( G ` y ) e. ( M ... m ) )
88 59 ffnd 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> G Fn NN )
89 88 adantr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> G Fn NN )
90 elpreima 
 |-  ( G Fn NN -> ( y e. ( `' G " ( M ... m ) ) <-> ( y e. NN /\ ( G ` y ) e. ( M ... m ) ) ) )
91 89 90 syl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> ( y e. ( `' G " ( M ... m ) ) <-> ( y e. NN /\ ( G ` y ) e. ( M ... m ) ) ) )
92 56 87 91 mpbir2and 
 |-  ( ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) /\ y e. ( 1 ... n ) ) -> y e. ( `' G " ( M ... m ) ) )
93 92 ex 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( y e. ( 1 ... n ) -> y e. ( `' G " ( M ... m ) ) ) )
94 93 ssrdv 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( 1 ... n ) C_ ( `' G " ( M ... m ) ) )
95 imass2 
 |-  ( ( 1 ... n ) C_ ( `' G " ( M ... m ) ) -> ( G " ( 1 ... n ) ) C_ ( G " ( `' G " ( M ... m ) ) ) )
96 94 95 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( G " ( 1 ... n ) ) C_ ( G " ( `' G " ( M ... m ) ) ) )
97 ssdomg 
 |-  ( ( G " ( `' G " ( M ... m ) ) ) e. Fin -> ( ( G " ( 1 ... n ) ) C_ ( G " ( `' G " ( M ... m ) ) ) -> ( G " ( 1 ... n ) ) ~<_ ( G " ( `' G " ( M ... m ) ) ) ) )
98 21 96 97 sylc 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( G " ( 1 ... n ) ) ~<_ ( G " ( `' G " ( M ... m ) ) ) )
99 hashdom 
 |-  ( ( ( G " ( 1 ... n ) ) e. Fin /\ ( G " ( `' G " ( M ... m ) ) ) e. Fin ) -> ( ( # ` ( G " ( 1 ... n ) ) ) <_ ( # ` ( G " ( `' G " ( M ... m ) ) ) ) <-> ( G " ( 1 ... n ) ) ~<_ ( G " ( `' G " ( M ... m ) ) ) ) )
100 46 21 99 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( ( # ` ( G " ( 1 ... n ) ) ) <_ ( # ` ( G " ( `' G " ( M ... m ) ) ) ) <-> ( G " ( 1 ... n ) ) ~<_ ( G " ( `' G " ( M ... m ) ) ) ) )
101 98 100 mpbird 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( # ` ( G " ( 1 ... n ) ) ) <_ ( # ` ( G " ( `' G " ( M ... m ) ) ) ) )
102 54 101 eqbrtrrd 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> n <_ ( # ` ( G " ( `' G " ( M ... m ) ) ) ) )
103 eluz2 
 |-  ( ( # ` ( G " ( `' G " ( M ... m ) ) ) ) e. ( ZZ>= ` n ) <-> ( n e. ZZ /\ ( # ` ( G " ( `' G " ( M ... m ) ) ) ) e. ZZ /\ n <_ ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) )
104 13 24 102 103 syl3anbrc 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( # ` ( G " ( `' G " ( M ... m ) ) ) ) e. ( ZZ>= ` n ) )
105 fveq2 
 |-  ( k = ( # ` ( G " ( `' G " ( M ... m ) ) ) ) -> ( seq 1 ( + , H ) ` k ) = ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) )
106 105 eleq1d 
 |-  ( k = ( # ` ( G " ( `' G " ( M ... m ) ) ) ) -> ( ( seq 1 ( + , H ) ` k ) e. CC <-> ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC ) )
107 105 fvoveq1d 
 |-  ( k = ( # ` ( G " ( `' G " ( M ... m ) ) ) ) -> ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) = ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) )
108 107 breq1d 
 |-  ( k = ( # ` ( G " ( `' G " ( M ... m ) ) ) ) -> ( ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x <-> ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) )
109 106 108 anbi12d 
 |-  ( k = ( # ` ( G " ( `' G " ( M ... m ) ) ) ) -> ( ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) <-> ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) ) )
110 109 rspcv 
 |-  ( ( # ` ( G " ( `' G " ( M ... m ) ) ) ) e. ( ZZ>= ` n ) -> ( A. k e. ( ZZ>= ` n ) ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) -> ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) ) )
111 104 110 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ m e. ( ZZ>= ` ( G ` n ) ) ) -> ( A. k e. ( ZZ>= ` n ) ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) -> ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) ) )
112 111 ralrimdva 
 |-  ( ( ph /\ n e. NN ) -> ( A. k e. ( ZZ>= ` n ) ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) -> A. m e. ( ZZ>= ` ( G ` n ) ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) ) )
113 fveq2 
 |-  ( j = ( G ` n ) -> ( ZZ>= ` j ) = ( ZZ>= ` ( G ` n ) ) )
114 113 raleqdv 
 |-  ( j = ( G ` n ) -> ( A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) <-> A. m e. ( ZZ>= ` ( G ` n ) ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) ) )
115 114 rspcev 
 |-  ( ( ( G ` n ) e. ZZ /\ A. m e. ( ZZ>= ` ( G ` n ) ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) ) -> E. j e. ZZ A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) )
116 11 112 115 syl6an 
 |-  ( ( ph /\ n e. NN ) -> ( A. k e. ( ZZ>= ` n ) ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) -> E. j e. ZZ A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) ) )
117 116 rexlimdva 
 |-  ( ph -> ( E. n e. NN A. k e. ( ZZ>= ` n ) ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) -> E. j e. ZZ A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) ) )
118 1nn 
 |-  1 e. NN
119 ffvelrn 
 |-  ( ( G : NN --> Z /\ 1 e. NN ) -> ( G ` 1 ) e. Z )
120 3 118 119 sylancl 
 |-  ( ph -> ( G ` 1 ) e. Z )
121 120 1 eleqtrdi 
 |-  ( ph -> ( G ` 1 ) e. ( ZZ>= ` M ) )
122 eluzelz 
 |-  ( ( G ` 1 ) e. ( ZZ>= ` M ) -> ( G ` 1 ) e. ZZ )
123 eqid 
 |-  ( ZZ>= ` ( G ` 1 ) ) = ( ZZ>= ` ( G ` 1 ) )
124 123 rexuz3 
 |-  ( ( G ` 1 ) e. ZZ -> ( E. j e. ( ZZ>= ` ( G ` 1 ) ) A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) <-> E. j e. ZZ A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) ) )
125 121 122 124 3syl 
 |-  ( ph -> ( E. j e. ( ZZ>= ` ( G ` 1 ) ) A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) <-> E. j e. ZZ A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) ) )
126 117 125 sylibrd 
 |-  ( ph -> ( E. n e. NN A. k e. ( ZZ>= ` n ) ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) -> E. j e. ( ZZ>= ` ( G ` 1 ) ) A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) ) )
127 fzfid 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( M ... j ) e. Fin )
128 funimacnv 
 |-  ( Fun G -> ( G " ( `' G " ( M ... j ) ) ) = ( ( M ... j ) i^i ran G ) )
129 3 15 128 3syl 
 |-  ( ph -> ( G " ( `' G " ( M ... j ) ) ) = ( ( M ... j ) i^i ran G ) )
130 inss1 
 |-  ( ( M ... j ) i^i ran G ) C_ ( M ... j )
131 129 130 eqsstrdi 
 |-  ( ph -> ( G " ( `' G " ( M ... j ) ) ) C_ ( M ... j ) )
132 131 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G " ( `' G " ( M ... j ) ) ) C_ ( M ... j ) )
133 127 132 ssfid 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G " ( `' G " ( M ... j ) ) ) e. Fin )
134 hashcl 
 |-  ( ( G " ( `' G " ( M ... j ) ) ) e. Fin -> ( # ` ( G " ( `' G " ( M ... j ) ) ) ) e. NN0 )
135 nn0p1nn 
 |-  ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) e. NN0 -> ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) e. NN )
136 133 134 135 3syl 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) e. NN )
137 eluzle 
 |-  ( k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) -> ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) <_ k )
138 137 adantl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) <_ k )
139 133 adantr 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( G " ( `' G " ( M ... j ) ) ) e. Fin )
140 nn0z 
 |-  ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) e. NN0 -> ( # ` ( G " ( `' G " ( M ... j ) ) ) ) e. ZZ )
141 139 134 140 3syl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( # ` ( G " ( `' G " ( M ... j ) ) ) ) e. ZZ )
142 eluzelz 
 |-  ( k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) -> k e. ZZ )
143 142 adantl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> k e. ZZ )
144 zltp1le 
 |-  ( ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) e. ZZ /\ k e. ZZ ) -> ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) < k <-> ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) <_ k ) )
145 141 143 144 syl2anc 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) < k <-> ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) <_ k ) )
146 138 145 mpbird 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( # ` ( G " ( `' G " ( M ... j ) ) ) ) < k )
147 nn0re 
 |-  ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) e. NN0 -> ( # ` ( G " ( `' G " ( M ... j ) ) ) ) e. RR )
148 133 134 147 3syl 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( # ` ( G " ( `' G " ( M ... j ) ) ) ) e. RR )
149 148 adantr 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( # ` ( G " ( `' G " ( M ... j ) ) ) ) e. RR )
150 eluznn 
 |-  ( ( ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) e. NN /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> k e. NN )
151 136 150 sylan 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> k e. NN )
152 151 nnred 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> k e. RR )
153 149 152 ltnled 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) < k <-> -. k <_ ( # ` ( G " ( `' G " ( M ... j ) ) ) ) ) )
154 146 153 mpbid 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> -. k <_ ( # ` ( G " ( `' G " ( M ... j ) ) ) ) )
155 fzss2 
 |-  ( j e. ( ZZ>= ` ( G ` k ) ) -> ( M ... ( G ` k ) ) C_ ( M ... j ) )
156 imass2 
 |-  ( ( M ... ( G ` k ) ) C_ ( M ... j ) -> ( `' G " ( M ... ( G ` k ) ) ) C_ ( `' G " ( M ... j ) ) )
157 imass2 
 |-  ( ( `' G " ( M ... ( G ` k ) ) ) C_ ( `' G " ( M ... j ) ) -> ( G " ( `' G " ( M ... ( G ` k ) ) ) ) C_ ( G " ( `' G " ( M ... j ) ) ) )
158 155 156 157 3syl 
 |-  ( j e. ( ZZ>= ` ( G ` k ) ) -> ( G " ( `' G " ( M ... ( G ` k ) ) ) ) C_ ( G " ( `' G " ( M ... j ) ) ) )
159 ssdomg 
 |-  ( ( G " ( `' G " ( M ... j ) ) ) e. Fin -> ( ( G " ( 1 ... k ) ) C_ ( G " ( `' G " ( M ... j ) ) ) -> ( G " ( 1 ... k ) ) ~<_ ( G " ( `' G " ( M ... j ) ) ) ) )
160 139 159 syl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( ( G " ( 1 ... k ) ) C_ ( G " ( `' G " ( M ... j ) ) ) -> ( G " ( 1 ... k ) ) ~<_ ( G " ( `' G " ( M ... j ) ) ) ) )
161 3 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> G : NN --> Z )
162 161 ffvelrnda 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) /\ x e. NN ) -> ( G ` x ) e. Z )
163 162 1 eleqtrdi 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) /\ x e. NN ) -> ( G ` x ) e. ( ZZ>= ` M ) )
164 161 151 ffvelrnd 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( G ` k ) e. Z )
165 9 164 sselid 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( G ` k ) e. ZZ )
166 165 adantr 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) /\ x e. NN ) -> ( G ` k ) e. ZZ )
167 elfz5 
 |-  ( ( ( G ` x ) e. ( ZZ>= ` M ) /\ ( G ` k ) e. ZZ ) -> ( ( G ` x ) e. ( M ... ( G ` k ) ) <-> ( G ` x ) <_ ( G ` k ) ) )
168 163 166 167 syl2anc 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) /\ x e. NN ) -> ( ( G ` x ) e. ( M ... ( G ` k ) ) <-> ( G ` x ) <_ ( G ` k ) ) )
169 32 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) /\ x e. NN ) -> G Isom < , < ( NN , ( G " NN ) ) )
170 nnssre 
 |-  NN C_ RR
171 ressxr 
 |-  RR C_ RR*
172 170 171 sstri 
 |-  NN C_ RR*
173 172 a1i 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) /\ x e. NN ) -> NN C_ RR* )
174 imassrn 
 |-  ( G " NN ) C_ ran G
175 161 adantr 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) /\ x e. NN ) -> G : NN --> Z )
176 175 frnd 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) /\ x e. NN ) -> ran G C_ Z )
177 176 58 sstrdi 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) /\ x e. NN ) -> ran G C_ RR )
178 174 177 sstrid 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) /\ x e. NN ) -> ( G " NN ) C_ RR )
179 178 171 sstrdi 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) /\ x e. NN ) -> ( G " NN ) C_ RR* )
180 simpr 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) /\ x e. NN ) -> x e. NN )
181 151 adantr 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) /\ x e. NN ) -> k e. NN )
182 leisorel 
 |-  ( ( G Isom < , < ( NN , ( G " NN ) ) /\ ( NN C_ RR* /\ ( G " NN ) C_ RR* ) /\ ( x e. NN /\ k e. NN ) ) -> ( x <_ k <-> ( G ` x ) <_ ( G ` k ) ) )
183 169 173 179 180 181 182 syl122anc 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) /\ x e. NN ) -> ( x <_ k <-> ( G ` x ) <_ ( G ` k ) ) )
184 168 183 bitr4d 
 |-  ( ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) /\ x e. NN ) -> ( ( G ` x ) e. ( M ... ( G ` k ) ) <-> x <_ k ) )
185 184 pm5.32da 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( ( x e. NN /\ ( G ` x ) e. ( M ... ( G ` k ) ) ) <-> ( x e. NN /\ x <_ k ) ) )
186 elpreima 
 |-  ( G Fn NN -> ( x e. ( `' G " ( M ... ( G ` k ) ) ) <-> ( x e. NN /\ ( G ` x ) e. ( M ... ( G ` k ) ) ) ) )
187 161 28 186 3syl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( x e. ( `' G " ( M ... ( G ` k ) ) ) <-> ( x e. NN /\ ( G ` x ) e. ( M ... ( G ` k ) ) ) ) )
188 fznn 
 |-  ( k e. ZZ -> ( x e. ( 1 ... k ) <-> ( x e. NN /\ x <_ k ) ) )
189 143 188 syl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( x e. ( 1 ... k ) <-> ( x e. NN /\ x <_ k ) ) )
190 185 187 189 3bitr4d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( x e. ( `' G " ( M ... ( G ` k ) ) ) <-> x e. ( 1 ... k ) ) )
191 190 eqrdv 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( `' G " ( M ... ( G ` k ) ) ) = ( 1 ... k ) )
192 191 imaeq2d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( G " ( `' G " ( M ... ( G ` k ) ) ) ) = ( G " ( 1 ... k ) ) )
193 192 sseq1d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( ( G " ( `' G " ( M ... ( G ` k ) ) ) ) C_ ( G " ( `' G " ( M ... j ) ) ) <-> ( G " ( 1 ... k ) ) C_ ( G " ( `' G " ( M ... j ) ) ) ) )
194 38 ad2antrr 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> G : NN -1-1-> Z )
195 fz1ssnn 
 |-  ( 1 ... k ) C_ NN
196 ovex 
 |-  ( 1 ... k ) e. _V
197 196 f1imaen 
 |-  ( ( G : NN -1-1-> Z /\ ( 1 ... k ) C_ NN ) -> ( G " ( 1 ... k ) ) ~~ ( 1 ... k ) )
198 194 195 197 sylancl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( G " ( 1 ... k ) ) ~~ ( 1 ... k ) )
199 fzfid 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( 1 ... k ) e. Fin )
200 enfii 
 |-  ( ( ( 1 ... k ) e. Fin /\ ( G " ( 1 ... k ) ) ~~ ( 1 ... k ) ) -> ( G " ( 1 ... k ) ) e. Fin )
201 199 198 200 syl2anc 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( G " ( 1 ... k ) ) e. Fin )
202 hashen 
 |-  ( ( ( G " ( 1 ... k ) ) e. Fin /\ ( 1 ... k ) e. Fin ) -> ( ( # ` ( G " ( 1 ... k ) ) ) = ( # ` ( 1 ... k ) ) <-> ( G " ( 1 ... k ) ) ~~ ( 1 ... k ) ) )
203 201 199 202 syl2anc 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( ( # ` ( G " ( 1 ... k ) ) ) = ( # ` ( 1 ... k ) ) <-> ( G " ( 1 ... k ) ) ~~ ( 1 ... k ) ) )
204 198 203 mpbird 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( # ` ( G " ( 1 ... k ) ) ) = ( # ` ( 1 ... k ) ) )
205 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
206 hashfz1 
 |-  ( k e. NN0 -> ( # ` ( 1 ... k ) ) = k )
207 151 205 206 3syl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( # ` ( 1 ... k ) ) = k )
208 204 207 eqtrd 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( # ` ( G " ( 1 ... k ) ) ) = k )
209 208 breq1d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( ( # ` ( G " ( 1 ... k ) ) ) <_ ( # ` ( G " ( `' G " ( M ... j ) ) ) ) <-> k <_ ( # ` ( G " ( `' G " ( M ... j ) ) ) ) ) )
210 hashdom 
 |-  ( ( ( G " ( 1 ... k ) ) e. Fin /\ ( G " ( `' G " ( M ... j ) ) ) e. Fin ) -> ( ( # ` ( G " ( 1 ... k ) ) ) <_ ( # ` ( G " ( `' G " ( M ... j ) ) ) ) <-> ( G " ( 1 ... k ) ) ~<_ ( G " ( `' G " ( M ... j ) ) ) ) )
211 201 139 210 syl2anc 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( ( # ` ( G " ( 1 ... k ) ) ) <_ ( # ` ( G " ( `' G " ( M ... j ) ) ) ) <-> ( G " ( 1 ... k ) ) ~<_ ( G " ( `' G " ( M ... j ) ) ) ) )
212 209 211 bitr3d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( k <_ ( # ` ( G " ( `' G " ( M ... j ) ) ) ) <-> ( G " ( 1 ... k ) ) ~<_ ( G " ( `' G " ( M ... j ) ) ) ) )
213 160 193 212 3imtr4d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( ( G " ( `' G " ( M ... ( G ` k ) ) ) ) C_ ( G " ( `' G " ( M ... j ) ) ) -> k <_ ( # ` ( G " ( `' G " ( M ... j ) ) ) ) ) )
214 158 213 syl5 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( j e. ( ZZ>= ` ( G ` k ) ) -> k <_ ( # ` ( G " ( `' G " ( M ... j ) ) ) ) ) )
215 154 214 mtod 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> -. j e. ( ZZ>= ` ( G ` k ) ) )
216 eluzelz 
 |-  ( j e. ( ZZ>= ` ( G ` 1 ) ) -> j e. ZZ )
217 216 ad2antlr 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> j e. ZZ )
218 uztric 
 |-  ( ( ( G ` k ) e. ZZ /\ j e. ZZ ) -> ( j e. ( ZZ>= ` ( G ` k ) ) \/ ( G ` k ) e. ( ZZ>= ` j ) ) )
219 165 217 218 syl2anc 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( j e. ( ZZ>= ` ( G ` k ) ) \/ ( G ` k ) e. ( ZZ>= ` j ) ) )
220 219 ord 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( -. j e. ( ZZ>= ` ( G ` k ) ) -> ( G ` k ) e. ( ZZ>= ` j ) ) )
221 215 220 mpd 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( G ` k ) e. ( ZZ>= ` j ) )
222 oveq2 
 |-  ( m = ( G ` k ) -> ( M ... m ) = ( M ... ( G ` k ) ) )
223 222 imaeq2d 
 |-  ( m = ( G ` k ) -> ( `' G " ( M ... m ) ) = ( `' G " ( M ... ( G ` k ) ) ) )
224 223 imaeq2d 
 |-  ( m = ( G ` k ) -> ( G " ( `' G " ( M ... m ) ) ) = ( G " ( `' G " ( M ... ( G ` k ) ) ) ) )
225 224 fveq2d 
 |-  ( m = ( G ` k ) -> ( # ` ( G " ( `' G " ( M ... m ) ) ) ) = ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) )
226 225 fveq2d 
 |-  ( m = ( G ` k ) -> ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) = ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) ) )
227 226 eleq1d 
 |-  ( m = ( G ` k ) -> ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC <-> ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) ) e. CC ) )
228 226 fvoveq1d 
 |-  ( m = ( G ` k ) -> ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) = ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) ) - A ) ) )
229 228 breq1d 
 |-  ( m = ( G ` k ) -> ( ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x <-> ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) ) - A ) ) < x ) )
230 227 229 anbi12d 
 |-  ( m = ( G ` k ) -> ( ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) <-> ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) ) - A ) ) < x ) ) )
231 230 rspcv 
 |-  ( ( G ` k ) e. ( ZZ>= ` j ) -> ( A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) -> ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) ) - A ) ) < x ) ) )
232 221 231 syl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) -> ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) ) - A ) ) < x ) ) )
233 192 fveq2d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) = ( # ` ( G " ( 1 ... k ) ) ) )
234 233 208 eqtrd 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) = k )
235 234 fveq2d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) ) = ( seq 1 ( + , H ) ` k ) )
236 235 eleq1d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) ) e. CC <-> ( seq 1 ( + , H ) ` k ) e. CC ) )
237 235 fvoveq1d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) ) - A ) ) = ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) )
238 237 breq1d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) ) - A ) ) < x <-> ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) )
239 236 238 anbi12d 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... ( G ` k ) ) ) ) ) ) - A ) ) < x ) <-> ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) ) )
240 232 239 sylibd 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ) -> ( A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) -> ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) ) )
241 240 ralrimdva 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) -> A. k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) ) )
242 fveq2 
 |-  ( n = ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) -> ( ZZ>= ` n ) = ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) )
243 242 raleqdv 
 |-  ( n = ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) -> ( A. k e. ( ZZ>= ` n ) ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) <-> A. k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) ) )
244 243 rspcev 
 |-  ( ( ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) e. NN /\ A. k e. ( ZZ>= ` ( ( # ` ( G " ( `' G " ( M ... j ) ) ) ) + 1 ) ) ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) ) -> E. n e. NN A. k e. ( ZZ>= ` n ) ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) )
245 136 241 244 syl6an 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) -> E. n e. NN A. k e. ( ZZ>= ` n ) ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) ) )
246 245 rexlimdva 
 |-  ( ph -> ( E. j e. ( ZZ>= ` ( G ` 1 ) ) A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) -> E. n e. NN A. k e. ( ZZ>= ` n ) ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) ) )
247 126 246 impbid 
 |-  ( ph -> ( E. n e. NN A. k e. ( ZZ>= ` n ) ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) <-> E. j e. ( ZZ>= ` ( G ` 1 ) ) A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) ) )
248 247 ralbidv 
 |-  ( ph -> ( A. x e. RR+ E. n e. NN A. k e. ( ZZ>= ` n ) ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) <-> A. x e. RR+ E. j e. ( ZZ>= ` ( G ` 1 ) ) A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) ) )
249 248 anbi2d 
 |-  ( ph -> ( ( A e. CC /\ A. x e. RR+ E. n e. NN A. k e. ( ZZ>= ` n ) ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) ) <-> ( A e. CC /\ A. x e. RR+ E. j e. ( ZZ>= ` ( G ` 1 ) ) A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) ) ) )
250 nnuz 
 |-  NN = ( ZZ>= ` 1 )
251 1zzd 
 |-  ( ph -> 1 e. ZZ )
252 seqex 
 |-  seq 1 ( + , H ) e. _V
253 252 a1i 
 |-  ( ph -> seq 1 ( + , H ) e. _V )
254 eqidd 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , H ) ` k ) = ( seq 1 ( + , H ) ` k ) )
255 250 251 253 254 clim2 
 |-  ( ph -> ( seq 1 ( + , H ) ~~> A <-> ( A e. CC /\ A. x e. RR+ E. n e. NN A. k e. ( ZZ>= ` n ) ( ( seq 1 ( + , H ) ` k ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` k ) - A ) ) < x ) ) ) )
256 121 122 syl 
 |-  ( ph -> ( G ` 1 ) e. ZZ )
257 seqex 
 |-  seq M ( + , F ) e. _V
258 257 a1i 
 |-  ( ph -> seq M ( + , F ) e. _V )
259 1 2 3 4 5 6 7 isercolllem3 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( seq M ( + , F ) ` m ) = ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) )
260 123 256 258 259 clim2 
 |-  ( ph -> ( seq M ( + , F ) ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. ( ZZ>= ` ( G ` 1 ) ) A. m e. ( ZZ>= ` j ) ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) e. CC /\ ( abs ` ( ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... m ) ) ) ) ) - A ) ) < x ) ) ) )
261 249 255 260 3bitr4d 
 |-  ( ph -> ( seq 1 ( + , H ) ~~> A <-> seq M ( + , F ) ~~> A ) )