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	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
	seqhomo.2	$⊢ (φ \land x \in (M \dots N)) \to F (x) \in S$
	seqz.3	$⊢ (φ \land x \in S) \to Z \underset{˙}{+} x = Z$
	seqz.4	$⊢ (φ \land x \in S) \to x \underset{˙}{+} Z = Z$
	seqz.5	$⊢ φ \to K \in (M \dots N)$
	seqz.6	$⊢ φ \to N \in V$
	seqz.7	$⊢ φ \to F (K) = Z$
Assertion	seqz	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) = Z$

Proof

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

Metamath Proof Explorer

Theorem seqz

Proof