Metamath Proof Explorer

Theorem sadeq

Description: Any element of a sequence sum only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Hypotheses sadeq.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
sadeq.b ⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
sadeq.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion sadeq ( 𝜑 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 sadeq.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2 sadeq.b ⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3 sadeq.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4 inass ⊢ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( 𝐴 ∩ ( ( 0 ..^ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) )
5 inidm ⊢ ( ( 0 ..^ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 )
6 5 ineq2i ⊢ ( 𝐴 ∩ ( ( 0 ..^ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( 𝐴 ∩ ( 0 ..^ 𝑁 ) )
7 4 6 eqtri ⊢ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( 𝐴 ∩ ( 0 ..^ 𝑁 ) )
8 7 fveq2i ⊢ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) )
9 inass ⊢ ( ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( 𝐵 ∩ ( ( 0 ..^ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) )
10 5 ineq2i ⊢ ( 𝐵 ∩ ( ( 0 ..^ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( 𝐵 ∩ ( 0 ..^ 𝑁 ) )
11 9 10 eqtri ⊢ ( ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( 𝐵 ∩ ( 0 ..^ 𝑁 ) )
12 11 fveq2i ⊢ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) )
13 8 12 oveq12i ⊢ ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) )
14 13 oveq1i ⊢ ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) )
15 inss1 ⊢ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ 𝐴
16 15 1 sstrid ⊢ ( 𝜑 → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
17 inss1 ⊢ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ 𝐵
18 17 2 sstrid ⊢ ( 𝜑 → ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
19 eqid ⊢ seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) , 𝑚 ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) , 𝑚 ∈ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
20 eqid ⊢ ◡ ( bits ↾ ℕ0 ) = ◡ ( bits ↾ ℕ0 )
21 16 18 19 3 20 sadadd3 ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) )
22 eqid ⊢ seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) ) = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
23 1 2 22 3 20 sadadd3 ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) )
24 14 21 23 3eqtr4a ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) )
25 inss1 ⊢ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) )
26 sadcl ⊢ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ) → ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ⊆ ℕ0 )
27 16 18 26 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ⊆ ℕ0 )
28 25 27 sstrid ⊢ ( 𝜑 → ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
29 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
30 29 a1i ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ∈ Fin )
31 inss2 ⊢ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
32 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
33 30 31 32 sylancl ⊢ ( 𝜑 → ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
34 elfpw ⊢ ( ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
35 28 33 34 sylanbrc ⊢ ( 𝜑 → ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
36 bitsf1o ⊢ ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin )
37 f1ocnv ⊢ ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) → ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 )
38 f1of ⊢ ( ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 → ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0 )
39 36 37 38 mp2b ⊢ ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0
40 39 ffvelcdmi ⊢ ( ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
41 35 40 syl ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
42 41 nn0red ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ )
43 2rp ⊢ 2 ∈ ℝ+
44 43 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
45 3 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
46 44 45 rpexpcld ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℝ+ )
47 41 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
48 41 fvresd ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) )
49 f1ocnvfv2 ⊢ ( ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ) → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) )
50 36 35 49 sylancr ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) )
51 48 50 eqtr3d ⊢ ( 𝜑 → ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) )
52 51 31 eqsstrdi ⊢ ( 𝜑 → ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) )
53 41 nn0zd ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ )
54 bitsfzo ⊢ ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) ↔ ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) ) )
55 53 3 54 syl2anc ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) ↔ ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) ) )
56 52 55 mpbird ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) )
57 elfzolt2 ⊢ ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) )
58 56 57 syl ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) )
59 modid ⊢ ( ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ+ ) ∧ ( 0 ≤ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∧ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) ) ) → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
60 42 46 47 58 59 syl22anc ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
61 inss1 ⊢ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 𝐴 sadd 𝐵 )
62 sadcl ⊢ ( ( 𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ) → ( 𝐴 sadd 𝐵 ) ⊆ ℕ0 )
63 1 2 62 syl2anc ⊢ ( 𝜑 → ( 𝐴 sadd 𝐵 ) ⊆ ℕ0 )
64 61 63 sstrid ⊢ ( 𝜑 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
65 inss2 ⊢ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
66 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
67 30 65 66 sylancl ⊢ ( 𝜑 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
68 elfpw ⊢ ( ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
69 64 67 68 sylanbrc ⊢ ( 𝜑 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
70 39 ffvelcdmi ⊢ ( ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
71 69 70 syl ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
72 71 nn0red ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ )
73 71 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) )
74 71 fvresd ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) )
75 f1ocnvfv2 ⊢ ( ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ) → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) )
76 36 69 75 sylancr ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) )
77 74 76 eqtr3d ⊢ ( 𝜑 → ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) )
78 77 65 eqsstrdi ⊢ ( 𝜑 → ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) )
79 71 nn0zd ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ )
80 bitsfzo ⊢ ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) ↔ ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) ) )
81 79 3 80 syl2anc ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) ↔ ( bits ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) ) )
82 78 81 mpbird ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) )
83 elfzolt2 ⊢ ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) )
84 82 83 syl ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) )
85 modid ⊢ ( ( ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ+ ) ∧ ( 0 ≤ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∧ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) ) ) → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) )
86 72 46 73 84 85 syl22anc ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) )
87 24 60 86 3eqtr3rd ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
88 f1of1 ⊢ ( ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 → ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1→ ℕ0 )
89 36 37 88 mp2b ⊢ ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1→ ℕ0
90 f1fveq ⊢ ( ( ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1→ ℕ0 ∧ ( ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ) ) → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ↔ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
91 89 90 mpan ⊢ ( ( ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ) → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ↔ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
92 69 35 91 syl2anc ⊢ ( 𝜑 → ( ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ↔ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
93 87 92 mpbid ⊢ ( 𝜑 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) = ( ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) sadd ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∩ ( 0 ..^ 𝑁 ) ) )