Metamath Proof Explorer

Theorem seqcaopr3

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

Ref Expression
Hypotheses seqcaopr3.1 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
seqcaopr3.2 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x Q y ) e. S )
seqcaopr3.3 
|- ( ph -> N e. ( ZZ>= ` M ) )
seqcaopr3.4 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. S )
seqcaopr3.5 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. S )
seqcaopr3.6 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( ( F ` k ) Q ( G ` k ) ) )
seqcaopr3.7 
|- ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( ( seq M ( .+ , F ) ` n ) Q ( seq M ( .+ , G ) ` n ) ) .+ ( ( F ` ( n + 1 ) ) Q ( G ` ( n + 1 ) ) ) ) = ( ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) Q ( ( seq M ( .+ , G ) ` n ) .+ ( G ` ( n + 1 ) ) ) ) )
Assertion seqcaopr3 
|- ( ph -> ( seq M ( .+ , H ) ` N ) = ( ( seq M ( .+ , F ) ` N ) Q ( seq M ( .+ , G ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 seqcaopr3.1 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
2 seqcaopr3.2 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x Q y ) e. S )
3 seqcaopr3.3 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
4 seqcaopr3.4 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. S )
5 seqcaopr3.5 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. S )
6 seqcaopr3.6 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( ( F ` k ) Q ( G ` k ) ) )
7 seqcaopr3.7 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( ( seq M ( .+ , F ) ` n ) Q ( seq M ( .+ , G ) ` n ) ) .+ ( ( F ` ( n + 1 ) ) Q ( G ` ( n + 1 ) ) ) ) = ( ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) Q ( ( seq M ( .+ , G ) ` n ) .+ ( G ` ( n + 1 ) ) ) ) )
8 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
9 3 8 syl 
 |-  ( ph -> N e. ( M ... N ) )
10 fveq2 
 |-  ( z = M -> ( seq M ( .+ , H ) ` z ) = ( seq M ( .+ , H ) ` M ) )
11 fveq2 
 |-  ( z = M -> ( seq M ( .+ , F ) ` z ) = ( seq M ( .+ , F ) ` M ) )
12 fveq2 
 |-  ( z = M -> ( seq M ( .+ , G ) ` z ) = ( seq M ( .+ , G ) ` M ) )
13 11 12 oveq12d 
 |-  ( z = M -> ( ( seq M ( .+ , F ) ` z ) Q ( seq M ( .+ , G ) ` z ) ) = ( ( seq M ( .+ , F ) ` M ) Q ( seq M ( .+ , G ) ` M ) ) )
14 10 13 eqeq12d 
 |-  ( z = M -> ( ( seq M ( .+ , H ) ` z ) = ( ( seq M ( .+ , F ) ` z ) Q ( seq M ( .+ , G ) ` z ) ) <-> ( seq M ( .+ , H ) ` M ) = ( ( seq M ( .+ , F ) ` M ) Q ( seq M ( .+ , G ) ` M ) ) ) )
15 14 imbi2d 
 |-  ( z = M -> ( ( ph -> ( seq M ( .+ , H ) ` z ) = ( ( seq M ( .+ , F ) ` z ) Q ( seq M ( .+ , G ) ` z ) ) ) <-> ( ph -> ( seq M ( .+ , H ) ` M ) = ( ( seq M ( .+ , F ) ` M ) Q ( seq M ( .+ , G ) ` M ) ) ) ) )
16 fveq2 
 |-  ( z = n -> ( seq M ( .+ , H ) ` z ) = ( seq M ( .+ , H ) ` n ) )
17 fveq2 
 |-  ( z = n -> ( seq M ( .+ , F ) ` z ) = ( seq M ( .+ , F ) ` n ) )
18 fveq2 
 |-  ( z = n -> ( seq M ( .+ , G ) ` z ) = ( seq M ( .+ , G ) ` n ) )
19 17 18 oveq12d 
 |-  ( z = n -> ( ( seq M ( .+ , F ) ` z ) Q ( seq M ( .+ , G ) ` z ) ) = ( ( seq M ( .+ , F ) ` n ) Q ( seq M ( .+ , G ) ` n ) ) )
20 16 19 eqeq12d 
 |-  ( z = n -> ( ( seq M ( .+ , H ) ` z ) = ( ( seq M ( .+ , F ) ` z ) Q ( seq M ( .+ , G ) ` z ) ) <-> ( seq M ( .+ , H ) ` n ) = ( ( seq M ( .+ , F ) ` n ) Q ( seq M ( .+ , G ) ` n ) ) ) )
21 20 imbi2d 
 |-  ( z = n -> ( ( ph -> ( seq M ( .+ , H ) ` z ) = ( ( seq M ( .+ , F ) ` z ) Q ( seq M ( .+ , G ) ` z ) ) ) <-> ( ph -> ( seq M ( .+ , H ) ` n ) = ( ( seq M ( .+ , F ) ` n ) Q ( seq M ( .+ , G ) ` n ) ) ) ) )
22 fveq2 
 |-  ( z = ( n + 1 ) -> ( seq M ( .+ , H ) ` z ) = ( seq M ( .+ , H ) ` ( n + 1 ) ) )
23 fveq2 
 |-  ( z = ( n + 1 ) -> ( seq M ( .+ , F ) ` z ) = ( seq M ( .+ , F ) ` ( n + 1 ) ) )
24 fveq2 
 |-  ( z = ( n + 1 ) -> ( seq M ( .+ , G ) ` z ) = ( seq M ( .+ , G ) ` ( n + 1 ) ) )
25 23 24 oveq12d 
 |-  ( z = ( n + 1 ) -> ( ( seq M ( .+ , F ) ` z ) Q ( seq M ( .+ , G ) ` z ) ) = ( ( seq M ( .+ , F ) ` ( n + 1 ) ) Q ( seq M ( .+ , G ) ` ( n + 1 ) ) ) )
26 22 25 eqeq12d 
 |-  ( z = ( n + 1 ) -> ( ( seq M ( .+ , H ) ` z ) = ( ( seq M ( .+ , F ) ` z ) Q ( seq M ( .+ , G ) ` z ) ) <-> ( seq M ( .+ , H ) ` ( n + 1 ) ) = ( ( seq M ( .+ , F ) ` ( n + 1 ) ) Q ( seq M ( .+ , G ) ` ( n + 1 ) ) ) ) )
27 26 imbi2d 
 |-  ( z = ( n + 1 ) -> ( ( ph -> ( seq M ( .+ , H ) ` z ) = ( ( seq M ( .+ , F ) ` z ) Q ( seq M ( .+ , G ) ` z ) ) ) <-> ( ph -> ( seq M ( .+ , H ) ` ( n + 1 ) ) = ( ( seq M ( .+ , F ) ` ( n + 1 ) ) Q ( seq M ( .+ , G ) ` ( n + 1 ) ) ) ) ) )
28 fveq2 
 |-  ( z = N -> ( seq M ( .+ , H ) ` z ) = ( seq M ( .+ , H ) ` N ) )
29 fveq2 
 |-  ( z = N -> ( seq M ( .+ , F ) ` z ) = ( seq M ( .+ , F ) ` N ) )
30 fveq2 
 |-  ( z = N -> ( seq M ( .+ , G ) ` z ) = ( seq M ( .+ , G ) ` N ) )
31 29 30 oveq12d 
 |-  ( z = N -> ( ( seq M ( .+ , F ) ` z ) Q ( seq M ( .+ , G ) ` z ) ) = ( ( seq M ( .+ , F ) ` N ) Q ( seq M ( .+ , G ) ` N ) ) )
32 28 31 eqeq12d 
 |-  ( z = N -> ( ( seq M ( .+ , H ) ` z ) = ( ( seq M ( .+ , F ) ` z ) Q ( seq M ( .+ , G ) ` z ) ) <-> ( seq M ( .+ , H ) ` N ) = ( ( seq M ( .+ , F ) ` N ) Q ( seq M ( .+ , G ) ` N ) ) ) )
33 32 imbi2d 
 |-  ( z = N -> ( ( ph -> ( seq M ( .+ , H ) ` z ) = ( ( seq M ( .+ , F ) ` z ) Q ( seq M ( .+ , G ) ` z ) ) ) <-> ( ph -> ( seq M ( .+ , H ) ` N ) = ( ( seq M ( .+ , F ) ` N ) Q ( seq M ( .+ , G ) ` N ) ) ) ) )
34 fveq2 
 |-  ( k = M -> ( H ` k ) = ( H ` M ) )
35 fveq2 
 |-  ( k = M -> ( F ` k ) = ( F ` M ) )
36 fveq2 
 |-  ( k = M -> ( G ` k ) = ( G ` M ) )
37 35 36 oveq12d 
 |-  ( k = M -> ( ( F ` k ) Q ( G ` k ) ) = ( ( F ` M ) Q ( G ` M ) ) )
38 34 37 eqeq12d 
 |-  ( k = M -> ( ( H ` k ) = ( ( F ` k ) Q ( G ` k ) ) <-> ( H ` M ) = ( ( F ` M ) Q ( G ` M ) ) ) )
39 6 ralrimiva 
 |-  ( ph -> A. k e. ( M ... N ) ( H ` k ) = ( ( F ` k ) Q ( G ` k ) ) )
40 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
41 3 40 syl 
 |-  ( ph -> M e. ( M ... N ) )
42 38 39 41 rspcdva 
 |-  ( ph -> ( H ` M ) = ( ( F ` M ) Q ( G ` M ) ) )
43 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
44 3 43 syl 
 |-  ( ph -> M e. ZZ )
45 seq1 
 |-  ( M e. ZZ -> ( seq M ( .+ , H ) ` M ) = ( H ` M ) )
46 44 45 syl 
 |-  ( ph -> ( seq M ( .+ , H ) ` M ) = ( H ` M ) )
47 seq1 
 |-  ( M e. ZZ -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) )
48 seq1 
 |-  ( M e. ZZ -> ( seq M ( .+ , G ) ` M ) = ( G ` M ) )
49 47 48 oveq12d 
 |-  ( M e. ZZ -> ( ( seq M ( .+ , F ) ` M ) Q ( seq M ( .+ , G ) ` M ) ) = ( ( F ` M ) Q ( G ` M ) ) )
50 44 49 syl 
 |-  ( ph -> ( ( seq M ( .+ , F ) ` M ) Q ( seq M ( .+ , G ) ` M ) ) = ( ( F ` M ) Q ( G ` M ) ) )
51 42 46 50 3eqtr4d 
 |-  ( ph -> ( seq M ( .+ , H ) ` M ) = ( ( seq M ( .+ , F ) ` M ) Q ( seq M ( .+ , G ) ` M ) ) )
52 51 a1i 
 |-  ( N e. ( ZZ>= ` M ) -> ( ph -> ( seq M ( .+ , H ) ` M ) = ( ( seq M ( .+ , F ) ` M ) Q ( seq M ( .+ , G ) ` M ) ) ) )
