MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  seqf1olem2 Structured version   Visualization version   GIF version

Theorem seqf1olem2 12881
Description: Lemma for seqf1o 12882. (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Mario Carneiro, 24-Apr-2016.)
Hypotheses
Ref Expression
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
Ref Expression
seqf1olem2 (𝜑 → (seq𝑀( + , (𝐺𝐹))‘(𝑁 + 1)) = (seq𝑀( + , 𝐺)‘(𝑁 + 1)))
Distinct variable groups:   𝑓,𝑔,𝑘,𝑥,𝑦,𝑧,𝐹   𝑓,𝐺,𝑔,𝑘,𝑥,𝑦,𝑧   𝑓,𝑀,𝑔,𝑘,𝑥,𝑦,𝑧   + ,𝑓,𝑔,𝑘,𝑥,𝑦,𝑧   𝑓,𝐽,𝑔,𝑥,𝑦,𝑧   𝑓,𝑁,𝑔,𝑘,𝑥,𝑦,𝑧   𝑘,𝐾,𝑥,𝑦,𝑧   𝜑,𝑓,𝑔,𝑘,𝑥,𝑦,𝑧   𝑆,𝑘,𝑥,𝑦,𝑧   𝐶,𝑓,𝑔,𝑘,𝑥,𝑦,𝑧
Allowed substitution hints:   𝑆(𝑓,𝑔)   𝐽(𝑘)   𝐾(𝑓,𝑔)

