This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... ( 𝑁 + 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 ffvelcdmd ⊢ ( 𝜑 → ( ◡ 𝐹 ‘ ( 𝑁 + 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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐽 ‘ 𝑥 ) ∈ ( 𝑀 ... 𝑁 ) )
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 ffvelcdmd ⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝐾 ) ∈ 𝐶 )
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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝐺 ↾ ( 𝑀 ... 𝑁 ) ) ∘ 𝐽 ) ‘ 𝑥 ) ∈ 𝑆 )
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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝑁 + 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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝐾 = ( 𝑁 + 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 imbitrrdi ⊢ ( ( ( 𝜑 ∧ 𝐾 = ( 𝑁 + 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 ) ) )