53 oveq1 
 |-  ( ( seq M ( .+ , H ) ` n ) = ( ( seq M ( .+ , F ) ` n ) Q ( seq M ( .+ , G ) ` n ) ) -> ( ( seq M ( .+ , H ) ` n ) .+ ( H ` ( n + 1 ) ) ) = ( ( ( seq M ( .+ , F ) ` n ) Q ( seq M ( .+ , G ) ` n ) ) .+ ( H ` ( n + 1 ) ) ) )
54 elfzouz 
 |-  ( n e. ( M ..^ N ) -> n e. ( ZZ>= ` M ) )
55 54 adantl 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> n e. ( ZZ>= ` M ) )
56 seqp1 
 |-  ( n e. ( ZZ>= ` M ) -> ( seq M ( .+ , H ) ` ( n + 1 ) ) = ( ( seq M ( .+ , H ) ` n ) .+ ( H ` ( n + 1 ) ) ) )
57 55 56 syl 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( seq M ( .+ , H ) ` ( n + 1 ) ) = ( ( seq M ( .+ , H ) ` n ) .+ ( H ` ( n + 1 ) ) ) )
58 fveq2 
 |-  ( k = ( n + 1 ) -> ( H ` k ) = ( H ` ( n + 1 ) ) )
59 fveq2 
 |-  ( k = ( n + 1 ) -> ( F ` k ) = ( F ` ( n + 1 ) ) )
60 fveq2 
 |-  ( k = ( n + 1 ) -> ( G ` k ) = ( G ` ( n + 1 ) ) )
61 59 60 oveq12d 
 |-  ( k = ( n + 1 ) -> ( ( F ` k ) Q ( G ` k ) ) = ( ( F ` ( n + 1 ) ) Q ( G ` ( n + 1 ) ) ) )
62 58 61 eqeq12d 
 |-  ( k = ( n + 1 ) -> ( ( H ` k ) = ( ( F ` k ) Q ( G ` k ) ) <-> ( H ` ( n + 1 ) ) = ( ( F ` ( n + 1 ) ) Q ( G ` ( n + 1 ) ) ) ) )
63 39 adantr 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> A. k e. ( M ... N ) ( H ` k ) = ( ( F ` k ) Q ( G ` k ) ) )
64 fzofzp1 
 |-  ( n e. ( M ..^ N ) -> ( n + 1 ) e. ( M ... N ) )
