Metamath Proof Explorer

Theorem sadasslem

Description: Lemma for sadass . (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Hypotheses sadasslem.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
sadasslem.2 ⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
sadasslem.3 ⊢ ( 𝜑 → 𝐶 ⊆ ℕ0 )
sadasslem.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion sadasslem ( 𝜑 → ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 sadasslem.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2 sadasslem.2 ⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3 sadasslem.3 ⊢ ( 𝜑 → 𝐶 ⊆ ℕ0 )
4 sadasslem.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 inss1 ⊢ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ 𝐴
6 5 1 sstrid ⊢ ( 𝜑 → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
7 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
8 7 a1i ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ∈ Fin )
9 inss2 ⊢ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
10 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
11 8 9 10 sylancl ⊢ ( 𝜑 → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
12 elfpw ⊢ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
13 6 11 12 sylanbrc ⊢ ( 𝜑 → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
14 bitsf1o ⊢ ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin )
15 f1ocnv ⊢ ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) → ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 )
16 f1of ⊢ ( ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 → ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0 )
17 14 15 16 mp2b ⊢ ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0
18 17 ffvelrni ⊢ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
19 13 18 syl ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
20 19 nn0cnd ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℂ )
21 inss1 ⊢ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ 𝐵
22 21 2 sstrid ⊢ ( 𝜑 → ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
23 inss2 ⊢ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
24 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
25 8 23 24 sylancl ⊢ ( 𝜑 → ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
26 elfpw ⊢ ( ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
27 22 25 26 sylanbrc ⊢ ( 𝜑 → ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
28 17 ffvelrni ⊢ ( ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
29 27 28 syl ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
30 29 nn0cnd ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℂ )
31 inss1 ⊢ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ⊆ 𝐶
32 31 3 sstrid ⊢ ( 𝜑 → ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
33 inss2 ⊢ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
34 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
35 8 33 34 sylancl ⊢ ( 𝜑 → ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
36 elfpw ⊢ ( ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
37 32 35 36 sylanbrc ⊢ ( 𝜑 → ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
38 17 ffvelrni ⊢ ( ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
39 37 38 syl ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
40 39 nn0cnd ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℂ )
41 20 30 40 addassd ⊢ ( 𝜑 → ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ) ) ) )
42 41 oveq1d ⊢ ( 𝜑 → ( ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ) ) ) mod ( 2 ↑ 𝑁 ) ) )
43 inss1 ⊢ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 𝐴 sadd 𝐵 )
44 sadcl ⊢ ( ( 𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ) → ( 𝐴 sadd 𝐵 ) ⊆ ℕ0 )
45 1 2 44 syl2anc ⊢ ( 𝜑 → ( 𝐴 sadd 𝐵 ) ⊆ ℕ0 )
46 43 45 sstrid ⊢ ( 𝜑 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
47 inss2 ⊢ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
48 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
49 8 47 48 sylancl ⊢ ( 𝜑 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
50 elfpw ⊢ ( ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
51 46 49 50 sylanbrc ⊢ ( 𝜑 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
52 17 ffvelrni ⊢ ( ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
53 51 52 syl ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
54 53 nn0red ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ )
55 19 nn0red ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ )
56 29 nn0red ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ )
57 55 56 readdcld ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ∈ ℝ )
58 39 nn0red ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ )
59 2rp ⊢ 2 ∈ ℝ+
60 59 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
61 4 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
62 60 61 rpexpcld ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℝ+ )
63 eqid ⊢ seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
64 eqid ⊢ ◡ ( bits ↾ ℕ0 ) = ◡ ( bits ↾ ℕ0 )
65 1 2 63 4 64 sadadd3 ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) )
66 eqidd ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) )
67 54 57 58 58 62 65 66 modadd12d ⊢ ( 𝜑 → ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) )
68 inss1 ⊢ ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 𝐵 sadd 𝐶 )
69 sadcl ⊢ ( ( 𝐵 ⊆ ℕ0 ∧ 𝐶 ⊆ ℕ0 ) → ( 𝐵 sadd 𝐶 ) ⊆ ℕ0 )
70 2 3 69 syl2anc ⊢ ( 𝜑 → ( 𝐵 sadd 𝐶 ) ⊆ ℕ0 )
71 68 70 sstrid ⊢ ( 𝜑 → ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
72 inss2 ⊢ ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
73 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
74 8 72 73 sylancl ⊢ ( 𝜑 → ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
75 elfpw ⊢ ( ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
76 71 74 75 sylanbrc ⊢ ( 𝜑 → ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
77 17 ffvelrni ⊢ ( ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
78 76 77 syl ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
79 78 nn0red ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ )
80 56 58 readdcld ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ) ) ∈ ℝ )
81 eqidd ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) )
82 eqid ⊢ seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐵 , 𝑚 ∈ 𝐶 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐵 , 𝑚 ∈ 𝐶 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
83 2 3 82 4 64 sadadd3 ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) )
84 55 55 79 80 62 81 83 modadd12d ⊢ ( 𝜑 → ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ) ) ) mod ( 2 ↑ 𝑁 ) ) )
85 42 67 84 3eqtr4d ⊢ ( 𝜑 → ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) )
86 eqid ⊢ seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ ( 𝐴 sadd 𝐵 ) , 𝑚 ∈ 𝐶 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ ( 𝐴 sadd 𝐵 ) , 𝑚 ∈ 𝐶 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
87 45 3 86 4 64 sadadd3 ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐶 ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) )
88 eqid ⊢ seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ ( 𝐵 sadd 𝐶 ) , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ ( 𝐵 sadd 𝐶 ) , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
89 1 70 88 4 64 sadadd3 ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐵 sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) )
90 85 87 89 3eqtr4d ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) )
91 inss1 ⊢ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 )
92 sadcl ⊢ ( ( ( 𝐴 sadd 𝐵 ) ⊆ ℕ0 ∧ 𝐶 ⊆ ℕ0 ) → ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ⊆ ℕ0 )
93 45 3 92 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ⊆ ℕ0 )
94 91 93 sstrid ⊢ ( 𝜑 → ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
95 inss2 ⊢ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
96 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
97 8 95 96 sylancl ⊢ ( 𝜑 → ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
98 elfpw ⊢ ( ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
99 94 97 98 sylanbrc ⊢ ( 𝜑 → ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
100 17 ffvelrni ⊢ ( ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
101 99 100 syl ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
102 101 nn0red ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ )
103 101 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) )
104 101 fvresd ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) )
105 f1ocnvfv2 ⊢ ( ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ) → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) )
106 14 99 105 sylancr ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) )
107 104 106 eqtr3d ⊢ ( 𝜑 → ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) )
108 107 95 eqsstrdi ⊢ ( 𝜑 → ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) )
109 101 nn0zd ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ )
110 bitsfzo ⊢ ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) ↔ ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) ) )
111 109 4 110 syl2anc ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) ↔ ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) ) )
112 108 111 mpbird ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) )
113 elfzolt2 ⊢ ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) )
114 112 113 syl ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) )
115 modid ⊢ ( ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ+ ) ∧ ( 0 ≤ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∧ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) ) ) → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) )
116 102 62 103 114 115 syl22anc ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) )
117 inss1 ⊢ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) )
118 sadcl ⊢ ( ( 𝐴 ⊆ ℕ0 ∧ ( 𝐵 sadd 𝐶 ) ⊆ ℕ0 ) → ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ⊆ ℕ0 )
119 1 70 118 syl2anc ⊢ ( 𝜑 → ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ⊆ ℕ0 )
120 117 119 sstrid ⊢ ( 𝜑 → ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
121 inss2 ⊢ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
122 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
123 8 121 122 sylancl ⊢ ( 𝜑 → ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
124 elfpw ⊢ ( ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
125 120 123 124 sylanbrc ⊢ ( 𝜑 → ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
126 17 ffvelrni ⊢ ( ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
127 125 126 syl ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
128 127 nn0red ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ )
129 2nn ⊢ 2 ∈ ℕ
130 129 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
131 130 4 nnexpcld ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℕ )
132 131 nnrpd ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℝ+ )
133 127 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
134 127 fvresd ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) )
135 f1ocnvfv2 ⊢ ( ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ) → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) )
136 14 125 135 sylancr ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) )
137 134 136 eqtr3d ⊢ ( 𝜑 → ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) )
138 137 121 eqsstrdi ⊢ ( 𝜑 → ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) )
139 127 nn0zd ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ )
140 bitsfzo ⊢ ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) ↔ ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) ) )
141 139 4 140 syl2anc ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) ↔ ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) ) )
142 138 141 mpbird ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) )
143 elfzolt2 ⊢ ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) )
144 142 143 syl ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) )
145 modid ⊢ ( ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ+ ) ∧ ( 0 ≤ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∧ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) ) ) → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
146 128 132 133 144 145 syl22anc ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
147 90 116 146 3eqtr3d ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
148 f1of1 ⊢ ( ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 → ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1→ ℕ0 )
149 14 15 148 mp2b ⊢ ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1→ ℕ0
150 f1fveq ⊢ ( ( ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1→ ℕ0 ∧ ( ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ) ) → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ↔ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
151 149 150 mpan ⊢ ( ( ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ) → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ↔ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
152 99 125 151 syl2anc ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ↔ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
153 147 152 mpbid ⊢ ( 𝜑 → ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ 𝑁 ) ) )