Metamath Proof Explorer


Theorem seqf1olem2

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

Ref Expression
Hypotheses seqf1o.1 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
seqf1o.2 ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐶 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
seqf1o.3 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆𝑧𝑆 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
seqf1o.4 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
seqf1o.5 ( 𝜑𝐶𝑆 )
seqf1olem.5 ( 𝜑𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑁 + 1 ) ) )
seqf1olem.6 ( 𝜑𝐺 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ 𝐶 )
seqf1olem.7 𝐽 = ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐹 ‘ if ( 𝑘 < 𝐾 , 𝑘 , ( 𝑘 + 1 ) ) ) )
seqf1olem.8 𝐾 = ( 𝐹 ‘ ( 𝑁 + 1 ) )
seqf1olem.9 ( 𝜑 → ∀ 𝑔𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔𝑓 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) ) )
Assertion seqf1olem2 ( 𝜑 → ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) = ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑁 + 1 ) ) )

Proof

Step Hyp Ref Expression
1 seqf1o.1 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
2 seqf1o.2 ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐶 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
3 seqf1o.3 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆𝑧𝑆 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
4 seqf1o.4 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
5 seqf1o.5 ( 𝜑𝐶𝑆 )
6 seqf1olem.5 ( 𝜑𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑁 + 1 ) ) )
7 seqf1olem.6 ( 𝜑𝐺 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ 𝐶 )
8 seqf1olem.7 𝐽 = ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐹 ‘ if ( 𝑘 < 𝐾 , 𝑘 , ( 𝑘 + 1 ) ) ) )
9 seqf1olem.8 𝐾 = ( 𝐹 ‘ ( 𝑁 + 1 ) )
10 seqf1olem.9 ( 𝜑 → ∀ 𝑔𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔𝑓 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) ) )
11 7 ffnd ( 𝜑𝐺 Fn ( 𝑀 ... ( 𝑁 + 1 ) ) )
12 fzssp1 ( 𝑀 ... 𝑁 ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) )
13 fnssres ( ( 𝐺 Fn ( 𝑀 ... ( 𝑁 + 1 ) ) ∧ ( 𝑀 ... 𝑁 ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) Fn ( 𝑀 ... 𝑁 ) )
14 11 12 13 sylancl ( 𝜑 → ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) Fn ( 𝑀 ... 𝑁 ) )
15 fzfid ( 𝜑 → ( 𝑀 ... 𝑁 ) ∈ Fin )
16 fnfi ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) Fn ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ... 𝑁 ) ∈ Fin ) → ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∈ Fin )
17 14 15 16 syl2anc ( 𝜑 → ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∈ Fin )
18 17 elexd ( 𝜑 → ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∈ V )
19 1 2 3 4 5 6 7 8 9 seqf1olem1 ( 𝜑𝐽 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )
20 f1of ( 𝐽 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) → 𝐽 : ( 𝑀 ... 𝑁 ) ⟶ ( 𝑀 ... 𝑁 ) )
21 19 20 syl ( 𝜑𝐽 : ( 𝑀 ... 𝑁 ) ⟶ ( 𝑀 ... 𝑁 ) )
22 fex2 ( ( 𝐽 : ( 𝑀 ... 𝑁 ) ⟶ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ... 𝑁 ) ∈ Fin ∧ ( 𝑀 ... 𝑁 ) ∈ Fin ) → 𝐽 ∈ V )
23 21 15 15 22 syl3anc ( 𝜑𝐽 ∈ V )
24 18 23 jca ( 𝜑 → ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∈ V ∧ 𝐽 ∈ V ) )
25 fssres ( ( 𝐺 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ 𝐶 ∧ ( 𝑀 ... 𝑁 ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 )
26 7 12 25 sylancl ( 𝜑 → ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 )
27 19 26 jca ( 𝜑 → ( 𝐽 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) )
28 f1oeq1 ( 𝑓 = 𝐽 → ( 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ↔ 𝐽 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ) )
29 feq1 ( 𝑔 = ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) → ( 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ↔ ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) )
30 28 29 bi2anan9r ( ( 𝑔 = ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∧ 𝑓 = 𝐽 ) → ( ( 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) ↔ ( 𝐽 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) ) )
31 coeq1 ( 𝑔 = ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) → ( 𝑔𝑓 ) = ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝑓 ) )
32 coeq2 ( 𝑓 = 𝐽 → ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝑓 ) = ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) )
33 31 32 sylan9eq ( ( 𝑔 = ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∧ 𝑓 = 𝐽 ) → ( 𝑔𝑓 ) = ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) )
34 33 seqeq3d ( ( 𝑔 = ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∧ 𝑓 = 𝐽 ) → seq 𝑀 ( + , ( 𝑔𝑓 ) ) = seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) )
35 34 fveq1d ( ( 𝑔 = ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∧ 𝑓 = 𝐽 ) → ( seq 𝑀 ( + , ( 𝑔𝑓 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) )
36 simpl ( ( 𝑔 = ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∧ 𝑓 = 𝐽 ) → 𝑔 = ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) )
37 36 seqeq3d ( ( 𝑔 = ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∧ 𝑓 = 𝐽 ) → seq 𝑀 ( + , 𝑔 ) = seq 𝑀 ( + , ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ) )
38 37 fveq1d ( ( 𝑔 = ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∧ 𝑓 = 𝐽 ) → ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ) ‘ 𝑁 ) )
39 35 38 eqeq12d ( ( 𝑔 = ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∧ 𝑓 = 𝐽 ) → ( ( seq 𝑀 ( + , ( 𝑔𝑓 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) ↔ ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ) ‘ 𝑁 ) ) )
40 30 39 imbi12d ( ( 𝑔 = ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∧ 𝑓 = 𝐽 ) → ( ( ( 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔𝑓 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) ) ↔ ( ( 𝐽 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ) ‘ 𝑁 ) ) ) )
41 40 spc2gv ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∈ V ∧ 𝐽 ∈ V ) → ( ∀ 𝑔𝑓 ( ( 𝑓 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ 𝑔 : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( 𝑔𝑓 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝑔 ) ‘ 𝑁 ) ) → ( ( 𝐽 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ∧ ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐶 ) → ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ) ‘ 𝑁 ) ) ) )
42 24 10 27 41 syl3c ( 𝜑 → ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ) ‘ 𝑁 ) )
43 fvres ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ‘ 𝑥 ) = ( 𝐺𝑥 ) )
44 43 adantl ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ‘ 𝑥 ) = ( 𝐺𝑥 ) )
45 4 44 seqfveq ( 𝜑 → ( seq 𝑀 ( + , ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) )
46 42 45 eqtrd ( 𝜑 → ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) )
47 46 oveq1d ( 𝜑 → ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
48 1 adantlr ( ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
49 3 adantlr ( ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ∧ ( 𝑥𝑆𝑦𝑆𝑧𝑆 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
50 elfzuz3 ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ𝐾 ) )
51 50 adantl ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ𝐾 ) )
52 eluzp1p1 ( 𝑁 ∈ ( ℤ𝐾 ) → ( 𝑁 + 1 ) ∈ ( ℤ ‘ ( 𝐾 + 1 ) ) )
53 51 52 syl ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑁 + 1 ) ∈ ( ℤ ‘ ( 𝐾 + 1 ) ) )
54 elfzuz ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ( ℤ𝑀 ) )
55 54 adantl ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ( ℤ𝑀 ) )
56 f1of ( 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑁 + 1 ) ) → 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ ( 𝑀 ... ( 𝑁 + 1 ) ) )
57 6 56 syl ( 𝜑𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ ( 𝑀 ... ( 𝑁 + 1 ) ) )
58 fco ( ( 𝐺 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ 𝐶𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → ( 𝐺𝐹 ) : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ 𝐶 )
59 7 57 58 syl2anc ( 𝜑 → ( 𝐺𝐹 ) : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ 𝐶 )
60 59 5 fssd ( 𝜑 → ( 𝐺𝐹 ) : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ 𝑆 )
61 60 ffvelrnda ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐺𝐹 ) ‘ 𝑥 ) ∈ 𝑆 )
62 61 adantlr ( ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐺𝐹 ) ‘ 𝑥 ) ∈ 𝑆 )
63 48 49 53 55 62 seqsplit ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ 𝐾 ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) )
64 elfzp12 ( 𝑁 ∈ ( ℤ𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 = 𝑀𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
65 64 biimpa ( ( 𝑁 ∈ ( ℤ𝑀 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 = 𝑀𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
66 4 65 sylan ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 = 𝑀𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
67 seqeq1 ( 𝐾 = 𝑀 → seq 𝐾 ( + , ( 𝐺𝐹 ) ) = seq 𝑀 ( + , ( 𝐺𝐹 ) ) )
68 67 eqcomd ( 𝐾 = 𝑀 → seq 𝑀 ( + , ( 𝐺𝐹 ) ) = seq 𝐾 ( + , ( 𝐺𝐹 ) ) )
69 68 fveq1d ( 𝐾 = 𝑀 → ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ 𝐾 ) = ( seq 𝐾 ( + , ( 𝐺𝐹 ) ) ‘ 𝐾 ) )
70 f1ocnv ( 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑁 + 1 ) ) → 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑁 + 1 ) ) )
71 f1of ( 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑁 + 1 ) ) → 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ ( 𝑀 ... ( 𝑁 + 1 ) ) )
72 6 70 71 3syl ( 𝜑 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ ( 𝑀 ... ( 𝑁 + 1 ) ) )
73 peano2uz ( 𝑁 ∈ ( ℤ𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ𝑀 ) )
74 eluzfz2 ( ( 𝑁 + 1 ) ∈ ( ℤ𝑀 ) → ( 𝑁 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
75 4 73 74 3syl ( 𝜑 → ( 𝑁 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
76 72 75 ffvelrnd ( 𝜑 → ( 𝐹 ‘ ( 𝑁 + 1 ) ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
77 9 76 eqeltrid ( 𝜑𝐾 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
78 elfzelz ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) → 𝐾 ∈ ℤ )
79 seq1 ( 𝐾 ∈ ℤ → ( seq 𝐾 ( + , ( 𝐺𝐹 ) ) ‘ 𝐾 ) = ( ( 𝐺𝐹 ) ‘ 𝐾 ) )
80 77 78 79 3syl ( 𝜑 → ( seq 𝐾 ( + , ( 𝐺𝐹 ) ) ‘ 𝐾 ) = ( ( 𝐺𝐹 ) ‘ 𝐾 ) )
81 69 80 sylan9eqr ( ( 𝜑𝐾 = 𝑀 ) → ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ 𝐾 ) = ( ( 𝐺𝐹 ) ‘ 𝐾 ) )
82 81 oveq1d ( ( 𝜑𝐾 = 𝑀 ) → ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ 𝐾 ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) = ( ( ( 𝐺𝐹 ) ‘ 𝐾 ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) )
83 simpr ( ( 𝜑𝐾 = 𝑀 ) → 𝐾 = 𝑀 )
84 eluzfz1 ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
85 4 84 syl ( 𝜑𝑀 ∈ ( 𝑀 ... 𝑁 ) )
86 85 adantr ( ( 𝜑𝐾 = 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
87 83 86 eqeltrd ( ( 𝜑𝐾 = 𝑀 ) → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )
88 2 adantlr ( ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ∧ ( 𝑥𝐶𝑦𝐶 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
89 5 adantr ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐶𝑆 )
90 59 adantr ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺𝐹 ) : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ 𝐶 )
91 77 adantr ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
92 peano2uz ( 𝐾 ∈ ( ℤ𝑀 ) → ( 𝐾 + 1 ) ∈ ( ℤ𝑀 ) )
93 fzss1 ( ( 𝐾 + 1 ) ∈ ( ℤ𝑀 ) → ( ( 𝐾 + 1 ) ... ( 𝑁 + 1 ) ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) ) )
94 55 92 93 3syl ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐾 + 1 ) ... ( 𝑁 + 1 ) ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) ) )
95 48 88 49 53 89 90 91 94 seqf1olem2a ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝐺𝐹 ) ‘ 𝐾 ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) + ( ( 𝐺𝐹 ) ‘ 𝐾 ) ) )
96 1zzd ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 1 ∈ ℤ )
97 elfzuz ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) → 𝐾 ∈ ( ℤ𝑀 ) )
98 fzss1 ( 𝐾 ∈ ( ℤ𝑀 ) → ( 𝐾 ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
99 77 97 98 3syl ( 𝜑 → ( 𝐾 ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
100 99 sselda ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) )
101 21 ffvelrnda ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐽𝑥 ) ∈ ( 𝑀 ... 𝑁 ) )
102 100 101 syldan ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → ( 𝐽𝑥 ) ∈ ( 𝑀 ... 𝑁 ) )
103 102 fvresd ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ‘ ( 𝐽𝑥 ) ) = ( 𝐺 ‘ ( 𝐽𝑥 ) ) )
104 breq1 ( 𝑘 = 𝑥 → ( 𝑘 < 𝐾𝑥 < 𝐾 ) )
105 id ( 𝑘 = 𝑥𝑘 = 𝑥 )
106 oveq1 ( 𝑘 = 𝑥 → ( 𝑘 + 1 ) = ( 𝑥 + 1 ) )
107 104 105 106 ifbieq12d ( 𝑘 = 𝑥 → if ( 𝑘 < 𝐾 , 𝑘 , ( 𝑘 + 1 ) ) = if ( 𝑥 < 𝐾 , 𝑥 , ( 𝑥 + 1 ) ) )
108 107 fveq2d ( 𝑘 = 𝑥 → ( 𝐹 ‘ if ( 𝑘 < 𝐾 , 𝑘 , ( 𝑘 + 1 ) ) ) = ( 𝐹 ‘ if ( 𝑥 < 𝐾 , 𝑥 , ( 𝑥 + 1 ) ) ) )
109 fvex ( 𝐹 ‘ if ( 𝑥 < 𝐾 , 𝑥 , ( 𝑥 + 1 ) ) ) ∈ V
110 108 8 109 fvmpt ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐽𝑥 ) = ( 𝐹 ‘ if ( 𝑥 < 𝐾 , 𝑥 , ( 𝑥 + 1 ) ) ) )
111 100 110 syl ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → ( 𝐽𝑥 ) = ( 𝐹 ‘ if ( 𝑥 < 𝐾 , 𝑥 , ( 𝑥 + 1 ) ) ) )
112 77 78 syl ( 𝜑𝐾 ∈ ℤ )
113 112 zred ( 𝜑𝐾 ∈ ℝ )
114 113 adantr ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → 𝐾 ∈ ℝ )
115 elfzelz ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → 𝑥 ∈ ℤ )
116 115 adantl ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → 𝑥 ∈ ℤ )
117 116 zred ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → 𝑥 ∈ ℝ )
118 elfzle1 ( 𝑥 ∈ ( 𝐾 ... 𝑁 ) → 𝐾𝑥 )
119 118 adantl ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → 𝐾𝑥 )
120 114 117 119 lensymd ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → ¬ 𝑥 < 𝐾 )
121 iffalse ( ¬ 𝑥 < 𝐾 → if ( 𝑥 < 𝐾 , 𝑥 , ( 𝑥 + 1 ) ) = ( 𝑥 + 1 ) )
122 121 fveq2d ( ¬ 𝑥 < 𝐾 → ( 𝐹 ‘ if ( 𝑥 < 𝐾 , 𝑥 , ( 𝑥 + 1 ) ) ) = ( 𝐹 ‘ ( 𝑥 + 1 ) ) )
123 120 122 syl ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → ( 𝐹 ‘ if ( 𝑥 < 𝐾 , 𝑥 , ( 𝑥 + 1 ) ) ) = ( 𝐹 ‘ ( 𝑥 + 1 ) ) )
124 111 123 eqtrd ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → ( 𝐽𝑥 ) = ( 𝐹 ‘ ( 𝑥 + 1 ) ) )
125 124 fveq2d ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → ( 𝐺 ‘ ( 𝐽𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) )
126 103 125 eqtrd ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ‘ ( 𝐽𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) )
127 fvco3 ( ( 𝐽 : ( 𝑀 ... 𝑁 ) ⟶ ( 𝑀 ... 𝑁 ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ‘ 𝑥 ) = ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ‘ ( 𝐽𝑥 ) ) )
128 21 127 sylan ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ‘ 𝑥 ) = ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ‘ ( 𝐽𝑥 ) ) )
129 100 128 syldan ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ‘ 𝑥 ) = ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ‘ ( 𝐽𝑥 ) ) )
130 fzp1elp1 ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑥 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
131 100 130 syl ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → ( 𝑥 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
132 fvco3 ( ( 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ ( 𝑀 ... ( 𝑁 + 1 ) ) ∧ ( 𝑥 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐺𝐹 ) ‘ ( 𝑥 + 1 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) )
133 57 132 sylan ( ( 𝜑 ∧ ( 𝑥 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐺𝐹 ) ‘ ( 𝑥 + 1 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) )
134 131 133 syldan ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → ( ( 𝐺𝐹 ) ‘ ( 𝑥 + 1 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) )
135 126 129 134 3eqtr4d ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ‘ 𝑥 ) = ( ( 𝐺𝐹 ) ‘ ( 𝑥 + 1 ) ) )
136 135 adantlr ( ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ‘ 𝑥 ) = ( ( 𝐺𝐹 ) ‘ ( 𝑥 + 1 ) ) )
137 51 96 136 seqshft2 ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) = ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) )
138 fvco3 ( ( 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ ( 𝑀 ... ( 𝑁 + 1 ) ) ∧ 𝐾 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐺𝐹 ) ‘ 𝐾 ) = ( 𝐺 ‘ ( 𝐹𝐾 ) ) )
139 57 77 138 syl2anc ( 𝜑 → ( ( 𝐺𝐹 ) ‘ 𝐾 ) = ( 𝐺 ‘ ( 𝐹𝐾 ) ) )
140 9 fveq2i ( 𝐹𝐾 ) = ( 𝐹 ‘ ( 𝐹 ‘ ( 𝑁 + 1 ) ) )
141 f1ocnvfv2 ( ( 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑁 + 1 ) ) ∧ ( 𝑁 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
142 6 75 141 syl2anc ( 𝜑 → ( 𝐹 ‘ ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
143 140 142 eqtrid ( 𝜑 → ( 𝐹𝐾 ) = ( 𝑁 + 1 ) )
144 143 fveq2d ( 𝜑 → ( 𝐺 ‘ ( 𝐹𝐾 ) ) = ( 𝐺 ‘ ( 𝑁 + 1 ) ) )
145 139 144 eqtr2d ( 𝜑 → ( 𝐺 ‘ ( 𝑁 + 1 ) ) = ( ( 𝐺𝐹 ) ‘ 𝐾 ) )
146 145 adantr ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ ( 𝑁 + 1 ) ) = ( ( 𝐺𝐹 ) ‘ 𝐾 ) )
147 137 146 oveq12d ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) = ( ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) + ( ( 𝐺𝐹 ) ‘ 𝐾 ) ) )
148 95 147 eqtr4d ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝐺𝐹 ) ‘ 𝐾 ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
149 87 148 syldan ( ( 𝜑𝐾 = 𝑀 ) → ( ( ( 𝐺𝐹 ) ‘ 𝐾 ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
150 83 seqeq1d ( ( 𝜑𝐾 = 𝑀 ) → seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) = seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) )
151 150 fveq1d ( ( 𝜑𝐾 = 𝑀 ) → ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) )
152 151 oveq1d ( ( 𝜑𝐾 = 𝑀 ) → ( ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
153 82 149 152 3eqtrd ( ( 𝜑𝐾 = 𝑀 ) → ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ 𝐾 ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
154 eluzel2 ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑀 ∈ ℤ )
155 4 154 syl ( 𝜑𝑀 ∈ ℤ )
156 elfzuz ( 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → 𝐾 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) )
157 eluzp1m1 ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( 𝐾 − 1 ) ∈ ( ℤ𝑀 ) )
158 155 156 157 syl2an ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝐾 − 1 ) ∈ ( ℤ𝑀 ) )
159 eluzelz ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑁 ∈ ℤ )
160 4 159 syl ( 𝜑𝑁 ∈ ℤ )
161 160 zcnd ( 𝜑𝑁 ∈ ℂ )
162 ax-1cn 1 ∈ ℂ
163 pncan ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
164 161 162 163 sylancl ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
165 peano2zm ( 𝐾 ∈ ℤ → ( 𝐾 − 1 ) ∈ ℤ )
166 77 78 165 3syl ( 𝜑 → ( 𝐾 − 1 ) ∈ ℤ )
167 elfzuz3 ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) → ( 𝑁 + 1 ) ∈ ( ℤ𝐾 ) )
168 77 167 syl ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ𝐾 ) )
169 112 zcnd ( 𝜑𝐾 ∈ ℂ )
170 npcan ( ( 𝐾 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
171 169 162 170 sylancl ( 𝜑 → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
172 171 fveq2d ( 𝜑 → ( ℤ ‘ ( ( 𝐾 − 1 ) + 1 ) ) = ( ℤ𝐾 ) )
173 168 172 eleqtrrd ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ ‘ ( ( 𝐾 − 1 ) + 1 ) ) )
174 eluzp1m1 ( ( ( 𝐾 − 1 ) ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ( ℤ ‘ ( ( 𝐾 − 1 ) + 1 ) ) ) → ( ( 𝑁 + 1 ) − 1 ) ∈ ( ℤ ‘ ( 𝐾 − 1 ) ) )
175 166 173 174 syl2anc ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) ∈ ( ℤ ‘ ( 𝐾 − 1 ) ) )
176 164 175 eqeltrrd ( 𝜑𝑁 ∈ ( ℤ ‘ ( 𝐾 − 1 ) ) )
177 fzss2 ( 𝑁 ∈ ( ℤ ‘ ( 𝐾 − 1 ) ) → ( 𝑀 ... ( 𝐾 − 1 ) ) ⊆ ( 𝑀 ... 𝑁 ) )
178 176 177 syl ( 𝜑 → ( 𝑀 ... ( 𝐾 − 1 ) ) ⊆ ( 𝑀 ... 𝑁 ) )
179 178 sselda ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) )
180 179 101 syldan ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( 𝐽𝑥 ) ∈ ( 𝑀 ... 𝑁 ) )
181 180 fvresd ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ‘ ( 𝐽𝑥 ) ) = ( 𝐺 ‘ ( 𝐽𝑥 ) ) )
182 179 110 syl ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( 𝐽𝑥 ) = ( 𝐹 ‘ if ( 𝑥 < 𝐾 , 𝑥 , ( 𝑥 + 1 ) ) ) )
183 elfzm11 ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ↔ ( 𝑥 ∈ ℤ ∧ 𝑀𝑥𝑥 < 𝐾 ) ) )
184 155 112 183 syl2anc ( 𝜑 → ( 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ↔ ( 𝑥 ∈ ℤ ∧ 𝑀𝑥𝑥 < 𝐾 ) ) )
185 184 biimpa ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( 𝑥 ∈ ℤ ∧ 𝑀𝑥𝑥 < 𝐾 ) )
186 185 simp3d ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → 𝑥 < 𝐾 )
187 iftrue ( 𝑥 < 𝐾 → if ( 𝑥 < 𝐾 , 𝑥 , ( 𝑥 + 1 ) ) = 𝑥 )
188 187 fveq2d ( 𝑥 < 𝐾 → ( 𝐹 ‘ if ( 𝑥 < 𝐾 , 𝑥 , ( 𝑥 + 1 ) ) ) = ( 𝐹𝑥 ) )
189 186 188 syl ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( 𝐹 ‘ if ( 𝑥 < 𝐾 , 𝑥 , ( 𝑥 + 1 ) ) ) = ( 𝐹𝑥 ) )
190 182 189 eqtrd ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( 𝐽𝑥 ) = ( 𝐹𝑥 ) )
191 190 fveq2d ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( 𝐺 ‘ ( 𝐽𝑥 ) ) = ( 𝐺 ‘ ( 𝐹𝑥 ) ) )
192 181 191 eqtr2d ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( 𝐺 ‘ ( 𝐹𝑥 ) ) = ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ‘ ( 𝐽𝑥 ) ) )
193 peano2uz ( 𝑁 ∈ ( ℤ ‘ ( 𝐾 − 1 ) ) → ( 𝑁 + 1 ) ∈ ( ℤ ‘ ( 𝐾 − 1 ) ) )
194 fzss2 ( ( 𝑁 + 1 ) ∈ ( ℤ ‘ ( 𝐾 − 1 ) ) → ( 𝑀 ... ( 𝐾 − 1 ) ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) ) )
195 176 193 194 3syl ( 𝜑 → ( 𝑀 ... ( 𝐾 − 1 ) ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) ) )
196 195 sselda ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → 𝑥 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
197 fvco3 ( ( 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ ( 𝑀 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐺𝐹 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹𝑥 ) ) )
198 57 197 sylan ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐺𝐹 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹𝑥 ) ) )
199 196 198 syldan ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐺𝐹 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹𝑥 ) ) )
200 179 128 syldan ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ‘ 𝑥 ) = ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ‘ ( 𝐽𝑥 ) ) )
201 192 199 200 3eqtr4d ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐺𝐹 ) ‘ 𝑥 ) = ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ‘ 𝑥 ) )
202 201 adantlr ( ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐺𝐹 ) ‘ 𝑥 ) = ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ‘ 𝑥 ) )
203 158 202 seqfveq ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝐾 − 1 ) ) = ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ ( 𝐾 − 1 ) ) )
204 fzp1ss ( 𝑀 ∈ ℤ → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
205 4 154 204 3syl ( 𝜑 → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
206 205 sselda ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )
207 206 148 syldan ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ( ( 𝐺𝐹 ) ‘ 𝐾 ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
208 203 207 oveq12d ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝐾 − 1 ) ) + ( ( ( 𝐺𝐹 ) ‘ 𝐾 ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) ) = ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ ( 𝐾 − 1 ) ) + ( ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) )
209 196 61 syldan ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐺𝐹 ) ‘ 𝑥 ) ∈ 𝑆 )
210 209 adantlr ( ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐺𝐹 ) ‘ 𝑥 ) ∈ 𝑆 )
211 1 adantlr ( ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
212 158 210 211 seqcl ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝐾 − 1 ) ) ∈ 𝑆 )
213 59 77 ffvelrnd ( 𝜑 → ( ( 𝐺𝐹 ) ‘ 𝐾 ) ∈ 𝐶 )
214 5 213 sseldd ( 𝜑 → ( ( 𝐺𝐹 ) ‘ 𝐾 ) ∈ 𝑆 )
215 214 adantr ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ( 𝐺𝐹 ) ‘ 𝐾 ) ∈ 𝑆 )
216 94 sselda ( ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑥 ∈ ( ( 𝐾 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑥 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
217 216 62 syldan ( ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑥 ∈ ( ( 𝐾 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝐺𝐹 ) ‘ 𝑥 ) ∈ 𝑆 )
218 53 217 48 seqcl ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ∈ 𝑆 )
219 206 218 syldan ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ∈ 𝑆 )
220 212 215 219 3jca ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝐾 − 1 ) ) ∈ 𝑆 ∧ ( ( 𝐺𝐹 ) ‘ 𝐾 ) ∈ 𝑆 ∧ ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ∈ 𝑆 ) )
221 3 caovassg ( ( 𝜑 ∧ ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝐾 − 1 ) ) ∈ 𝑆 ∧ ( ( 𝐺𝐹 ) ‘ 𝐾 ) ∈ 𝑆 ∧ ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ∈ 𝑆 ) ) → ( ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝐾 − 1 ) ) + ( ( 𝐺𝐹 ) ‘ 𝐾 ) ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝐾 − 1 ) ) + ( ( ( 𝐺𝐹 ) ‘ 𝐾 ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) ) )
222 220 221 syldan ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝐾 − 1 ) ) + ( ( 𝐺𝐹 ) ‘ 𝐾 ) ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝐾 − 1 ) ) + ( ( ( 𝐺𝐹 ) ‘ 𝐾 ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) ) )
223 7 5 fssd ( 𝜑𝐺 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ 𝑆 )
224 fssres ( ( 𝐺 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ 𝑆 ∧ ( 𝑀 ... 𝑁 ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝑆 )
225 223 12 224 sylancl ( 𝜑 → ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝑆 )
226 fco ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝑆𝐽 : ( 𝑀 ... 𝑁 ) ⟶ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) : ( 𝑀 ... 𝑁 ) ⟶ 𝑆 )
227 225 21 226 syl2anc ( 𝜑 → ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) : ( 𝑀 ... 𝑁 ) ⟶ 𝑆 )
228 227 ffvelrnda ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ‘ 𝑥 ) ∈ 𝑆 )
229 179 228 syldan ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ‘ 𝑥 ) ∈ 𝑆 )
230 229 adantlr ( ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ‘ 𝑥 ) ∈ 𝑆 )
231 158 230 211 seqcl ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ ( 𝐾 − 1 ) ) ∈ 𝑆 )
232 elfzuz3 ( 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → 𝑁 ∈ ( ℤ𝐾 ) )
233 232 adantl ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑁 ∈ ( ℤ𝐾 ) )
234 100 228 syldan ( ( 𝜑𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ‘ 𝑥 ) ∈ 𝑆 )
235 234 adantlr ( ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ∧ 𝑥 ∈ ( 𝐾 ... 𝑁 ) ) → ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ‘ 𝑥 ) ∈ 𝑆 )
236 233 235 211 seqcl ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) ∈ 𝑆 )
237 223 75 ffvelrnd ( 𝜑 → ( 𝐺 ‘ ( 𝑁 + 1 ) ) ∈ 𝑆 )
238 237 adantr ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝐺 ‘ ( 𝑁 + 1 ) ) ∈ 𝑆 )
239 231 236 238 3jca ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ ( 𝐾 − 1 ) ) ∈ 𝑆 ∧ ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) ∈ 𝑆 ∧ ( 𝐺 ‘ ( 𝑁 + 1 ) ) ∈ 𝑆 ) )
240 3 caovassg ( ( 𝜑 ∧ ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ ( 𝐾 − 1 ) ) ∈ 𝑆 ∧ ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) ∈ 𝑆 ∧ ( 𝐺 ‘ ( 𝑁 + 1 ) ) ∈ 𝑆 ) ) → ( ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ ( 𝐾 − 1 ) ) + ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ ( 𝐾 − 1 ) ) + ( ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) )
241 239 240 syldan ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ ( 𝐾 − 1 ) ) + ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ ( 𝐾 − 1 ) ) + ( ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) )
242 208 222 241 3eqtr4d ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝐾 − 1 ) ) + ( ( 𝐺𝐹 ) ‘ 𝐾 ) ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) = ( ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ ( 𝐾 − 1 ) ) + ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
243 seqm1 ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ 𝐾 ) = ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝐾 − 1 ) ) + ( ( 𝐺𝐹 ) ‘ 𝐾 ) ) )
244 155 156 243 syl2an ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ 𝐾 ) = ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝐾 − 1 ) ) + ( ( 𝐺𝐹 ) ‘ 𝐾 ) ) )
245 244 oveq1d ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ 𝐾 ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) = ( ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝐾 − 1 ) ) + ( ( 𝐺𝐹 ) ‘ 𝐾 ) ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) )
246 3 adantlr ( ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ∧ ( 𝑥𝑆𝑦𝑆𝑧𝑆 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
247 elfzelz ( 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → 𝐾 ∈ ℤ )
248 247 adantl ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝐾 ∈ ℤ )
249 248 zcnd ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝐾 ∈ ℂ )
250 249 162 170 sylancl ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
251 250 fveq2d ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ℤ ‘ ( ( 𝐾 − 1 ) + 1 ) ) = ( ℤ𝐾 ) )
252 233 251 eleqtrrd ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑁 ∈ ( ℤ ‘ ( ( 𝐾 − 1 ) + 1 ) ) )
253 228 adantlr ( ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ‘ 𝑥 ) ∈ 𝑆 )
254 211 246 252 158 253 seqsplit ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) = ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ ( 𝐾 − 1 ) ) + ( seq ( ( 𝐾 − 1 ) + 1 ) ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) ) )
255 250 seqeq1d ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → seq ( ( 𝐾 − 1 ) + 1 ) ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) = seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) )
256 255 fveq1d ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( seq ( ( 𝐾 − 1 ) + 1 ) ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) = ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) )
257 256 oveq2d ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ ( 𝐾 − 1 ) ) + ( seq ( ( 𝐾 − 1 ) + 1 ) ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) ) = ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ ( 𝐾 − 1 ) ) + ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) ) )
258 254 257 eqtrd ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) = ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ ( 𝐾 − 1 ) ) + ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) ) )
259 258 oveq1d ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) = ( ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ ( 𝐾 − 1 ) ) + ( seq 𝐾 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
260 242 245 259 3eqtr4d ( ( 𝜑𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ 𝐾 ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
261 153 260 jaodan ( ( 𝜑 ∧ ( 𝐾 = 𝑀𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) → ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ 𝐾 ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
262 66 261 syldan ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ 𝐾 ) + ( seq ( 𝐾 + 1 ) ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
263 63 262 eqtrd ( ( 𝜑𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
264 4 adantr ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) → 𝑁 ∈ ( ℤ𝑀 ) )
265 seqp1 ( 𝑁 ∈ ( ℤ𝑀 ) → ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ 𝑁 ) + ( ( 𝐺𝐹 ) ‘ ( 𝑁 + 1 ) ) ) )
266 264 265 syl ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) → ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ 𝑁 ) + ( ( 𝐺𝐹 ) ‘ ( 𝑁 + 1 ) ) ) )
267 110 adantl ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐽𝑥 ) = ( 𝐹 ‘ if ( 𝑥 < 𝐾 , 𝑥 , ( 𝑥 + 1 ) ) ) )
268 elfzelz ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ℤ )
269 268 zred ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ℝ )
270 269 adantl ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑥 ∈ ℝ )
271 160 zred ( 𝜑𝑁 ∈ ℝ )
272 271 adantr ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ℝ )
273 peano2re ( 𝑁 ∈ ℝ → ( 𝑁 + 1 ) ∈ ℝ )
274 272 273 syl ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑁 + 1 ) ∈ ℝ )
275 elfzle2 ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥𝑁 )
276 275 adantl ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑥𝑁 )
277 272 ltp1d ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 < ( 𝑁 + 1 ) )
278 270 272 274 276 277 lelttrd ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑥 < ( 𝑁 + 1 ) )
279 278 adantlr ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑥 < ( 𝑁 + 1 ) )
280 simplr ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 = ( 𝑁 + 1 ) )
281 279 280 breqtrrd ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑥 < 𝐾 )
282 281 188 syl ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ if ( 𝑥 < 𝐾 , 𝑥 , ( 𝑥 + 1 ) ) ) = ( 𝐹𝑥 ) )
283 267 282 eqtrd ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐽𝑥 ) = ( 𝐹𝑥 ) )
284 283 fveq2d ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ‘ ( 𝐽𝑥 ) ) = ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ‘ ( 𝐹𝑥 ) ) )
285 269 adantl ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑥 ∈ ℝ )
286 285 281 gtned ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾𝑥 )
287 57 ad2antrr ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ ( 𝑀 ... ( 𝑁 + 1 ) ) )
288 fzelp1 ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑥 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
289 288 adantl ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑥 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
290 287 289 ffvelrnd ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹𝑥 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )
291 4 ad2antrr ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ𝑀 ) )
292 elfzp1 ( 𝑁 ∈ ( ℤ𝑀 ) → ( ( 𝐹𝑥 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ↔ ( ( 𝐹𝑥 ) ∈ ( 𝑀 ... 𝑁 ) ∨ ( 𝐹𝑥 ) = ( 𝑁 + 1 ) ) ) )
293 291 292 syl ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐹𝑥 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ↔ ( ( 𝐹𝑥 ) ∈ ( 𝑀 ... 𝑁 ) ∨ ( 𝐹𝑥 ) = ( 𝑁 + 1 ) ) ) )
294 290 293 mpbid ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐹𝑥 ) ∈ ( 𝑀 ... 𝑁 ) ∨ ( 𝐹𝑥 ) = ( 𝑁 + 1 ) ) )
295 294 ord ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ¬ ( 𝐹𝑥 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝐹𝑥 ) = ( 𝑁 + 1 ) ) )
296 6 ad2antrr ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑁 + 1 ) ) )
297 f1ocnvfv ( ( 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹𝑥 ) = ( 𝑁 + 1 ) → ( 𝐹 ‘ ( 𝑁 + 1 ) ) = 𝑥 ) )
298 296 289 297 syl2anc ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐹𝑥 ) = ( 𝑁 + 1 ) → ( 𝐹 ‘ ( 𝑁 + 1 ) ) = 𝑥 ) )
299 9 eqeq1i ( 𝐾 = 𝑥 ↔ ( 𝐹 ‘ ( 𝑁 + 1 ) ) = 𝑥 )
300 298 299 syl6ibr ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐹𝑥 ) = ( 𝑁 + 1 ) → 𝐾 = 𝑥 ) )
301 295 300 syld ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ¬ ( 𝐹𝑥 ) ∈ ( 𝑀 ... 𝑁 ) → 𝐾 = 𝑥 ) )
302 301 necon1ad ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾𝑥 → ( 𝐹𝑥 ) ∈ ( 𝑀 ... 𝑁 ) ) )
303 286 302 mpd ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹𝑥 ) ∈ ( 𝑀 ... 𝑁 ) )
304 303 fvresd ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ‘ ( 𝐹𝑥 ) ) = ( 𝐺 ‘ ( 𝐹𝑥 ) ) )
305 284 304 eqtr2d ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ ( 𝐹𝑥 ) ) = ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ‘ ( 𝐽𝑥 ) ) )
306 57 288 197 syl2an ( ( 𝜑𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐺𝐹 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹𝑥 ) ) )
307 306 adantlr ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐺𝐹 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹𝑥 ) ) )
308 128 adantlr ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ‘ 𝑥 ) = ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ‘ ( 𝐽𝑥 ) ) )
309 305 307 308 3eqtr4d ( ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐺𝐹 ) ‘ 𝑥 ) = ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ‘ 𝑥 ) )
310 264 309 seqfveq ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) → ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) )
311 fvco3 ( ( 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ ( 𝑀 ... ( 𝑁 + 1 ) ) ∧ ( 𝑁 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐺𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
312 57 75 311 syl2anc ( 𝜑 → ( ( 𝐺𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
313 312 adantr ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) → ( ( 𝐺𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( 𝐺 ‘ ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
314 simpr ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) → 𝐾 = ( 𝑁 + 1 ) )
315 9 314 eqtr3id ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) → ( 𝐹 ‘ ( 𝑁 + 1 ) ) = ( 𝑁 + 1 ) )
316 315 fveq2d ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) → ( 𝐹 ‘ ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) = ( 𝐹 ‘ ( 𝑁 + 1 ) ) )
317 142 adantr ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) → ( 𝐹 ‘ ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
318 316 317 eqtr3d ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) → ( 𝐹 ‘ ( 𝑁 + 1 ) ) = ( 𝑁 + 1 ) )
319 318 fveq2d ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) → ( 𝐺 ‘ ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) = ( 𝐺 ‘ ( 𝑁 + 1 ) ) )
320 313 319 eqtrd ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) → ( ( 𝐺𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( 𝐺 ‘ ( 𝑁 + 1 ) ) )
321 310 320 oveq12d ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) → ( ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ 𝑁 ) + ( ( 𝐺𝐹 ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
322 266 321 eqtrd ( ( 𝜑𝐾 = ( 𝑁 + 1 ) ) → ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
323 elfzp1 ( 𝑁 ∈ ( ℤ𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ↔ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∨ 𝐾 = ( 𝑁 + 1 ) ) ) )
324 4 323 syl ( 𝜑 → ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ↔ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∨ 𝐾 = ( 𝑁 + 1 ) ) ) )
325 77 324 mpbid ( 𝜑 → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ∨ 𝐾 = ( 𝑁 + 1 ) ) )
326 263 322 325 mpjaodan ( 𝜑 → ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
327 seqp1 ( 𝑁 ∈ ( ℤ𝑀 ) → ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
328 4 327 syl ( 𝜑 → ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
329 47 326 328 3eqtr4d ( 𝜑 → ( seq 𝑀 ( + , ( 𝐺𝐹 ) ) ‘ ( 𝑁 + 1 ) ) = ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑁 + 1 ) ) )