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