Step |
Hyp |
Ref |
Expression |
1 |
|
seqfeq3.m |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
2 |
|
seqfeq3.f |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 ) |
3 |
|
seqfeq3.cl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 ) |
4 |
|
seqfeq3.id |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥 𝑄 𝑦 ) ) |
5 |
|
seqfn |
⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑀 ) ) |
6 |
1 5
|
syl |
⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑀 ) ) |
7 |
|
seqfn |
⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( 𝑄 , 𝐹 ) Fn ( ℤ≥ ‘ 𝑀 ) ) |
8 |
1 7
|
syl |
⊢ ( 𝜑 → seq 𝑀 ( 𝑄 , 𝐹 ) Fn ( ℤ≥ ‘ 𝑀 ) ) |
9 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑎 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
10 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑎 ) ) → 𝜑 ) |
11 |
|
elfzuz |
⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑎 ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
12 |
11
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑎 ) ) → 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
13 |
10 12 2
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑎 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 ) |
14 |
3
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 ) |
15 |
4
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥 𝑄 𝑦 ) ) |
16 |
9 13 14 15
|
seqfeq4 |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑎 ) = ( seq 𝑀 ( 𝑄 , 𝐹 ) ‘ 𝑎 ) ) |
17 |
6 8 16
|
eqfnfvd |
⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) = seq 𝑀 ( 𝑄 , 𝐹 ) ) |