Metamath Proof Explorer

Theorem sadcp1

Description: The carry sequence (which is a sequence of wffs, encoded as 1o and (/) ) is defined recursively as the carry operation applied to the previous carry and the two current inputs. (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Hypotheses sadval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
sadval.b ⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
sadval.c ⊢ 𝐶 = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
sadcp1.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion sadcp1 ( 𝜑 → ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) ↔ cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 sadval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2 sadval.b ⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3 sadval.c ⊢ 𝐶 = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
4 sadcp1.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
6 4 5 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
7 seqp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑁 ) ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) ) )
8 6 7 syl ⊢ ( 𝜑 → ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑁 ) ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) ) )
9 3 fveq1i ⊢ ( 𝐶 ‘ ( 𝑁 + 1 ) ) = ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ ( 𝑁 + 1 ) )
10 3 fveq1i ⊢ ( 𝐶 ‘ 𝑁 ) = ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑁 )
11 10 oveq1i ⊢ ( ( 𝐶 ‘ 𝑁 ) ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) ‘ 𝑁 ) ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) )
12 8 9 11 3eqtr4g ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝑁 + 1 ) ) = ( ( 𝐶 ‘ 𝑁 ) ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) ) )
13 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
14 eqeq1 ⊢ ( 𝑛 = ( 𝑁 + 1 ) → ( 𝑛 = 0 ↔ ( 𝑁 + 1 ) = 0 ) )
15 oveq1 ⊢ ( 𝑛 = ( 𝑁 + 1 ) → ( 𝑛 − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
16 14 15 ifbieq2d ⊢ ( 𝑛 = ( 𝑁 + 1 ) → if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) = if ( ( 𝑁 + 1 ) = 0 , ∅ , ( ( 𝑁 + 1 ) − 1 ) ) )
17 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) )
18 0ex ⊢ ∅ ∈ V
19 ovex ⊢ ( ( 𝑁 + 1 ) − 1 ) ∈ V
20 18 19 ifex ⊢ if ( ( 𝑁 + 1 ) = 0 , ∅ , ( ( 𝑁 + 1 ) − 1 ) ) ∈ V
21 16 17 20 fvmpt ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) = if ( ( 𝑁 + 1 ) = 0 , ∅ , ( ( 𝑁 + 1 ) − 1 ) ) )
22 4 13 21 3syl ⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) = if ( ( 𝑁 + 1 ) = 0 , ∅ , ( ( 𝑁 + 1 ) − 1 ) ) )
23 nn0p1nn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
24 4 23 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ )
25 24 nnne0d ⊢ ( 𝜑 → ( 𝑁 + 1 ) ≠ 0 )
26 ifnefalse ⊢ ( ( 𝑁 + 1 ) ≠ 0 → if ( ( 𝑁 + 1 ) = 0 , ∅ , ( ( 𝑁 + 1 ) − 1 ) ) = ( ( 𝑁 + 1 ) − 1 ) )
27 25 26 syl ⊢ ( 𝜑 → if ( ( 𝑁 + 1 ) = 0 , ∅ , ( ( 𝑁 + 1 ) − 1 ) ) = ( ( 𝑁 + 1 ) − 1 ) )
28 4 nn0cnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
29 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
30 28 29 pncand ⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
31 22 27 30 3eqtrd ⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) = 𝑁 )
32 31 oveq2d ⊢ ( 𝜑 → ( ( 𝐶 ‘ 𝑁 ) ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ‘ ( 𝑁 + 1 ) ) ) = ( ( 𝐶 ‘ 𝑁 ) ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) 𝑁 ) )
33 1 2 3 sadcf ⊢ ( 𝜑 → 𝐶 : ℕ0 ⟶ 2o )
34 33 4 ffvelrnd ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑁 ) ∈ 2o )
35 simpr ⊢ ( ( 𝑥 = ( 𝐶 ‘ 𝑁 ) ∧ 𝑦 = 𝑁 ) → 𝑦 = 𝑁 )
36 35 eleq1d ⊢ ( ( 𝑥 = ( 𝐶 ‘ 𝑁 ) ∧ 𝑦 = 𝑁 ) → ( 𝑦 ∈ 𝐴 ↔ 𝑁 ∈ 𝐴 ) )
37 35 eleq1d ⊢ ( ( 𝑥 = ( 𝐶 ‘ 𝑁 ) ∧ 𝑦 = 𝑁 ) → ( 𝑦 ∈ 𝐵 ↔ 𝑁 ∈ 𝐵 ) )
38 simpl ⊢ ( ( 𝑥 = ( 𝐶 ‘ 𝑁 ) ∧ 𝑦 = 𝑁 ) → 𝑥 = ( 𝐶 ‘ 𝑁 ) )
39 38 eleq2d ⊢ ( ( 𝑥 = ( 𝐶 ‘ 𝑁 ) ∧ 𝑦 = 𝑁 ) → ( ∅ ∈ 𝑥 ↔ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) )
40 36 37 39 cadbi123d ⊢ ( ( 𝑥 = ( 𝐶 ‘ 𝑁 ) ∧ 𝑦 = 𝑁 ) → ( cadd ( 𝑦 ∈ 𝐴 , 𝑦 ∈ 𝐵 , ∅ ∈ 𝑥 ) ↔ cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ) )
41 40 ifbid ⊢ ( ( 𝑥 = ( 𝐶 ‘ 𝑁 ) ∧ 𝑦 = 𝑁 ) → if ( cadd ( 𝑦 ∈ 𝐴 , 𝑦 ∈ 𝐵 , ∅ ∈ 𝑥 ) , 1o , ∅ ) = if ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , 1o , ∅ ) )
42 biidd ⊢ ( 𝑐 = 𝑥 → ( 𝑚 ∈ 𝐴 ↔ 𝑚 ∈ 𝐴 ) )
43 biidd ⊢ ( 𝑐 = 𝑥 → ( 𝑚 ∈ 𝐵 ↔ 𝑚 ∈ 𝐵 ) )
44 eleq2w ⊢ ( 𝑐 = 𝑥 → ( ∅ ∈ 𝑐 ↔ ∅ ∈ 𝑥 ) )
45 42 43 44 cadbi123d ⊢ ( 𝑐 = 𝑥 → ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) ↔ cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑥 ) ) )
46 45 ifbid ⊢ ( 𝑐 = 𝑥 → if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) = if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑥 ) , 1o , ∅ ) )
47 eleq1w ⊢ ( 𝑚 = 𝑦 → ( 𝑚 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
48 eleq1w ⊢ ( 𝑚 = 𝑦 → ( 𝑚 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
49 biidd ⊢ ( 𝑚 = 𝑦 → ( ∅ ∈ 𝑥 ↔ ∅ ∈ 𝑥 ) )
50 47 48 49 cadbi123d ⊢ ( 𝑚 = 𝑦 → ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑥 ) ↔ cadd ( 𝑦 ∈ 𝐴 , 𝑦 ∈ 𝐵 , ∅ ∈ 𝑥 ) ) )
51 50 ifbid ⊢ ( 𝑚 = 𝑦 → if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑥 ) , 1o , ∅ ) = if ( cadd ( 𝑦 ∈ 𝐴 , 𝑦 ∈ 𝐵 , ∅ ∈ 𝑥 ) , 1o , ∅ ) )
52 46 51 cbvmpov ⊢ ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) = ( 𝑥 ∈ 2o , 𝑦 ∈ ℕ0 ↦ if ( cadd ( 𝑦 ∈ 𝐴 , 𝑦 ∈ 𝐵 , ∅ ∈ 𝑥 ) , 1o , ∅ ) )
53 1oex ⊢ 1o ∈ V
54 53 18 ifex ⊢ if ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , 1o , ∅ ) ∈ V
55 41 52 54 ovmpoa ⊢ ( ( ( 𝐶 ‘ 𝑁 ) ∈ 2o ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐶 ‘ 𝑁 ) ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) 𝑁 ) = if ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , 1o , ∅ ) )
56 34 4 55 syl2anc ⊢ ( 𝜑 → ( ( 𝐶 ‘ 𝑁 ) ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) 𝑁 ) = if ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , 1o , ∅ ) )
57 12 32 56 3eqtrd ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝑁 + 1 ) ) = if ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , 1o , ∅ ) )
58 57 eleq2d ⊢ ( 𝜑 → ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) ↔ ∅ ∈ if ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , 1o , ∅ ) ) )
59 noel ⊢ ¬ ∅ ∈ ∅
60 iffalse ⊢ ( ¬ cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → if ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , 1o , ∅ ) = ∅ )
61 60 eleq2d ⊢ ( ¬ cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ∅ ∈ if ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , 1o , ∅ ) ↔ ∅ ∈ ∅ ) )
62 59 61 mtbiri ⊢ ( ¬ cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ¬ ∅ ∈ if ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , 1o , ∅ ) )
63 62 con4i ⊢ ( ∅ ∈ if ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , 1o , ∅ ) → cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) )
64 0lt1o ⊢ ∅ ∈ 1o
65 iftrue ⊢ ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → if ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , 1o , ∅ ) = 1o )
66 64 65 eleqtrrid ⊢ ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ∅ ∈ if ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , 1o , ∅ ) )
67 63 66 impbii ⊢ ( ∅ ∈ if ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , 1o , ∅ ) ↔ cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) )
68 58 67 bitrdi ⊢ ( 𝜑 → ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) ↔ cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ) )