This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isercolllem3

Description: Lemma for isercoll . (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses isercoll.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
isercoll.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
isercoll.g ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ 𝑍 )
isercoll.i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) < ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
isercoll.0 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑍 ∖ ran 𝐺 ) ) → ( 𝐹 ‘ 𝑛 ) = 0 )
isercoll.f ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
isercoll.h ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
Assertion isercolllem3 ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isercoll.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 isercoll.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 isercoll.g ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ 𝑍 )
4 isercoll.i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) < ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
5 isercoll.0 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑍 ∖ ran 𝐺 ) ) → ( 𝐹 ‘ 𝑛 ) = 0 )
6 isercoll.f ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
7 isercoll.h ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
8 addlid ⊢ ( 𝑛 ∈ ℂ → ( 0 + 𝑛 ) = 𝑛 )
9 8 adantl ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑛 ∈ ℂ ) → ( 0 + 𝑛 ) = 𝑛 )
10 addrid ⊢ ( 𝑛 ∈ ℂ → ( 𝑛 + 0 ) = 𝑛 )
11 10 adantl ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑛 ∈ ℂ ) → ( 𝑛 + 0 ) = 𝑛 )
12 addcl ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝑛 + 𝑘 ) ∈ ℂ )
13 12 adantl ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ ) ) → ( 𝑛 + 𝑘 ) ∈ ℂ )
14 0cnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → 0 ∈ ℂ )
15 cnvimass ⊢ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ⊆ dom 𝐺
16 3 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → 𝐺 : ℕ ⟶ 𝑍 )
17 15 16 fssdm ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ⊆ ℕ )
18 1 2 3 4 isercolllem1 ⊢ ( ( 𝜑 ∧ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ⊆ ℕ ) → ( 𝐺 ↾ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) Isom < , < ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) )
19 17 18 syldan ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 ↾ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) Isom < , < ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) )
20 1 2 3 4 isercolllem2 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 1 ... ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) = ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) )
21 isoeq4 ⊢ ( ( 1 ... ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) = ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐺 ↾ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) Isom < , < ( ( 1 ... ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) , ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ↔ ( 𝐺 ↾ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) Isom < , < ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) )
22 20 21 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ( 𝐺 ↾ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) Isom < , < ( ( 1 ... ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) , ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ↔ ( 𝐺 ↾ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) Isom < , < ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) , ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) )
23 19 22 mpbird ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 ↾ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) Isom < , < ( ( 1 ... ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) , ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) )
24 15 a1i ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ⊆ dom 𝐺 )
25 sseqin2 ⊢ ( ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ⊆ dom 𝐺 ↔ ( dom 𝐺 ∩ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) = ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) )
26 24 25 sylib ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( dom 𝐺 ∩ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) = ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) )
27 1nn ⊢ 1 ∈ ℕ
28 27 a1i ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → 1 ∈ ℕ )
29 ffvelcdm ⊢ ( ( 𝐺 : ℕ ⟶ 𝑍 ∧ 1 ∈ ℕ ) → ( 𝐺 ‘ 1 ) ∈ 𝑍 )
30 3 27 29 sylancl ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) ∈ 𝑍 )
31 30 1 eleqtrdi ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 ‘ 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) )
34 elfzuzb ⊢ ( ( 𝐺 ‘ 1 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝐺 ‘ 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) )
35 32 33 34 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 ‘ 1 ) ∈ ( 𝑀 ... 𝑁 ) )
36 ffn ⊢ ( 𝐺 : ℕ ⟶ 𝑍 → 𝐺 Fn ℕ )
37 elpreima ⊢ ( 𝐺 Fn ℕ → ( 1 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ↔ ( 1 ∈ ℕ ∧ ( 𝐺 ‘ 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) )
38 16 36 37 3syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 1 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ↔ ( 1 ∈ ℕ ∧ ( 𝐺 ‘ 1 ) ∈ ( 𝑀 ... 𝑁 ) ) ) )
39 28 35 38 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → 1 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) )
40 39 ne0d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ≠ ∅ )
41 26 40 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( dom 𝐺 ∩ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ≠ ∅ )
42 imadisj ⊢ ( ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) = ∅ ↔ ( dom 𝐺 ∩ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) = ∅ )
43 42 necon3bii ⊢ ( ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ≠ ∅ ↔ ( dom 𝐺 ∩ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ≠ ∅ )
44 41 43 sylibr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ≠ ∅ )
45 ffun ⊢ ( 𝐺 : ℕ ⟶ 𝑍 → Fun 𝐺 )
46 funimacnv ⊢ ( Fun 𝐺 → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) = ( ( 𝑀 ... 𝑁 ) ∩ ran 𝐺 ) )
47 16 45 46 3syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) = ( ( 𝑀 ... 𝑁 ) ∩ ran 𝐺 ) )
48 inss1 ⊢ ( ( 𝑀 ... 𝑁 ) ∩ ran 𝐺 ) ⊆ ( 𝑀 ... 𝑁 )
49 47 48 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ⊆ ( 𝑀 ... 𝑁 ) )
50 simpl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → 𝜑 )
51 elfzuz ⊢ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
52 51 1 eleqtrrdi ⊢ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → 𝑛 ∈ 𝑍 )
53 50 52 6 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
54 47 difeq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ( 𝑀 ... 𝑁 ) ∖ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) = ( ( 𝑀 ... 𝑁 ) ∖ ( ( 𝑀 ... 𝑁 ) ∩ ran 𝐺 ) ) )
55 difin ⊢ ( ( 𝑀 ... 𝑁 ) ∖ ( ( 𝑀 ... 𝑁 ) ∩ ran 𝐺 ) ) = ( ( 𝑀 ... 𝑁 ) ∖ ran 𝐺 )
56 54 55 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ( 𝑀 ... 𝑁 ) ∖ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) = ( ( 𝑀 ... 𝑁 ) ∖ ran 𝐺 ) )
57 52 ssriv ⊢ ( 𝑀 ... 𝑁 ) ⊆ 𝑍
58 ssdif ⊢ ( ( 𝑀 ... 𝑁 ) ⊆ 𝑍 → ( ( 𝑀 ... 𝑁 ) ∖ ran 𝐺 ) ⊆ ( 𝑍 ∖ ran 𝐺 ) )
59 57 58 mp1i ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ( 𝑀 ... 𝑁 ) ∖ ran 𝐺 ) ⊆ ( 𝑍 ∖ ran 𝐺 ) )
60 56 59 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ( 𝑀 ... 𝑁 ) ∖ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ⊆ ( 𝑍 ∖ ran 𝐺 ) )
61 60 sselda ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑛 ∈ ( ( 𝑀 ... 𝑁 ) ∖ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) → 𝑛 ∈ ( 𝑍 ∖ ran 𝐺 ) )
62 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑛 ∈ ( 𝑍 ∖ ran 𝐺 ) ) → ( 𝐹 ‘ 𝑛 ) = 0 )
63 61 62 syldan ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑛 ∈ ( ( 𝑀 ... 𝑁 ) ∖ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) → ( 𝐹 ‘ 𝑛 ) = 0 )
64 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) → 𝑘 ∈ ℕ )
65 50 64 7 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
66 20 eleq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝑘 ∈ ( 1 ... ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) ↔ 𝑘 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) )
67 66 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) ) → 𝑘 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) )
68 67 fvresd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) ) → ( ( 𝐺 ↾ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
69 68 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) ) → ( 𝐹 ‘ ( ( 𝐺 ↾ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ‘ 𝑘 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
70 65 69 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ ( ( 𝐺 ↾ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ‘ 𝑘 ) ) )
71 9 11 13 14 23 44 49 53 63 70 seqcoll2 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑁 ) ) ) ) ) )