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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐾 ) ∈ 𝐶 )
32 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
33 seq1 ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) = ( 𝐺 ‘ 𝑀 ) )
34 4 32 33 3syl ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) = ( 𝐺 ‘ 𝑀 ) )
35 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
36 4 35 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
37 8 36 sseldd ⊢ ( 𝜑 → 𝑀 ∈ 𝐴 )
38 6 37 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑀 ) ∈ 𝐶 )
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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐶 )
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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐺 ‘ ( 𝑛 + 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 imbitrrid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( 𝐺 ‘ 𝐾 ) + ( 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 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) + ( 𝐺 ‘ 𝐾 ) ) )