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 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
seqhomo.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
seqz.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑍 + 𝑥 ) = 𝑍 )
seqz.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 + 𝑍 ) = 𝑍 )
seqz.5 ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )
seqz.6 ⊢ ( 𝜑 → 𝑁 ∈ 𝑉 )
seqz.7 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐾 ) = 𝑍 )
Assertion seqz ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = 𝑍 )

Proof

Step Hyp Ref Expression
1 seqhomo.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
2 seqhomo.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
3 seqz.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑍 + 𝑥 ) = 𝑍 )
4 seqz.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 + 𝑍 ) = 𝑍 )
5 seqz.5 ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )
6 seqz.6 ⊢ ( 𝜑 → 𝑁 ∈ 𝑉 )
7 seqz.7 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐾 ) = 𝑍 )
8 elfzuz ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
9 5 8 syl ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
10 eluzelz ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝐾 ∈ ℤ )
11 9 10 syl ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
12 seq1 ⊢ ( 𝐾 ∈ ℤ → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝐾 ) = ( 𝐹 ‘ 𝐾 ) )
13 11 12 syl ⊢ ( 𝜑 → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝐾 ) = ( 𝐹 ‘ 𝐾 ) )
14 13 7 eqtrd ⊢ ( 𝜑 → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝐾 ) = 𝑍 )
15 seqeq1 ⊢ ( 𝐾 = 𝑀 → seq 𝐾 ( + , 𝐹 ) = seq 𝑀 ( + , 𝐹 ) )
16 15 fveq1d ⊢ ( 𝐾 = 𝑀 → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) )
17 16 eqeq1d ⊢ ( 𝐾 = 𝑀 → ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝐾 ) = 𝑍 ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = 𝑍 ) )
18 14 17 syl5ibcom ⊢ ( 𝜑 → ( 𝐾 = 𝑀 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = 𝑍 ) )
19 eluzel2 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
20 9 19 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
21 seqm1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐾 − 1 ) ) + ( 𝐹 ‘ 𝐾 ) ) )
22 20 21 sylan ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐾 − 1 ) ) + ( 𝐹 ‘ 𝐾 ) ) )
23 7 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝐹 ‘ 𝐾 ) = 𝑍 )
24 23 oveq2d ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐾 − 1 ) ) + ( 𝐹 ‘ 𝐾 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐾 − 1 ) ) + 𝑍 ) )
25 oveq1 ⊢ ( 𝑥 = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐾 − 1 ) ) → ( 𝑥 + 𝑍 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐾 − 1 ) ) + 𝑍 ) )
26 25 eqeq1d ⊢ ( 𝑥 = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐾 − 1 ) ) → ( ( 𝑥 + 𝑍 ) = 𝑍 ↔ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐾 − 1 ) ) + 𝑍 ) = 𝑍 ) )
27 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ( 𝑥 + 𝑍 ) = 𝑍 )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ∀ 𝑥 ∈ 𝑆 ( 𝑥 + 𝑍 ) = 𝑍 )
29 eluzp1m1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝐾 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
30 20 29 sylan ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝐾 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
31 fzssp1 ⊢ ( 𝑀 ... ( 𝐾 − 1 ) ) ⊆ ( 𝑀 ... ( ( 𝐾 − 1 ) + 1 ) )
32 11 zcnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
33 ax-1cn ⊢ 1 ∈ ℂ
34 npcan ⊢ ( ( 𝐾 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
35 32 33 34 sylancl ⊢ ( 𝜑 → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
36 35 oveq2d ⊢ ( 𝜑 → ( 𝑀 ... ( ( 𝐾 − 1 ) + 1 ) ) = ( 𝑀 ... 𝐾 ) )
37 31 36 sseqtrid ⊢ ( 𝜑 → ( 𝑀 ... ( 𝐾 − 1 ) ) ⊆ ( 𝑀 ... 𝐾 ) )
38 elfzuz3 ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
39 5 38 syl ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
40 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑀 ... 𝐾 ) ⊆ ( 𝑀 ... 𝑁 ) )
41 39 40 syl ⊢ ( 𝜑 → ( 𝑀 ... 𝐾 ) ⊆ ( 𝑀 ... 𝑁 ) )
42 37 41 sstrd ⊢ ( 𝜑 → ( 𝑀 ... ( 𝐾 − 1 ) ) ⊆ ( 𝑀 ... 𝑁 ) )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑀 ... ( 𝐾 − 1 ) ) ⊆ ( 𝑀 ... 𝑁 ) )
44 43 sselda ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) )
45 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
46 44 45 syldan ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝐾 − 1 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
47 1 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
48 30 46 47 seqcl ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐾 − 1 ) ) ∈ 𝑆 )
49 26 28 48 rspcdva ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐾 − 1 ) ) + 𝑍 ) = 𝑍 )
50 24 49 eqtrd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝐾 − 1 ) ) + ( 𝐹 ‘ 𝐾 ) ) = 𝑍 )
51 22 50 eqtrd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = 𝑍 )
52 51 ex ⊢ ( 𝜑 → ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = 𝑍 ) )
53 uzp1 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
54 9 53 syl ⊢ ( 𝜑 → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
55 18 52 54 mpjaod ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = 𝑍 )
56 55 7 eqtr4d ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( 𝐹 ‘ 𝐾 ) )
57 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
58 9 56 39 57 seqfveq2 ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑁 ) )
59 fvex ⊢ ( 𝐹 ‘ 𝐾 ) ∈ V
60 59 elsn ⊢ ( ( 𝐹 ‘ 𝐾 ) ∈ { 𝑍 } ↔ ( 𝐹 ‘ 𝐾 ) = 𝑍 )
61 7 60 sylibr ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐾 ) ∈ { 𝑍 } )
62 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑍 } ∧ 𝑦 ∈ 𝑆 ) ) → 𝑥 ∈ { 𝑍 } )
63 velsn ⊢ ( 𝑥 ∈ { 𝑍 } ↔ 𝑥 = 𝑍 )
64 62 63 sylib ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑍 } ∧ 𝑦 ∈ 𝑆 ) ) → 𝑥 = 𝑍 )
65 64 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑍 } ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑍 + 𝑦 ) )
66 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑍 + 𝑥 ) = ( 𝑍 + 𝑦 ) )
67 66 eqeq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑍 + 𝑥 ) = 𝑍 ↔ ( 𝑍 + 𝑦 ) = 𝑍 ) )
68 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ( 𝑍 + 𝑥 ) = 𝑍 )
69 68 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑍 } ∧ 𝑦 ∈ 𝑆 ) ) → ∀ 𝑥 ∈ 𝑆 ( 𝑍 + 𝑥 ) = 𝑍 )
70 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑍 } ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ∈ 𝑆 )
71 67 69 70 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑍 } ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑍 + 𝑦 ) = 𝑍 )
72 65 71 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑍 } ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) = 𝑍 )
73 ovex ⊢ ( 𝑥 + 𝑦 ) ∈ V
74 73 elsn ⊢ ( ( 𝑥 + 𝑦 ) ∈ { 𝑍 } ↔ ( 𝑥 + 𝑦 ) = 𝑍 )
75 72 74 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑍 } ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ { 𝑍 } )
76 peano2uz ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
77 9 76 syl ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
78 fzss1 ⊢ ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝐾 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
79 77 78 syl ⊢ ( 𝜑 → ( ( 𝐾 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
80 79 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) )
81 80 2 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
82 61 75 39 81 seqcl2 ⊢ ( 𝜑 → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑁 ) ∈ { 𝑍 } )
83 elsni ⊢ ( ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑁 ) ∈ { 𝑍 } → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑁 ) = 𝑍 )
84 82 83 syl ⊢ ( 𝜑 → ( seq 𝐾 ( + , 𝐹 ) ‘ 𝑁 ) = 𝑍 )
85 58 84 eqtrd ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = 𝑍 )