Metamath Proof Explorer

Theorem sadaddlem

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

Ref Expression
Hypotheses sadaddlem.c ⊢ 𝐶 = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ ( bits ‘ 𝐴 ) , 𝑚 ∈ ( bits ‘ 𝐵 ) , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
sadaddlem.k ⊢ 𝐾 = ◡ ( bits ↾ ℕ0 )
sadaddlem.1 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
sadaddlem.2 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
sadaddlem.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion sadaddlem ( 𝜑 → ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( bits ‘ ( ( 𝐴 + 𝐵 ) mod ( 2 ↑ 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 sadaddlem.c ⊢ 𝐶 = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ ( bits ‘ 𝐴 ) , 𝑚 ∈ ( bits ‘ 𝐵 ) , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
2 sadaddlem.k ⊢ 𝐾 = ◡ ( bits ↾ ℕ0 )
3 sadaddlem.1 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
4 sadaddlem.2 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
5 sadaddlem.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6 2nn ⊢ 2 ∈ ℕ
7 6 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
8 7 5 nnexpcld ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℕ )
9 8 nnzd ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℤ )
10 inss1 ⊢ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( bits ‘ 𝐴 )
11 bitsss ⊢ ( bits ‘ 𝐴 ) ⊆ ℕ0
12 10 11 sstri ⊢ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0
13 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
14 inss2 ⊢ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
15 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
16 13 14 15 mp2an ⊢ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin
17 elfpw ⊢ ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
18 12 16 17 mpbir2an ⊢ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin )
19 bitsf1o ⊢ ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin )
20 f1ocnv ⊢ ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) → ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 )
21 f1of ⊢ ( ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 → ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0 )
22 19 20 21 mp2b ⊢ ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0
23 2 feq1i ⊢ ( 𝐾 : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0 ↔ ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0 )
24 22 23 mpbir ⊢ 𝐾 : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0
25 24 ffvelrni ⊢ ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
26 18 25 mp1i ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
27 26 nn0zd ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ )
28 3 27 zsubcld ⊢ ( 𝜑 → ( 𝐴 − ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ∈ ℤ )
29 inss1 ⊢ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( bits ‘ 𝐵 )
30 bitsss ⊢ ( bits ‘ 𝐵 ) ⊆ ℕ0
31 29 30 sstri ⊢ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0
32 inss2 ⊢ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
33 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
34 13 32 33 mp2an ⊢ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin
35 elfpw ⊢ ( ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
36 31 34 35 mpbir2an ⊢ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin )
37 24 ffvelrni ⊢ ( ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
38 36 37 mp1i ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
39 38 nn0zd ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ )
40 4 39 zsubcld ⊢ ( 𝜑 → ( 𝐵 − ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ∈ ℤ )
41 2 fveq1i ⊢ ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) )
42 3 8 zmodcld ⊢ ( 𝜑 → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ∈ ℕ0 )
43 42 fvresd ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) = ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) )
44 bitsmod ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) = ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) )
45 3 5 44 syl2anc ⊢ ( 𝜑 → ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) = ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) )
46 43 45 eqtrd ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) = ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) )
47 f1ocnvfv ⊢ ( ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ∈ ℕ0 ) → ( ( ( bits ↾ ℕ0 ) ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) = ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) )
48 19 42 47 sylancr ⊢ ( 𝜑 → ( ( ( bits ↾ ℕ0 ) ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) = ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) )
49 46 48 mpd ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( 𝐴 mod ( 2 ↑ 𝑁 ) ) )
50 41 49 eqtrid ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( 𝐴 mod ( 2 ↑ 𝑁 ) ) )
51 50 oveq2d ⊢ ( 𝜑 → ( 𝐴 − ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( 𝐴 − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) )
52 51 oveq1d ⊢ ( 𝜑 → ( ( 𝐴 − ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) / ( 2 ↑ 𝑁 ) ) = ( ( 𝐴 − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) )
53 3 zred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
54 8 nnrpd ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℝ+ )
55 moddifz ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ+ ) → ( ( 𝐴 − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) ∈ ℤ )
56 53 54 55 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) ∈ ℤ )
57 52 56 eqeltrd ⊢ ( 𝜑 → ( ( 𝐴 − ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) / ( 2 ↑ 𝑁 ) ) ∈ ℤ )
58 8 nnne0d ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ≠ 0 )
59 dvdsval2 ⊢ ( ( ( 2 ↑ 𝑁 ) ∈ ℤ ∧ ( 2 ↑ 𝑁 ) ≠ 0 ∧ ( 𝐴 − ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ∈ ℤ ) → ( ( 2 ↑ 𝑁 ) ∥ ( 𝐴 − ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ↔ ( ( 𝐴 − ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) / ( 2 ↑ 𝑁 ) ) ∈ ℤ ) )
60 9 58 28 59 syl3anc ⊢ ( 𝜑 → ( ( 2 ↑ 𝑁 ) ∥ ( 𝐴 − ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ↔ ( ( 𝐴 − ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) / ( 2 ↑ 𝑁 ) ) ∈ ℤ ) )
61 57 60 mpbird ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∥ ( 𝐴 − ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) )
62 2 fveq1i ⊢ ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) )
63 4 8 zmodcld ⊢ ( 𝜑 → ( 𝐵 mod ( 2 ↑ 𝑁 ) ) ∈ ℕ0 )
64 63 fvresd ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( 𝐵 mod ( 2 ↑ 𝑁 ) ) ) = ( bits ‘ ( 𝐵 mod ( 2 ↑ 𝑁 ) ) ) )
65 bitsmod ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( bits ‘ ( 𝐵 mod ( 2 ↑ 𝑁 ) ) ) = ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) )
66 4 5 65 syl2anc ⊢ ( 𝜑 → ( bits ‘ ( 𝐵 mod ( 2 ↑ 𝑁 ) ) ) = ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) )
67 64 66 eqtrd ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( 𝐵 mod ( 2 ↑ 𝑁 ) ) ) = ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) )
68 f1ocnvfv ⊢ ( ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( 𝐵 mod ( 2 ↑ 𝑁 ) ) ∈ ℕ0 ) → ( ( ( bits ↾ ℕ0 ) ‘ ( 𝐵 mod ( 2 ↑ 𝑁 ) ) ) = ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( 𝐵 mod ( 2 ↑ 𝑁 ) ) ) )
69 19 63 68 sylancr ⊢ ( 𝜑 → ( ( ( bits ↾ ℕ0 ) ‘ ( 𝐵 mod ( 2 ↑ 𝑁 ) ) ) = ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( 𝐵 mod ( 2 ↑ 𝑁 ) ) ) )
70 67 69 mpd ⊢ ( 𝜑 → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( 𝐵 mod ( 2 ↑ 𝑁 ) ) )
71 62 70 eqtrid ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( 𝐵 mod ( 2 ↑ 𝑁 ) ) )
72 71 oveq2d ⊢ ( 𝜑 → ( 𝐵 − ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( 𝐵 − ( 𝐵 mod ( 2 ↑ 𝑁 ) ) ) )
73 72 oveq1d ⊢ ( 𝜑 → ( ( 𝐵 − ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) / ( 2 ↑ 𝑁 ) ) = ( ( 𝐵 − ( 𝐵 mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) )
74 4 zred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
75 moddifz ⊢ ( ( 𝐵 ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ+ ) → ( ( 𝐵 − ( 𝐵 mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) ∈ ℤ )
76 74 54 75 syl2anc ⊢ ( 𝜑 → ( ( 𝐵 − ( 𝐵 mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) ∈ ℤ )
77 73 76 eqeltrd ⊢ ( 𝜑 → ( ( 𝐵 − ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) / ( 2 ↑ 𝑁 ) ) ∈ ℤ )
78 dvdsval2 ⊢ ( ( ( 2 ↑ 𝑁 ) ∈ ℤ ∧ ( 2 ↑ 𝑁 ) ≠ 0 ∧ ( 𝐵 − ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ∈ ℤ ) → ( ( 2 ↑ 𝑁 ) ∥ ( 𝐵 − ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ↔ ( ( 𝐵 − ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) / ( 2 ↑ 𝑁 ) ) ∈ ℤ ) )
79 9 58 40 78 syl3anc ⊢ ( 𝜑 → ( ( 2 ↑ 𝑁 ) ∥ ( 𝐵 − ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ↔ ( ( 𝐵 − ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) / ( 2 ↑ 𝑁 ) ) ∈ ℤ ) )
80 77 79 mpbird ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∥ ( 𝐵 − ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) )
81 9 28 40 61 80 dvds2addd ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∥ ( ( 𝐴 − ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( 𝐵 − ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ) )
82 3 zcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
83 4 zcnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
84 26 nn0cnd ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℂ )
85 38 nn0cnd ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℂ )
86 82 83 84 85 addsub4d ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) − ( ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ) = ( ( 𝐴 − ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( 𝐵 − ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ) )
87 81 86 breqtrrd ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∥ ( ( 𝐴 + 𝐵 ) − ( ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ) )
88 3 4 zaddcld ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℤ )
89 27 39 zaddcld ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ∈ ℤ )
90 moddvds ⊢ ( ( ( 2 ↑ 𝑁 ) ∈ ℕ ∧ ( 𝐴 + 𝐵 ) ∈ ℤ ∧ ( ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ∈ ℤ ) → ( ( ( 𝐴 + 𝐵 ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) ↔ ( 2 ↑ 𝑁 ) ∥ ( ( 𝐴 + 𝐵 ) − ( ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ) ) )
91 8 88 89 90 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) ↔ ( 2 ↑ 𝑁 ) ∥ ( ( 𝐴 + 𝐵 ) − ( ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ) ) )
92 87 91 mpbird ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) )
93 11 a1i ⊢ ( 𝜑 → ( bits ‘ 𝐴 ) ⊆ ℕ0 )
94 30 a1i ⊢ ( 𝜑 → ( bits ‘ 𝐵 ) ⊆ ℕ0 )
95 93 94 1 5 2 sadadd3 ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( 𝐾 ‘ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( ( bits ‘ 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) )
96 inss1 ⊢ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) )
97 sadcl ⊢ ( ( ( bits ‘ 𝐴 ) ⊆ ℕ0 ∧ ( bits ‘ 𝐵 ) ⊆ ℕ0 ) → ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ⊆ ℕ0 )
98 11 30 97 mp2an ⊢ ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ⊆ ℕ0
99 96 98 sstri ⊢ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0
100 inss2 ⊢ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
101 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
102 13 100 101 mp2an ⊢ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin
103 elfpw ⊢ ( ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
104 99 102 103 mpbir2an ⊢ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin )
105 24 ffvelrni ⊢ ( ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
106 104 105 mp1i ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
107 106 nn0red ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ )
108 106 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
109 2 fveq1i ⊢ ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) )
110 109 fveq2i ⊢ ( ( bits ↾ ℕ0 ) ‘ ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
111 106 fvresd ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( bits ‘ ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) )
112 104 a1i ⊢ ( 𝜑 → ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
113 f1ocnvfv2 ⊢ ( ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ) → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) )
114 19 112 113 sylancr ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) )
115 110 111 114 3eqtr3a ⊢ ( 𝜑 → ( bits ‘ ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) )
116 115 100 eqsstrdi ⊢ ( 𝜑 → ( bits ‘ ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) )
117 106 nn0zd ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ )
118 bitsfzo ⊢ ( ( ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) ↔ ( bits ‘ ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) ) )
119 117 5 118 syl2anc ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) ↔ ( bits ‘ ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) ) )
120 116 119 mpbird ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) )
121 elfzolt2 ⊢ ( ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) → ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) )
122 120 121 syl ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) )
123 modid ⊢ ( ( ( ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ∧ ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) ) ) → ( ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
124 107 54 108 122 123 syl22anc ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
125 92 95 124 3eqtr2d ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) mod ( 2 ↑ 𝑁 ) ) = ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) )
126 125 fveq2d ⊢ ( 𝜑 → ( bits ‘ ( ( 𝐴 + 𝐵 ) mod ( 2 ↑ 𝑁 ) ) ) = ( bits ‘ ( 𝐾 ‘ ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) ) ) )
127 126 115 eqtr2d ⊢ ( 𝜑 → ( ( ( bits ‘ 𝐴 ) sadd ( bits ‘ 𝐵 ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( bits ‘ ( ( 𝐴 + 𝐵 ) mod ( 2 ↑ 𝑁 ) ) ) )