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