Metamath Proof Explorer


Theorem seqf1olem2a

Description: Lemma for seqf1o . (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses seqf1o.1 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
seqf1o.2 ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐶 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
seqf1o.3 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆𝑧𝑆 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
seqf1o.4 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
seqf1o.5 ( 𝜑𝐶𝑆 )
seqf1olem2a.1 ( 𝜑𝐺 : 𝐴𝐶 )
seqf1olem2a.3 ( 𝜑𝐾𝐴 )
seqf1olem2a.4 ( 𝜑 → ( 𝑀 ... 𝑁 ) ⊆ 𝐴 )
Assertion seqf1olem2a ( 𝜑 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) + ( 𝐺𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 seqf1o.1 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
2 seqf1o.2 ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐶 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
3 seqf1o.3 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆𝑧𝑆 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
4 seqf1o.4 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
5 seqf1o.5 ( 𝜑𝐶𝑆 )
6 seqf1olem2a.1 ( 𝜑𝐺 : 𝐴𝐶 )
7 seqf1olem2a.3 ( 𝜑𝐾𝐴 )
8 seqf1olem2a.4 ( 𝜑 → ( 𝑀 ... 𝑁 ) ⊆ 𝐴 )
9 eluzfz2 ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
10 4 9 syl ( 𝜑𝑁 ∈ ( 𝑀 ... 𝑁 ) )
11 fveq2 ( 𝑚 = 𝑀 → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) )
12 11 oveq2d ( 𝑚 = 𝑀 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) = ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) ) )
13 11 oveq1d ( 𝑚 = 𝑀 → ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) + ( 𝐺𝐾 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) + ( 𝐺𝐾 ) ) )
14 12 13 eqeq12d ( 𝑚 = 𝑀 → ( ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) + ( 𝐺𝐾 ) ) ↔ ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) + ( 𝐺𝐾 ) ) ) )
15 14 imbi2d ( 𝑚 = 𝑀 → ( ( 𝜑 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) + ( 𝐺𝐾 ) ) ) ↔ ( 𝜑 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) + ( 𝐺𝐾 ) ) ) ) )
16 fveq2 ( 𝑚 = 𝑛 → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) )
17 16 oveq2d ( 𝑚 = 𝑛 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) = ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) )
18 16 oveq1d ( 𝑚 = 𝑛 → ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) + ( 𝐺𝐾 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺𝐾 ) ) )
19 17 18 eqeq12d ( 𝑚 = 𝑛 → ( ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) + ( 𝐺𝐾 ) ) ↔ ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺𝐾 ) ) ) )
20 19 imbi2d ( 𝑚 = 𝑛 → ( ( 𝜑 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) + ( 𝐺𝐾 ) ) ) ↔ ( 𝜑 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺𝐾 ) ) ) ) )
21 fveq2 ( 𝑚 = ( 𝑛 + 1 ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) )
22 21 oveq2d ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) = ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) )
23 21 oveq1d ( 𝑚 = ( 𝑛 + 1 ) → ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) + ( 𝐺𝐾 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) + ( 𝐺𝐾 ) ) )
24 22 23 eqeq12d ( 𝑚 = ( 𝑛 + 1 ) → ( ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) + ( 𝐺𝐾 ) ) ↔ ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) + ( 𝐺𝐾 ) ) ) )
25 24 imbi2d ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) + ( 𝐺𝐾 ) ) ) ↔ ( 𝜑 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) + ( 𝐺𝐾 ) ) ) ) )
26 fveq2 ( 𝑚 = 𝑁 → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) )
27 26 oveq2d ( 𝑚 = 𝑁 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) = ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )
28 26 oveq1d ( 𝑚 = 𝑁 → ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) + ( 𝐺𝐾 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) + ( 𝐺𝐾 ) ) )
29 27 28 eqeq12d ( 𝑚 = 𝑁 → ( ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) + ( 𝐺𝐾 ) ) ↔ ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) + ( 𝐺𝐾 ) ) ) )
30 29 imbi2d ( 𝑚 = 𝑁 → ( ( 𝜑 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑚 ) + ( 𝐺𝐾 ) ) ) ↔ ( 𝜑 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) + ( 𝐺𝐾 ) ) ) ) )
31 6 7 ffvelrnd ( 𝜑 → ( 𝐺𝐾 ) ∈ 𝐶 )
32 eluzel2 ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑀 ∈ ℤ )
33 seq1 ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) = ( 𝐺𝑀 ) )
34 4 32 33 3syl ( 𝜑 → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) = ( 𝐺𝑀 ) )
35 eluzfz1 ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
36 4 35 syl ( 𝜑𝑀 ∈ ( 𝑀 ... 𝑁 ) )
37 8 36 sseldd ( 𝜑𝑀𝐴 )
38 6 37 ffvelrnd ( 𝜑 → ( 𝐺𝑀 ) ∈ 𝐶 )
39 34 38 eqeltrd ( 𝜑 → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) ∈ 𝐶 )
40 2 31 39 caovcomd ( 𝜑 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) + ( 𝐺𝐾 ) ) )
41 40 a1i ( 𝑁 ∈ ( ℤ𝑀 ) → ( 𝜑 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) + ( 𝐺𝐾 ) ) ) )
42 oveq1 ( ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺𝐾 ) ) → ( ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) = ( ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺𝐾 ) ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
43 elfzouz ( 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑛 ∈ ( ℤ𝑀 ) )
44 43 adantl ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑛 ∈ ( ℤ𝑀 ) )
45 seqp1 ( 𝑛 ∈ ( ℤ𝑀 ) → ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
46 44 45 syl ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
47 46 oveq2d ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( 𝐺𝐾 ) + ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
48 3 adantlr ( ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥𝑆𝑦𝑆𝑧𝑆 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
49 5 31 sseldd ( 𝜑 → ( 𝐺𝐾 ) ∈ 𝑆 )
50 49 adantr ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐺𝐾 ) ∈ 𝑆 )
51 5 adantr ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐶𝑆 )
52 51 adantr ( ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑛 ) ) → 𝐶𝑆 )
53 6 adantr ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐺 : 𝐴𝐶 )
54 53 adantr ( ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑛 ) ) → 𝐺 : 𝐴𝐶 )
55 elfzouz2 ( 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ( ℤ𝑛 ) )
56 55 adantl ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑁 ∈ ( ℤ𝑛 ) )
57 fzss2 ( 𝑁 ∈ ( ℤ𝑛 ) → ( 𝑀 ... 𝑛 ) ⊆ ( 𝑀 ... 𝑁 ) )
58 56 57 syl ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 ... 𝑛 ) ⊆ ( 𝑀 ... 𝑁 ) )
59 8 adantr ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 ... 𝑁 ) ⊆ 𝐴 )
60 58 59 sstrd ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 ... 𝑛 ) ⊆ 𝐴 )
61 60 sselda ( ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑛 ) ) → 𝑥𝐴 )
62 54 61 ffvelrnd ( ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐺𝑥 ) ∈ 𝐶 )
63 52 62 sseldd ( ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐺𝑥 ) ∈ 𝑆 )
64 1 adantlr ( ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
65 44 63 64 seqcl ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ 𝑆 )
66 fzofzp1 ( 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
67 66 adantl ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
68 59 67 sseldd ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑛 + 1 ) ∈ 𝐴 )
69 53 68 ffvelrnd ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐺 ‘ ( 𝑛 + 1 ) ) ∈ 𝐶 )
70 51 69 sseldd ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐺 ‘ ( 𝑛 + 1 ) ) ∈ 𝑆 )
71 48 50 65 70 caovassd ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) = ( ( 𝐺𝐾 ) + ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
72 47 71 eqtr4d ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
73 48 65 70 50 caovassd ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) + ( 𝐺𝐾 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( ( 𝐺 ‘ ( 𝑛 + 1 ) ) + ( 𝐺𝐾 ) ) ) )
74 46 oveq1d ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) + ( 𝐺𝐾 ) ) = ( ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) + ( 𝐺𝐾 ) ) )
75 48 65 50 70 caovassd ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺𝐾 ) ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( ( 𝐺𝐾 ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
76 2 adantlr ( ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥𝐶𝑦𝐶 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
77 31 adantr ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐺𝐾 ) ∈ 𝐶 )
78 76 69 77 caovcomd ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ ( 𝑛 + 1 ) ) + ( 𝐺𝐾 ) ) = ( ( 𝐺𝐾 ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
79 78 oveq2d ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( ( 𝐺 ‘ ( 𝑛 + 1 ) ) + ( 𝐺𝐾 ) ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( ( 𝐺𝐾 ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
80 75 79 eqtr4d ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺𝐾 ) ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( ( 𝐺 ‘ ( 𝑛 + 1 ) ) + ( 𝐺𝐾 ) ) ) )
81 73 74 80 3eqtr4d ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) + ( 𝐺𝐾 ) ) = ( ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺𝐾 ) ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
82 72 81 eqeq12d ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) + ( 𝐺𝐾 ) ) ↔ ( ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) = ( ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺𝐾 ) ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
83 42 82 syl5ibr ( ( 𝜑𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺𝐾 ) ) → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) + ( 𝐺𝐾 ) ) ) )
84 83 expcom ( 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝜑 → ( ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺𝐾 ) ) → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) + ( 𝐺𝐾 ) ) ) ) )
85 84 a2d ( 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) → ( ( 𝜑 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺𝐾 ) ) ) → ( 𝜑 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) + ( 𝐺𝐾 ) ) ) ) )
86 15 20 25 30 41 85 fzind2 ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( 𝜑 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) + ( 𝐺𝐾 ) ) ) )
87 10 86 mpcom ( 𝜑 → ( ( 𝐺𝐾 ) + ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) + ( 𝐺𝐾 ) ) )