Metamath Proof Explorer

Theorem seqcaopr3

Description: Lemma for seqcaopr2 . (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses seqcaopr3.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
seqcaopr3.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 𝑄 𝑦 ) ∈ 𝑆 )
seqcaopr3.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
seqcaopr3.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 )
seqcaopr3.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝑆 )
seqcaopr3.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) 𝑄 ( 𝐺 ‘ 𝑘 ) ) )
seqcaopr3.7 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) + ( ( 𝐹 ‘ ( 𝑛 + 1 ) ) 𝑄 ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) = ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) 𝑄 ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
Assertion seqcaopr3 ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 seqcaopr3.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
2 seqcaopr3.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 𝑄 𝑦 ) ∈ 𝑆 )
3 seqcaopr3.3 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
4 seqcaopr3.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑆 )
5 seqcaopr3.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝑆 )
6 seqcaopr3.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) 𝑄 ( 𝐺 ‘ 𝑘 ) ) )
7 seqcaopr3.7 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) + ( ( 𝐹 ‘ ( 𝑛 + 1 ) ) 𝑄 ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) = ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) 𝑄 ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
8 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
9 3 8 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
10 fveq2 ⊢ ( 𝑧 = 𝑀 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑧 ) = ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑀 ) )
11 fveq2 ⊢ ( 𝑧 = 𝑀 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) )
12 fveq2 ⊢ ( 𝑧 = 𝑀 → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑧 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) )
13 11 12 oveq12d ⊢ ( 𝑧 = 𝑀 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑧 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) ) )
14 10 13 eqeq12d ⊢ ( 𝑧 = 𝑀 → ( ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑧 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑧 ) ) ↔ ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑀 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) ) ) )
15 14 imbi2d ⊢ ( 𝑧 = 𝑀 → ( ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑧 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑧 ) ) ) ↔ ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑀 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) ) ) ) )
16 fveq2 ⊢ ( 𝑧 = 𝑛 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑧 ) = ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑛 ) )
17 fveq2 ⊢ ( 𝑧 = 𝑛 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) )
18 fveq2 ⊢ ( 𝑧 = 𝑛 → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑧 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) )
19 17 18 oveq12d ⊢ ( 𝑧 = 𝑛 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑧 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) )
20 16 19 eqeq12d ⊢ ( 𝑧 = 𝑛 → ( ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑧 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑧 ) ) ↔ ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) ) )
21 20 imbi2d ⊢ ( 𝑧 = 𝑛 → ( ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑧 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑧 ) ) ) ↔ ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) ) ) )
22 fveq2 ⊢ ( 𝑧 = ( 𝑛 + 1 ) → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑧 ) = ( seq 𝑀 ( + , 𝐻 ) ‘ ( 𝑛 + 1 ) ) )
23 fveq2 ⊢ ( 𝑧 = ( 𝑛 + 1 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) )
24 fveq2 ⊢ ( 𝑧 = ( 𝑛 + 1 ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑧 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) )
25 23 24 oveq12d ⊢ ( 𝑧 = ( 𝑛 + 1 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑧 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) )
26 22 25 eqeq12d ⊢ ( 𝑧 = ( 𝑛 + 1 ) → ( ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑧 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑧 ) ) ↔ ( seq 𝑀 ( + , 𝐻 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) ) )
27 26 imbi2d ⊢ ( 𝑧 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑧 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑧 ) ) ) ↔ ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) ) ) )
28 fveq2 ⊢ ( 𝑧 = 𝑁 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑧 ) = ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑁 ) )
29 fveq2 ⊢ ( 𝑧 = 𝑁 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
30 fveq2 ⊢ ( 𝑧 = 𝑁 → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑧 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) )
31 29 30 oveq12d ⊢ ( 𝑧 = 𝑁 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑧 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )
32 28 31 eqeq12d ⊢ ( 𝑧 = 𝑁 → ( ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑧 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑧 ) ) ↔ ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) ) )
33 32 imbi2d ⊢ ( 𝑧 = 𝑁 → ( ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑧 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑧 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑧 ) ) ) ↔ ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) ) ) )
34 fveq2 ⊢ ( 𝑘 = 𝑀 → ( 𝐻 ‘ 𝑘 ) = ( 𝐻 ‘ 𝑀 ) )
35 fveq2 ⊢ ( 𝑘 = 𝑀 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑀 ) )
36 fveq2 ⊢ ( 𝑘 = 𝑀 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑀 ) )
37 35 36 oveq12d ⊢ ( 𝑘 = 𝑀 → ( ( 𝐹 ‘ 𝑘 ) 𝑄 ( 𝐺 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑀 ) 𝑄 ( 𝐺 ‘ 𝑀 ) ) )
38 34 37 eqeq12d ⊢ ( 𝑘 = 𝑀 → ( ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) 𝑄 ( 𝐺 ‘ 𝑘 ) ) ↔ ( 𝐻 ‘ 𝑀 ) = ( ( 𝐹 ‘ 𝑀 ) 𝑄 ( 𝐺 ‘ 𝑀 ) ) ) )
39 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) 𝑄 ( 𝐺 ‘ 𝑘 ) ) )
40 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
41 3 40 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
42 38 39 41 rspcdva ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑀 ) = ( ( 𝐹 ‘ 𝑀 ) 𝑄 ( 𝐺 ‘ 𝑀 ) ) )
43 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
44 3 43 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
45 seq1 ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑀 ) = ( 𝐻 ‘ 𝑀 ) )
46 44 45 syl ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑀 ) = ( 𝐻 ‘ 𝑀 ) )
47 seq1 ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
48 seq1 ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) = ( 𝐺 ‘ 𝑀 ) )
49 47 48 oveq12d ⊢ ( 𝑀 ∈ ℤ → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) ) = ( ( 𝐹 ‘ 𝑀 ) 𝑄 ( 𝐺 ‘ 𝑀 ) ) )
50 44 49 syl ⊢ ( 𝜑 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) ) = ( ( 𝐹 ‘ 𝑀 ) 𝑄 ( 𝐺 ‘ 𝑀 ) ) )
51 42 46 50 3eqtr4d ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑀 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) ) )
52 51 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑀 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑀 ) ) ) )
53 oveq1 ⊢ ( ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) → ( ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑛 ) + ( 𝐻 ‘ ( 𝑛 + 1 ) ) ) = ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) + ( 𝐻 ‘ ( 𝑛 + 1 ) ) ) )
54 elfzouz ⊢ ( 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
55 54 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
56 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐻 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑛 ) + ( 𝐻 ‘ ( 𝑛 + 1 ) ) ) )
57 55 56 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( seq 𝑀 ( + , 𝐻 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑛 ) + ( 𝐻 ‘ ( 𝑛 + 1 ) ) ) )
58 fveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐻 ‘ ( 𝑛 + 1 ) ) )
59 fveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
60 fveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑛 + 1 ) ) )
61 59 60 oveq12d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) 𝑄 ( 𝐺 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ ( 𝑛 + 1 ) ) 𝑄 ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
62 58 61 eqeq12d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) 𝑄 ( 𝐺 ‘ 𝑘 ) ) ↔ ( 𝐻 ‘ ( 𝑛 + 1 ) ) = ( ( 𝐹 ‘ ( 𝑛 + 1 ) ) 𝑄 ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
63 39 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ( 𝐻 ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) 𝑄 ( 𝐺 ‘ 𝑘 ) ) )
64 fzofzp1 ⊢ ( 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
65 64 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
66 62 63 65 rspcdva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐻 ‘ ( 𝑛 + 1 ) ) = ( ( 𝐹 ‘ ( 𝑛 + 1 ) ) 𝑄 ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
67 66 oveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) + ( 𝐻 ‘ ( 𝑛 + 1 ) ) ) = ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) + ( ( 𝐹 ‘ ( 𝑛 + 1 ) ) 𝑄 ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
68 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
69 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) )
70 68 69 oveq12d ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) 𝑄 ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
71 55 70 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) + ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) 𝑄 ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) + ( 𝐺 ‘ ( 𝑛 + 1 ) ) ) ) )
72 7 67 71 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) = ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) + ( 𝐻 ‘ ( 𝑛 + 1 ) ) ) )
73 57 72 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( seq 𝑀 ( + , 𝐻 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) ↔ ( ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑛 ) + ( 𝐻 ‘ ( 𝑛 + 1 ) ) ) = ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) + ( 𝐻 ‘ ( 𝑛 + 1 ) ) ) ) )
74 53 73 syl5ibr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) → ( seq 𝑀 ( + , 𝐻 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) ) )
75 74 expcom ⊢ ( 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝜑 → ( ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) → ( seq 𝑀 ( + , 𝐻 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) ) ) )
76 75 a2d ⊢ ( 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) → ( ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑛 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ) ) → ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑛 + 1 ) ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ ( 𝑛 + 1 ) ) ) ) ) )
77 15 21 27 33 52 76 fzind2 ⊢ ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) ) )
78 9 77 mpcom ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) 𝑄 ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )