Metamath Proof Explorer

Theorem sadadd2lem

Description: Lemma for sadadd2 . (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 )
sadadd2lem.1 ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) )
Assertion sadadd2lem ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ) )

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 sadadd2lem.1 ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) )
7 inss1 ⊢ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 𝐴 sadd 𝐵 )
8 1 2 3 sadfval ⊢ ( 𝜑 → ( 𝐴 sadd 𝐵 ) = { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑘 ) ) } )
9 ssrab2 ⊢ { 𝑘 ∈ ℕ0 ∣ hadd ( 𝑘 ∈ 𝐴 , 𝑘 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑘 ) ) } ⊆ ℕ0
10 8 9 eqsstrdi ⊢ ( 𝜑 → ( 𝐴 sadd 𝐵 ) ⊆ ℕ0 )
11 7 10 sstrid ⊢ ( 𝜑 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
12 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
13 12 a1i ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ∈ Fin )
14 inss2 ⊢ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
15 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
16 13 14 15 sylancl ⊢ ( 𝜑 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
17 elfpw ⊢ ( ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
18 11 16 17 sylanbrc ⊢ ( 𝜑 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 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 5 feq1i ⊢ ( 𝐾 : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0 ↔ ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0 )
24 22 23 mpbir ⊢ 𝐾 : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0
25 24 ffvelcdmi ⊢ ( ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
26 18 25 syl ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
27 26 nn0cnd ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℂ )
28 2nn0 ⊢ 2 ∈ ℕ0
29 28 a1i ⊢ ( 𝜑 → 2 ∈ ℕ0 )
30 29 4 nn0expcld ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℕ0 )
31 0nn0 ⊢ 0 ∈ ℕ0
32 ifcl ⊢ ( ( ( 2 ↑ 𝑁 ) ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℕ0 )
33 30 31 32 sylancl ⊢ ( 𝜑 → if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℕ0 )
34 33 nn0cnd ⊢ ( 𝜑 → if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℂ )
35 1nn0 ⊢ 1 ∈ ℕ0
36 35 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
37 4 36 nn0addcld ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
38 29 37 nn0expcld ⊢ ( 𝜑 → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℕ0 )
39 ifcl ⊢ ( ( ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ∈ ℕ0 )
40 38 31 39 sylancl ⊢ ( 𝜑 → if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ∈ ℕ0 )
41 40 nn0cnd ⊢ ( 𝜑 → if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ∈ ℂ )
42 34 41 addcld ⊢ ( 𝜑 → ( if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ) ∈ ℂ )
43 27 42 addcld ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ) ) ∈ ℂ )
44 inss1 ⊢ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ 𝐴
45 44 1 sstrid ⊢ ( 𝜑 → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
46 inss2 ⊢ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
47 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
48 13 46 47 sylancl ⊢ ( 𝜑 → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
49 elfpw ⊢ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
50 45 48 49 sylanbrc ⊢ ( 𝜑 → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
51 24 ffvelcdmi ⊢ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
52 50 51 syl ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
53 52 nn0cnd ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℂ )
54 inss1 ⊢ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ 𝐵
55 54 2 sstrid ⊢ ( 𝜑 → ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
56 inss2 ⊢ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
57 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
58 13 56 57 sylancl ⊢ ( 𝜑 → ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
59 elfpw ⊢ ( ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
60 55 58 59 sylanbrc ⊢ ( 𝜑 → ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
61 24 ffvelcdmi ⊢ ( ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
62 60 61 syl ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
63 62 nn0cnd ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℂ )
64 53 63 addcld ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ∈ ℂ )
65 ifcl ⊢ ( ( ( 2 ↑ 𝑁 ) ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℕ0 )
66 30 31 65 sylancl ⊢ ( 𝜑 → if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℕ0 )
67 66 nn0cnd ⊢ ( 𝜑 → if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℂ )
68 ifcl ⊢ ( ( ( 2 ↑ 𝑁 ) ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℕ0 )
69 30 31 68 sylancl ⊢ ( 𝜑 → if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℕ0 )
70 69 nn0cnd ⊢ ( 𝜑 → if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℂ )
71 67 70 addcld ⊢ ( 𝜑 → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ∈ ℂ )
72 64 71 addcld ⊢ ( 𝜑 → ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) ∈ ℂ )
73 30 nn0cnd ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℂ )
74 73 adantr ⊢ ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 2 ↑ 𝑁 ) ∈ ℂ )
75 0cnd ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → 0 ∈ ℂ )
76 74 75 ifclda ⊢ ( 𝜑 → if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℂ )
77 1 2 3 4 sadval ⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) ↔ hadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ) )
78 77 ifbid ⊢ ( 𝜑 → if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) = if ( hadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , ( 2 ↑ 𝑁 ) , 0 ) )
79 1 2 3 4 sadcp1 ⊢ ( 𝜑 → ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) ↔ cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ) )
80 29 nn0cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
81 80 4 expp1d ⊢ ( 𝜑 → ( 2 ↑ ( 𝑁 + 1 ) ) = ( ( 2 ↑ 𝑁 ) · 2 ) )
82 73 80 mulcomd ⊢ ( 𝜑 → ( ( 2 ↑ 𝑁 ) · 2 ) = ( 2 · ( 2 ↑ 𝑁 ) ) )
83 81 82 eqtrd ⊢ ( 𝜑 → ( 2 ↑ ( 𝑁 + 1 ) ) = ( 2 · ( 2 ↑ 𝑁 ) ) )
84 79 83 ifbieq1d ⊢ ( 𝜑 → if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) = if ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , ( 2 · ( 2 ↑ 𝑁 ) ) , 0 ) )
85 78 84 oveq12d ⊢ ( 𝜑 → ( if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ) = ( if ( hadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , ( 2 ↑ 𝑁 ) , 0 ) + if ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , ( 2 · ( 2 ↑ 𝑁 ) ) , 0 ) ) )
86 sadadd2lem2 ⊢ ( ( 2 ↑ 𝑁 ) ∈ ℂ → ( if ( hadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , ( 2 ↑ 𝑁 ) , 0 ) + if ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , ( 2 · ( 2 ↑ 𝑁 ) ) , 0 ) ) = ( ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) )
87 73 86 syl ⊢ ( 𝜑 → ( if ( hadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , ( 2 ↑ 𝑁 ) , 0 ) + if ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) , ( 2 · ( 2 ↑ 𝑁 ) ) , 0 ) ) = ( ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) )
88 85 87 eqtrd ⊢ ( 𝜑 → ( if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ) = ( ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) )
89 6 88 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) + ( if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ) ) = ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) ) )
90 27 42 76 add32d ⊢ ( 𝜑 → ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) = ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) + ( if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ) ) )
91 64 71 76 addassd ⊢ ( 𝜑 → ( ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) = ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) ) )
92 89 90 91 3eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) = ( ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) )
93 43 72 76 92 addcan2ad ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ) ) = ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) )
94 27 34 41 addassd ⊢ ( 𝜑 → ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ) = ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + ( if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ) ) )
95 53 67 63 70 add4d ⊢ ( 𝜑 → ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ) + ( ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) = ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) )
96 93 94 95 3eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ) = ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ) + ( ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) )
97 5 bitsinvp1 ⊢ ( ( ( 𝐴 sadd 𝐵 ) ⊆ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) ) )
98 10 4 97 syl2anc ⊢ ( 𝜑 → ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) ) )
99 98 oveq1d ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ) = ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ ( 𝐴 sadd 𝐵 ) , ( 2 ↑ 𝑁 ) , 0 ) ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ) )
100 5 bitsinvp1 ⊢ ( ( 𝐴 ⊆ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ) )
101 1 4 100 syl2anc ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ) )
102 5 bitsinvp1 ⊢ ( ( 𝐵 ⊆ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) )
103 2 4 102 syl2anc ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) )
104 101 103 oveq12d ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ) = ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ) + ( ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) )
105 96 99 104 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) , ( 2 ↑ ( 𝑁 + 1 ) ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ) )