smupvallem

Description: If A only has elements less than N , then all elements of the partial sum sequence past N already equal the final value. (Contributed by Mario Carneiro, 20-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}$
	smupvallem.a	$⊢ φ \to A \subseteq (0 ..^N)$
	smupvallem.m	$⊢ φ \to M \in ℤ_{\geq N}$
Assertion	smupvallem	$⊢ φ \to P (M) = A smul B$

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		smupvallem.a	$⊢ φ \to A \subseteq (0 ..^N)$
6		smupvallem.m	$⊢ φ \to M \in ℤ_{\geq N}$
7	1 2 3	smupf	$⊢ φ \to P : ℕ_{0} ⟶ 𝒫 ℕ_{0}$
8		eluznn0	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N}) \to M \in ℕ_{0}$
9	4 6 8	syl2anc	$⊢ φ \to M \in ℕ_{0}$
10	7 9	ffvelcdmd	$⊢ φ \to P (M) \in 𝒫 ℕ_{0}$
11	10	elpwid	$⊢ φ \to P (M) \subseteq ℕ_{0}$
12	11	sseld	$⊢ φ \to (k \in P (M) \to k \in ℕ_{0})$
13	1 2 3	smufval	$⊢ φ \to A smul B = \{k \in ℕ_{0} \| k \in P (k + 1)\}$
14		ssrab2	$⊢ \{k \in ℕ_{0} \| k \in P (k + 1)\} \subseteq ℕ_{0}$
15	13 14	eqsstrdi	$⊢ φ \to A smul B \subseteq ℕ_{0}$
16	15	sseld	$⊢ φ \to (k \in (A smul B) \to k \in ℕ_{0})$
17	1	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land N \in ℤ_{\geq (k + 1)}) \to A \subseteq ℕ_{0}$
18	2	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land N \in ℤ_{\geq (k + 1)}) \to B \subseteq ℕ_{0}$
19		simplr	$⊢ ((φ \land k \in ℕ_{0}) \land N \in ℤ_{\geq (k + 1)}) \to k \in ℕ_{0}$
20	6	adantr	$⊢ (φ \land k \in ℕ_{0}) \to M \in ℤ_{\geq N}$
21		uztrn	$⊢ (M \in ℤ_{\geq N} \land N \in ℤ_{\geq (k + 1)}) \to M \in ℤ_{\geq (k + 1)}$
22	20 21	sylan	$⊢ ((φ \land k \in ℕ_{0}) \land N \in ℤ_{\geq (k + 1)}) \to M \in ℤ_{\geq (k + 1)}$
23	17 18 3 19 22	smuval2	$⊢ ((φ \land k \in ℕ_{0}) \land N \in ℤ_{\geq (k + 1)}) \to (k \in (A smul B) \leftrightarrow k \in P (M))$
24	23	bicomd	$⊢ ((φ \land k \in ℕ_{0}) \land N \in ℤ_{\geq (k + 1)}) \to (k \in P (M) \leftrightarrow k \in (A smul B))$
25	6	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land k + 1 \in ℤ_{\geq N}) \to M \in ℤ_{\geq N}$
26		simpll	$⊢ ((φ \land k \in ℕ_{0}) \land k + 1 \in ℤ_{\geq N}) \to φ$
27		fveqeq2	$⊢ x = N \to (P (x) = P (N) \leftrightarrow P (N) = P (N))$
28	27	imbi2d	$⊢ x = N \to ((φ \to P (x) = P (N)) \leftrightarrow (φ \to P (N) = P (N)))$
29		fveqeq2	$⊢ x = k \to (P (x) = P (N) \leftrightarrow P (k) = P (N))$
30	29	imbi2d	$⊢ x = k \to ((φ \to P (x) = P (N)) \leftrightarrow (φ \to P (k) = P (N)))$
31		fveqeq2	$⊢ x = k + 1 \to (P (x) = P (N) \leftrightarrow P (k + 1) = P (N))$
32	31	imbi2d	$⊢ x = k + 1 \to ((φ \to P (x) = P (N)) \leftrightarrow (φ \to P (k + 1) = P (N)))$
33		fveqeq2	$⊢ x = M \to (P (x) = P (N) \leftrightarrow P (M) = P (N))$
34	33	imbi2d	$⊢ x = M \to ((φ \to P (x) = P (N)) \leftrightarrow (φ \to P (M) = P (N)))$
35		eqidd	$⊢ φ \to P (N) = P (N)$
36	1	adantr	$⊢ (φ \land k \in ℤ_{\geq N}) \to A \subseteq ℕ_{0}$
37	2	adantr	$⊢ (φ \land k \in ℤ_{\geq N}) \to B \subseteq ℕ_{0}$
38		eluznn0	$⊢ (N \in ℕ_{0} \land k \in ℤ_{\geq N}) \to k \in ℕ_{0}$
39	4 38	sylan	$⊢ (φ \land k \in ℤ_{\geq N}) \to k \in ℕ_{0}$
40	36 37 3 39	smupp1	$⊢ (φ \land k \in ℤ_{\geq N}) \to P (k + 1) = P (k) sadd \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\}$
41	4	nn0red	$⊢ φ \to N \in ℝ$
42	41	adantr	$⊢ (φ \land k \in ℤ_{\geq N}) \to N \in ℝ$
43	39	nn0red	$⊢ (φ \land k \in ℤ_{\geq N}) \to k \in ℝ$
44		eluzle	$⊢ k \in ℤ_{\geq N} \to N \leq k$
45	44	adantl	$⊢ (φ \land k \in ℤ_{\geq N}) \to N \leq k$
46	42 43 45	lensymd	$⊢ (φ \land k \in ℤ_{\geq N}) \to \neg k < N$
47	5	adantr	$⊢ (φ \land k \in ℤ_{\geq N}) \to A \subseteq (0 ..^N)$
48	47	sseld	$⊢ (φ \land k \in ℤ_{\geq N}) \to (k \in A \to k \in (0 ..^N))$
49		elfzolt2	$⊢ k \in (0 ..^N) \to k < N$
50	48 49	syl6	$⊢ (φ \land k \in ℤ_{\geq N}) \to (k \in A \to k < N)$
51	50	adantrd	$⊢ (φ \land k \in ℤ_{\geq N}) \to ((k \in A \land n - k \in B) \to k < N)$
52	46 51	mtod	$⊢ (φ \land k \in ℤ_{\geq N}) \to \neg (k \in A \land n - k \in B)$
53	52	ralrimivw	$⊢ (φ \land k \in ℤ_{\geq N}) \to \forall n \in ℕ_{0} \neg (k \in A \land n - k \in B)$
54		rabeq0	$⊢ \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\} = \emptyset \leftrightarrow \forall n \in ℕ_{0} \neg (k \in A \land n - k \in B)$
55	53 54	sylibr	$⊢ (φ \land k \in ℤ_{\geq N}) \to \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\} = \emptyset$
56	55	oveq2d	$⊢ (φ \land k \in ℤ_{\geq N}) \to P (k) sadd \{n \in ℕ_{0} \| (k \in A \land n - k \in B)\} = P (k) sadd \emptyset$
57	7	adantr	$⊢ (φ \land k \in ℤ_{\geq N}) \to P : ℕ_{0} ⟶ 𝒫 ℕ_{0}$
58	57 39	ffvelcdmd	$⊢ (φ \land k \in ℤ_{\geq N}) \to P (k) \in 𝒫 ℕ_{0}$
59	58	elpwid	$⊢ (φ \land k \in ℤ_{\geq N}) \to P (k) \subseteq ℕ_{0}$
60		sadid1	$⊢ P (k) \subseteq ℕ_{0} \to P (k) sadd \emptyset = P (k)$
61	59 60	syl	$⊢ (φ \land k \in ℤ_{\geq N}) \to P (k) sadd \emptyset = P (k)$
62	40 56 61	3eqtrd	$⊢ (φ \land k \in ℤ_{\geq N}) \to P (k + 1) = P (k)$
63	62	eqeq1d	$⊢ (φ \land k \in ℤ_{\geq N}) \to (P (k + 1) = P (N) \leftrightarrow P (k) = P (N))$
64	63	biimprd	$⊢ (φ \land k \in ℤ_{\geq N}) \to (P (k) = P (N) \to P (k + 1) = P (N))$
65	64	expcom	$⊢ k \in ℤ_{\geq N} \to (φ \to (P (k) = P (N) \to P (k + 1) = P (N)))$
66	65	a2d	$⊢ k \in ℤ_{\geq N} \to ((φ \to P (k) = P (N)) \to (φ \to P (k + 1) = P (N)))$
67	28 30 32 34 35 66	uzind4i	$⊢ M \in ℤ_{\geq N} \to (φ \to P (M) = P (N))$
68	25 26 67	sylc	$⊢ ((φ \land k \in ℕ_{0}) \land k + 1 \in ℤ_{\geq N}) \to P (M) = P (N)$
69		simpr	$⊢ ((φ \land k \in ℕ_{0}) \land k + 1 \in ℤ_{\geq N}) \to k + 1 \in ℤ_{\geq N}$
70	28 30 32 32 35 66	uzind4i	$⊢ k + 1 \in ℤ_{\geq N} \to (φ \to P (k + 1) = P (N))$
71	69 26 70	sylc	$⊢ ((φ \land k \in ℕ_{0}) \land k + 1 \in ℤ_{\geq N}) \to P (k + 1) = P (N)$
72	68 71	eqtr4d	$⊢ ((φ \land k \in ℕ_{0}) \land k + 1 \in ℤ_{\geq N}) \to P (M) = P (k + 1)$
73	72	eleq2d	$⊢ ((φ \land k \in ℕ_{0}) \land k + 1 \in ℤ_{\geq N}) \to (k \in P (M) \leftrightarrow k \in P (k + 1))$
74	1	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land k + 1 \in ℤ_{\geq N}) \to A \subseteq ℕ_{0}$
75	2	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land k + 1 \in ℤ_{\geq N}) \to B \subseteq ℕ_{0}$
76		simplr	$⊢ ((φ \land k \in ℕ_{0}) \land k + 1 \in ℤ_{\geq N}) \to k \in ℕ_{0}$
77	74 75 3 76	smuval	$⊢ ((φ \land k \in ℕ_{0}) \land k + 1 \in ℤ_{\geq N}) \to (k \in (A smul B) \leftrightarrow k \in P (k + 1))$
78	73 77	bitr4d	$⊢ ((φ \land k \in ℕ_{0}) \land k + 1 \in ℤ_{\geq N}) \to (k \in P (M) \leftrightarrow k \in (A smul B))$
79		simpr	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
80	79	nn0zd	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℤ$
81	80	peano2zd	$⊢ (φ \land k \in ℕ_{0}) \to k + 1 \in ℤ$
82	4	nn0zd	$⊢ φ \to N \in ℤ$
83	82	adantr	$⊢ (φ \land k \in ℕ_{0}) \to N \in ℤ$
84		uztric	$⊢ (k + 1 \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq (k + 1)} \lor k + 1 \in ℤ_{\geq N})$
85	81 83 84	syl2anc	$⊢ (φ \land k \in ℕ_{0}) \to (N \in ℤ_{\geq (k + 1)} \lor k + 1 \in ℤ_{\geq N})$
86	24 78 85	mpjaodan	$⊢ (φ \land k \in ℕ_{0}) \to (k \in P (M) \leftrightarrow k \in (A smul B))$
87	86	ex	$⊢ φ \to (k \in ℕ_{0} \to (k \in P (M) \leftrightarrow k \in (A smul B)))$
88	12 16 87	pm5.21ndd	$⊢ φ \to (k \in P (M) \leftrightarrow k \in (A smul B))$
89	88	eqrdv	$⊢ φ \to P (M) = A smul B$

Metamath Proof Explorer

Theorem smupvallem

Proof