Metamath Proof Explorer

Theorem seqsplit

Description: Split a sequence into two sequences. (Contributed by NM, 17-Mar-2005) (Revised by Mario Carneiro, 27-May-2014)

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

Proof

Step Hyp Ref Expression
1 seqsplit.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
2 seqsplit.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
3 seqsplit.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
4 seqsplit.4 ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) )
5 seqsplit.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
6 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
7 3 6 syl ⊢ ( 𝜑 → 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
8 eleq1 ⊢ ( 𝑥 = ( 𝑀 + 1 ) → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↔ ( 𝑀 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
9 fveq2 ⊢ ( 𝑥 = ( 𝑀 + 1 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) )
10 fveq2 ⊢ ( 𝑥 = ( 𝑀 + 1 ) → ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) )
11 10 oveq2d ⊢ ( 𝑥 = ( 𝑀 + 1 ) → ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) ) )
12 9 11 eqeq12d ⊢ ( 𝑥 = ( 𝑀 + 1 ) → ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) ) ↔ ( seq 𝐾 ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) ) ) )
13 8 12 imbi12d ⊢ ( 𝑥 = ( 𝑀 + 1 ) → ( ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) ) ) ↔ ( ( 𝑀 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) ) ) ) )
14 13 imbi2d ⊢ ( 𝑥 = ( 𝑀 + 1 ) → ( ( 𝜑 → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) ) ) ) ↔ ( 𝜑 → ( ( 𝑀 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) ) ) ) ) )
15 eleq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↔ 𝑛 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
16 fveq2 ⊢ ( 𝑥 = 𝑛 → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑛 ) )
17 fveq2 ⊢ ( 𝑥 = 𝑛 → ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) )
18 17 oveq2d ⊢ ( 𝑥 = 𝑛 → ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) ) )
19 16 18 eqeq12d ⊢ ( 𝑥 = 𝑛 → ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) ) ↔ ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) ) ) )
20 15 19 imbi12d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) ) ) ↔ ( 𝑛 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) ) ) ) )
21 20 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝜑 → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) ) ) ) ↔ ( 𝜑 → ( 𝑛 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) ) ) ) ) )
22 eleq1 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↔ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
23 fveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) )
24 fveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) )
25 24 oveq2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) )
26 23 25 eqeq12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) ) ↔ ( seq 𝐾 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) )
27 22 26 imbi12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) ) ) ↔ ( ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) ) )
28 27 imbi2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) ) ) ) ↔ ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) ) ) )
29 eleq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ↔ 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
30 fveq2 ⊢ ( 𝑥 = 𝑁 → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑥 ) = ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑁 ) )
31 fveq2 ⊢ ( 𝑥 = 𝑁 → ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) = ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑁 ) )
32 31 oveq2d ⊢ ( 𝑥 = 𝑁 → ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑁 ) ) )
33 30 32 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) ) ↔ ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑁 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
34 29 33 imbi12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) ) ) ↔ ( 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑁 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
35 34 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑥 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑥 ) ) ) ) ↔ ( 𝜑 → ( 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑁 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) ) )
36 seqp1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( 𝐹 ‘ ( 𝑀 + 1 ) ) ) )
37 4 36 syl ⊢ ( 𝜑 → ( seq 𝐾 ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( 𝐹 ‘ ( 𝑀 + 1 ) ) ) )
38 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝑀 + 1 ) ∈ ℤ )
39 seq1 ⊢ ( ( 𝑀 + 1 ) ∈ ℤ → ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) = ( 𝐹 ‘ ( 𝑀 + 1 ) ) )
40 3 38 39 3syl ⊢ ( 𝜑 → ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) = ( 𝐹 ‘ ( 𝑀 + 1 ) ) )
41 40 oveq2d ⊢ ( 𝜑 → ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( 𝐹 ‘ ( 𝑀 + 1 ) ) ) )
42 37 41 eqtr4d ⊢ ( 𝜑 → ( seq 𝐾 ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) ) )
43 42 a1i13 ⊢ ( ( 𝑀 + 1 ) ∈ ℤ → ( 𝜑 → ( ( 𝑀 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) ) ) ) )
44 peano2fzr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑛 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
45 44 adantl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → 𝑛 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
46 45 expr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → 𝑛 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
47 46 imim1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑛 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) ) ) → ( ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) ) ) ) )
48 oveq1 ⊢ ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) ) → ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
49 simprl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
50 peano2uz ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝐾 ) )
51 4 50 syl ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝐾 ) )
52 51 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝐾 ) )
53 uztrn ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) )
54 49 52 53 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) )
55 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝐾 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
56 54 55 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( seq 𝐾 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
57 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
58 49 57 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
59 58 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
60 simpl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → 𝜑 )
61 eluzelz ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝑀 ∈ ℤ )
62 4 61 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
63 peano2uzr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
64 62 3 63 syl2anc ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
65 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ... 𝑀 ) ⊆ ( 𝐾 ... 𝑁 ) )
66 64 65 syl ⊢ ( 𝜑 → ( 𝐾 ... 𝑀 ) ⊆ ( 𝐾 ... 𝑁 ) )
67 66 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐾 ... 𝑀 ) ) → 𝑥 ∈ ( 𝐾 ... 𝑁 ) )
68 67 5 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐾 ... 𝑀 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
69 4 68 1 seqcl ⊢ ( 𝜑 → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) ∈ 𝑆 )
70 69 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) ∈ 𝑆 )
71 elfzuz3 ⊢ ( 𝑛 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑛 ) )
72 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑛 ) → ( ( 𝑀 + 1 ) ... 𝑛 ) ⊆ ( ( 𝑀 + 1 ) ... 𝑁 ) )
73 45 71 72 3syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( 𝑀 + 1 ) ... 𝑛 ) ⊆ ( ( 𝑀 + 1 ) ... 𝑁 ) )
74 fzss1 ⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝐾 ) → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝐾 ... 𝑁 ) )
75 4 50 74 3syl ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝐾 ... 𝑁 ) )
76 75 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝐾 ... 𝑁 ) )
77 73 76 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( 𝑀 + 1 ) ... 𝑛 ) ⊆ ( 𝐾 ... 𝑁 ) )
78 77 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑛 ) ) → 𝑥 ∈ ( 𝐾 ... 𝑁 ) )
79 5 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
80 78 79 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑛 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
81 1 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
82 49 80 81 seqcl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) ∈ 𝑆 )
83 fveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
84 83 eleq1d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ 𝑆 ) )
85 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐾 ... 𝑁 ) ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
86 85 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ∀ 𝑥 ∈ ( 𝐾 ... 𝑁 ) ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
87 simpr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) )
88 ssel2 ⊢ ( ( ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝐾 ... 𝑁 ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) )
89 75 87 88 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( 𝑛 + 1 ) ∈ ( 𝐾 ... 𝑁 ) )
90 84 86 89 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ 𝑆 )
91 2 caovassg ⊢ ( ( 𝜑 ∧ ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) ∈ 𝑆 ∧ ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) ∈ 𝑆 ∧ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ 𝑆 ) ) → ( ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
92 60 70 82 90 91 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
93 59 92 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
94 56 93 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( seq 𝐾 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ↔ ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) )
95 48 94 syl5ibr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) ) → ( seq 𝐾 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) )
96 47 95 animpimp2impd ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( ( 𝜑 → ( 𝑛 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑛 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑛 ) ) ) ) → ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ) ) ) ) )
97 14 21 28 35 43 96 uzind4 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝜑 → ( 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑁 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
98 3 97 mpcom ⊢ ( 𝜑 → ( 𝑁 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑁 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
99 7 98 mpd ⊢ ( 𝜑 → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑁 ) = ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑁 ) ) )