Metamath Proof Explorer

Theorem seqcoll

Description: The function F contains a sparse set of nonzero values to be summed. The function G is an order isomorphism from the set of nonzero values of F to a 1-based finite sequence, and H collects these nonzero values together. Under these conditions, the sum over the values in H yields the same result as the sum over the original set F . (Contributed by Mario Carneiro, 2-Apr-2014)

Ref Expression
Hypotheses seqcoll.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑍 + 𝑘 ) = 𝑘 )
seqcoll.1b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑘 + 𝑍 ) = 𝑘 )
seqcoll.c ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆 ) ) → ( 𝑘 + 𝑛 ) ∈ 𝑆 )
seqcoll.a ⊢ ( 𝜑 → 𝑍 ∈ 𝑆 )
seqcoll.2 ⊢ ( 𝜑 → 𝐺 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
seqcoll.3 ⊢ ( 𝜑 → 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
seqcoll.4 ⊢ ( 𝜑 → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
seqcoll.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 )
seqcoll.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
seqcoll.7 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐻 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑛 ) ) )
Assertion seqcoll ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑁 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 seqcoll.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑍 + 𝑘 ) = 𝑘 )
2 seqcoll.1b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑘 + 𝑍 ) = 𝑘 )
3 seqcoll.c ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆 ) ) → ( 𝑘 + 𝑛 ) ∈ 𝑆 )
4 seqcoll.a ⊢ ( 𝜑 → 𝑍 ∈ 𝑆 )
5 seqcoll.2 ⊢ ( 𝜑 → 𝐺 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
6 seqcoll.3 ⊢ ( 𝜑 → 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
7 seqcoll.4 ⊢ ( 𝜑 → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
8 seqcoll.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 )
9 seqcoll.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
10 seqcoll.7 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐻 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑛 ) ) )
11 elfznn ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → 𝑁 ∈ ℕ )
12 6 11 syl ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
13 eleq1 ⊢ ( 𝑦 = 1 → ( 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↔ 1 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) )
14 2fveq3 ⊢ ( 𝑦 = 1 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑦 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 1 ) ) )
15 fveq2 ⊢ ( 𝑦 = 1 → ( seq 1 ( + , 𝐻 ) ‘ 𝑦 ) = ( seq 1 ( + , 𝐻 ) ‘ 1 ) )
16 14 15 eqeq12d ⊢ ( 𝑦 = 1 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑦 ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 1 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 1 ) ) )
17 13 16 imbi12d ⊢ ( 𝑦 = 1 → ( ( 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑦 ) ) ↔ ( 1 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 1 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 1 ) ) ) )
18 17 imbi2d ⊢ ( 𝑦 = 1 → ( ( 𝜑 → ( 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑦 ) ) ) ↔ ( 𝜑 → ( 1 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 1 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 1 ) ) ) ) )
19 eleq1 ⊢ ( 𝑦 = 𝑚 → ( 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↔ 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) )
20 2fveq3 ⊢ ( 𝑦 = 𝑚 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑦 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) )
21 fveq2 ⊢ ( 𝑦 = 𝑚 → ( seq 1 ( + , 𝐻 ) ‘ 𝑦 ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑚 ) )
22 20 21 eqeq12d ⊢ ( 𝑦 = 𝑚 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑦 ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑚 ) ) )
23 19 22 imbi12d ⊢ ( 𝑦 = 𝑚 → ( ( 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑦 ) ) ↔ ( 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑚 ) ) ) )
24 23 imbi2d ⊢ ( 𝑦 = 𝑚 → ( ( 𝜑 → ( 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑦 ) ) ) ↔ ( 𝜑 → ( 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑚 ) ) ) ) )
25 eleq1 ⊢ ( 𝑦 = ( 𝑚 + 1 ) → ( 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↔ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) )
26 2fveq3 ⊢ ( 𝑦 = ( 𝑚 + 1 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑦 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) )
27 fveq2 ⊢ ( 𝑦 = ( 𝑚 + 1 ) → ( seq 1 ( + , 𝐻 ) ‘ 𝑦 ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑚 + 1 ) ) )
28 26 27 eqeq12d ⊢ ( 𝑦 = ( 𝑚 + 1 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑦 ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑚 + 1 ) ) ) )
29 25 28 imbi12d ⊢ ( 𝑦 = ( 𝑚 + 1 ) → ( ( 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑦 ) ) ↔ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑚 + 1 ) ) ) ) )
30 29 imbi2d ⊢ ( 𝑦 = ( 𝑚 + 1 ) → ( ( 𝜑 → ( 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑦 ) ) ) ↔ ( 𝜑 → ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑚 + 1 ) ) ) ) ) )
31 eleq1 ⊢ ( 𝑦 = 𝑁 → ( 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↔ 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) )
32 2fveq3 ⊢ ( 𝑦 = 𝑁 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑦 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑁 ) ) )
33 fveq2 ⊢ ( 𝑦 = 𝑁 → ( seq 1 ( + , 𝐻 ) ‘ 𝑦 ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑁 ) )
34 32 33 eqeq12d ⊢ ( 𝑦 = 𝑁 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑦 ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑁 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑁 ) ) )
35 31 34 imbi12d ⊢ ( 𝑦 = 𝑁 → ( ( 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑦 ) ) ↔ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑁 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑁 ) ) ) )
36 35 imbi2d ⊢ ( 𝑦 = 𝑁 → ( ( 𝜑 → ( 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑦 ) ) ) ↔ ( 𝜑 → ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑁 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑁 ) ) ) ) )
37 isof1o ⊢ ( 𝐺 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) → 𝐺 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
38 5 37 syl ⊢ ( 𝜑 → 𝐺 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
39 f1of ⊢ ( 𝐺 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → 𝐺 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
40 38 39 syl ⊢ ( 𝜑 → 𝐺 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
41 elfzuz2 ⊢ ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) )
42 6 41 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) )
43 eluzfz1 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
44 42 43 syl ⊢ ( 𝜑 → 1 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
45 40 44 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) ∈ 𝐴 )
46 7 45 sseldd ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
47 eluzle ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) → 1 ≤ ( ♯ ‘ 𝐴 ) )
48 42 47 syl ⊢ ( 𝜑 → 1 ≤ ( ♯ ‘ 𝐴 ) )
49 fzssz ⊢ ( 1 ... ( ♯ ‘ 𝐴 ) ) ⊆ ℤ
50 zssre ⊢ ℤ ⊆ ℝ
51 49 50 sstri ⊢ ( 1 ... ( ♯ ‘ 𝐴 ) ) ⊆ ℝ
52 51 a1i ⊢ ( 𝜑 → ( 1 ... ( ♯ ‘ 𝐴 ) ) ⊆ ℝ )
53 ressxr ⊢ ℝ ⊆ ℝ*
54 52 53 sstrdi ⊢ ( 𝜑 → ( 1 ... ( ♯ ‘ 𝐴 ) ) ⊆ ℝ* )
55 eluzelre ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℝ )
56 55 ssriv ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℝ
57 7 56 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
58 57 53 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
59 eluzfz2 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) → ( ♯ ‘ 𝐴 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
60 42 59 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
61 leisorel ⊢ ( ( 𝐺 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ∧ ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ⊆ ℝ* ∧ 𝐴 ⊆ ℝ* ) ∧ ( 1 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) → ( 1 ≤ ( ♯ ‘ 𝐴 ) ↔ ( 𝐺 ‘ 1 ) ≤ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
62 5 54 58 44 60 61 syl122anc ⊢ ( 𝜑 → ( 1 ≤ ( ♯ ‘ 𝐴 ) ↔ ( 𝐺 ‘ 1 ) ≤ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
63 48 62 mpbid ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) ≤ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) )
64 40 60 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ 𝐴 )
65 7 64 sseldd ⊢ ( 𝜑 → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) )
66 eluzelz ⊢ ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ℤ )
67 65 66 syl ⊢ ( 𝜑 → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ℤ )
68 elfz5 ⊢ ( ( ( 𝐺 ‘ 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ℤ ) → ( ( 𝐺 ‘ 1 ) ∈ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ↔ ( 𝐺 ‘ 1 ) ≤ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
69 46 67 68 syl2anc ⊢ ( 𝜑 → ( ( 𝐺 ‘ 1 ) ∈ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ↔ ( 𝐺 ‘ 1 ) ≤ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
70 63 69 mpbird ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) ∈ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
71 fveq2 ⊢ ( 𝑘 = ( 𝐺 ‘ 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝐺 ‘ 1 ) ) )
72 71 eleq1d ⊢ ( 𝑘 = ( 𝐺 ‘ 1 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 ↔ ( 𝐹 ‘ ( 𝐺 ‘ 1 ) ) ∈ 𝑆 ) )
73 72 imbi2d ⊢ ( 𝑘 = ( 𝐺 ‘ 1 ) → ( ( 𝜑 → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 ) ↔ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ 1 ) ) ∈ 𝑆 ) ) )
74 8 expcom ⊢ ( 𝑘 ∈ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) → ( 𝜑 → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 ) )
75 73 74 vtoclga ⊢ ( ( 𝐺 ‘ 1 ) ∈ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) → ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ 1 ) ) ∈ 𝑆 ) )
76 70 75 mpcom ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ 1 ) ) ∈ 𝑆 )
77 eluzelz ⊢ ( ( 𝐺 ‘ 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐺 ‘ 1 ) ∈ ℤ )
78 46 77 syl ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) ∈ ℤ )
79 peano2zm ⊢ ( ( 𝐺 ‘ 1 ) ∈ ℤ → ( ( 𝐺 ‘ 1 ) − 1 ) ∈ ℤ )
80 78 79 syl ⊢ ( 𝜑 → ( ( 𝐺 ‘ 1 ) − 1 ) ∈ ℤ )
81 80 zred ⊢ ( 𝜑 → ( ( 𝐺 ‘ 1 ) − 1 ) ∈ ℝ )
82 78 zred ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) ∈ ℝ )
83 67 zred ⊢ ( 𝜑 → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ℝ )
84 82 lem1d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 1 ) − 1 ) ≤ ( 𝐺 ‘ 1 ) )
85 81 82 83 84 63 letrd ⊢ ( 𝜑 → ( ( 𝐺 ‘ 1 ) − 1 ) ≤ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) )
86 eluz ⊢ ( ( ( ( 𝐺 ‘ 1 ) − 1 ) ∈ ℤ ∧ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ℤ ) → ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( ( 𝐺 ‘ 1 ) − 1 ) ) ↔ ( ( 𝐺 ‘ 1 ) − 1 ) ≤ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
87 80 67 86 syl2anc ⊢ ( 𝜑 → ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( ( 𝐺 ‘ 1 ) − 1 ) ) ↔ ( ( 𝐺 ‘ 1 ) − 1 ) ≤ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
88 85 87 mpbird ⊢ ( 𝜑 → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( ( 𝐺 ‘ 1 ) − 1 ) ) )
89 fzss2 ⊢ ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( ( 𝐺 ‘ 1 ) − 1 ) ) → ( 𝑀 ... ( ( 𝐺 ‘ 1 ) − 1 ) ) ⊆ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
90 88 89 syl ⊢ ( 𝜑 → ( 𝑀 ... ( ( 𝐺 ‘ 1 ) − 1 ) ) ⊆ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
91 90 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( ( 𝐺 ‘ 1 ) − 1 ) ) ) → 𝑘 ∈ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
92 eluzel2 ⊢ ( ( 𝐺 ‘ 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
93 46 92 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
94 elfzm11 ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝐺 ‘ 1 ) ∈ ℤ ) → ( 𝑘 ∈ ( 𝑀 ... ( ( 𝐺 ‘ 1 ) − 1 ) ) ↔ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < ( 𝐺 ‘ 1 ) ) ) )
95 93 78 94 syl2anc ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝑀 ... ( ( 𝐺 ‘ 1 ) − 1 ) ) ↔ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < ( 𝐺 ‘ 1 ) ) ) )
96 simp3 ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < ( 𝐺 ‘ 1 ) ) → 𝑘 < ( 𝐺 ‘ 1 ) )
97 82 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐺 ‘ 1 ) ∈ ℝ )
98 57 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ ℝ )
99 f1ocnv ⊢ ( 𝐺 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ◡ 𝐺 : 𝐴 –1-1-onto→ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
100 38 99 syl ⊢ ( 𝜑 → ◡ 𝐺 : 𝐴 –1-1-onto→ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
101 f1of ⊢ ( ◡ 𝐺 : 𝐴 –1-1-onto→ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ◡ 𝐺 : 𝐴 ⟶ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
102 100 101 syl ⊢ ( 𝜑 → ◡ 𝐺 : 𝐴 ⟶ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
103 102 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ◡ 𝐺 ‘ 𝑘 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
104 elfznn ⊢ ( ( ◡ 𝐺 ‘ 𝑘 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( ◡ 𝐺 ‘ 𝑘 ) ∈ ℕ )
105 103 104 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ◡ 𝐺 ‘ 𝑘 ) ∈ ℕ )
106 105 nnge1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 1 ≤ ( ◡ 𝐺 ‘ 𝑘 ) )
107 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐺 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
108 54 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 1 ... ( ♯ ‘ 𝐴 ) ) ⊆ ℝ* )
109 58 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐴 ⊆ ℝ* )
110 44 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 1 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
111 leisorel ⊢ ( ( 𝐺 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ∧ ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ⊆ ℝ* ∧ 𝐴 ⊆ ℝ* ) ∧ ( 1 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ ( ◡ 𝐺 ‘ 𝑘 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) → ( 1 ≤ ( ◡ 𝐺 ‘ 𝑘 ) ↔ ( 𝐺 ‘ 1 ) ≤ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) )
112 107 108 109 110 103 111 syl122anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 1 ≤ ( ◡ 𝐺 ‘ 𝑘 ) ↔ ( 𝐺 ‘ 1 ) ≤ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) )
113 106 112 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐺 ‘ 1 ) ≤ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) )
114 f1ocnvfv2 ⊢ ( ( 𝐺 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) = 𝑘 )
115 38 114 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) = 𝑘 )
116 113 115 breqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐺 ‘ 1 ) ≤ 𝑘 )
117 97 98 116 lensymd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ¬ 𝑘 < ( 𝐺 ‘ 1 ) )
118 117 ex ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → ¬ 𝑘 < ( 𝐺 ‘ 1 ) ) )
119 118 con2d ⊢ ( 𝜑 → ( 𝑘 < ( 𝐺 ‘ 1 ) → ¬ 𝑘 ∈ 𝐴 ) )
120 96 119 syl5 ⊢ ( 𝜑 → ( ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < ( 𝐺 ‘ 1 ) ) → ¬ 𝑘 ∈ 𝐴 ) )
121 95 120 sylbid ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝑀 ... ( ( 𝐺 ‘ 1 ) − 1 ) ) → ¬ 𝑘 ∈ 𝐴 ) )
122 121 imp ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( ( 𝐺 ‘ 1 ) − 1 ) ) ) → ¬ 𝑘 ∈ 𝐴 )
123 91 122 eldifd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( ( 𝐺 ‘ 1 ) − 1 ) ) ) → 𝑘 ∈ ( ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) )
124 123 9 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( ( 𝐺 ‘ 1 ) − 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
125 1 4 46 76 124 seqid ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) = seq ( 𝐺 ‘ 1 ) ( + , 𝐹 ) )
126 125 fveq1d ⊢ ( 𝜑 → ( ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ‘ ( 𝐺 ‘ 1 ) ) = ( seq ( 𝐺 ‘ 1 ) ( + , 𝐹 ) ‘ ( 𝐺 ‘ 1 ) ) )
127 uzid ⊢ ( ( 𝐺 ‘ 1 ) ∈ ℤ → ( 𝐺 ‘ 1 ) ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) )
128 78 127 syl ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) )
129 128 fvresd ⊢ ( 𝜑 → ( ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ‘ ( 𝐺 ‘ 1 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 1 ) ) )
130 seq1 ⊢ ( ( 𝐺 ‘ 1 ) ∈ ℤ → ( seq ( 𝐺 ‘ 1 ) ( + , 𝐹 ) ‘ ( 𝐺 ‘ 1 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 1 ) ) )
131 78 130 syl ⊢ ( 𝜑 → ( seq ( 𝐺 ‘ 1 ) ( + , 𝐹 ) ‘ ( 𝐺 ‘ 1 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 1 ) ) )
132 fveq2 ⊢ ( 𝑛 = 1 → ( 𝐻 ‘ 𝑛 ) = ( 𝐻 ‘ 1 ) )
133 2fveq3 ⊢ ( 𝑛 = 1 → ( 𝐹 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 1 ) ) )
134 132 133 eqeq12d ⊢ ( 𝑛 = 1 → ( ( 𝐻 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑛 ) ) ↔ ( 𝐻 ‘ 1 ) = ( 𝐹 ‘ ( 𝐺 ‘ 1 ) ) ) )
135 134 imbi2d ⊢ ( 𝑛 = 1 → ( ( 𝜑 → ( 𝐻 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ↔ ( 𝜑 → ( 𝐻 ‘ 1 ) = ( 𝐹 ‘ ( 𝐺 ‘ 1 ) ) ) ) )
136 10 expcom ⊢ ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( 𝜑 → ( 𝐻 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
137 135 136 vtoclga ⊢ ( 1 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( 𝜑 → ( 𝐻 ‘ 1 ) = ( 𝐹 ‘ ( 𝐺 ‘ 1 ) ) ) )
138 44 137 mpcom ⊢ ( 𝜑 → ( 𝐻 ‘ 1 ) = ( 𝐹 ‘ ( 𝐺 ‘ 1 ) ) )
139 131 138 eqtr4d ⊢ ( 𝜑 → ( seq ( 𝐺 ‘ 1 ) ( + , 𝐹 ) ‘ ( 𝐺 ‘ 1 ) ) = ( 𝐻 ‘ 1 ) )
140 126 129 139 3eqtr3d ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 1 ) ) = ( 𝐻 ‘ 1 ) )
141 1z ⊢ 1 ∈ ℤ
142 seq1 ⊢ ( 1 ∈ ℤ → ( seq 1 ( + , 𝐻 ) ‘ 1 ) = ( 𝐻 ‘ 1 ) )
143 141 142 ax-mp ⊢ ( seq 1 ( + , 𝐻 ) ‘ 1 ) = ( 𝐻 ‘ 1 )
144 140 143 eqtr4di ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 1 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 1 ) )
145 144 a1d ⊢ ( 𝜑 → ( 1 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 1 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 1 ) ) )
146 simplr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝑚 ∈ ℕ )
147 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
148 146 147 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝑚 ∈ ( ℤ≥ ‘ 1 ) )
149 nnz ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℤ )
150 149 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝑚 ∈ ℤ )
151 elfzuz3 ⊢ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) )
152 151 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) )
153 peano2uzr ⊢ ( ( 𝑚 ∈ ℤ ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑚 ) )
154 150 152 153 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑚 ) )
155 elfzuzb ⊢ ( 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↔ ( 𝑚 ∈ ( ℤ≥ ‘ 1 ) ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑚 ) ) )
156 148 154 155 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
157 156 ex ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) )
158 157 imim1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑚 ) ) → ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑚 ) ) ) )
159 oveq1 ⊢ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑚 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) + ( 𝐻 ‘ ( 𝑚 + 1 ) ) ) = ( ( seq 1 ( + , 𝐻 ) ‘ 𝑚 ) + ( 𝐻 ‘ ( 𝑚 + 1 ) ) ) )
160 2 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ 𝑆 ) → ( 𝑘 + 𝑍 ) = 𝑘 )
161 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
162 40 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝐺 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
163 162 156 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐺 ‘ 𝑚 ) ∈ 𝐴 )
164 161 163 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐺 ‘ 𝑚 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
165 nnre ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ )
166 165 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝑚 ∈ ℝ )
167 166 ltp1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝑚 < ( 𝑚 + 1 ) )
168 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝐺 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
169 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
170 isorel ⊢ ( ( 𝐺 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ∧ ( 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) → ( 𝑚 < ( 𝑚 + 1 ) ↔ ( 𝐺 ‘ 𝑚 ) < ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) )
171 168 156 169 170 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝑚 < ( 𝑚 + 1 ) ↔ ( 𝐺 ‘ 𝑚 ) < ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) )
172 167 171 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐺 ‘ 𝑚 ) < ( 𝐺 ‘ ( 𝑚 + 1 ) ) )
173 eluzelz ⊢ ( ( 𝐺 ‘ 𝑚 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐺 ‘ 𝑚 ) ∈ ℤ )
174 164 173 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐺 ‘ 𝑚 ) ∈ ℤ )
175 162 169 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐺 ‘ ( 𝑚 + 1 ) ) ∈ 𝐴 )
176 161 175 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐺 ‘ ( 𝑚 + 1 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) )
177 eluzelz ⊢ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐺 ‘ ( 𝑚 + 1 ) ) ∈ ℤ )
178 176 177 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐺 ‘ ( 𝑚 + 1 ) ) ∈ ℤ )
179 zltlem1 ⊢ ( ( ( 𝐺 ‘ 𝑚 ) ∈ ℤ ∧ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ∈ ℤ ) → ( ( 𝐺 ‘ 𝑚 ) < ( 𝐺 ‘ ( 𝑚 + 1 ) ) ↔ ( 𝐺 ‘ 𝑚 ) ≤ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) )
180 174 178 179 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐺 ‘ 𝑚 ) < ( 𝐺 ‘ ( 𝑚 + 1 ) ) ↔ ( 𝐺 ‘ 𝑚 ) ≤ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) )
181 172 180 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐺 ‘ 𝑚 ) ≤ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) )
182 peano2zm ⊢ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) ∈ ℤ → ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ∈ ℤ )
183 178 182 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ∈ ℤ )
184 eluz ⊢ ( ( ( 𝐺 ‘ 𝑚 ) ∈ ℤ ∧ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ∈ ℤ ) → ( ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑚 ) ) ↔ ( 𝐺 ‘ 𝑚 ) ≤ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) )
185 174 183 184 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑚 ) ) ↔ ( 𝐺 ‘ 𝑚 ) ≤ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) )
186 181 185 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑚 ) ) )
187 183 zred ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ∈ ℝ )
188 178 zred ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐺 ‘ ( 𝑚 + 1 ) ) ∈ ℝ )
189 83 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ℝ )
190 188 lem1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ≤ ( 𝐺 ‘ ( 𝑚 + 1 ) ) )
191 elfzle2 ⊢ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( 𝑚 + 1 ) ≤ ( ♯ ‘ 𝐴 ) )
192 191 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝑚 + 1 ) ≤ ( ♯ ‘ 𝐴 ) )
193 54 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 1 ... ( ♯ ‘ 𝐴 ) ) ⊆ ℝ* )
194 58 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝐴 ⊆ ℝ* )
195 60 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
196 leisorel ⊢ ( ( 𝐺 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ∧ ( ( 1 ... ( ♯ ‘ 𝐴 ) ) ⊆ ℝ* ∧ 𝐴 ⊆ ℝ* ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) → ( ( 𝑚 + 1 ) ≤ ( ♯ ‘ 𝐴 ) ↔ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ≤ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
197 168 193 194 169 195 196 syl122anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝑚 + 1 ) ≤ ( ♯ ‘ 𝐴 ) ↔ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ≤ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
198 192 197 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐺 ‘ ( 𝑚 + 1 ) ) ≤ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) )
199 187 188 189 190 198 letrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ≤ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) )
200 67 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ℤ )
201 eluz ⊢ ( ( ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ∈ ℤ ∧ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ℤ ) → ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) ↔ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ≤ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
202 183 200 201 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) ↔ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ≤ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
203 199 202 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) )
204 uztrn ⊢ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) ∧ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑚 ) ) ) → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑚 ) ) )
205 203 186 204 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑚 ) ) )
206 fzss2 ⊢ ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑚 ) ) → ( 𝑀 ... ( 𝐺 ‘ 𝑚 ) ) ⊆ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
207 205 206 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝑀 ... ( 𝐺 ‘ 𝑚 ) ) ⊆ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
208 207 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... ( 𝐺 ‘ 𝑚 ) ) ) → 𝑘 ∈ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
209 8 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 )
210 208 209 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... ( 𝐺 ‘ 𝑚 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 )
211 3 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆 ) ) → ( 𝑘 + 𝑛 ) ∈ 𝑆 )
212 164 210 211 seqcl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) ∈ 𝑆 )
213 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ 𝑚 ) + 1 ) ... ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) ) → 𝜑 )
214 elfzuz ⊢ ( 𝑘 ∈ ( ( ( 𝐺 ‘ 𝑚 ) + 1 ) ... ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝐺 ‘ 𝑚 ) + 1 ) ) )
215 peano2uz ⊢ ( ( 𝐺 ‘ 𝑚 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝐺 ‘ 𝑚 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
216 164 215 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐺 ‘ 𝑚 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
217 uztrn ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝐺 ‘ 𝑚 ) + 1 ) ) ∧ ( ( 𝐺 ‘ 𝑚 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
218 214 216 217 syl2anr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ 𝑚 ) + 1 ) ... ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
219 elfzuz3 ⊢ ( 𝑘 ∈ ( ( ( 𝐺 ‘ 𝑚 ) + 1 ) ... ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) → ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ∈ ( ℤ≥ ‘ 𝑘 ) )
220 uztrn ⊢ ( ( ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) ∧ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ 𝑘 ) )
221 203 219 220 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ 𝑚 ) + 1 ) ... ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) ) → ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ 𝑘 ) )
222 elfzuzb ⊢ ( 𝑘 ∈ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ↔ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ 𝑘 ) ) )
223 218 221 222 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ 𝑚 ) + 1 ) ... ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) ) → 𝑘 ∈ ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) )
224 149 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → 𝑚 ∈ ℤ )
225 102 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ◡ 𝐺 : 𝐴 ⟶ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
226 simprr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → 𝑘 ∈ 𝐴 )
227 225 226 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ◡ 𝐺 ‘ 𝑘 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
228 227 elfzelzd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ◡ 𝐺 ‘ 𝑘 ) ∈ ℤ )
229 btwnnz ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑚 < ( ◡ 𝐺 ‘ 𝑘 ) ∧ ( ◡ 𝐺 ‘ 𝑘 ) < ( 𝑚 + 1 ) ) → ¬ ( ◡ 𝐺 ‘ 𝑘 ) ∈ ℤ )
230 229 3expib ⊢ ( 𝑚 ∈ ℤ → ( ( 𝑚 < ( ◡ 𝐺 ‘ 𝑘 ) ∧ ( ◡ 𝐺 ‘ 𝑘 ) < ( 𝑚 + 1 ) ) → ¬ ( ◡ 𝐺 ‘ 𝑘 ) ∈ ℤ ) )
231 230 con2d ⊢ ( 𝑚 ∈ ℤ → ( ( ◡ 𝐺 ‘ 𝑘 ) ∈ ℤ → ¬ ( 𝑚 < ( ◡ 𝐺 ‘ 𝑘 ) ∧ ( ◡ 𝐺 ‘ 𝑘 ) < ( 𝑚 + 1 ) ) ) )
232 224 228 231 sylc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ¬ ( 𝑚 < ( ◡ 𝐺 ‘ 𝑘 ) ∧ ( ◡ 𝐺 ‘ 𝑘 ) < ( 𝑚 + 1 ) ) )
233 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → 𝐺 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
234 156 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
235 isorel ⊢ ( ( 𝐺 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ∧ ( 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ ( ◡ 𝐺 ‘ 𝑘 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) → ( 𝑚 < ( ◡ 𝐺 ‘ 𝑘 ) ↔ ( 𝐺 ‘ 𝑚 ) < ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) )
236 233 234 227 235 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ( 𝑚 < ( ◡ 𝐺 ‘ 𝑘 ) ↔ ( 𝐺 ‘ 𝑚 ) < ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ) )
237 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → 𝐺 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
238 237 226 114 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) = 𝑘 )
239 238 breq2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ( 𝐺 ‘ 𝑚 ) < ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) ↔ ( 𝐺 ‘ 𝑚 ) < 𝑘 ) )
240 174 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ( 𝐺 ‘ 𝑚 ) ∈ ℤ )
241 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
242 241 226 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
243 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℤ )
244 242 243 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → 𝑘 ∈ ℤ )
245 zltp1le ⊢ ( ( ( 𝐺 ‘ 𝑚 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝐺 ‘ 𝑚 ) < 𝑘 ↔ ( ( 𝐺 ‘ 𝑚 ) + 1 ) ≤ 𝑘 ) )
246 240 244 245 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ( 𝐺 ‘ 𝑚 ) < 𝑘 ↔ ( ( 𝐺 ‘ 𝑚 ) + 1 ) ≤ 𝑘 ) )
247 236 239 246 3bitrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ( 𝑚 < ( ◡ 𝐺 ‘ 𝑘 ) ↔ ( ( 𝐺 ‘ 𝑚 ) + 1 ) ≤ 𝑘 ) )
248 169 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) )
249 isorel ⊢ ( ( 𝐺 Isom < , < ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ∧ ( ( ◡ 𝐺 ‘ 𝑘 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) → ( ( ◡ 𝐺 ‘ 𝑘 ) < ( 𝑚 + 1 ) ↔ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) < ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) )
250 233 227 248 249 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ( ◡ 𝐺 ‘ 𝑘 ) < ( 𝑚 + 1 ) ↔ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) < ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) )
251 238 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝑘 ) ) < ( 𝐺 ‘ ( 𝑚 + 1 ) ) ↔ 𝑘 < ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) )
252 178 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ( 𝐺 ‘ ( 𝑚 + 1 ) ) ∈ ℤ )
253 zltlem1 ⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ∈ ℤ ) → ( 𝑘 < ( 𝐺 ‘ ( 𝑚 + 1 ) ) ↔ 𝑘 ≤ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) )
254 244 252 253 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ( 𝑘 < ( 𝐺 ‘ ( 𝑚 + 1 ) ) ↔ 𝑘 ≤ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) )
255 250 251 254 3bitrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ( ◡ 𝐺 ‘ 𝑘 ) < ( 𝑚 + 1 ) ↔ 𝑘 ≤ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) )
256 247 255 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ( ( 𝑚 < ( ◡ 𝐺 ‘ 𝑘 ) ∧ ( ◡ 𝐺 ‘ 𝑘 ) < ( 𝑚 + 1 ) ) ↔ ( ( ( 𝐺 ‘ 𝑚 ) + 1 ) ≤ 𝑘 ∧ 𝑘 ≤ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) ) )
257 232 256 mtbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) ) → ¬ ( ( ( 𝐺 ‘ 𝑚 ) + 1 ) ≤ 𝑘 ∧ 𝑘 ≤ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) )
258 257 expr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝑘 ∈ 𝐴 → ¬ ( ( ( 𝐺 ‘ 𝑚 ) + 1 ) ≤ 𝑘 ∧ 𝑘 ≤ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) ) )
259 258 con2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( ( 𝐺 ‘ 𝑚 ) + 1 ) ≤ 𝑘 ∧ 𝑘 ≤ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) → ¬ 𝑘 ∈ 𝐴 ) )
260 elfzle1 ⊢ ( 𝑘 ∈ ( ( ( 𝐺 ‘ 𝑚 ) + 1 ) ... ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) → ( ( 𝐺 ‘ 𝑚 ) + 1 ) ≤ 𝑘 )
261 elfzle2 ⊢ ( 𝑘 ∈ ( ( ( 𝐺 ‘ 𝑚 ) + 1 ) ... ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) → 𝑘 ≤ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) )
262 260 261 jca ⊢ ( 𝑘 ∈ ( ( ( 𝐺 ‘ 𝑚 ) + 1 ) ... ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) → ( ( ( 𝐺 ‘ 𝑚 ) + 1 ) ≤ 𝑘 ∧ 𝑘 ≤ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) )
263 259 262 impel ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ 𝑚 ) + 1 ) ... ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) ) → ¬ 𝑘 ∈ 𝐴 )
264 223 263 eldifd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ 𝑚 ) + 1 ) ... ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) ) → 𝑘 ∈ ( ( 𝑀 ... ( 𝐺 ‘ ( ♯ ‘ 𝐴 ) ) ) ∖ 𝐴 ) )
265 213 264 9 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( ( ( 𝐺 ‘ 𝑚 ) + 1 ) ... ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
266 160 164 186 212 265 seqid2 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) )
267 266 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) + ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) + ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) ) )
268 fveq2 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝐻 ‘ 𝑛 ) = ( 𝐻 ‘ ( 𝑚 + 1 ) ) )
269 2fveq3 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) )
270 268 269 eqeq12d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝐻 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑛 ) ) ↔ ( 𝐻 ‘ ( 𝑚 + 1 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) ) )
271 270 imbi2d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝜑 → ( 𝐻 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ↔ ( 𝜑 → ( 𝐻 ‘ ( 𝑚 + 1 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) ) ) )
272 271 136 vtoclga ⊢ ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( 𝜑 → ( 𝐻 ‘ ( 𝑚 + 1 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) ) )
273 272 impcom ⊢ ( ( 𝜑 ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐻 ‘ ( 𝑚 + 1 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) )
274 273 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐻 ‘ ( 𝑚 + 1 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) )
275 274 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) + ( 𝐻 ‘ ( 𝑚 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) + ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) ) )
276 93 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → 𝑀 ∈ ℤ )
277 178 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐺 ‘ ( 𝑚 + 1 ) ) ∈ ℂ )
278 ax-1cn ⊢ 1 ∈ ℂ
279 npcan ⊢ ( ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) + 1 ) = ( 𝐺 ‘ ( 𝑚 + 1 ) ) )
280 277 278 279 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) + 1 ) = ( 𝐺 ‘ ( 𝑚 + 1 ) ) )
281 uztrn ⊢ ( ( ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑚 ) ) ∧ ( 𝐺 ‘ 𝑚 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
282 186 164 281 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
283 eluzp1p1 ⊢ ( ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
284 282 283 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
285 280 284 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐺 ‘ ( 𝑚 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
286 seqm1 ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) + ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) ) )
287 276 285 286 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝐺 ‘ ( 𝑚 + 1 ) ) − 1 ) ) + ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) ) )
288 267 275 287 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) + ( 𝐻 ‘ ( 𝑚 + 1 ) ) ) )
289 seqp1 ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , 𝐻 ) ‘ ( 𝑚 + 1 ) ) = ( ( seq 1 ( + , 𝐻 ) ‘ 𝑚 ) + ( 𝐻 ‘ ( 𝑚 + 1 ) ) ) )
290 148 289 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( seq 1 ( + , 𝐻 ) ‘ ( 𝑚 + 1 ) ) = ( ( seq 1 ( + , 𝐻 ) ‘ 𝑚 ) + ( 𝐻 ‘ ( 𝑚 + 1 ) ) ) )
291 288 290 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑚 + 1 ) ) ↔ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) + ( 𝐻 ‘ ( 𝑚 + 1 ) ) ) = ( ( seq 1 ( + , 𝐻 ) ‘ 𝑚 ) + ( 𝐻 ‘ ( 𝑚 + 1 ) ) ) ) )
292 159 291 imbitrrid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑚 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑚 + 1 ) ) ) )
293 292 ex ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑚 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑚 + 1 ) ) ) ) )
294 293 a2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑚 ) ) → ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑚 + 1 ) ) ) ) )
295 158 294 syld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑚 ) ) → ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑚 + 1 ) ) ) ) )
296 295 expcom ⊢ ( 𝑚 ∈ ℕ → ( 𝜑 → ( ( 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑚 ) ) → ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑚 + 1 ) ) ) ) ) )
297 296 a2d ⊢ ( 𝑚 ∈ ℕ → ( ( 𝜑 → ( 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑚 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑚 ) ) ) → ( 𝜑 → ( ( 𝑚 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( 𝑚 + 1 ) ) ) ) ) )
298 18 24 30 36 145 297 nnind ⊢ ( 𝑁 ∈ ℕ → ( 𝜑 → ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑁 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑁 ) ) ) )
299 12 298 mpcom ⊢ ( 𝜑 → ( 𝑁 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑁 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑁 ) ) )
300 6 299 mpd ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐺 ‘ 𝑁 ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑁 ) )