Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sadeq Structured version   Visualization version   GIF version

 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.)
Hypotheses
Ref Expression
Assertion
Ref Expression
sadeq (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) = (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))

Dummy variables 𝑚 𝑐 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inass 3785 . . . . . . . 8 ((𝐴 ∩ (0..^𝑁)) ∩ (0..^𝑁)) = (𝐴 ∩ ((0..^𝑁) ∩ (0..^𝑁)))
2 inidm 3784 . . . . . . . . 9 ((0..^𝑁) ∩ (0..^𝑁)) = (0..^𝑁)
32ineq2i 3773 . . . . . . . 8 (𝐴 ∩ ((0..^𝑁) ∩ (0..^𝑁))) = (𝐴 ∩ (0..^𝑁))
41, 3eqtri 2632 . . . . . . 7 ((𝐴 ∩ (0..^𝑁)) ∩ (0..^𝑁)) = (𝐴 ∩ (0..^𝑁))
54fveq2i 6106 . . . . . 6 ((bits ↾ ℕ0)‘((𝐴 ∩ (0..^𝑁)) ∩ (0..^𝑁))) = ((bits ↾ ℕ0)‘(𝐴 ∩ (0..^𝑁)))
6 inass 3785 . . . . . . . 8 ((𝐵 ∩ (0..^𝑁)) ∩ (0..^𝑁)) = (𝐵 ∩ ((0..^𝑁) ∩ (0..^𝑁)))
72ineq2i 3773 . . . . . . . 8 (𝐵 ∩ ((0..^𝑁) ∩ (0..^𝑁))) = (𝐵 ∩ (0..^𝑁))
86, 7eqtri 2632 . . . . . . 7 ((𝐵 ∩ (0..^𝑁)) ∩ (0..^𝑁)) = (𝐵 ∩ (0..^𝑁))
98fveq2i 6106 . . . . . 6 ((bits ↾ ℕ0)‘((𝐵 ∩ (0..^𝑁)) ∩ (0..^𝑁))) = ((bits ↾ ℕ0)‘(𝐵 ∩ (0..^𝑁)))
105, 9oveq12i 6561 . . . . 5 (((bits ↾ ℕ0)‘((𝐴 ∩ (0..^𝑁)) ∩ (0..^𝑁))) + ((bits ↾ ℕ0)‘((𝐵 ∩ (0..^𝑁)) ∩ (0..^𝑁)))) = (((bits ↾ ℕ0)‘(𝐴 ∩ (0..^𝑁))) + ((bits ↾ ℕ0)‘(𝐵 ∩ (0..^𝑁))))
1110oveq1i 6559 . . . 4 ((((bits ↾ ℕ0)‘((𝐴 ∩ (0..^𝑁)) ∩ (0..^𝑁))) + ((bits ↾ ℕ0)‘((𝐵 ∩ (0..^𝑁)) ∩ (0..^𝑁)))) mod (2↑𝑁)) = ((((bits ↾ ℕ0)‘(𝐴 ∩ (0..^𝑁))) + ((bits ↾ ℕ0)‘(𝐵 ∩ (0..^𝑁)))) mod (2↑𝑁))
12 inss1 3795 . . . . . 6 (𝐴 ∩ (0..^𝑁)) ⊆ 𝐴
13 sadeq.a . . . . . 6 (𝜑𝐴 ⊆ ℕ0)
1412, 13syl5ss 3579 . . . . 5 (𝜑 → (𝐴 ∩ (0..^𝑁)) ⊆ ℕ0)
15 inss1 3795 . . . . . 6 (𝐵 ∩ (0..^𝑁)) ⊆ 𝐵
16 sadeq.b . . . . . 6 (𝜑𝐵 ⊆ ℕ0)
1715, 16syl5ss 3579 . . . . 5 (𝜑 → (𝐵 ∩ (0..^𝑁)) ⊆ ℕ0)
18 eqid 2610 . . . . 5 seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ (𝐴 ∩ (0..^𝑁)), 𝑚 ∈ (𝐵 ∩ (0..^𝑁)), ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ (𝐴 ∩ (0..^𝑁)), 𝑚 ∈ (𝐵 ∩ (0..^𝑁)), ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
19 sadeq.n . . . . 5 (𝜑𝑁 ∈ ℕ0)
20 eqid 2610 . . . . 5 (bits ↾ ℕ0) = (bits ↾ ℕ0)
2114, 17, 18, 19, 20sadadd3 15021 . . . 4 (𝜑 → (((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) mod (2↑𝑁)) = ((((bits ↾ ℕ0)‘((𝐴 ∩ (0..^𝑁)) ∩ (0..^𝑁))) + ((bits ↾ ℕ0)‘((𝐵 ∩ (0..^𝑁)) ∩ (0..^𝑁)))) mod (2↑𝑁)))
22 eqid 2610 . . . . 5 seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
2313, 16, 22, 19, 20sadadd3 15021 . . . 4 (𝜑 → (((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)) = ((((bits ↾ ℕ0)‘(𝐴 ∩ (0..^𝑁))) + ((bits ↾ ℕ0)‘(𝐵 ∩ (0..^𝑁)))) mod (2↑𝑁)))
2411, 21, 233eqtr4a 2670 . . 3 (𝜑 → (((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) mod (2↑𝑁)) = (((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)))
25 inss1 3795 . . . . . . . 8 (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ⊆ ((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁)))
26 sadcl 15022 . . . . . . . . 9 (((𝐴 ∩ (0..^𝑁)) ⊆ ℕ0 ∧ (𝐵 ∩ (0..^𝑁)) ⊆ ℕ0) → ((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ⊆ ℕ0)
2714, 17, 26syl2anc 691 . . . . . . . 8 (𝜑 → ((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ⊆ ℕ0)
2825, 27syl5ss 3579 . . . . . . 7 (𝜑 → (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ⊆ ℕ0)
29 fzofi 12635 . . . . . . . . 9 (0..^𝑁) ∈ Fin
3029a1i 11 . . . . . . . 8 (𝜑 → (0..^𝑁) ∈ Fin)
31 inss2 3796 . . . . . . . 8 (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ⊆ (0..^𝑁)
32 ssfi 8065 . . . . . . . 8 (((0..^𝑁) ∈ Fin ∧ (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ∈ Fin)
3330, 31, 32sylancl 693 . . . . . . 7 (𝜑 → (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ∈ Fin)
34 elfpw 8151 . . . . . . 7 ((((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) ↔ ((((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ⊆ ℕ0 ∧ (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ∈ Fin))
3528, 33, 34sylanbrc 695 . . . . . 6 (𝜑 → (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin))
36 bitsf1o 15005 . . . . . . . 8 (bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin)
37 f1ocnv 6062 . . . . . . . 8 ((bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin) → (bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0)
38 f1of 6050 . . . . . . . 8 ((bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0(bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)⟶ℕ0)
3936, 37, 38mp2b 10 . . . . . . 7 (bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)⟶ℕ0
4039ffvelrni 6266 . . . . . 6 ((((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) → ((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ ℕ0)
4135, 40syl 17 . . . . 5 (𝜑 → ((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ ℕ0)
4241nn0red 11229 . . . 4 (𝜑 → ((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ ℝ)
43 2rp 11713 . . . . . 6 2 ∈ ℝ+
4443a1i 11 . . . . 5 (𝜑 → 2 ∈ ℝ+)
4519nn0zd 11356 . . . . 5 (𝜑𝑁 ∈ ℤ)
4644, 45rpexpcld 12894 . . . 4 (𝜑 → (2↑𝑁) ∈ ℝ+)
4741nn0ge0d 11231 . . . 4 (𝜑 → 0 ≤ ((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))))
48 fvres 6117 . . . . . . . . 9 (((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ ℕ0 → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) = (bits‘((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))))
4941, 48syl 17 . . . . . . . 8 (𝜑 → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) = (bits‘((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))))
50 f1ocnvfv2 6433 . . . . . . . . 9 (((bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin) ∧ (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin)) → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) = (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))
5136, 35, 50sylancr 694 . . . . . . . 8 (𝜑 → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) = (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))
5249, 51eqtr3d 2646 . . . . . . 7 (𝜑 → (bits‘((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) = (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))
5352, 31syl6eqss 3618 . . . . . 6 (𝜑 → (bits‘((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) ⊆ (0..^𝑁))
5441nn0zd 11356 . . . . . . 7 (𝜑 → ((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ ℤ)
55 bitsfzo 14995 . . . . . . 7 ((((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
5654, 19, 55syl2anc 691 . . . . . 6 (𝜑 → (((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
5753, 56mpbird 246 . . . . 5 (𝜑 → ((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)))
58 elfzolt2 12348 . . . . 5 (((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → ((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) < (2↑𝑁))
5957, 58syl 17 . . . 4 (𝜑 → ((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) < (2↑𝑁))
60 modid 12557 . . . 4 (((((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..^𝑁))))
6142, 46, 47, 59, 60syl22anc 1319 . . 3 (𝜑 → (((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) mod (2↑𝑁)) = ((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))))
62 inss1 3795 . . . . . . . 8 ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (𝐴 sadd 𝐵)
63 sadcl 15022 . . . . . . . . 9 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) ⊆ ℕ0)
6413, 16, 63syl2anc 691 . . . . . . . 8 (𝜑 → (𝐴 sadd 𝐵) ⊆ ℕ0)
6562, 64syl5ss 3579 . . . . . . 7 (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ ℕ0)
66 inss2 3796 . . . . . . . 8 ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁)
67 ssfi 8065 . . . . . . . 8 (((0..^𝑁) ∈ Fin ∧ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin)
6830, 66, 67sylancl 693 . . . . . . 7 (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin)
69 elfpw 8151 . . . . . . 7 (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) ↔ (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ ℕ0 ∧ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin))
7065, 68, 69sylanbrc 695 . . . . . 6 (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin))
7139ffvelrni 6266 . . . . . 6 (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) → ((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℕ0)
7270, 71syl 17 . . . . 5 (𝜑 → ((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℕ0)
7372nn0red 11229 . . . 4 (𝜑 → ((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℝ)
7472nn0ge0d 11231 . . . 4 (𝜑 → 0 ≤ ((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))))
75 fvres 6117 . . . . . . . . 9 (((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℕ0 → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) = (bits‘((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))))
7672, 75syl 17 . . . . . . . 8 (𝜑 → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) = (bits‘((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))))
77 f1ocnvfv2 6433 . . . . . . . . 9 (((bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin) ∧ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin)) → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) = ((𝐴 sadd 𝐵) ∩ (0..^𝑁)))
7836, 70, 77sylancr 694 . . . . . . . 8 (𝜑 → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) = ((𝐴 sadd 𝐵) ∩ (0..^𝑁)))
7976, 78eqtr3d 2646 . . . . . . 7 (𝜑 → (bits‘((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) = ((𝐴 sadd 𝐵) ∩ (0..^𝑁)))
8079, 66syl6eqss 3618 . . . . . 6 (𝜑 → (bits‘((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) ⊆ (0..^𝑁))
8172nn0zd 11356 . . . . . . 7 (𝜑 → ((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℤ)
82 bitsfzo 14995 . . . . . . 7 ((((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
8381, 19, 82syl2anc 691 . . . . . 6 (𝜑 → (((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
8480, 83mpbird 246 . . . . 5 (𝜑 → ((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)))
85 elfzolt2 12348 . . . . 5 (((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → ((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) < (2↑𝑁))
8684, 85syl 17 . . . 4 (𝜑 → ((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) < (2↑𝑁))
87 modid 12557 . . . 4 (((((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..^𝑁))))
8873, 46, 74, 86, 87syl22anc 1319 . . 3 (𝜑 → (((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)) = ((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))))
8924, 61, 883eqtr3rd 2653 . 2 (𝜑 → ((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) = ((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))))
90 f1of1 6049 . . . . 5 ((bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0(bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1→ℕ0)
9136, 37, 90mp2b 10 . . . 4 (bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1→ℕ0
92 f1fveq 6420 . . . 4 (((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..^𝑁))))
9391, 92mpan 702 . . 3 ((((𝐴 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..^𝑁))))
9470, 35, 93syl2anc 691 . 2 (𝜑 → (((bits ↾ ℕ0)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) = ((bits ↾ ℕ0)‘(((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) ↔ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) = (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))))
9589, 94mpbid 221 1 (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) = (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁)))