Proof of Theorem seqf1olem2
StepHypRef Expression
1 seqf1olem.6 . . . . . . . . . 10 (𝜑𝐺:(𝑀...(𝑁 + 1))⟶𝐶)
2 ffn 6083 . . . . . . . . . 10 (𝐺:(𝑀...(𝑁 + 1))⟶𝐶𝐺 Fn (𝑀...(𝑁 + 1)))
31, 2syl 17 . . . . . . . . 9 (𝜑𝐺 Fn (𝑀...(𝑁 + 1)))
4 fzssp1 12422 . . . . . . . . 9 (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))
5 fnssres 6042 . . . . . . . . 9 ((𝐺 Fn (𝑀...(𝑁 + 1)) ∧ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))) → (𝐺 ↾ (𝑀...𝑁)) Fn (𝑀...𝑁))
63, 4, 5sylancl 695 . . . . . . . 8 (𝜑 → (𝐺 ↾ (𝑀...𝑁)) Fn (𝑀...𝑁))
7 fzfid 12812 . . . . . . . 8 (𝜑 → (𝑀...𝑁) ∈ Fin)
8 fnfi 8279 . . . . . . . 8 (((𝐺 ↾ (𝑀...𝑁)) Fn (𝑀...𝑁) ∧ (𝑀...𝑁) ∈ Fin) → (𝐺 ↾ (𝑀...𝑁)) ∈ Fin)
96, 7, 8syl2anc 694 . . . . . . 7 (𝜑 → (𝐺 ↾ (𝑀...𝑁)) ∈ Fin)
10 elex 3243 . . . . . . 7 ((𝐺 ↾ (𝑀...𝑁)) ∈ Fin → (𝐺 ↾ (𝑀...𝑁)) ∈ V)
119, 10syl 17 . . . . . 6 (𝜑 → (𝐺 ↾ (𝑀...𝑁)) ∈ V)
12 seqf1o.1 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
13 seqf1o.2 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐶𝑦𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
14 seqf1o.3 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
15 seqf1o.4 . . . . . . . . 9 (𝜑𝑁 ∈ (ℤ𝑀))
16 seqf1o.5 . . . . . . . . 9 (𝜑𝐶𝑆)
17 seqf1olem.5 . . . . . . . . 9 (𝜑𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
18 seqf1olem.7 . . . . . . . . 9 𝐽 = (𝑘 ∈ (𝑀...𝑁) ↦ (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
19 seqf1olem.8 . . . . . . . . 9 𝐾 = (𝐹‘(𝑁 + 1))
2012, 13, 14, 15, 16, 17, 1, 18, 19seqf1olem1 12880 . . . . . . . 8 (𝜑𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
21 f1of 6175 . . . . . . . 8 (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → 𝐽:(𝑀...𝑁)⟶(𝑀...𝑁))
2220, 21syl 17 . . . . . . 7 (𝜑𝐽:(𝑀...𝑁)⟶(𝑀...𝑁))
23 fex2 7163 . . . . . . 7 ((𝐽:(𝑀...𝑁)⟶(𝑀...𝑁) ∧ (𝑀...𝑁) ∈ Fin ∧ (𝑀...𝑁) ∈ Fin) → 𝐽 ∈ V)
2422, 7, 7, 23syl3anc 1366 . . . . . 6 (𝜑𝐽 ∈ V)
2511, 24jca 553 . . . . 5 (𝜑 → ((𝐺 ↾ (𝑀...𝑁)) ∈ V ∧ 𝐽 ∈ V))
26 seqf1olem.9 . . . . 5 (𝜑 → ∀𝑔𝑓((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , (𝑔𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁)))
27 fssres 6108 . . . . . . 7 ((𝐺:(𝑀...(𝑁 + 1))⟶𝐶 ∧ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))) → (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶)
281, 4, 27sylancl 695 . . . . . 6 (𝜑 → (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶)
2920, 28jca 553 . . . . 5 (𝜑 → (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶))
30 f1oeq1 6165 . . . . . . . 8 (𝑓 = 𝐽 → (𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ↔ 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)))
31 feq1 6064 . . . . . . . 8 (𝑔 = (𝐺 ↾ (𝑀...𝑁)) → (𝑔:(𝑀...𝑁)⟶𝐶 ↔ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶))
3230, 31bi2anan9r 936 . . . . . . 7 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → ((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) ↔ (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶)))
33 coeq1 5312 . . . . . . . . . . 11 (𝑔 = (𝐺 ↾ (𝑀...𝑁)) → (𝑔𝑓) = ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝑓))
34 coeq2 5313 . . . . . . . . . . 11 (𝑓 = 𝐽 → ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝑓) = ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))
3533, 34sylan9eq 2705 . . . . . . . . . 10 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → (𝑔𝑓) = ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))
3635seqeq3d 12849 . . . . . . . . 9 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → seq𝑀( + , (𝑔𝑓)) = seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)))
3736fveq1d 6231 . . . . . . . 8 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → (seq𝑀( + , (𝑔𝑓))‘𝑁) = (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁))
38 simpl 472 . . . . . . . . . 10 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → 𝑔 = (𝐺 ↾ (𝑀...𝑁)))
3938seqeq3d 12849 . . . . . . . . 9 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → seq𝑀( + , 𝑔) = seq𝑀( + , (𝐺 ↾ (𝑀...𝑁))))
4039fveq1d 6231 . . . . . . . 8 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → (seq𝑀( + , 𝑔)‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁))
4137, 40eqeq12d 2666 . . . . . . 7 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → ((seq𝑀( + , (𝑔𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁) ↔ (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁)))
4232, 41imbi12d 333 . . . . . 6 ((𝑔 = (𝐺 ↾ (𝑀...𝑁)) ∧ 𝑓 = 𝐽) → (((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , (𝑔𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁)) ↔ ((𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁))))
4342spc2gv 3327 . . . . 5 (((𝐺 ↾ (𝑀...𝑁)) ∈ V ∧ 𝐽 ∈ V) → (∀𝑔𝑓((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , (𝑔𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁)) → ((𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁))))
4425, 26, 29, 43syl3c 66 . . . 4 (𝜑 → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁))
45 fvres 6245 . . . . . 6 (𝑥 ∈ (𝑀...𝑁) → ((𝐺 ↾ (𝑀...𝑁))‘𝑥) = (𝐺𝑥))
4645adantl 481 . . . . 5 ((𝜑𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘𝑥) = (𝐺𝑥))
4715, 46seqfveq 12865 . . . 4 (𝜑 → (seq𝑀( + , (𝐺 ↾ (𝑀...𝑁)))‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁))
4844, 47eqtrd 2685 . . 3 (𝜑 → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁))
4948oveq1d 6705 . 2 (𝜑 → ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘(𝑁 + 1))))
5012adantlr 751 . . . . 5 (((𝜑𝐾 ∈ (𝑀...𝑁)) ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
5114adantlr 751 . . . . 5 (((𝜑𝐾 ∈ (𝑀...𝑁)) ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
52 elfzuz3 12377 . . . . . . 7 (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ𝐾))
5352adantl 481 . . . . . 6 ((𝜑𝐾 ∈ (𝑀...𝑁)) → 𝑁 ∈ (ℤ𝐾))
54 eluzp1p1 11751 . . . . . 6 (𝑁 ∈ (ℤ𝐾) → (𝑁 + 1) ∈ (ℤ‘(𝐾 + 1)))
5553, 54syl 17 . . . . 5 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈ (ℤ‘(𝐾 + 1)))
56 elfzuz 12376 . . . . . 6 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ𝑀))
5756adantl 481 . . . . 5 ((𝜑𝐾 ∈ (𝑀...𝑁)) → 𝐾 ∈ (ℤ𝑀))
58 f1of 6175 . . . . . . . . . 10 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
5917, 58syl 17 . . . . . . . . 9 (𝜑𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
60 fco 6096 . . . . . . . . 9 ((𝐺:(𝑀...(𝑁 + 1))⟶𝐶𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1))) → (𝐺𝐹):(𝑀...(𝑁 + 1))⟶𝐶)
611, 59, 60syl2anc 694 . . . . . . . 8 (𝜑 → (𝐺𝐹):(𝑀...(𝑁 + 1))⟶𝐶)
6261, 16fssd 6095 . . . . . . 7 (𝜑 → (𝐺𝐹):(𝑀...(𝑁 + 1))⟶𝑆)
6362ffvelrnda 6399 . . . . . 6 ((𝜑𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐺𝐹)‘𝑥) ∈ 𝑆)
6463adantlr 751 . . . . 5 (((𝜑𝐾 ∈ (𝑀...𝑁)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐺𝐹)‘𝑥) ∈ 𝑆)
6550, 51, 55, 57, 64seqsplit 12874 . . . 4 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (seq𝑀( + , (𝐺𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , (𝐺𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))))
66 elfzp12 12457 . . . . . . 7 (𝑁 ∈ (ℤ𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 = 𝑀𝐾 ∈ ((𝑀 + 1)...𝑁))))
6766biimpa 500 . . . . . 6 ((𝑁 ∈ (ℤ𝑀) ∧ 𝐾 ∈ (𝑀...𝑁)) → (𝐾 = 𝑀𝐾 ∈ ((𝑀 + 1)...𝑁)))
6815, 67sylan 487 . . . . 5 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (𝐾 = 𝑀𝐾 ∈ ((𝑀 + 1)...𝑁)))
69 seqeq1 12844 . . . . . . . . . . 11 (𝐾 = 𝑀 → seq𝐾( + , (𝐺𝐹)) = seq𝑀( + , (𝐺𝐹)))
7069eqcomd 2657 . . . . . . . . . 10 (𝐾 = 𝑀 → seq𝑀( + , (𝐺𝐹)) = seq𝐾( + , (𝐺𝐹)))
7170fveq1d 6231 . . . . . . . . 9 (𝐾 = 𝑀 → (seq𝑀( + , (𝐺𝐹))‘𝐾) = (seq𝐾( + , (𝐺𝐹))‘𝐾))
72 f1ocnv 6187 . . . . . . . . . . . . 13 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
73 f1of 6175 . . . . . . . . . . . . 13 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
7417, 72, 733syl 18 . . . . . . . . . . . 12 (𝜑𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
75 peano2uz 11779 . . . . . . . . . . . . 13 (𝑁 ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (ℤ𝑀))
76 eluzfz2 12387 . . . . . . . . . . . . 13 ((𝑁 + 1) ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
7715, 75, 763syl 18 . . . . . . . . . . . 12 (𝜑 → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
7874, 77ffvelrnd 6400 . . . . . . . . . . 11 (𝜑 → (𝐹‘(𝑁 + 1)) ∈ (𝑀...(𝑁 + 1)))
7919, 78syl5eqel 2734 . . . . . . . . . 10 (𝜑𝐾 ∈ (𝑀...(𝑁 + 1)))
80 elfzelz 12380 . . . . . . . . . 10 (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ∈ ℤ)
81 seq1 12854 . . . . . . . . . 10 (𝐾 ∈ ℤ → (seq𝐾( + , (𝐺𝐹))‘𝐾) = ((𝐺𝐹)‘𝐾))
8279, 80, 813syl 18 . . . . . . . . 9 (𝜑 → (seq𝐾( + , (𝐺𝐹))‘𝐾) = ((𝐺𝐹)‘𝐾))
8371, 82sylan9eqr 2707 . . . . . . . 8 ((𝜑𝐾 = 𝑀) → (seq𝑀( + , (𝐺𝐹))‘𝐾) = ((𝐺𝐹)‘𝐾))
8483oveq1d 6705 . . . . . . 7 ((𝜑𝐾 = 𝑀) → ((seq𝑀( + , (𝐺𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = (((𝐺𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))))
85 simpr 476 . . . . . . . . 9 ((𝜑𝐾 = 𝑀) → 𝐾 = 𝑀)
86 eluzfz1 12386 . . . . . . . . . . 11 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑁))
8715, 86syl 17 . . . . . . . . . 10 (𝜑𝑀 ∈ (𝑀...𝑁))
8887adantr 480 . . . . . . . . 9 ((𝜑𝐾 = 𝑀) → 𝑀 ∈ (𝑀...𝑁))
8985, 88eqeltrd 2730 . . . . . . . 8 ((𝜑𝐾 = 𝑀) → 𝐾 ∈ (𝑀...𝑁))
9013adantlr 751 . . . . . . . . . 10 (((𝜑𝐾 ∈ (𝑀...𝑁)) ∧ (𝑥𝐶𝑦𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
9116adantr 480 . . . . . . . . . 10 ((𝜑𝐾 ∈ (𝑀...𝑁)) → 𝐶𝑆)
9261adantr 480 . . . . . . . . . 10 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (𝐺𝐹):(𝑀...(𝑁 + 1))⟶𝐶)
9379adantr 480 . . . . . . . . . 10 ((𝜑𝐾 ∈ (𝑀...𝑁)) → 𝐾 ∈ (𝑀...(𝑁 + 1)))
94 peano2uz 11779 . . . . . . . . . . 11 (𝐾 ∈ (ℤ𝑀) → (𝐾 + 1) ∈ (ℤ𝑀))
95 fzss1 12418 . . . . . . . . . . 11 ((𝐾 + 1) ∈ (ℤ𝑀) → ((𝐾 + 1)...(𝑁 + 1)) ⊆ (𝑀...(𝑁 + 1)))
9657, 94, 953syl 18 . . . . . . . . . 10 ((𝜑𝐾 ∈ (𝑀...𝑁)) → ((𝐾 + 1)...(𝑁 + 1)) ⊆ (𝑀...(𝑁 + 1)))
9750, 90, 51, 55, 91, 92, 93, 96seqf1olem2a 12879 . . . . . . . . 9 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (((𝐺𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)) + ((𝐺𝐹)‘𝐾)))
98 1zzd 11446 . . . . . . . . . . 11 ((𝜑𝐾 ∈ (𝑀...𝑁)) → 1 ∈ ℤ)
99 elfzuz 12376 . . . . . . . . . . . . . . . . . 18 (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ∈ (ℤ𝑀))
100 fzss1 12418 . . . . . . . . . . . . . . . . . 18 (𝐾 ∈ (ℤ𝑀) → (𝐾...𝑁) ⊆ (𝑀...𝑁))
10179, 99, 1003syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐾...𝑁) ⊆ (𝑀...𝑁))
102101sselda 3636 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐾...𝑁)) → 𝑥 ∈ (𝑀...𝑁))
10322ffvelrnda 6399 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝐽𝑥) ∈ (𝑀...𝑁))
104102, 103syldan 486 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (𝐽𝑥) ∈ (𝑀...𝑁))
105 fvres 6245 . . . . . . . . . . . . . . 15 ((𝐽𝑥) ∈ (𝑀...𝑁) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)) = (𝐺‘(𝐽𝑥)))
106104, 105syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐾...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)) = (𝐺‘(𝐽𝑥)))
107 breq1 4688 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑥 → (𝑘 < 𝐾𝑥 < 𝐾))
108 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑥𝑘 = 𝑥)
109 oveq1 6697 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑥 → (𝑘 + 1) = (𝑥 + 1))
110107, 108, 109ifbieq12d 4146 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑥 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)))
111110fveq2d 6233 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑥 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))))
112 fvex 6239 . . . . . . . . . . . . . . . . . 18 (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) ∈ V
113111, 18, 112fvmpt 6321 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝑀...𝑁) → (𝐽𝑥) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))))
114102, 113syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (𝐽𝑥) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))))
115 elfzle1 12382 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐾...𝑁) → 𝐾𝑥)
116115adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝐾...𝑁)) → 𝐾𝑥)
11779, 80syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐾 ∈ ℤ)
118117zred 11520 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 ∈ ℝ)
119118adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝐾...𝑁)) → 𝐾 ∈ ℝ)
120 elfzelz 12380 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐾...𝑁) → 𝑥 ∈ ℤ)
121120adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (𝐾...𝑁)) → 𝑥 ∈ ℤ)
122121zred 11520 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝐾...𝑁)) → 𝑥 ∈ ℝ)
123119, 122lenltd 10221 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (𝐾𝑥 ↔ ¬ 𝑥 < 𝐾))
124116, 123mpbid 222 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝐾...𝑁)) → ¬ 𝑥 < 𝐾)
125 iffalse 4128 . . . . . . . . . . . . . . . . . 18 𝑥 < 𝐾 → if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)) = (𝑥 + 1))
126125fveq2d 6233 . . . . . . . . . . . . . . . . 17 𝑥 < 𝐾 → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹‘(𝑥 + 1)))
127124, 126syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹‘(𝑥 + 1)))
128114, 127eqtrd 2685 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (𝐽𝑥) = (𝐹‘(𝑥 + 1)))
129128fveq2d 6233 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (𝐺‘(𝐽𝑥)) = (𝐺‘(𝐹‘(𝑥 + 1))))
130106, 129eqtrd 2685 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐾...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)) = (𝐺‘(𝐹‘(𝑥 + 1))))
131 fvco3 6314 . . . . . . . . . . . . . . 15 ((𝐽:(𝑀...𝑁)⟶(𝑀...𝑁) ∧ 𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)))
13222, 131sylan 487 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)))
133102, 132syldan 486 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)))
134 fzp1elp1 12432 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑀...𝑁) → (𝑥 + 1) ∈ (𝑀...(𝑁 + 1)))
135102, 134syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (𝑥 + 1) ∈ (𝑀...(𝑁 + 1)))
136 fvco3 6314 . . . . . . . . . . . . . . 15 ((𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)) ∧ (𝑥 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐺𝐹)‘(𝑥 + 1)) = (𝐺‘(𝐹‘(𝑥 + 1))))
13759, 136sylan 487 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐺𝐹)‘(𝑥 + 1)) = (𝐺‘(𝐹‘(𝑥 + 1))))
138135, 137syldan 486 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐾...𝑁)) → ((𝐺𝐹)‘(𝑥 + 1)) = (𝐺‘(𝐹‘(𝑥 + 1))))
139130, 133, 1383eqtr4d 2695 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺𝐹)‘(𝑥 + 1)))
140139adantlr 751 . . . . . . . . . . 11 (((𝜑𝐾 ∈ (𝑀...𝑁)) ∧ 𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺𝐹)‘(𝑥 + 1)))
14153, 98, 140seqshft2 12867 . . . . . . . . . 10 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)))
142 fvco3 6314 . . . . . . . . . . . . 13 ((𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)) ∧ 𝐾 ∈ (𝑀...(𝑁 + 1))) → ((𝐺𝐹)‘𝐾) = (𝐺‘(𝐹𝐾)))
14359, 79, 142syl2anc 694 . . . . . . . . . . . 12 (𝜑 → ((𝐺𝐹)‘𝐾) = (𝐺‘(𝐹𝐾)))
14419fveq2i 6232 . . . . . . . . . . . . . 14 (𝐹𝐾) = (𝐹‘(𝐹‘(𝑁 + 1)))
145 f1ocnvfv2 6573 . . . . . . . . . . . . . . 15 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) → (𝐹‘(𝐹‘(𝑁 + 1))) = (𝑁 + 1))
14617, 77, 145syl2anc 694 . . . . . . . . . . . . . 14 (𝜑 → (𝐹‘(𝐹‘(𝑁 + 1))) = (𝑁 + 1))
147144, 146syl5eq 2697 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝐾) = (𝑁 + 1))
148147fveq2d 6233 . . . . . . . . . . . 12 (𝜑 → (𝐺‘(𝐹𝐾)) = (𝐺‘(𝑁 + 1)))
149143, 148eqtr2d 2686 . . . . . . . . . . 11 (𝜑 → (𝐺‘(𝑁 + 1)) = ((𝐺𝐹)‘𝐾))
150149adantr 480 . . . . . . . . . 10 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (𝐺‘(𝑁 + 1)) = ((𝐺𝐹)‘𝐾))
151141, 150oveq12d 6708 . . . . . . . . 9 ((𝜑𝐾 ∈ (𝑀...𝑁)) → ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))) = ((seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)) + ((𝐺𝐹)‘𝐾)))
15297, 151eqtr4d 2688 . . . . . . . 8 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (((𝐺𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
15389, 152syldan 486 . . . . . . 7 ((𝜑𝐾 = 𝑀) → (((𝐺𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
15485seqeq1d 12847 . . . . . . . . 9 ((𝜑𝐾 = 𝑀) → seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)) = seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)))
155154fveq1d 6231 . . . . . . . 8 ((𝜑𝐾 = 𝑀) → (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁))
156155oveq1d 6705 . . . . . . 7 ((𝜑𝐾 = 𝑀) → ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
15784, 153, 1563eqtrd 2689 . . . . . 6 ((𝜑𝐾 = 𝑀) → ((seq𝑀( + , (𝐺𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
158 eluzel2 11730 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
15915, 158syl 17 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℤ)
160 elfzuz 12376 . . . . . . . . . . 11 (𝐾 ∈ ((𝑀 + 1)...𝑁) → 𝐾 ∈ (ℤ‘(𝑀 + 1)))
161 eluzp1m1 11749 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (ℤ‘(𝑀 + 1))) → (𝐾 − 1) ∈ (ℤ𝑀))
162159, 160, 161syl2an 493 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (𝐾 − 1) ∈ (ℤ𝑀))
163 eluzelz 11735 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
16415, 163syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℤ)
165164zcnd 11521 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℂ)
166 ax-1cn 10032 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℂ
167 pncan 10325 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
168165, 166, 167sylancl 695 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
169 peano2zm 11458 . . . . . . . . . . . . . . . . . . . 20 (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ)
17079, 80, 1693syl 18 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐾 − 1) ∈ ℤ)
171 elfzuz3 12377 . . . . . . . . . . . . . . . . . . . . 21 (𝐾 ∈ (𝑀...(𝑁 + 1)) → (𝑁 + 1) ∈ (ℤ𝐾))
17279, 171syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑁 + 1) ∈ (ℤ𝐾))
173117zcnd 11521 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐾 ∈ ℂ)
174 npcan 10328 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 − 1) + 1) = 𝐾)
175173, 166, 174sylancl 695 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐾 − 1) + 1) = 𝐾)
176175fveq2d 6233 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ℤ‘((𝐾 − 1) + 1)) = (ℤ𝐾))
177172, 176eleqtrrd 2733 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 + 1) ∈ (ℤ‘((𝐾 − 1) + 1)))
178 eluzp1m1 11749 . . . . . . . . . . . . . . . . . . 19 (((𝐾 − 1) ∈ ℤ ∧ (𝑁 + 1) ∈ (ℤ‘((𝐾 − 1) + 1))) → ((𝑁 + 1) − 1) ∈ (ℤ‘(𝐾 − 1)))
179170, 177, 178syl2anc 694 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑁 + 1) − 1) ∈ (ℤ‘(𝐾 − 1)))
180168, 179eqeltrrd 2731 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ (ℤ‘(𝐾 − 1)))
181 fzss2 12419 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘(𝐾 − 1)) → (𝑀...(𝐾 − 1)) ⊆ (𝑀...𝑁))
182180, 181syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀...(𝐾 − 1)) ⊆ (𝑀...𝑁))
183182sselda 3636 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → 𝑥 ∈ (𝑀...𝑁))
184183, 103syldan 486 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐽𝑥) ∈ (𝑀...𝑁))
185184, 105syl 17 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)) = (𝐺‘(𝐽𝑥)))
186183, 113syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐽𝑥) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))))
187 elfzm11 12449 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑥 ∈ (𝑀...(𝐾 − 1)) ↔ (𝑥 ∈ ℤ ∧ 𝑀𝑥𝑥 < 𝐾)))
188159, 117, 187syl2anc 694 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑥 ∈ (𝑀...(𝐾 − 1)) ↔ (𝑥 ∈ ℤ ∧ 𝑀𝑥𝑥 < 𝐾)))
189188biimpa 500 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝑥 ∈ ℤ ∧ 𝑀𝑥𝑥 < 𝐾))
190189simp3d 1095 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → 𝑥 < 𝐾)
191 iftrue 4125 . . . . . . . . . . . . . . . . 17 (𝑥 < 𝐾 → if(𝑥 < 𝐾, 𝑥, (𝑥 + 1)) = 𝑥)
192191fveq2d 6233 . . . . . . . . . . . . . . . 16 (𝑥 < 𝐾 → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹𝑥))
193190, 192syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹𝑥))
194186, 193eqtrd 2685 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐽𝑥) = (𝐹𝑥))
195194fveq2d 6233 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐺‘(𝐽𝑥)) = (𝐺‘(𝐹𝑥)))
196185, 195eqtr2d 2686 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (𝐺‘(𝐹𝑥)) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)))
197 peano2uz 11779 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ‘(𝐾 − 1)) → (𝑁 + 1) ∈ (ℤ‘(𝐾 − 1)))
198 fzss2 12419 . . . . . . . . . . . . . . 15 ((𝑁 + 1) ∈ (ℤ‘(𝐾 − 1)) → (𝑀...(𝐾 − 1)) ⊆ (𝑀...(𝑁 + 1)))
199180, 197, 1983syl 18 . . . . . . . . . . . . . 14 (𝜑 → (𝑀...(𝐾 − 1)) ⊆ (𝑀...(𝑁 + 1)))
200199sselda 3636 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
201 fvco3 6314 . . . . . . . . . . . . . 14 ((𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
20259, 201sylan 487 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
203200, 202syldan 486 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
204183, 132syldan 486 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)))
205196, 203, 2043eqtr4d 2695 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺𝐹)‘𝑥) = (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥))
206205adantlr 751 . . . . . . . . . 10 (((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺𝐹)‘𝑥) = (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥))
207162, 206seqfveq 12865 . . . . . . . . 9 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) = (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)))
208 fzp1ss 12430 . . . . . . . . . . . 12 (𝑀 ∈ ℤ → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁))
20915, 158, 2083syl 18 . . . . . . . . . . 11 (𝜑 → ((𝑀 + 1)...𝑁) ⊆ (𝑀...𝑁))
210209sselda 3636 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝐾 ∈ (𝑀...𝑁))
211210, 152syldan 486 . . . . . . . . 9 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (((𝐺𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
212207, 211oveq12d 6708 . . . . . . . 8 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) + (((𝐺𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))))
213200, 63syldan 486 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺𝐹)‘𝑥) ∈ 𝑆)
214213adantlr 751 . . . . . . . . . . 11 (((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → ((𝐺𝐹)‘𝑥) ∈ 𝑆)
21512adantlr 751 . . . . . . . . . . 11 (((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
216162, 214, 215seqcl 12861 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) ∈ 𝑆)
21761, 79ffvelrnd 6400 . . . . . . . . . . . 12 (𝜑 → ((𝐺𝐹)‘𝐾) ∈ 𝐶)
21816, 217sseldd 3637 . . . . . . . . . . 11 (𝜑 → ((𝐺𝐹)‘𝐾) ∈ 𝑆)
219218adantr 480 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((𝐺𝐹)‘𝐾) ∈ 𝑆)
22096sselda 3636 . . . . . . . . . . . . 13 (((𝜑𝐾 ∈ (𝑀...𝑁)) ∧ 𝑥 ∈ ((𝐾 + 1)...(𝑁 + 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
221220, 64syldan 486 . . . . . . . . . . . 12 (((𝜑𝐾 ∈ (𝑀...𝑁)) ∧ 𝑥 ∈ ((𝐾 + 1)...(𝑁 + 1))) → ((𝐺𝐹)‘𝑥) ∈ 𝑆)
22255, 221, 50seqcl 12861 . . . . . . . . . . 11 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)) ∈ 𝑆)
223210, 222syldan 486 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)) ∈ 𝑆)
224216, 219, 2233jca 1261 . . . . . . . . 9 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) ∈ 𝑆 ∧ ((𝐺𝐹)‘𝐾) ∈ 𝑆 ∧ (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)) ∈ 𝑆))
22514caovassg 6874 . . . . . . . . 9 ((𝜑 ∧ ((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) ∈ 𝑆 ∧ ((𝐺𝐹)‘𝐾) ∈ 𝑆 ∧ (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)) ∈ 𝑆)) → (((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) + ((𝐺𝐹)‘𝐾)) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) + (((𝐺𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)))))
226224, 225syldan 486 . . . . . . . 8 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) + ((𝐺𝐹)‘𝐾)) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) + (((𝐺𝐹)‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1)))))
2271, 16fssd 6095 . . . . . . . . . . . . . . . 16 (𝜑𝐺:(𝑀...(𝑁 + 1))⟶𝑆)
228 fssres 6108 . . . . . . . . . . . . . . . 16 ((𝐺:(𝑀...(𝑁 + 1))⟶𝑆 ∧ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))) → (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝑆)
229227, 4, 228sylancl 695 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝑆)
230 fco 6096 . . . . . . . . . . . . . . 15 (((𝐺 ↾ (𝑀...𝑁)):(𝑀...𝑁)⟶𝑆𝐽:(𝑀...𝑁)⟶(𝑀...𝑁)) → ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽):(𝑀...𝑁)⟶𝑆)
231229, 22, 230syl2anc 694 . . . . . . . . . . . . . 14 (𝜑 → ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽):(𝑀...𝑁)⟶𝑆)
232231ffvelrnda 6399 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆)
233183, 232syldan 486 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝑀...(𝐾 − 1))) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆)
234233adantlr 751 . . . . . . . . . . 11 (((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝑀...(𝐾 − 1))) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆)
235162, 234, 215seqcl 12861 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) ∈ 𝑆)
236 elfzuz3 12377 . . . . . . . . . . . 12 (𝐾 ∈ ((𝑀 + 1)...𝑁) → 𝑁 ∈ (ℤ𝐾))
237236adantl 481 . . . . . . . . . . 11 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝑁 ∈ (ℤ𝐾))
238102, 232syldan 486 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆)
239238adantlr 751 . . . . . . . . . . 11 (((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝐾...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆)
240237, 239, 215seqcl 12861 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) ∈ 𝑆)
241227, 77ffvelrnd 6400 . . . . . . . . . . 11 (𝜑 → (𝐺‘(𝑁 + 1)) ∈ 𝑆)
242241adantr 480 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (𝐺‘(𝑁 + 1)) ∈ 𝑆)
243235, 240, 2423jca 1261 . . . . . . . . 9 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) ∈ 𝑆 ∧ (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) ∈ 𝑆 ∧ (𝐺‘(𝑁 + 1)) ∈ 𝑆))
24414caovassg 6874 . . . . . . . . 9 ((𝜑 ∧ ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) ∈ 𝑆 ∧ (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) ∈ 𝑆 ∧ (𝐺‘(𝑁 + 1)) ∈ 𝑆)) → (((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) + (𝐺‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))))
245243, 244syldan 486 . . . . . . . 8 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) + (𝐺‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + ((seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1)))))
246212, 226, 2453eqtr4d 2695 . . . . . . 7 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) + ((𝐺𝐹)‘𝐾)) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = (((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) + (𝐺‘(𝑁 + 1))))
247 seqm1 12858 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (ℤ‘(𝑀 + 1))) → (seq𝑀( + , (𝐺𝐹))‘𝐾) = ((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) + ((𝐺𝐹)‘𝐾)))
248159, 160, 247syl2an 493 . . . . . . . 8 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , (𝐺𝐹))‘𝐾) = ((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) + ((𝐺𝐹)‘𝐾)))
249248oveq1d 6705 . . . . . . 7 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , (𝐺𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = (((seq𝑀( + , (𝐺𝐹))‘(𝐾 − 1)) + ((𝐺𝐹)‘𝐾)) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))))
25014adantlr 751 . . . . . . . . . 10 (((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
251 elfzelz 12380 . . . . . . . . . . . . . . 15 (𝐾 ∈ ((𝑀 + 1)...𝑁) → 𝐾 ∈ ℤ)
252251adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝐾 ∈ ℤ)
253252zcnd 11521 . . . . . . . . . . . . 13 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝐾 ∈ ℂ)
254253, 166, 174sylancl 695 . . . . . . . . . . . 12 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((𝐾 − 1) + 1) = 𝐾)
255254fveq2d 6233 . . . . . . . . . . 11 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (ℤ‘((𝐾 − 1) + 1)) = (ℤ𝐾))
256237, 255eleqtrrd 2733 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → 𝑁 ∈ (ℤ‘((𝐾 − 1) + 1)))
257232adantlr 751 . . . . . . . . . 10 (((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) ∈ 𝑆)
258215, 250, 256, 162, 257seqsplit 12874 . . . . . . . . 9 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq((𝐾 − 1) + 1)( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)))
259254seqeq1d 12847 . . . . . . . . . . 11 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → seq((𝐾 − 1) + 1)( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)) = seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)))
260259fveq1d 6231 . . . . . . . . . 10 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq((𝐾 − 1) + 1)( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁))
261260oveq2d 6706 . . . . . . . . 9 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq((𝐾 − 1) + 1)( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)))
262258, 261eqtrd 2685 . . . . . . . 8 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)))
263262oveq1d 6705 . . . . . . 7 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))) = (((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘(𝐾 − 1)) + (seq𝐾( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁)) + (𝐺‘(𝑁 + 1))))
264246, 249, 2633eqtr4d 2695 . . . . . 6 ((𝜑𝐾 ∈ ((𝑀 + 1)...𝑁)) → ((seq𝑀( + , (𝐺𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
265157, 264jaodan 843 . . . . 5 ((𝜑 ∧ (𝐾 = 𝑀𝐾 ∈ ((𝑀 + 1)...𝑁))) → ((seq𝑀( + , (𝐺𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
26668, 265syldan 486 . . . 4 ((𝜑𝐾 ∈ (𝑀...𝑁)) → ((seq𝑀( + , (𝐺𝐹))‘𝐾) + (seq(𝐾 + 1)( + , (𝐺𝐹))‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
26765, 266eqtrd 2685 . . 3 ((𝜑𝐾 ∈ (𝑀...𝑁)) → (seq𝑀( + , (𝐺𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
26815adantr 480 . . . . 5 ((𝜑𝐾 = (𝑁 + 1)) → 𝑁 ∈ (ℤ𝑀))
269 seqp1 12856 . . . . 5 (𝑁 ∈ (ℤ𝑀) → (seq𝑀( + , (𝐺𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , (𝐺𝐹))‘𝑁) + ((𝐺𝐹)‘(𝑁 + 1))))
270268, 269syl 17 . . . 4 ((𝜑𝐾 = (𝑁 + 1)) → (seq𝑀( + , (𝐺𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , (𝐺𝐹))‘𝑁) + ((𝐺𝐹)‘(𝑁 + 1))))
271113adantl 481 . . . . . . . . . 10 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐽𝑥) = (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))))
272 elfzelz 12380 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ)
273272zred 11520 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℝ)
274273adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ)
275164zred 11520 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℝ)
276275adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℝ)
277 peano2re 10247 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
278276, 277syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈ ℝ)
279 elfzle2 12383 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑀...𝑁) → 𝑥𝑁)
280279adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥𝑁)
281276ltp1d 10992 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑁 < (𝑁 + 1))
282274, 276, 278, 280, 281lelttrd 10233 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1))
283282adantlr 751 . . . . . . . . . . . 12 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1))
284 simplr 807 . . . . . . . . . . . 12 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 = (𝑁 + 1))
285283, 284breqtrrd 4713 . . . . . . . . . . 11 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 < 𝐾)
286285, 192syl 17 . . . . . . . . . 10 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘if(𝑥 < 𝐾, 𝑥, (𝑥 + 1))) = (𝐹𝑥))
287271, 286eqtrd 2685 . . . . . . . . 9 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐽𝑥) = (𝐹𝑥))
288287fveq2d 6233 . . . . . . . 8 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐹𝑥)))
289273adantl 481 . . . . . . . . . . 11 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ)
290289, 285gtned 10210 . . . . . . . . . 10 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾𝑥)
29159ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
292 fzelp1 12431 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
293292adantl 481 . . . . . . . . . . . . . . 15 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
294291, 293ffvelrnd 6400 . . . . . . . . . . . . . 14 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹𝑥) ∈ (𝑀...(𝑁 + 1)))
29515ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ (ℤ𝑀))
296 elfzp1 12429 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ𝑀) → ((𝐹𝑥) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹𝑥) ∈ (𝑀...𝑁) ∨ (𝐹𝑥) = (𝑁 + 1))))
297295, 296syl 17 . . . . . . . . . . . . . 14 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹𝑥) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹𝑥) ∈ (𝑀...𝑁) ∨ (𝐹𝑥) = (𝑁 + 1))))
298294, 297mpbid 222 . . . . . . . . . . . . 13 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹𝑥) ∈ (𝑀...𝑁) ∨ (𝐹𝑥) = (𝑁 + 1)))
299298ord 391 . . . . . . . . . . . 12 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (¬ (𝐹𝑥) ∈ (𝑀...𝑁) → (𝐹𝑥) = (𝑁 + 1)))
30017ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
301 f1ocnvfv 6574 . . . . . . . . . . . . . 14 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → ((𝐹𝑥) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = 𝑥))
302300, 293, 301syl2anc 694 . . . . . . . . . . . . 13 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹𝑥) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = 𝑥))
30319eqeq1i 2656 . . . . . . . . . . . . 13 (𝐾 = 𝑥 ↔ (𝐹‘(𝑁 + 1)) = 𝑥)
304302, 303syl6ibr 242 . . . . . . . . . . . 12 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐹𝑥) = (𝑁 + 1) → 𝐾 = 𝑥))
305299, 304syld 47 . . . . . . . . . . 11 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (¬ (𝐹𝑥) ∈ (𝑀...𝑁) → 𝐾 = 𝑥))
306305necon1ad 2840 . . . . . . . . . 10 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐾𝑥 → (𝐹𝑥) ∈ (𝑀...𝑁)))
307290, 306mpd 15 . . . . . . . . 9 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹𝑥) ∈ (𝑀...𝑁))
308 fvres 6245 . . . . . . . . 9 ((𝐹𝑥) ∈ (𝑀...𝑁) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐹𝑥)) = (𝐺‘(𝐹𝑥)))
309307, 308syl 17 . . . . . . . 8 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺 ↾ (𝑀...𝑁))‘(𝐹𝑥)) = (𝐺‘(𝐹𝑥)))
310288, 309eqtr2d 2686 . . . . . . 7 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐺‘(𝐹𝑥)) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)))
31159, 292, 201syl2an 493 . . . . . . . 8 ((𝜑𝑥 ∈ (𝑀...𝑁)) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
312311adantlr 751 . . . . . . 7 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
313132adantlr 751 . . . . . . 7 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥) = ((𝐺 ↾ (𝑀...𝑁))‘(𝐽𝑥)))
314310, 312, 3133eqtr4d 2695 . . . . . 6 (((𝜑𝐾 = (𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...𝑁)) → ((𝐺𝐹)‘𝑥) = (((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽)‘𝑥))
315268, 314seqfveq 12865 . . . . 5 ((𝜑𝐾 = (𝑁 + 1)) → (seq𝑀( + , (𝐺𝐹))‘𝑁) = (seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁))
316 fvco3 6314 . . . . . . . 8 ((𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)) ∧ (𝑁 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐺𝐹)‘(𝑁 + 1)) = (𝐺‘(𝐹‘(𝑁 + 1))))
31759, 77, 316syl2anc 694 . . . . . . 7 (𝜑 → ((𝐺𝐹)‘(𝑁 + 1)) = (𝐺‘(𝐹‘(𝑁 + 1))))
318317adantr 480 . . . . . 6 ((𝜑𝐾 = (𝑁 + 1)) → ((𝐺𝐹)‘(𝑁 + 1)) = (𝐺‘(𝐹‘(𝑁 + 1))))
319 simpr 476 . . . . . . . . . 10 ((𝜑𝐾 = (𝑁 + 1)) → 𝐾 = (𝑁 + 1))
32019, 319syl5eqr 2699 . . . . . . . . 9 ((𝜑𝐾 = (𝑁 + 1)) → (𝐹‘(𝑁 + 1)) = (𝑁 + 1))
321320fveq2d 6233 . . . . . . . 8 ((𝜑𝐾 = (𝑁 + 1)) → (𝐹‘(𝐹‘(𝑁 + 1))) = (𝐹‘(𝑁 + 1)))
322146adantr 480 . . . . . . . 8 ((𝜑𝐾 = (𝑁 + 1)) → (𝐹‘(𝐹‘(𝑁 + 1))) = (𝑁 + 1))
323321, 322eqtr3d 2687 . . . . . . 7 ((𝜑𝐾 = (𝑁 + 1)) → (𝐹‘(𝑁 + 1)) = (𝑁 + 1))
324323fveq2d 6233 . . . . . 6 ((𝜑𝐾 = (𝑁 + 1)) → (𝐺‘(𝐹‘(𝑁 + 1))) = (𝐺‘(𝑁 + 1)))
325318, 324eqtrd 2685 . . . . 5 ((𝜑𝐾 = (𝑁 + 1)) → ((𝐺𝐹)‘(𝑁 + 1)) = (𝐺‘(𝑁 + 1)))
326315, 325oveq12d 6708 . . . 4 ((𝜑𝐾 = (𝑁 + 1)) → ((seq𝑀( + , (𝐺𝐹))‘𝑁) + ((𝐺𝐹)‘(𝑁 + 1))) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
327270, 326eqtrd 2685 . . 3 ((𝜑𝐾 = (𝑁 + 1)) → (seq𝑀( + , (𝐺𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
328 elfzp1 12429 . . . . 5 (𝑁 ∈ (ℤ𝑀) → (𝐾 ∈ (𝑀...(𝑁 + 1)) ↔ (𝐾 ∈ (𝑀...𝑁) ∨ 𝐾 = (𝑁 + 1))))
32915, 328syl 17 . . . 4 (𝜑 → (𝐾 ∈ (𝑀...(𝑁 + 1)) ↔ (𝐾 ∈ (𝑀...𝑁) ∨ 𝐾 = (𝑁 + 1))))
33079, 329mpbid 222 . . 3 (𝜑 → (𝐾 ∈ (𝑀...𝑁) ∨ 𝐾 = (𝑁 + 1)))
331267, 327, 330mpjaodan 844 . 2 (𝜑 → (seq𝑀( + , (𝐺𝐹))‘(𝑁 + 1)) = ((seq𝑀( + , ((𝐺 ↾ (𝑀...𝑁)) ∘ 𝐽))‘𝑁) + (𝐺‘(𝑁 + 1))))
332 seqp1 12856 . . 3 (𝑁 ∈ (ℤ𝑀) → (seq𝑀( + , 𝐺)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘(𝑁 + 1))))
33315, 332syl 17 . 2 (𝜑 → (seq𝑀( + , 𝐺)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘(𝑁 + 1))))
33449, 331, 3333eqtr4d 2695 1 (𝜑 → (seq𝑀( + , (𝐺𝐹))‘(𝑁 + 1)) = (seq𝑀( + , 𝐺)‘(𝑁 + 1)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054  wal 1521   = wceq 1523  wcel 2030  wne 2823  Vcvv 3231  wss 3607  ifcif 4119   class class class wbr 4685  cmpt 4762  ccnv 5142  cres 5145  ccom 5147   Fn wfn 5921  wf 5922  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  Fincfn 7997  cc 9972  cr 9973  1c1 9975   + caddc 9977   < clt 10112  cle 10113  cmin 10304  cz 11415  cuz 11725  ...cfz 12364  seqcseq 12841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505  df-seq 12842
This theorem is referenced by:  seqf1o  12882
  Copyright terms: Public domain W3C validator