Metamath Proof Explorer

Theorem seqid2

Description: The last few partial sums of a sequence that ends with all zeroes (or any element which is a right-identity for .+ ) are all the same. (Contributed by Mario Carneiro, 13-Jul-2013) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses seqid2.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 + 𝑍 ) = 𝑥 )
seqid2.2 ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
seqid2.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
seqid2.4 ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) ∈ 𝑆 )
seqid2.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) = 𝑍 )
Assertion seqid2 ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 seqid2.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 + 𝑍 ) = 𝑥 )
2 seqid2.2 ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
3 seqid2.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
4 seqid2.4 ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) ∈ 𝑆 )
5 seqid2.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) = 𝑍 )
6 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝑁 ∈ ( 𝐾 ... 𝑁 ) )
7 3 6 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐾 ... 𝑁 ) )
8 eleq1 ⊢ ( 𝑥 = 𝐾 → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) ↔ 𝐾 ∈ ( 𝐾 ... 𝑁 ) ) )
9 fveq2 ⊢ ( 𝑥 = 𝐾 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) )
10 9 eqeq2d ⊢ ( 𝑥 = 𝐾 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) ) )
11 8 10 imbi12d ⊢ ( 𝑥 = 𝐾 → ( ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) ↔ ( 𝐾 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) ) ) )
12 11 imbi2d ⊢ ( 𝑥 = 𝐾 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝐾 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) ) ) ) )
13 eleq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) ↔ 𝑛 ∈ ( 𝐾 ... 𝑁 ) ) )
14 fveq2 ⊢ ( 𝑥 = 𝑛 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) )
15 14 eqeq2d ⊢ ( 𝑥 = 𝑛 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) )
16 13 15 imbi12d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) ↔ ( 𝑛 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ) )
17 16 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑛 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ) ) )
18 eleq1 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) ↔ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) )
19 fveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) )
20 19 eqeq2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) )
21 18 20 imbi12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) ↔ ( ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) )
22 21 imbi2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) ) )
23 eleq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) ↔ 𝑁 ∈ ( 𝐾 ... 𝑁 ) ) )
24 fveq2 ⊢ ( 𝑥 = 𝑁 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
25 24 eqeq2d ⊢ ( 𝑥 = 𝑁 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
26 23 25 imbi12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) ↔ ( 𝑁 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
27 26 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑁 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
28 eqidd ⊢ ( 𝐾 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) )
29 28 2a1i ⊢ ( 𝐾 ∈ ℤ → ( 𝜑 → ( 𝐾 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) ) ) )
30 peano2fzr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) → 𝑛 ∈ ( 𝐾 ... 𝑁 ) )
31 30 adantl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → 𝑛 ∈ ( 𝐾 ... 𝑁 ) )
32 31 expr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) → 𝑛 ∈ ( 𝐾 ... 𝑁 ) ) )
33 32 imim1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝑛 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) → ( ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ) )
34 oveq1 ⊢ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
35 fveqeq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑍 ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) = 𝑍 ) )
36 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝐹 ‘ 𝑥 ) = 𝑍 )
37 36 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ∀ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝐹 ‘ 𝑥 ) = 𝑍 )
38 eluzp1p1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
39 38 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
40 elfzuz3 ⊢ ( ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
41 40 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
42 elfzuzb ⊢ ( ( 𝑛 + 1 ) ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ↔ ( ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) )
43 39 41 42 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( 𝑛 + 1 ) ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) )
44 35 37 43 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) = 𝑍 )
45 44 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) + 𝑍 ) )
46 oveq1 ⊢ ( 𝑥 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) → ( 𝑥 + 𝑍 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) + 𝑍 ) )
47 id ⊢ ( 𝑥 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) → 𝑥 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) )
48 46 47 eqeq12d ⊢ ( 𝑥 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) → ( ( 𝑥 + 𝑍 ) = 𝑥 ↔ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) + 𝑍 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) ) )
49 1 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ( 𝑥 + 𝑍 ) = 𝑥 )
50 48 49 4 rspcdva ⊢ ( 𝜑 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) + 𝑍 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) )
51 50 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) + 𝑍 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) )
52 45 51 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
53 simprl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) )
54 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
55 uztrn ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
56 53 54 55 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
57 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
58 56 57 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
59 52 58 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ↔ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
60 34 59 imbitrrid ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) )
61 33 60 animpimp2impd ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) → ( ( 𝜑 → ( 𝑛 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ) ) → ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) ) )
62 12 17 22 27 29 61 uzind4 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝜑 → ( 𝑁 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
63 3 62 mpcom ⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝐾 ... 𝑁 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
64 7 63 mpd ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )