Metamath Proof Explorer

Theorem seqz

Description: If the operation .+ has an absorbing element Z (a.k.a. zero element), then any sequence containing a Z evaluates to Z . (Contributed by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses seqhomo.1 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
seqhomo.2 
|- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. S )
seqz.3 
|- ( ( ph /\ x e. S ) -> ( Z .+ x ) = Z )
seqz.4 
|- ( ( ph /\ x e. S ) -> ( x .+ Z ) = Z )
seqz.5 
|- ( ph -> K e. ( M ... N ) )
seqz.6 
|- ( ph -> N e. V )
seqz.7 
|- ( ph -> ( F ` K ) = Z )
Assertion seqz 
|- ( ph -> ( seq M ( .+ , F ) ` N ) = Z )

Proof

Step Hyp Ref Expression
1 seqhomo.1 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
2 seqhomo.2 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. S )
3 seqz.3 
 |-  ( ( ph /\ x e. S ) -> ( Z .+ x ) = Z )
4 seqz.4 
 |-  ( ( ph /\ x e. S ) -> ( x .+ Z ) = Z )
5 seqz.5 
 |-  ( ph -> K e. ( M ... N ) )
6 seqz.6 
 |-  ( ph -> N e. V )
7 seqz.7 
 |-  ( ph -> ( F ` K ) = Z )
8 elfzuz 
 |-  ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )
9 5 8 syl 
 |-  ( ph -> K e. ( ZZ>= ` M ) )
10 5 elfzelzd 
 |-  ( ph -> K e. ZZ )
11 seq1 
 |-  ( K e. ZZ -> ( seq K ( .+ , F ) ` K ) = ( F ` K ) )
12 10 11 syl 
 |-  ( ph -> ( seq K ( .+ , F ) ` K ) = ( F ` K ) )
13 12 7 eqtrd 
 |-  ( ph -> ( seq K ( .+ , F ) ` K ) = Z )
14 seqeq1 
 |-  ( K = M -> seq K ( .+ , F ) = seq M ( .+ , F ) )
15 14 fveq1d 
 |-  ( K = M -> ( seq K ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` K ) )
16 15 eqeq1d 
 |-  ( K = M -> ( ( seq K ( .+ , F ) ` K ) = Z <-> ( seq M ( .+ , F ) ` K ) = Z ) )
17 13 16 syl5ibcom 
 |-  ( ph -> ( K = M -> ( seq M ( .+ , F ) ` K ) = Z ) )
18 eluzel2 
 |-  ( K e. ( ZZ>= ` M ) -> M e. ZZ )
19 9 18 syl 
 |-  ( ph -> M e. ZZ )
20 seqm1 
 |-  ( ( M e. ZZ /\ K e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq M ( .+ , F ) ` K ) = ( ( seq M ( .+ , F ) ` ( K - 1 ) ) .+ ( F ` K ) ) )
21 19 20 sylan 
 |-  ( ( ph /\ K e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq M ( .+ , F ) ` K ) = ( ( seq M ( .+ , F ) ` ( K - 1 ) ) .+ ( F ` K ) ) )
22 7 adantr 
 |-  ( ( ph /\ K e. ( ZZ>= ` ( M + 1 ) ) ) -> ( F ` K ) = Z )
23 22 oveq2d 
 |-  ( ( ph /\ K e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( seq M ( .+ , F ) ` ( K - 1 ) ) .+ ( F ` K ) ) = ( ( seq M ( .+ , F ) ` ( K - 1 ) ) .+ Z ) )
24 oveq1 
 |-  ( x = ( seq M ( .+ , F ) ` ( K - 1 ) ) -> ( x .+ Z ) = ( ( seq M ( .+ , F ) ` ( K - 1 ) ) .+ Z ) )
25 24 eqeq1d 
 |-  ( x = ( seq M ( .+ , F ) ` ( K - 1 ) ) -> ( ( x .+ Z ) = Z <-> ( ( seq M ( .+ , F ) ` ( K - 1 ) ) .+ Z ) = Z ) )
26 4 ralrimiva 
 |-  ( ph -> A. x e. S ( x .+ Z ) = Z )
27 26 adantr 
 |-  ( ( ph /\ K e. ( ZZ>= ` ( M + 1 ) ) ) -> A. x e. S ( x .+ Z ) = Z )
28 eluzp1m1 
 |-  ( ( M e. ZZ /\ K e. ( ZZ>= ` ( M + 1 ) ) ) -> ( K - 1 ) e. ( ZZ>= ` M ) )
29 19 28 sylan 
 |-  ( ( ph /\ K e. ( ZZ>= ` ( M + 1 ) ) ) -> ( K - 1 ) e. ( ZZ>= ` M ) )
30 fzssp1 
 |-  ( M ... ( K - 1 ) ) C_ ( M ... ( ( K - 1 ) + 1 ) )
31 10 zcnd 
 |-  ( ph -> K e. CC )
32 ax-1cn 
 |-  1 e. CC
33 npcan 
 |-  ( ( K e. CC /\ 1 e. CC ) -> ( ( K - 1 ) + 1 ) = K )
34 31 32 33 sylancl 
 |-  ( ph -> ( ( K - 1 ) + 1 ) = K )
35 34 oveq2d 
 |-  ( ph -> ( M ... ( ( K - 1 ) + 1 ) ) = ( M ... K ) )
36 30 35 sseqtrid 
 |-  ( ph -> ( M ... ( K - 1 ) ) C_ ( M ... K ) )
37 elfzuz3 
 |-  ( K e. ( M ... N ) -> N e. ( ZZ>= ` K ) )
38 5 37 syl 
 |-  ( ph -> N e. ( ZZ>= ` K ) )
39 fzss2 
 |-  ( N e. ( ZZ>= ` K ) -> ( M ... K ) C_ ( M ... N ) )
40 38 39 syl 
 |-  ( ph -> ( M ... K ) C_ ( M ... N ) )
41 36 40 sstrd 
 |-  ( ph -> ( M ... ( K - 1 ) ) C_ ( M ... N ) )
42 41 adantr 
 |-  ( ( ph /\ K e. ( ZZ>= ` ( M + 1 ) ) ) -> ( M ... ( K - 1 ) ) C_ ( M ... N ) )
43 42 sselda 
 |-  ( ( ( ph /\ K e. ( ZZ>= ` ( M + 1 ) ) ) /\ x e. ( M ... ( K - 1 ) ) ) -> x e. ( M ... N ) )
44 2 adantlr 
 |-  ( ( ( ph /\ K e. ( ZZ>= ` ( M + 1 ) ) ) /\ x e. ( M ... N ) ) -> ( F ` x ) e. S )
45 43 44 syldan 
 |-  ( ( ( ph /\ K e. ( ZZ>= ` ( M + 1 ) ) ) /\ x e. ( M ... ( K - 1 ) ) ) -> ( F ` x ) e. S )
46 1 adantlr 
 |-  ( ( ( ph /\ K e. ( ZZ>= ` ( M + 1 ) ) ) /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
47 29 45 46 seqcl 
 |-  ( ( ph /\ K e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq M ( .+ , F ) ` ( K - 1 ) ) e. S )
48 25 27 47 rspcdva 
 |-  ( ( ph /\ K e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( seq M ( .+ , F ) ` ( K - 1 ) ) .+ Z ) = Z )
49 23 48 eqtrd 
 |-  ( ( ph /\ K e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( seq M ( .+ , F ) ` ( K - 1 ) ) .+ ( F ` K ) ) = Z )
50 21 49 eqtrd 
 |-  ( ( ph /\ K e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq M ( .+ , F ) ` K ) = Z )
51 50 ex 
 |-  ( ph -> ( K e. ( ZZ>= ` ( M + 1 ) ) -> ( seq M ( .+ , F ) ` K ) = Z ) )
52 uzp1 
 |-  ( K e. ( ZZ>= ` M ) -> ( K = M \/ K e. ( ZZ>= ` ( M + 1 ) ) ) )
53 9 52 syl 
 |-  ( ph -> ( K = M \/ K e. ( ZZ>= ` ( M + 1 ) ) ) )
54 17 51 53 mpjaod 
 |-  ( ph -> ( seq M ( .+ , F ) ` K ) = Z )
55 54 7 eqtr4d 
 |-  ( ph -> ( seq M ( .+ , F ) ` K ) = ( F ` K ) )
56 eqidd 
 |-  ( ( ph /\ x e. ( ( K + 1 ) ... N ) ) -> ( F ` x ) = ( F ` x ) )
57 9 55 38 56 seqfveq2 
 |-  ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq K ( .+ , F ) ` N ) )
58 fvex 
 |-  ( F ` K ) e. _V
59 58 elsn 
 |-  ( ( F ` K ) e. { Z } <-> ( F ` K ) = Z )
60 7 59 sylibr 
 |-  ( ph -> ( F ` K ) e. { Z } )
61 simprl 
 |-  ( ( ph /\ ( x e. { Z } /\ y e. S ) ) -> x e. { Z } )
62 velsn 
 |-  ( x e. { Z } <-> x = Z )
63 61 62 sylib 
 |-  ( ( ph /\ ( x e. { Z } /\ y e. S ) ) -> x = Z )
64 63 oveq1d 
 |-  ( ( ph /\ ( x e. { Z } /\ y e. S ) ) -> ( x .+ y ) = ( Z .+ y ) )
65 oveq2 
 |-  ( x = y -> ( Z .+ x ) = ( Z .+ y ) )
66 65 eqeq1d 
 |-  ( x = y -> ( ( Z .+ x ) = Z <-> ( Z .+ y ) = Z ) )
67 3 ralrimiva 
 |-  ( ph -> A. x e. S ( Z .+ x ) = Z )
68 67 adantr 
 |-  ( ( ph /\ ( x e. { Z } /\ y e. S ) ) -> A. x e. S ( Z .+ x ) = Z )
69 simprr 
 |-  ( ( ph /\ ( x e. { Z } /\ y e. S ) ) -> y e. S )
70 66 68 69 rspcdva 
 |-  ( ( ph /\ ( x e. { Z } /\ y e. S ) ) -> ( Z .+ y ) = Z )
71 64 70 eqtrd 
 |-  ( ( ph /\ ( x e. { Z } /\ y e. S ) ) -> ( x .+ y ) = Z )
72 ovex 
 |-  ( x .+ y ) e. _V
73 72 elsn 
 |-  ( ( x .+ y ) e. { Z } <-> ( x .+ y ) = Z )
74 71 73 sylibr 
 |-  ( ( ph /\ ( x e. { Z } /\ y e. S ) ) -> ( x .+ y ) e. { Z } )
75 peano2uz 
 |-  ( K e. ( ZZ>= ` M ) -> ( K + 1 ) e. ( ZZ>= ` M ) )
76 9 75 syl 
 |-  ( ph -> ( K + 1 ) e. ( ZZ>= ` M ) )
77 fzss1 
 |-  ( ( K + 1 ) e. ( ZZ>= ` M ) -> ( ( K + 1 ) ... N ) C_ ( M ... N ) )
78 76 77 syl 
 |-  ( ph -> ( ( K + 1 ) ... N ) C_ ( M ... N ) )
79 78 sselda 
 |-  ( ( ph /\ x e. ( ( K + 1 ) ... N ) ) -> x e. ( M ... N ) )
80 79 2 syldan 
 |-  ( ( ph /\ x e. ( ( K + 1 ) ... N ) ) -> ( F ` x ) e. S )
81 60 74 38 80 seqcl2 
 |-  ( ph -> ( seq K ( .+ , F ) ` N ) e. { Z } )
82 elsni 
 |-  ( ( seq K ( .+ , F ) ` N ) e. { Z } -> ( seq K ( .+ , F ) ` N ) = Z )
83 81 82 syl 
 |-  ( ph -> ( seq K ( .+ , F ) ` N ) = Z )
84 57 83 eqtrd 
 |-  ( ph -> ( seq M ( .+ , F ) ` N ) = Z )