Metamath Proof Explorer

Theorem sadadd3

Description: Sum of initial segments of the sadd sequence. (Contributed by Mario Carneiro, 9-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 )
sadcadd.k ⊢ 𝐾 = ◡ ( bits ↾ ℕ0 )
Assertion sadadd3 ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) )

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 sadcadd.k ⊢ 𝐾 = ◡ ( bits ↾ ℕ0 )
6 2nn ⊢ 2 ∈ ℕ
7 6 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
8 7 4 nnexpcld ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℕ )
9 8 nnzd ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℤ )
10 iddvds ⊢ ( ( 2 ↑ 𝑁 ) ∈ ℤ → ( 2 ↑ 𝑁 ) ∥ ( 2 ↑ 𝑁 ) )
11 9 10 syl ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∥ ( 2 ↑ 𝑁 ) )
12 dvds0 ⊢ ( ( 2 ↑ 𝑁 ) ∈ ℤ → ( 2 ↑ 𝑁 ) ∥ 0 )
13 9 12 syl ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∥ 0 )
14 breq2 ⊢ ( ( 2 ↑ 𝑁 ) = if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) → ( ( 2 ↑ 𝑁 ) ∥ ( 2 ↑ 𝑁 ) ↔ ( 2 ↑ 𝑁 ) ∥ if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) )
15 breq2 ⊢ ( 0 = if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) → ( ( 2 ↑ 𝑁 ) ∥ 0 ↔ ( 2 ↑ 𝑁 ) ∥ if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) )
16 14 15 ifboth ⊢ ( ( ( 2 ↑ 𝑁 ) ∥ ( 2 ↑ 𝑁 ) ∧ ( 2 ↑ 𝑁 ) ∥ 0 ) → ( 2 ↑ 𝑁 ) ∥ if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) )
17 11 13 16 syl2anc ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∥ if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) )
18 inss1 ⊢ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 𝐴 sadd 𝐵 )
19 1 2 3 sadfval ⊢ ( 𝜑 → ( 𝐴 sadd 𝐵 ) = { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑘 ) ) } )
20 ssrab2 ⊢ { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑘 ) ) } ⊆ ℕ0
21 19 20 eqsstrdi ⊢ ( 𝜑 → ( 𝐴 sadd 𝐵 ) ⊆ ℕ0 )
22 18 21 sstrid ⊢ ( 𝜑 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
23 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
24 23 a1i ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ∈ Fin )
25 inss2 ⊢ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
26 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
27 24 25 26 sylancl ⊢ ( 𝜑 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
28 elfpw ⊢ ( ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
29 22 27 28 sylanbrc ⊢ ( 𝜑 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
30 bitsf1o ⊢ ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin )
31 f1ocnv ⊢ ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) → ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 )
32 f1of ⊢ ( ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 → ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0 )
33 30 31 32 mp2b ⊢ ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0
34 5 feq1i ⊢ ( 𝐾 : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0 ↔ ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0 )
35 33 34 mpbir ⊢ 𝐾 : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0
36 35 ffvelrni ⊢ ( ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
37 29 36 syl ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
38 37 nn0cnd ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℂ )
39 8 nncnd ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℂ )
40 0cn ⊢ 0 ∈ ℂ
41 ifcl ⊢ ( ( ( 2 ↑ 𝑁 ) ∈ ℂ ∧ 0 ∈ ℂ ) → if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℂ )
42 39 40 41 sylancl ⊢ ( 𝜑 → if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℂ )
43 38 42 pncan2d ⊢ ( 𝜑 → ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) − ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) = if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) )
44 17 43 breqtrrd ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∥ ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) − ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) )
45 37 nn0zd ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ )
46 9 adantr ⊢ ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 2 ↑ 𝑁 ) ∈ ℤ )
47 0zd ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → 0 ∈ ℤ )
48 46 47 ifclda ⊢ ( 𝜑 → if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℤ )
49 45 48 zaddcld ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) ∈ ℤ )
50 moddvds ⊢ ( ( ( 2 ↑ 𝑁 ) ∈ ℕ ∧ ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) ∈ ℤ ∧ ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ ) → ( ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) ↔ ( 2 ↑ 𝑁 ) ∥ ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) − ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ) )
51 8 49 45 50 syl3anc ⊢ ( 𝜑 → ( ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) ↔ ( 2 ↑ 𝑁 ) ∥ ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) − ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) ) )
52 44 51 mpbird ⊢ ( 𝜑 → ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) )
53 1 2 3 4 5 sadadd2 ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) )
54 53 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) )
55 52 54 eqtr3d ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) mod ( 2 ↑ 𝑁 ) ) )