| 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 |
|
oveq2 |
⊢ ( 𝑥 = 0 → ( 0 ..^ 𝑥 ) = ( 0 ..^ 0 ) ) |
| 7 |
|
fzo0 |
⊢ ( 0 ..^ 0 ) = ∅ |
| 8 |
6 7
|
eqtrdi |
⊢ ( 𝑥 = 0 → ( 0 ..^ 𝑥 ) = ∅ ) |
| 9 |
8
|
ineq2d |
⊢ ( 𝑥 = 0 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) = ( ( 𝐴 sadd 𝐵 ) ∩ ∅ ) ) |
| 10 |
|
in0 |
⊢ ( ( 𝐴 sadd 𝐵 ) ∩ ∅ ) = ∅ |
| 11 |
9 10
|
eqtrdi |
⊢ ( 𝑥 = 0 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) = ∅ ) |
| 12 |
11
|
fveq2d |
⊢ ( 𝑥 = 0 → ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) ) = ( 𝐾 ‘ ∅ ) ) |
| 13 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
| 14 |
|
fvres |
⊢ ( 0 ∈ ℕ0 → ( ( bits ↾ ℕ0 ) ‘ 0 ) = ( bits ‘ 0 ) ) |
| 15 |
13 14
|
ax-mp |
⊢ ( ( bits ↾ ℕ0 ) ‘ 0 ) = ( bits ‘ 0 ) |
| 16 |
|
0bits |
⊢ ( bits ‘ 0 ) = ∅ |
| 17 |
15 16
|
eqtr2i |
⊢ ∅ = ( ( bits ↾ ℕ0 ) ‘ 0 ) |
| 18 |
5 17
|
fveq12i |
⊢ ( 𝐾 ‘ ∅ ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( bits ↾ ℕ0 ) ‘ 0 ) ) |
| 19 |
|
bitsf1o |
⊢ ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) |
| 20 |
|
f1ocnvfv1 |
⊢ ( ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ 0 ∈ ℕ0 ) → ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( bits ↾ ℕ0 ) ‘ 0 ) ) = 0 ) |
| 21 |
19 13 20
|
mp2an |
⊢ ( ◡ ( bits ↾ ℕ0 ) ‘ ( ( bits ↾ ℕ0 ) ‘ 0 ) ) = 0 |
| 22 |
18 21
|
eqtri |
⊢ ( 𝐾 ‘ ∅ ) = 0 |
| 23 |
12 22
|
eqtrdi |
⊢ ( 𝑥 = 0 → ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) ) = 0 ) |
| 24 |
|
fveq2 |
⊢ ( 𝑥 = 0 → ( 𝐶 ‘ 𝑥 ) = ( 𝐶 ‘ 0 ) ) |
| 25 |
24
|
eleq2d |
⊢ ( 𝑥 = 0 → ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) ↔ ∅ ∈ ( 𝐶 ‘ 0 ) ) ) |
| 26 |
|
oveq2 |
⊢ ( 𝑥 = 0 → ( 2 ↑ 𝑥 ) = ( 2 ↑ 0 ) ) |
| 27 |
25 26
|
ifbieq1d |
⊢ ( 𝑥 = 0 → if ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) , ( 2 ↑ 𝑥 ) , 0 ) = if ( ∅ ∈ ( 𝐶 ‘ 0 ) , ( 2 ↑ 0 ) , 0 ) ) |
| 28 |
23 27
|
oveq12d |
⊢ ( 𝑥 = 0 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) , ( 2 ↑ 𝑥 ) , 0 ) ) = ( 0 + if ( ∅ ∈ ( 𝐶 ‘ 0 ) , ( 2 ↑ 0 ) , 0 ) ) ) |
| 29 |
8
|
ineq2d |
⊢ ( 𝑥 = 0 → ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) = ( 𝐴 ∩ ∅ ) ) |
| 30 |
|
in0 |
⊢ ( 𝐴 ∩ ∅ ) = ∅ |
| 31 |
29 30
|
eqtrdi |
⊢ ( 𝑥 = 0 → ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) = ∅ ) |
| 32 |
31
|
fveq2d |
⊢ ( 𝑥 = 0 → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) = ( 𝐾 ‘ ∅ ) ) |
| 33 |
32 22
|
eqtrdi |
⊢ ( 𝑥 = 0 → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) = 0 ) |
| 34 |
8
|
ineq2d |
⊢ ( 𝑥 = 0 → ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) = ( 𝐵 ∩ ∅ ) ) |
| 35 |
|
in0 |
⊢ ( 𝐵 ∩ ∅ ) = ∅ |
| 36 |
34 35
|
eqtrdi |
⊢ ( 𝑥 = 0 → ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) = ∅ ) |
| 37 |
36
|
fveq2d |
⊢ ( 𝑥 = 0 → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) = ( 𝐾 ‘ ∅ ) ) |
| 38 |
37 22
|
eqtrdi |
⊢ ( 𝑥 = 0 → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) = 0 ) |
| 39 |
33 38
|
oveq12d |
⊢ ( 𝑥 = 0 → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) ) = ( 0 + 0 ) ) |
| 40 |
|
00id |
⊢ ( 0 + 0 ) = 0 |
| 41 |
39 40
|
eqtrdi |
⊢ ( 𝑥 = 0 → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) ) = 0 ) |
| 42 |
28 41
|
eqeq12d |
⊢ ( 𝑥 = 0 → ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) , ( 2 ↑ 𝑥 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) ) ↔ ( 0 + if ( ∅ ∈ ( 𝐶 ‘ 0 ) , ( 2 ↑ 0 ) , 0 ) ) = 0 ) ) |
| 43 |
42
|
imbi2d |
⊢ ( 𝑥 = 0 → ( ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) , ( 2 ↑ 𝑥 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) ) ) ↔ ( 𝜑 → ( 0 + if ( ∅ ∈ ( 𝐶 ‘ 0 ) , ( 2 ↑ 0 ) , 0 ) ) = 0 ) ) ) |
| 44 |
|
oveq2 |
⊢ ( 𝑥 = 𝑘 → ( 0 ..^ 𝑥 ) = ( 0 ..^ 𝑘 ) ) |
| 45 |
44
|
ineq2d |
⊢ ( 𝑥 = 𝑘 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) = ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑘 ) ) ) |
| 46 |
45
|
fveq2d |
⊢ ( 𝑥 = 𝑘 → ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) ) = ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑘 ) ) ) ) |
| 47 |
|
fveq2 |
⊢ ( 𝑥 = 𝑘 → ( 𝐶 ‘ 𝑥 ) = ( 𝐶 ‘ 𝑘 ) ) |
| 48 |
47
|
eleq2d |
⊢ ( 𝑥 = 𝑘 → ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) ↔ ∅ ∈ ( 𝐶 ‘ 𝑘 ) ) ) |
| 49 |
|
oveq2 |
⊢ ( 𝑥 = 𝑘 → ( 2 ↑ 𝑥 ) = ( 2 ↑ 𝑘 ) ) |
| 50 |
48 49
|
ifbieq1d |
⊢ ( 𝑥 = 𝑘 → if ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) , ( 2 ↑ 𝑥 ) , 0 ) = if ( ∅ ∈ ( 𝐶 ‘ 𝑘 ) , ( 2 ↑ 𝑘 ) , 0 ) ) |
| 51 |
46 50
|
oveq12d |
⊢ ( 𝑥 = 𝑘 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) , ( 2 ↑ 𝑥 ) , 0 ) ) = ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑘 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑘 ) , ( 2 ↑ 𝑘 ) , 0 ) ) ) |
| 52 |
44
|
ineq2d |
⊢ ( 𝑥 = 𝑘 → ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) = ( 𝐴 ∩ ( 0 ..^ 𝑘 ) ) ) |
| 53 |
52
|
fveq2d |
⊢ ( 𝑥 = 𝑘 → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) = ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑘 ) ) ) ) |
| 54 |
44
|
ineq2d |
⊢ ( 𝑥 = 𝑘 → ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) = ( 𝐵 ∩ ( 0 ..^ 𝑘 ) ) ) |
| 55 |
54
|
fveq2d |
⊢ ( 𝑥 = 𝑘 → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) = ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑘 ) ) ) ) |
| 56 |
53 55
|
oveq12d |
⊢ ( 𝑥 = 𝑘 → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑘 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑘 ) ) ) ) ) |
| 57 |
51 56
|
eqeq12d |
⊢ ( 𝑥 = 𝑘 → ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) , ( 2 ↑ 𝑥 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) ) ↔ ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑘 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑘 ) , ( 2 ↑ 𝑘 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑘 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑘 ) ) ) ) ) ) |
| 58 |
57
|
imbi2d |
⊢ ( 𝑥 = 𝑘 → ( ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) , ( 2 ↑ 𝑥 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) ) ) ↔ ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑘 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑘 ) , ( 2 ↑ 𝑘 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑘 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑘 ) ) ) ) ) ) ) |
| 59 |
|
oveq2 |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 0 ..^ 𝑥 ) = ( 0 ..^ ( 𝑘 + 1 ) ) ) |
| 60 |
59
|
ineq2d |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) = ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) |
| 61 |
60
|
fveq2d |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) ) = ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) ) |
| 62 |
|
fveq2 |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝐶 ‘ 𝑥 ) = ( 𝐶 ‘ ( 𝑘 + 1 ) ) ) |
| 63 |
62
|
eleq2d |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) ↔ ∅ ∈ ( 𝐶 ‘ ( 𝑘 + 1 ) ) ) ) |
| 64 |
|
oveq2 |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 2 ↑ 𝑥 ) = ( 2 ↑ ( 𝑘 + 1 ) ) ) |
| 65 |
63 64
|
ifbieq1d |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → if ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) , ( 2 ↑ 𝑥 ) , 0 ) = if ( ∅ ∈ ( 𝐶 ‘ ( 𝑘 + 1 ) ) , ( 2 ↑ ( 𝑘 + 1 ) ) , 0 ) ) |
| 66 |
61 65
|
oveq12d |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) , ( 2 ↑ 𝑥 ) , 0 ) ) = ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑘 + 1 ) ) , ( 2 ↑ ( 𝑘 + 1 ) ) , 0 ) ) ) |
| 67 |
59
|
ineq2d |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) = ( 𝐴 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) |
| 68 |
67
|
fveq2d |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) = ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) ) |
| 69 |
59
|
ineq2d |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) = ( 𝐵 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) |
| 70 |
69
|
fveq2d |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) = ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) ) |
| 71 |
68 70
|
oveq12d |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) ) ) |
| 72 |
66 71
|
eqeq12d |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) , ( 2 ↑ 𝑥 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) ) ↔ ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑘 + 1 ) ) , ( 2 ↑ ( 𝑘 + 1 ) ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) ) ) ) |
| 73 |
72
|
imbi2d |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) , ( 2 ↑ 𝑥 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) ) ) ↔ ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑘 + 1 ) ) , ( 2 ↑ ( 𝑘 + 1 ) ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) ) ) ) ) |
| 74 |
|
oveq2 |
⊢ ( 𝑥 = 𝑁 → ( 0 ..^ 𝑥 ) = ( 0 ..^ 𝑁 ) ) |
| 75 |
74
|
ineq2d |
⊢ ( 𝑥 = 𝑁 → ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) = ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) |
| 76 |
75
|
fveq2d |
⊢ ( 𝑥 = 𝑁 → ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) ) = ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) ) |
| 77 |
|
fveq2 |
⊢ ( 𝑥 = 𝑁 → ( 𝐶 ‘ 𝑥 ) = ( 𝐶 ‘ 𝑁 ) ) |
| 78 |
77
|
eleq2d |
⊢ ( 𝑥 = 𝑁 → ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) ↔ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ) |
| 79 |
|
oveq2 |
⊢ ( 𝑥 = 𝑁 → ( 2 ↑ 𝑥 ) = ( 2 ↑ 𝑁 ) ) |
| 80 |
78 79
|
ifbieq1d |
⊢ ( 𝑥 = 𝑁 → if ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) , ( 2 ↑ 𝑥 ) , 0 ) = if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) |
| 81 |
76 80
|
oveq12d |
⊢ ( 𝑥 = 𝑁 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) , ( 2 ↑ 𝑥 ) , 0 ) ) = ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) ) |
| 82 |
74
|
ineq2d |
⊢ ( 𝑥 = 𝑁 → ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) = ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) |
| 83 |
82
|
fveq2d |
⊢ ( 𝑥 = 𝑁 → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) = ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ) |
| 84 |
74
|
ineq2d |
⊢ ( 𝑥 = 𝑁 → ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) = ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) |
| 85 |
84
|
fveq2d |
⊢ ( 𝑥 = 𝑁 → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) = ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) |
| 86 |
83 85
|
oveq12d |
⊢ ( 𝑥 = 𝑁 → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ) |
| 87 |
81 86
|
eqeq12d |
⊢ ( 𝑥 = 𝑁 → ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) , ( 2 ↑ 𝑥 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) ) ↔ ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ) ) |
| 88 |
87
|
imbi2d |
⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑥 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑥 ) , ( 2 ↑ 𝑥 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑥 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑥 ) ) ) ) ) ↔ ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ) ) ) |
| 89 |
1 2 3
|
sadc0 |
⊢ ( 𝜑 → ¬ ∅ ∈ ( 𝐶 ‘ 0 ) ) |
| 90 |
89
|
iffalsed |
⊢ ( 𝜑 → if ( ∅ ∈ ( 𝐶 ‘ 0 ) , ( 2 ↑ 0 ) , 0 ) = 0 ) |
| 91 |
90
|
oveq2d |
⊢ ( 𝜑 → ( 0 + if ( ∅ ∈ ( 𝐶 ‘ 0 ) , ( 2 ↑ 0 ) , 0 ) ) = ( 0 + 0 ) ) |
| 92 |
91 40
|
eqtrdi |
⊢ ( 𝜑 → ( 0 + if ( ∅ ∈ ( 𝐶 ‘ 0 ) , ( 2 ↑ 0 ) , 0 ) ) = 0 ) |
| 93 |
1
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑘 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑘 ) , ( 2 ↑ 𝑘 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑘 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑘 ) ) ) ) ) → 𝐴 ⊆ ℕ0 ) |
| 94 |
2
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑘 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑘 ) , ( 2 ↑ 𝑘 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑘 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑘 ) ) ) ) ) → 𝐵 ⊆ ℕ0 ) |
| 95 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑘 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑘 ) , ( 2 ↑ 𝑘 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑘 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑘 ) ) ) ) ) → 𝑘 ∈ ℕ0 ) |
| 96 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑘 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑘 ) , ( 2 ↑ 𝑘 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑘 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑘 ) ) ) ) ) → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑘 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑘 ) , ( 2 ↑ 𝑘 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑘 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑘 ) ) ) ) ) |
| 97 |
93 94 3 95 5 96
|
sadadd2lem |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑘 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑘 ) , ( 2 ↑ 𝑘 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑘 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑘 ) ) ) ) ) → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑘 + 1 ) ) , ( 2 ↑ ( 𝑘 + 1 ) ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) ) ) |
| 98 |
97
|
ex |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑘 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑘 ) , ( 2 ↑ 𝑘 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑘 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑘 ) ) ) ) → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑘 + 1 ) ) , ( 2 ↑ ( 𝑘 + 1 ) ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) ) ) ) |
| 99 |
98
|
expcom |
⊢ ( 𝑘 ∈ ℕ0 → ( 𝜑 → ( ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑘 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑘 ) , ( 2 ↑ 𝑘 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑘 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑘 ) ) ) ) → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑘 + 1 ) ) , ( 2 ↑ ( 𝑘 + 1 ) ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) ) ) ) ) |
| 100 |
99
|
a2d |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑘 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑘 ) , ( 2 ↑ 𝑘 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑘 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑘 ) ) ) ) ) → ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ ( 𝑘 + 1 ) ) , ( 2 ↑ ( 𝑘 + 1 ) ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) ) ) ) ) |
| 101 |
43 58 73 88 92 100
|
nn0ind |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ) ) |
| 102 |
4 101
|
mpcom |
⊢ ( 𝜑 → ( ( 𝐾 ‘ ( ( 𝐴 sadd 𝐵 ) ∩ ( 0 ..^ 𝑁 ) ) ) + if ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) , ( 2 ↑ 𝑁 ) , 0 ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ) |