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

Theorem seqsplit 14040
Description: Split a sequence into two sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.)
Hypotheses
Ref Expression
seqsplit.1 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
seqsplit.2 ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
seqsplit.3 (𝜑𝑁 ∈ (ℤ‘(𝑀 + 1)))
seqsplit.4 (𝜑𝑀 ∈ (ℤ𝐾))
seqsplit.5 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (𝐹𝑥) ∈ 𝑆)
Assertion
Ref Expression
seqsplit (𝜑 → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁)))
Distinct variable groups:   𝑥,𝑦,𝑧,𝐹   𝑥,𝐾,𝑦,𝑧   𝑥,𝑀,𝑦,𝑧   𝜑,𝑥,𝑦,𝑧   𝑥,𝑁,𝑦,𝑧   𝑥, + ,𝑦,𝑧   𝑥,𝑆,𝑦,𝑧

Proof of Theorem seqsplit
Dummy variable 𝑛 is distinct from all other variables.
StepHypRef Expression
1 seqsplit.3 . . 3 (𝜑𝑁 ∈ (ℤ‘(𝑀 + 1)))
2 eluzfz2 13549 . . 3 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → 𝑁 ∈ ((𝑀 + 1)...𝑁))
31, 2syl 17 . 2 (𝜑𝑁 ∈ ((𝑀 + 1)...𝑁))
4 eleq1 2817 . . . . . 6 (𝑥 = (𝑀 + 1) → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...𝑁)))
5 fveq2 6902 . . . . . . 7 (𝑥 = (𝑀 + 1) → (seq𝐾( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐹)‘(𝑀 + 1)))
6 fveq2 6902 . . . . . . . 8 (𝑥 = (𝑀 + 1) → (seq(𝑀 + 1)( + , 𝐹)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1)))
76oveq2d 7442 . . . . . . 7 (𝑥 = (𝑀 + 1) → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1))))
85, 7eqeq12d 2744 . . . . . 6 (𝑥 = (𝑀 + 1) → ((seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) ↔ (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1)))))
94, 8imbi12d 343 . . . . 5 (𝑥 = (𝑀 + 1) → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥))) ↔ ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1))))))
109imbi2d 339 . . . 4 (𝑥 = (𝑀 + 1) → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)))) ↔ (𝜑 → ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1)))))))
11 eleq1 2817 . . . . . 6 (𝑥 = 𝑛 → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ 𝑛 ∈ ((𝑀 + 1)...𝑁)))
12 fveq2 6902 . . . . . . 7 (𝑥 = 𝑛 → (seq𝐾( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐹)‘𝑛))
13 fveq2 6902 . . . . . . . 8 (𝑥 = 𝑛 → (seq(𝑀 + 1)( + , 𝐹)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹)‘𝑛))
1413oveq2d 7442 . . . . . . 7 (𝑥 = 𝑛 → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)))
1512, 14eqeq12d 2744 . . . . . 6 (𝑥 = 𝑛 → ((seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) ↔ (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛))))
1611, 15imbi12d 343 . . . . 5 (𝑥 = 𝑛 → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥))) ↔ (𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)))))
1716imbi2d 339 . . . 4 (𝑥 = 𝑛 → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)))) ↔ (𝜑 → (𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛))))))
18 eleq1 2817 . . . . . 6 (𝑥 = (𝑛 + 1) → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)))
19 fveq2 6902 . . . . . . 7 (𝑥 = (𝑛 + 1) → (seq𝐾( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐹)‘(𝑛 + 1)))
20 fveq2 6902 . . . . . . . 8 (𝑥 = (𝑛 + 1) → (seq(𝑀 + 1)( + , 𝐹)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1)))
2120oveq2d 7442 . . . . . . 7 (𝑥 = (𝑛 + 1) → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))))
2219, 21eqeq12d 2744 . . . . . 6 (𝑥 = (𝑛 + 1) → ((seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) ↔ (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1)))))
2318, 22imbi12d 343 . . . . 5 (𝑥 = (𝑛 + 1) → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥))) ↔ ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))))))
2423imbi2d 339 . . . 4 (𝑥 = (𝑛 + 1) → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)))) ↔ (𝜑 → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1)))))))
25 eleq1 2817 . . . . . 6 (𝑥 = 𝑁 → (𝑥 ∈ ((𝑀 + 1)...𝑁) ↔ 𝑁 ∈ ((𝑀 + 1)...𝑁)))
26 fveq2 6902 . . . . . . 7 (𝑥 = 𝑁 → (seq𝐾( + , 𝐹)‘𝑥) = (seq𝐾( + , 𝐹)‘𝑁))
27 fveq2 6902 . . . . . . . 8 (𝑥 = 𝑁 → (seq(𝑀 + 1)( + , 𝐹)‘𝑥) = (seq(𝑀 + 1)( + , 𝐹)‘𝑁))
2827oveq2d 7442 . . . . . . 7 (𝑥 = 𝑁 → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁)))
2926, 28eqeq12d 2744 . . . . . 6 (𝑥 = 𝑁 → ((seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)) ↔ (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁))))
3025, 29imbi12d 343 . . . . 5 (𝑥 = 𝑁 → ((𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥))) ↔ (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁)))))
3130imbi2d 339 . . . 4 (𝑥 = 𝑁 → ((𝜑 → (𝑥 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑥) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑥)))) ↔ (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁))))))
32 seqsplit.4 . . . . . . 7 (𝜑𝑀 ∈ (ℤ𝐾))
33 seqp1 14021 . . . . . . 7 (𝑀 ∈ (ℤ𝐾) → (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (𝐹‘(𝑀 + 1))))
3432, 33syl 17 . . . . . 6 (𝜑 → (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (𝐹‘(𝑀 + 1))))
35 eluzel2 12865 . . . . . . . 8 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → (𝑀 + 1) ∈ ℤ)
36 seq1 14019 . . . . . . . 8 ((𝑀 + 1) ∈ ℤ → (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1)) = (𝐹‘(𝑀 + 1)))
371, 35, 363syl 18 . . . . . . 7 (𝜑 → (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1)) = (𝐹‘(𝑀 + 1)))
3837oveq2d 7442 . . . . . 6 (𝜑 → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1))) = ((seq𝐾( + , 𝐹)‘𝑀) + (𝐹‘(𝑀 + 1))))
3934, 38eqtr4d 2771 . . . . 5 (𝜑 → (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1))))
4039a1i13 27 . . . 4 ((𝑀 + 1) ∈ ℤ → (𝜑 → ((𝑀 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑀 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑀 + 1))))))
41 peano2fzr 13554 . . . . . . . 8 ((𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → 𝑛 ∈ ((𝑀 + 1)...𝑁))
4241adantl 480 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ ((𝑀 + 1)...𝑁))
4342expr 455 . . . . . 6 ((𝜑𝑛 ∈ (ℤ‘(𝑀 + 1))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → 𝑛 ∈ ((𝑀 + 1)...𝑁)))
4443imim1d 82 . . . . 5 ((𝜑𝑛 ∈ (ℤ‘(𝑀 + 1))) → ((𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛))) → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)))))
45 oveq1 7433 . . . . . 6 ((seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) → ((seq𝐾( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))) = (((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) + (𝐹‘(𝑛 + 1))))
46 simprl 769 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ (ℤ‘(𝑀 + 1)))
47 peano2uz 12923 . . . . . . . . . . 11 (𝑀 ∈ (ℤ𝐾) → (𝑀 + 1) ∈ (ℤ𝐾))
4832, 47syl 17 . . . . . . . . . 10 (𝜑 → (𝑀 + 1) ∈ (ℤ𝐾))
4948adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝑀 + 1) ∈ (ℤ𝐾))
50 uztrn 12878 . . . . . . . . 9 ((𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑀 + 1) ∈ (ℤ𝐾)) → 𝑛 ∈ (ℤ𝐾))
5146, 49, 50syl2anc 582 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝑛 ∈ (ℤ𝐾))
52 seqp1 14021 . . . . . . . 8 (𝑛 ∈ (ℤ𝐾) → (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))
5351, 52syl 17 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))
54 seqp1 14021 . . . . . . . . . 10 (𝑛 ∈ (ℤ‘(𝑀 + 1)) → (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1)) = ((seq(𝑀 + 1)( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))
5546, 54syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1)) = ((seq(𝑀 + 1)( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))))
5655oveq2d 7442 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))) = ((seq𝐾( + , 𝐹)‘𝑀) + ((seq(𝑀 + 1)( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))))
57 simpl 481 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → 𝜑)
58 eluzelz 12870 . . . . . . . . . . . . . . . 16 (𝑀 ∈ (ℤ𝐾) → 𝑀 ∈ ℤ)
5932, 58syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℤ)
60 peano2uzr 12925 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ‘(𝑀 + 1))) → 𝑁 ∈ (ℤ𝑀))
6159, 1, 60syl2anc 582 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ (ℤ𝑀))
62 fzss2 13581 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ𝑀) → (𝐾...𝑀) ⊆ (𝐾...𝑁))
6361, 62syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝐾...𝑀) ⊆ (𝐾...𝑁))
6463sselda 3982 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐾...𝑀)) → 𝑥 ∈ (𝐾...𝑁))
65 seqsplit.5 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐾...𝑁)) → (𝐹𝑥) ∈ 𝑆)
6664, 65syldan 589 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐾...𝑀)) → (𝐹𝑥) ∈ 𝑆)
67 seqsplit.1 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
6832, 66, 67seqcl 14027 . . . . . . . . . 10 (𝜑 → (seq𝐾( + , 𝐹)‘𝑀) ∈ 𝑆)
6968adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq𝐾( + , 𝐹)‘𝑀) ∈ 𝑆)
70 elfzuz3 13538 . . . . . . . . . . . . . 14 (𝑛 ∈ ((𝑀 + 1)...𝑁) → 𝑁 ∈ (ℤ𝑛))
71 fzss2 13581 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ𝑛) → ((𝑀 + 1)...𝑛) ⊆ ((𝑀 + 1)...𝑁))
7242, 70, 713syl 18 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((𝑀 + 1)...𝑛) ⊆ ((𝑀 + 1)...𝑁))
73 fzss1 13580 . . . . . . . . . . . . . . 15 ((𝑀 + 1) ∈ (ℤ𝐾) → ((𝑀 + 1)...𝑁) ⊆ (𝐾...𝑁))
7432, 47, 733syl 18 . . . . . . . . . . . . . 14 (𝜑 → ((𝑀 + 1)...𝑁) ⊆ (𝐾...𝑁))
7574adantr 479 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((𝑀 + 1)...𝑁) ⊆ (𝐾...𝑁))
7672, 75sstrd 3992 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((𝑀 + 1)...𝑛) ⊆ (𝐾...𝑁))
7776sselda 3982 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) ∧ 𝑥 ∈ ((𝑀 + 1)...𝑛)) → 𝑥 ∈ (𝐾...𝑁))
7865adantlr 713 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) ∧ 𝑥 ∈ (𝐾...𝑁)) → (𝐹𝑥) ∈ 𝑆)
7977, 78syldan 589 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) ∧ 𝑥 ∈ ((𝑀 + 1)...𝑛)) → (𝐹𝑥) ∈ 𝑆)
8067adantlr 713 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)
8146, 79, 80seqcl 14027 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (seq(𝑀 + 1)( + , 𝐹)‘𝑛) ∈ 𝑆)
82 fveq2 6902 . . . . . . . . . . 11 (𝑥 = (𝑛 + 1) → (𝐹𝑥) = (𝐹‘(𝑛 + 1)))
8382eleq1d 2814 . . . . . . . . . 10 (𝑥 = (𝑛 + 1) → ((𝐹𝑥) ∈ 𝑆 ↔ (𝐹‘(𝑛 + 1)) ∈ 𝑆))
8465ralrimiva 3143 . . . . . . . . . . 11 (𝜑 → ∀𝑥 ∈ (𝐾...𝑁)(𝐹𝑥) ∈ 𝑆)
8584adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ∀𝑥 ∈ (𝐾...𝑁)(𝐹𝑥) ∈ 𝑆)
86 simpr 483 . . . . . . . . . . 11 ((𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))
87 ssel2 3977 . . . . . . . . . . 11 ((((𝑀 + 1)...𝑁) ⊆ (𝐾...𝑁) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁)) → (𝑛 + 1) ∈ (𝐾...𝑁))
8874, 86, 87syl2an 594 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝑛 + 1) ∈ (𝐾...𝑁))
8983, 85, 88rspcdva 3612 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (𝐹‘(𝑛 + 1)) ∈ 𝑆)
90 seqsplit.2 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
9190caovassg 7625 . . . . . . . . 9 ((𝜑 ∧ ((seq𝐾( + , 𝐹)‘𝑀) ∈ 𝑆 ∧ (seq(𝑀 + 1)( + , 𝐹)‘𝑛) ∈ 𝑆 ∧ (𝐹‘(𝑛 + 1)) ∈ 𝑆)) → (((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) + (𝐹‘(𝑛 + 1))) = ((seq𝐾( + , 𝐹)‘𝑀) + ((seq(𝑀 + 1)( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))))
9257, 69, 81, 89, 91syl13anc 1369 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → (((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) + (𝐹‘(𝑛 + 1))) = ((seq𝐾( + , 𝐹)‘𝑀) + ((seq(𝑀 + 1)( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))))
9356, 92eqtr4d 2771 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))) = (((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) + (𝐹‘(𝑛 + 1))))
9453, 93eqeq12d 2744 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1))) ↔ ((seq𝐾( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1))) = (((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) + (𝐹‘(𝑛 + 1)))))
9545, 94imbitrrid 245 . . . . 5 ((𝜑 ∧ (𝑛 ∈ (ℤ‘(𝑀 + 1)) ∧ (𝑛 + 1) ∈ ((𝑀 + 1)...𝑁))) → ((seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)) → (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1)))))
9644, 95animpimp2impd 844 . . . 4 (𝑛 ∈ (ℤ‘(𝑀 + 1)) → ((𝜑 → (𝑛 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑛) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑛)))) → (𝜑 → ((𝑛 + 1) ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘(𝑛 + 1)) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘(𝑛 + 1)))))))
9710, 17, 24, 31, 40, 96uzind4 12928 . . 3 (𝑁 ∈ (ℤ‘(𝑀 + 1)) → (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁)))))
981, 97mpcom 38 . 2 (𝜑 → (𝑁 ∈ ((𝑀 + 1)...𝑁) → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁))))
993, 98mpd 15 1 (𝜑 → (seq𝐾( + , 𝐹)‘𝑁) = ((seq𝐾( + , 𝐹)‘𝑀) + (seq(𝑀 + 1)( + , 𝐹)‘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3058  wss 3949  cfv 6553  (class class class)co 7426  1c1 11147   + caddc 11149  cz 12596  cuz 12860  ...cfz 13524  seqcseq 14006
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-1st 7999  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-er 8731  df-en 8971  df-dom 8972  df-sdom 8973  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-nn 12251  df-n0 12511  df-z 12597  df-uz 12861  df-fz 13525  df-seq 14007
This theorem is referenced by:  seq1p  14041  seqf1olem2  14047  bcval5  14317  clim2ser  15641  clim2ser2  15642  isumsplit  15826  clim2div  15875  gsumsgrpccat  18799  mulgnndir  19065  mblfinlem2  37164  fmul01lt1lem1  45001  fmul01lt1lem2  45002
  Copyright terms: Public domain W3C validator