65 64 adantl 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( n + 1 ) e. ( M ... N ) )
66 62 63 65 rspcdva 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( H ` ( n + 1 ) ) = ( ( F ` ( n + 1 ) ) Q ( G ` ( n + 1 ) ) ) )
67 66 oveq2d 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( ( seq M ( .+ , F ) ` n ) Q ( seq M ( .+ , G ) ` n ) ) .+ ( H ` ( n + 1 ) ) ) = ( ( ( seq M ( .+ , F ) ` n ) Q ( seq M ( .+ , G ) ` n ) ) .+ ( ( F ` ( n + 1 ) ) Q ( G ` ( n + 1 ) ) ) ) )
68 seqp1 
 |-  ( n e. ( ZZ>= ` M ) -> ( seq M ( .+ , F ) ` ( n + 1 ) ) = ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) )
69 seqp1 
 |-  ( n e. ( ZZ>= ` M ) -> ( seq M ( .+ , G ) ` ( n + 1 ) ) = ( ( seq M ( .+ , G ) ` n ) .+ ( G ` ( n + 1 ) ) ) )
70 68 69 oveq12d 
 |-  ( n e. ( ZZ>= ` M ) -> ( ( seq M ( .+ , F ) ` ( n + 1 ) ) Q ( seq M ( .+ , G ) ` ( n + 1 ) ) ) = ( ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) Q ( ( seq M ( .+ , G ) ` n ) .+ ( G ` ( n + 1 ) ) ) ) )
71 55 70 syl 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( seq M ( .+ , F ) ` ( n + 1 ) ) Q ( seq M ( .+ , G ) ` ( n + 1 ) ) ) = ( ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) Q ( ( seq M ( .+ , G ) ` n ) .+ ( G ` ( n + 1 ) ) ) ) )
72 7 67 71 3eqtr4rd 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( seq M ( .+ , F ) ` ( n + 1 ) ) Q ( seq M ( .+ , G ) ` ( n + 1 ) ) ) = ( ( ( seq M ( .+ , F ) ` n ) Q ( seq M ( .+ , G ) ` n ) ) .+ ( H ` ( n + 1 ) ) ) )
73 57 72 eqeq12d 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( seq M ( .+ , H ) ` ( n + 1 ) ) = ( ( seq M ( .+ , F ) ` ( n + 1 ) ) Q ( seq M ( .+ , G ) ` ( n + 1 ) ) ) <-> ( ( seq M ( .+ , H ) ` n ) .+ ( H ` ( n + 1 ) ) ) = ( ( ( seq M ( .+ , F ) ` n ) Q ( seq M ( .+ , G ) ` n ) ) .+ ( H ` ( n + 1 ) ) ) ) )
74 53 73 syl5ibr 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( seq M ( .+ , H ) ` n ) = ( ( seq M ( .+ , F ) ` n ) Q ( seq M ( .+ , G ) ` n ) ) -> ( seq M ( .+ , H ) ` ( n + 1 ) ) = ( ( seq M ( .+ , F ) ` ( n + 1 ) ) Q ( seq M ( .+ , G ) ` ( n + 1 ) ) ) ) )
75 74 expcom 
 |-  ( n e. ( M ..^ N ) -> ( ph -> ( ( seq M ( .+ , H ) ` n ) = ( ( seq M ( .+ , F ) ` n ) Q ( seq M ( .+ , G ) ` n ) ) -> ( seq M ( .+ , H ) ` ( n + 1 ) ) = ( ( seq M ( .+ , F ) ` ( n + 1 ) ) Q ( seq M ( .+ , G ) ` ( n + 1 ) ) ) ) ) )
76 75 a2d 
 |-  ( n e. ( M ..^ N ) -> ( ( ph -> ( seq M ( .+ , H ) ` n ) = ( ( seq M ( .+ , F ) ` n ) Q ( seq M ( .+ , G ) ` n ) ) ) -> ( ph -> ( seq M ( .+ , H ) ` ( n + 1 ) ) = ( ( seq M ( .+ , F ) ` ( n + 1 ) ) Q ( seq M ( .+ , G ) ` ( n + 1 ) ) ) ) ) )
77 15 21 27 33 52 76 fzind2 
 |-  ( N e. ( M ... N ) -> ( ph -> ( seq M ( .+ , H ) ` N ) = ( ( seq M ( .+ , F ) ` N ) Q ( seq M ( .+ , G ) ` N ) ) ) )
78 9 77 mpcom 
 |-  ( ph -> ( seq M ( .+ , H ) ` N ) = ( ( seq M ( .+ , F ) ` N ) Q ( seq M ( .+ , G ) ` N ) ) )