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

 Description: Sum of initial segments of the sadd sequence. (Contributed by Mario Carneiro, 9-Sep-2016.)
Hypotheses
Ref Expression
sadval.c 𝐶 = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
Assertion
Ref Expression
sadadd3 (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) mod (2↑𝑁)))
Distinct variable groups:   𝑚,𝑐,𝑛   𝐴,𝑐,𝑚   𝐵,𝑐,𝑚   𝑛,𝑁
Allowed substitution hints:   𝜑(𝑚,𝑛,𝑐)   𝐴(𝑛)   𝐵(𝑛)   𝐶(𝑚,𝑛,𝑐)   𝐾(𝑚,𝑛,𝑐)   𝑁(𝑚,𝑐)

Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 2nn 11130 . . . . . . . . 9 2 ∈ ℕ
21a1i 11 . . . . . . . 8 (𝜑 → 2 ∈ ℕ)
3 sadcp1.n . . . . . . . 8 (𝜑𝑁 ∈ ℕ0)
42, 3nnexpcld 12967 . . . . . . 7 (𝜑 → (2↑𝑁) ∈ ℕ)
54nnzd 11425 . . . . . 6 (𝜑 → (2↑𝑁) ∈ ℤ)
6 iddvds 14914 . . . . . 6 ((2↑𝑁) ∈ ℤ → (2↑𝑁) ∥ (2↑𝑁))
75, 6syl 17 . . . . 5 (𝜑 → (2↑𝑁) ∥ (2↑𝑁))
8 dvds0 14916 . . . . . 6 ((2↑𝑁) ∈ ℤ → (2↑𝑁) ∥ 0)
95, 8syl 17 . . . . 5 (𝜑 → (2↑𝑁) ∥ 0)
10 breq2 4622 . . . . . 6 ((2↑𝑁) = if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0) → ((2↑𝑁) ∥ (2↑𝑁) ↔ (2↑𝑁) ∥ if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0)))
11 breq2 4622 . . . . . 6 (0 = if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0) → ((2↑𝑁) ∥ 0 ↔ (2↑𝑁) ∥ if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0)))
1210, 11ifboth 4101 . . . . 5 (((2↑𝑁) ∥ (2↑𝑁) ∧ (2↑𝑁) ∥ 0) → (2↑𝑁) ∥ if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0))
137, 9, 12syl2anc 692 . . . 4 (𝜑 → (2↑𝑁) ∥ if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0))
14 inss1 3816 . . . . . . . . 9 ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (𝐴 sadd 𝐵)
15 sadval.a . . . . . . . . . . 11 (𝜑𝐴 ⊆ ℕ0)
16 sadval.b . . . . . . . . . . 11 (𝜑𝐵 ⊆ ℕ0)
17 sadval.c . . . . . . . . . . 11 𝐶 = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
1815, 16, 17sadfval 15093 . . . . . . . . . 10 (𝜑 → (𝐴 sadd 𝐵) = {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘))})
19 ssrab2 3671 . . . . . . . . . 10 {𝑘 ∈ ℕ0 ∣ hadd(𝑘𝐴, 𝑘𝐵, ∅ ∈ (𝐶𝑘))} ⊆ ℕ0
2018, 19syl6eqss 3639 . . . . . . . . 9 (𝜑 → (𝐴 sadd 𝐵) ⊆ ℕ0)
2114, 20syl5ss 3599 . . . . . . . 8 (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ ℕ0)
22 fzofi 12710 . . . . . . . . . 10 (0..^𝑁) ∈ Fin
2322a1i 11 . . . . . . . . 9 (𝜑 → (0..^𝑁) ∈ Fin)
24 inss2 3817 . . . . . . . . 9 ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁)
25 ssfi 8125 . . . . . . . . 9 (((0..^𝑁) ∈ Fin ∧ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin)
2623, 24, 25sylancl 693 . . . . . . . 8 (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin)
27 elfpw 8213 . . . . . . . 8 (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) ↔ (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ ℕ0 ∧ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin))
2821, 26, 27sylanbrc 697 . . . . . . 7 (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin))
29 bitsf1o 15086 . . . . . . . . . 10 (bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin)
30 f1ocnv 6108 . . . . . . . . . 10 ((bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin) → (bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0)
31 f1of 6096 . . . . . . . . . 10 ((bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0(bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)⟶ℕ0)
3229, 30, 31mp2b 10 . . . . . . . . 9 (bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)⟶ℕ0
33 sadcadd.k . . . . . . . . . 10 𝐾 = (bits ↾ ℕ0)
3433feq1i 5995 . . . . . . . . 9 (𝐾:(𝒫 ℕ0 ∩ Fin)⟶ℕ0(bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)⟶ℕ0)
3532, 34mpbir 221 . . . . . . . 8 𝐾:(𝒫 ℕ0 ∩ Fin)⟶ℕ0
3635ffvelrni 6315 . . . . . . 7 (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) → (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℕ0)
3728, 36syl 17 . . . . . 6 (𝜑 → (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℕ0)
3837nn0cnd 11298 . . . . 5 (𝜑 → (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℂ)
394nncnd 10981 . . . . . 6 (𝜑 → (2↑𝑁) ∈ ℂ)
40 0cn 9977 . . . . . 6 0 ∈ ℂ
41 ifcl 4107 . . . . . 6 (((2↑𝑁) ∈ ℂ ∧ 0 ∈ ℂ) → if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0) ∈ ℂ)
4239, 40, 41sylancl 693 . . . . 5 (𝜑 → if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0) ∈ ℂ)
4338, 42pncan2d 10339 . . . 4 (𝜑 → (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0)) − (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))) = if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0))
4413, 43breqtrrd 4646 . . 3 (𝜑 → (2↑𝑁) ∥ (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0)) − (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁)))))
4537nn0zd 11424 . . . . 5 (𝜑 → (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℤ)
465adantr 481 . . . . . 6 ((𝜑 ∧ ∅ ∈ (𝐶𝑁)) → (2↑𝑁) ∈ ℤ)
47 0zd 11334 . . . . . 6 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → 0 ∈ ℤ)
4846, 47ifclda 4097 . . . . 5 (𝜑 → if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0) ∈ ℤ)
4945, 48zaddcld 11430 . . . 4 (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0)) ∈ ℤ)
50 moddvds 14910 . . . 4 (((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..^𝑁))))))
514, 49, 45, 50syl3anc 1323 . . 3 (𝜑 → ((((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0)) mod (2↑𝑁)) = ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)) ↔ (2↑𝑁) ∥ (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0)) − (𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))))))
5244, 51mpbird 247 . 2 (𝜑 → (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0)) mod (2↑𝑁)) = ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)))
5315, 16, 17, 3, 33sadadd2 15101 . . 3 (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0)) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))
5453oveq1d 6620 . 2 (𝜑 → (((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶𝑁), (2↑𝑁), 0)) mod (2↑𝑁)) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) mod (2↑𝑁)))
5552, 54eqtr3d 2662 1 (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) mod (2↑𝑁)))