Theorem 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	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
	smuval.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
	smuval.p	⊢ 𝑃 = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
	smuval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	smupvallem.a	⊢ ( 𝜑 → 𝐴 ⊆ ( 0 ..^ 𝑁 ) )
	smupvallem.m	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
Assertion	smupvallem	⊢ ( 𝜑 → ( 𝑃 ‘ 𝑀 ) = ( 𝐴 smul 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		smuval.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2		smuval.b	⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3		smuval.p	⊢ 𝑃 = seq 0 ( ( 𝑝 ∈ 𝒫 ℕ0 , 𝑚 ∈ ℕ0 ↦ ( 𝑝 sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑚 ∈ 𝐴 ∧ ( 𝑛 − 𝑚 ) ∈ 𝐵 ) } ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
4		smuval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5		smupvallem.a	⊢ ( 𝜑 → 𝐴 ⊆ ( 0 ..^ 𝑁 ) )
6		smupvallem.m	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
7	1 2 3	smupf	⊢ ( 𝜑 → 𝑃 : ℕ0 ⟶ 𝒫 ℕ0 )
8		eluznn0	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ℕ0 )
9	4 6 8	syl2anc	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
10	7 9	ffvelcdmd	⊢ ( 𝜑 → ( 𝑃 ‘ 𝑀 ) ∈ 𝒫 ℕ0 )
11	10	elpwid	⊢ ( 𝜑 → ( 𝑃 ‘ 𝑀 ) ⊆ ℕ0 )
12	11	sseld	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝑃 ‘ 𝑀 ) → 𝑘 ∈ ℕ0 ) )
13	1 2 3	smufval	⊢ ( 𝜑 → ( 𝐴 smul 𝐵 ) = { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
14		ssrab2	⊢ { 𝑘 ∈ ℕ0 ∣ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ℕ0
15	13 14	eqsstrdi	⊢ ( 𝜑 → ( 𝐴 smul 𝐵 ) ⊆ ℕ0 )
16	15	sseld	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 smul 𝐵 ) → 𝑘 ∈ ℕ0 ) )
17	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → 𝐴 ⊆ ℕ0 )
18	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → 𝐵 ⊆ ℕ0 )
19		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
20	6	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
21		uztrn	⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) )
22	20 21	sylan	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) )
23	17 18 3 19 22	smuval2	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → ( 𝑘 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑘 ∈ ( 𝑃 ‘ 𝑀 ) ) )
24	23	bicomd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → ( 𝑘 ∈ ( 𝑃 ‘ 𝑀 ) ↔ 𝑘 ∈ ( 𝐴 smul 𝐵 ) ) )
25	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
26		simpll	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝜑 )
27		fveqeq2	⊢ ( 𝑥 = 𝑁 → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) ↔ ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 𝑁 ) ) )
28	27	imbi2d	⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) ) ↔ ( 𝜑 → ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 𝑁 ) ) ) )
29		fveqeq2	⊢ ( 𝑥 = 𝑘 → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) ↔ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑁 ) ) )
30	29	imbi2d	⊢ ( 𝑥 = 𝑘 → ( ( 𝜑 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) ) ↔ ( 𝜑 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑁 ) ) ) )
31		fveqeq2	⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) ↔ ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑁 ) ) )
32	31	imbi2d	⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) ) ↔ ( 𝜑 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑁 ) ) ) )
33		fveqeq2	⊢ ( 𝑥 = 𝑀 → ( ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) ↔ ( 𝑃 ‘ 𝑀 ) = ( 𝑃 ‘ 𝑁 ) ) )
34	33	imbi2d	⊢ ( 𝑥 = 𝑀 → ( ( 𝜑 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑁 ) ) ↔ ( 𝜑 → ( 𝑃 ‘ 𝑀 ) = ( 𝑃 ‘ 𝑁 ) ) ) )
35		eqidd	⊢ ( 𝜑 → ( 𝑃 ‘ 𝑁 ) = ( 𝑃 ‘ 𝑁 ) )
36	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐴 ⊆ ℕ0 )
37	2	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐵 ⊆ ℕ0 )
38		eluznn0	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ℕ0 )
39	4 38	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ℕ0 )
40	36 37 3 39	smupp1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) )
41	4	nn0red	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
42	41	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ℝ )
43	39	nn0red	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ℝ )
44		eluzle	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ 𝑘 )
45	44	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ≤ 𝑘 )
46	42 43 45	lensymd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ¬ 𝑘 < 𝑁 )
47	5	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐴 ⊆ ( 0 ..^ 𝑁 ) )
48	47	sseld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑘 ∈ 𝐴 → 𝑘 ∈ ( 0 ..^ 𝑁 ) ) )
49		elfzolt2	⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → 𝑘 < 𝑁 )
50	48 49	syl6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑘 ∈ 𝐴 → 𝑘 < 𝑁 ) )
51	50	adantrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) → 𝑘 < 𝑁 ) )
52	46 51	mtod	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) )
53	52	ralrimivw	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ∀ 𝑛 ∈ ℕ0 ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) )
54		rabeq0	⊢ ( { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } = ∅ ↔ ∀ 𝑛 ∈ ℕ0 ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) )
55	53 54	sylibr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } = ∅ )
56	55	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑃 ‘ 𝑘 ) sadd { 𝑛 ∈ ℕ0 ∣ ( 𝑘 ∈ 𝐴 ∧ ( 𝑛 − 𝑘 ) ∈ 𝐵 ) } ) = ( ( 𝑃 ‘ 𝑘 ) sadd ∅ ) )
57	7	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑃 : ℕ0 ⟶ 𝒫 ℕ0 )
58	57 39	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ 𝒫 ℕ0 )
59	58	elpwid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑃 ‘ 𝑘 ) ⊆ ℕ0 )
60		sadid1	⊢ ( ( 𝑃 ‘ 𝑘 ) ⊆ ℕ0 → ( ( 𝑃 ‘ 𝑘 ) sadd ∅ ) = ( 𝑃 ‘ 𝑘 ) )
61	59 60	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑃 ‘ 𝑘 ) sadd ∅ ) = ( 𝑃 ‘ 𝑘 ) )
62	40 56 61	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑘 ) )
63	62	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑁 ) ↔ ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑁 ) ) )
64	63	biimprd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑁 ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑁 ) ) )
65	64	expcom	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝜑 → ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑁 ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑁 ) ) ) )
66	65	a2d	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ( 𝜑 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑁 ) ) → ( 𝜑 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑁 ) ) ) )
67	28 30 32 34 35 66	uzind4i	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝜑 → ( 𝑃 ‘ 𝑀 ) = ( 𝑃 ‘ 𝑁 ) ) )
68	25 26 67	sylc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑃 ‘ 𝑀 ) = ( 𝑃 ‘ 𝑁 ) )
69		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
70	28 30 32 32 35 66	uzind4i	⊢ ( ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝜑 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑁 ) ) )
71	69 26 70	sylc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 𝑁 ) )
72	68 71	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑃 ‘ 𝑀 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) )
73	72	eleq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑘 ∈ ( 𝑃 ‘ 𝑀 ) ↔ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
74	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐴 ⊆ ℕ0 )
75	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐵 ⊆ ℕ0 )
76		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ℕ0 )
77	74 75 3 76	smuval	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑘 ∈ ( 𝐴 smul 𝐵 ) ↔ 𝑘 ∈ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) )
78	73 77	bitr4d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑘 ∈ ( 𝑃 ‘ 𝑀 ) ↔ 𝑘 ∈ ( 𝐴 smul 𝐵 ) ) )
79		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
80	79	nn0zd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℤ )
81	80	peano2zd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℤ )
82	4	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
83	82	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
84		uztric	⊢ ( ( ( 𝑘 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ∨ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) )
85	81 83 84	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ∨ ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) )
86	24 78 85	mpjaodan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ∈ ( 𝑃 ‘ 𝑀 ) ↔ 𝑘 ∈ ( 𝐴 smul 𝐵 ) ) )
87	86	ex	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 → ( 𝑘 ∈ ( 𝑃 ‘ 𝑀 ) ↔ 𝑘 ∈ ( 𝐴 smul 𝐵 ) ) ) )
88	12 16 87	pm5.21ndd	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝑃 ‘ 𝑀 ) ↔ 𝑘 ∈ ( 𝐴 smul 𝐵 ) ) )
89	88	eqrdv	⊢ ( 𝜑 → ( 𝑃 ‘ 𝑀 ) = ( 𝐴 smul 𝐵 ) )