smuval2

Description: The partial sum sequence stabilizes at N after the N + 1 -th element of the sequence; this stable value is the value of the sequence multiplication. (Contributed by Mario Carneiro, 9-Sep-2016)

	Ref	Expression
Hypotheses	smuval.a	$⊢ φ \to A \subseteq ℕ_{0}$
	smuval.b	$⊢ φ \to B \subseteq ℕ_{0}$
	smuval.p	$⊢ P = seq 0 ((p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)))$
	smuval.n	$⊢ φ \to N \in ℕ_{0}$
	smuval2.m	$⊢ φ \to M \in ℤ_{\geq (N + 1)}$
Assertion	smuval2	$⊢ φ \to (N \in (A smul B) \leftrightarrow N \in P (M))$

Proof

Step	Hyp	Ref	Expression
1		smuval.a	$⊢ φ \to A \subseteq ℕ_{0}$
2		smuval.b	$⊢ φ \to B \subseteq ℕ_{0}$
3		smuval.p	$⊢ P = seq 0 ((p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)))$
4		smuval.n	$⊢ φ \to N \in ℕ_{0}$
5		smuval2.m	$⊢ φ \to M \in ℤ_{\geq (N + 1)}$
6		fveq2	$⊢ x = N + 1 \to P (x) = P (N + 1)$
7	6	eleq2d	$⊢ x = N + 1 \to (N \in P (x) \leftrightarrow N \in P (N + 1))$
8	7	bibi2d	$⊢ x = N + 1 \to ((N \in (A smul B) \leftrightarrow N \in P (x)) \leftrightarrow (N \in (A smul B) \leftrightarrow N \in P (N + 1)))$
9	8	imbi2d	$⊢ x = N + 1 \to ((φ \to (N \in (A smul B) \leftrightarrow N \in P (x))) \leftrightarrow (φ \to (N \in (A smul B) \leftrightarrow N \in P (N + 1))))$
10		fveq2	$⊢ x = k \to P (x) = P (k)$
11	10	eleq2d	$⊢ x = k \to (N \in P (x) \leftrightarrow N \in P (k))$
12	11	bibi2d	$⊢ x = k \to ((N \in (A smul B) \leftrightarrow N \in P (x)) \leftrightarrow (N \in (A smul B) \leftrightarrow N \in P (k)))$
13	12	imbi2d	$⊢ x = k \to ((φ \to (N \in (A smul B) \leftrightarrow N \in P (x))) \leftrightarrow (φ \to (N \in (A smul B) \leftrightarrow N \in P (k))))$
14		fveq2	$⊢ x = k + 1 \to P (x) = P (k + 1)$
15	14	eleq2d	$⊢ x = k + 1 \to (N \in P (x) \leftrightarrow N \in P (k + 1))$
16	15	bibi2d	$⊢ x = k + 1 \to ((N \in (A smul B) \leftrightarrow N \in P (x)) \leftrightarrow (N \in (A smul B) \leftrightarrow N \in P (k + 1)))$
17	16	imbi2d	$⊢ x = k + 1 \to ((φ \to (N \in (A smul B) \leftrightarrow N \in P (x))) \leftrightarrow (φ \to (N \in (A smul B) \leftrightarrow N \in P (k + 1))))$
18		fveq2	$⊢ x = M \to P (x) = P (M)$
19	18	eleq2d	$⊢ x = M \to (N \in P (x) \leftrightarrow N \in P (M))$
20	19	bibi2d	$⊢ x = M \to ((N \in (A smul B) \leftrightarrow N \in P (x)) \leftrightarrow (N \in (A smul B) \leftrightarrow N \in P (M)))$
21	20	imbi2d	$⊢ x = M \to ((φ \to (N \in (A smul B) \leftrightarrow N \in P (x))) \leftrightarrow (φ \to (N \in (A smul B) \leftrightarrow N \in P (M))))$
22	1 2 3 4	smuval	$⊢ φ \to (N \in (A smul B) \leftrightarrow N \in P (N + 1))$
23	1	adantr	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to A \subseteq ℕ_{0}$
24	2	adantr	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to B \subseteq ℕ_{0}$
25		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
26	4 25	syl	$⊢ φ \to N + 1 \in ℕ_{0}$
27		eluznn0	$⊢ (N + 1 \in ℕ_{0} \land k \in ℤ_{\geq (N + 1)}) \to k \in ℕ_{0}$
28	26 27	sylan	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to k \in ℕ_{0}$
29	23 24 3 28	smupp1	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to P (k + 1) = P (k) sadd \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\}$
30	29	eleq2d	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to (N \in P (k + 1) \leftrightarrow N \in (P (k) sadd \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\}))$
31	23 24 3	smupf	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to P : ℕ_{0} ⟶ 𝒫 ℕ_{0}$
32	31 28	ffvelrnd	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to P (k) \in 𝒫 ℕ_{0}$
33	32	elpwid	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to P (k) \subseteq ℕ_{0}$
34		ssrab2	$⊢ \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\} \subseteq ℕ_{0}$
35	34	a1i	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\} \subseteq ℕ_{0}$
36	26	adantr	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to N + 1 \in ℕ_{0}$
37	33 35 36	sadeq	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to (P (k) sadd \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\}) \cap (0 ..^N + 1) = ((P (k) \cap (0 ..^N + 1)) sadd (\{n \in ℕ_{0} \| (k \in A \land n - k \in B)\} \cap (0 ..^N + 1))) \cap (0 ..^N + 1)$
38		inrab2	$⊢ \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\} \cap (0 ..^N + 1) = \{n \in (ℕ_{0} \cap (0 ..^N + 1)) \| (k \in A \land n - k \in B)\}$
39		simpr	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to n \in (ℕ_{0} \cap (0 ..^N + 1))$
40	39	elin1d	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to n \in ℕ_{0}$
41	40	nn0red	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to n \in ℝ$
42	4	adantr	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to N \in ℕ_{0}$
43	42	adantr	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to N \in ℕ_{0}$
44	43	nn0red	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to N \in ℝ$
45		1red	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to 1 \in ℝ$
46	44 45	readdcld	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to N + 1 \in ℝ$
47	28	adantr	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to k \in ℕ_{0}$
48	47	nn0red	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to k \in ℝ$
49	39	elin2d	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to n \in (0 ..^N + 1)$
50		elfzolt2	$⊢ n \in (0 ..^N + 1) \to n < N + 1$
51	49 50	syl	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to n < N + 1$
52		eluzle	$⊢ k \in ℤ_{\geq (N + 1)} \to N + 1 \leq k$
53	52	ad2antlr	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to N + 1 \leq k$
54	41 46 48 51 53	ltletrd	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to n < k$
55	41 48	ltnled	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to (n < k \leftrightarrow \neg k \leq n)$
56	54 55	mpbid	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to \neg k \leq n$
57	24	adantr	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to B \subseteq ℕ_{0}$
58	57	sseld	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to (n - k \in B \to n - k \in ℕ_{0})$
59		nn0ge0	$⊢ n - k \in ℕ_{0} \to 0 \leq n - k$
60	58 59	syl6	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to (n - k \in B \to 0 \leq n - k)$
61	41 48	subge0d	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to (0 \leq n - k \leftrightarrow k \leq n)$
62	60 61	sylibd	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to (n - k \in B \to k \leq n)$
63	62	adantld	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to ((k \in A \land n - k \in B) \to k \leq n)$
64	56 63	mtod	$⊢ ((φ \land k \in ℤ_{\geq (N + 1)}) \land n \in (ℕ_{0} \cap (0 ..^N + 1))) \to \neg (k \in A \land n - k \in B)$
65	64	ralrimiva	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to \forall n \in (ℕ_{0} \cap (0 ..^N + 1)) \neg (k \in A \land n - k \in B)$
66		rabeq0	$⊢ \{n \in (ℕ_{0} \cap (0 ..^N + 1)) \| (k \in A \land n - k \in B)\} = \emptyset \leftrightarrow \forall n \in (ℕ_{0} \cap (0 ..^N + 1)) \neg (k \in A \land n - k \in B)$
67	65 66	sylibr	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to \{n \in (ℕ_{0} \cap (0 ..^N + 1)) \| (k \in A \land n - k \in B)\} = \emptyset$
68	38 67	eqtrid	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\} \cap (0 ..^N + 1) = \emptyset$
69	68	oveq2d	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to (P (k) \cap (0 ..^N + 1)) sadd (\{n \in ℕ_{0} \| (k \in A \land n - k \in B)\} \cap (0 ..^N + 1)) = (P (k) \cap (0 ..^N + 1)) sadd \emptyset$
70		inss1	$⊢ P (k) \cap (0 ..^N + 1) \subseteq P (k)$
71	70 33	sstrid	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to P (k) \cap (0 ..^N + 1) \subseteq ℕ_{0}$
72		sadid1	$⊢ P (k) \cap (0 ..^N + 1) \subseteq ℕ_{0} \to (P (k) \cap (0 ..^N + 1)) sadd \emptyset = P (k) \cap (0 ..^N + 1)$
73	71 72	syl	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to (P (k) \cap (0 ..^N + 1)) sadd \emptyset = P (k) \cap (0 ..^N + 1)$
74	69 73	eqtrd	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to (P (k) \cap (0 ..^N + 1)) sadd (\{n \in ℕ_{0} \| (k \in A \land n - k \in B)\} \cap (0 ..^N + 1)) = P (k) \cap (0 ..^N + 1)$
75	74	ineq1d	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to ((P (k) \cap (0 ..^N + 1)) sadd (\{n \in ℕ_{0} \| (k \in A \land n - k \in B)\} \cap (0 ..^N + 1))) \cap (0 ..^N + 1) = (P (k) \cap (0 ..^N + 1)) \cap (0 ..^N + 1)$
76		inass	$⊢ (P (k) \cap (0 ..^N + 1)) \cap (0 ..^N + 1) = P (k) \cap ((0 ..^N + 1) \cap (0 ..^N + 1))$
77		inidm	$⊢ (0 ..^N + 1) \cap (0 ..^N + 1) = (0 ..^N + 1)$
78	77	ineq2i	$⊢ P (k) \cap ((0 ..^N + 1) \cap (0 ..^N + 1)) = P (k) \cap (0 ..^N + 1)$
79	76 78	eqtri	$⊢ (P (k) \cap (0 ..^N + 1)) \cap (0 ..^N + 1) = P (k) \cap (0 ..^N + 1)$
80	75 79	eqtrdi	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to ((P (k) \cap (0 ..^N + 1)) sadd (\{n \in ℕ_{0} \| (k \in A \land n - k \in B)\} \cap (0 ..^N + 1))) \cap (0 ..^N + 1) = P (k) \cap (0 ..^N + 1)$
81	37 80	eqtrd	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to (P (k) sadd \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\}) \cap (0 ..^N + 1) = P (k) \cap (0 ..^N + 1)$
82	81	eleq2d	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to (N \in ((P (k) sadd \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\}) \cap (0 ..^N + 1)) \leftrightarrow N \in (P (k) \cap (0 ..^N + 1)))$
83		elin	$⊢ N \in ((P (k) sadd \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\}) \cap (0 ..^N + 1)) \leftrightarrow (N \in (P (k) sadd \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\}) \land N \in (0 ..^N + 1))$
84		elin	$⊢ N \in (P (k) \cap (0 ..^N + 1)) \leftrightarrow (N \in P (k) \land N \in (0 ..^N + 1))$
85	82 83 84	3bitr3g	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to ((N \in (P (k) sadd \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\}) \land N \in (0 ..^N + 1)) \leftrightarrow (N \in P (k) \land N \in (0 ..^N + 1)))$
86		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
87	42 86	eleqtrdi	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to N \in ℤ_{\geq 0}$
88		eluzfz2	$⊢ N \in ℤ_{\geq 0} \to N \in (0 \dots N)$
89	87 88	syl	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to N \in (0 \dots N)$
90	42	nn0zd	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to N \in ℤ$
91		fzval3	$⊢ N \in ℤ \to (0 \dots N) = (0 ..^N + 1)$
92	90 91	syl	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to (0 \dots N) = (0 ..^N + 1)$
93	89 92	eleqtrd	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to N \in (0 ..^N + 1)$
94	93	biantrud	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to (N \in (P (k) sadd \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\}) \leftrightarrow (N \in (P (k) sadd \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\}) \land N \in (0 ..^N + 1)))$
95	93	biantrud	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to (N \in P (k) \leftrightarrow (N \in P (k) \land N \in (0 ..^N + 1)))$
96	85 94 95	3bitr4d	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to (N \in (P (k) sadd \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\}) \leftrightarrow N \in P (k))$
97	30 96	bitrd	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to (N \in P (k + 1) \leftrightarrow N \in P (k))$
98	97	bibi2d	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to ((N \in (A smul B) \leftrightarrow N \in P (k + 1)) \leftrightarrow (N \in (A smul B) \leftrightarrow N \in P (k)))$
99	98	biimprd	$⊢ (φ \land k \in ℤ_{\geq (N + 1)}) \to ((N \in (A smul B) \leftrightarrow N \in P (k)) \to (N \in (A smul B) \leftrightarrow N \in P (k + 1)))$
100	99	expcom	$⊢ k \in ℤ_{\geq (N + 1)} \to (φ \to ((N \in (A smul B) \leftrightarrow N \in P (k)) \to (N \in (A smul B) \leftrightarrow N \in P (k + 1))))$
101	100	a2d	$⊢ k \in ℤ_{\geq (N + 1)} \to ((φ \to (N \in (A smul B) \leftrightarrow N \in P (k))) \to (φ \to (N \in (A smul B) \leftrightarrow N \in P (k + 1))))$
102	9 13 17 21 22 101	uzind4i	$⊢ M \in ℤ_{\geq (N + 1)} \to (φ \to (N \in (A smul B) \leftrightarrow N \in P (M)))$
103	5 102	mpcom	$⊢ φ \to (N \in (A smul B) \leftrightarrow N \in P (M))$

Metamath Proof Explorer

Theorem smuval2

Proof