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

Metamath Proof Explorer

Theorem seqz

Proof