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

Theorem sadaddlem 15652
Description: Lemma for sadadd 15653. (Contributed by Mario Carneiro, 9-Sep-2016.)
Hypotheses
Ref Expression
sadaddlem.c 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ (bits‘𝐴), 𝑚 ∈ (bits‘𝐵), ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
sadaddlem.k 𝐾 = (bits ↾ ℕ0)
sadaddlem.1 (𝜑𝐴 ∈ ℤ)
sadaddlem.2 (𝜑𝐵 ∈ ℤ)
sadaddlem.3 (𝜑𝑁 ∈ ℕ0)
Assertion
Ref Expression
sadaddlem (𝜑 → (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) = (bits‘((𝐴 + 𝐵) mod (2↑𝑁))))
Distinct variable groups:   𝑚,𝑐,𝑛   𝐴,𝑐,𝑚   𝐵,𝑐,𝑚   𝑛,𝑁
Allowed substitution hints:   𝜑(𝑚,𝑛,𝑐)   𝐴(𝑛)   𝐵(𝑛)   𝐶(𝑚,𝑛,𝑐)   𝐾(𝑚,𝑛,𝑐)   𝑁(𝑚,𝑐)

Proof of Theorem sadaddlem
StepHypRef Expression
1 sadaddlem.k . . . . . . . . . . . . 13 𝐾 = (bits ↾ ℕ0)
21fveq1i 6546 . . . . . . . . . . . 12 (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) = ((bits ↾ ℕ0)‘((bits‘𝐴) ∩ (0..^𝑁)))
3 sadaddlem.1 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℤ)
4 2nn 11564 . . . . . . . . . . . . . . . . . 18 2 ∈ ℕ
54a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ∈ ℕ)
6 sadaddlem.3 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℕ0)
75, 6nnexpcld 13460 . . . . . . . . . . . . . . . 16 (𝜑 → (2↑𝑁) ∈ ℕ)
83, 7zmodcld 13114 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 mod (2↑𝑁)) ∈ ℕ0)
98fvresd 6565 . . . . . . . . . . . . . 14 (𝜑 → ((bits ↾ ℕ0)‘(𝐴 mod (2↑𝑁))) = (bits‘(𝐴 mod (2↑𝑁))))
10 bitsmod 15622 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (bits‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁)))
113, 6, 10syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (bits‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁)))
129, 11eqtrd 2833 . . . . . . . . . . . . 13 (𝜑 → ((bits ↾ ℕ0)‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁)))
13 bitsf1o 15631 . . . . . . . . . . . . . 14 (bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin)
14 f1ocnvfv 6907 . . . . . . . . . . . . . 14 (((bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin) ∧ (𝐴 mod (2↑𝑁)) ∈ ℕ0) → (((bits ↾ ℕ0)‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁)) → ((bits ↾ ℕ0)‘((bits‘𝐴) ∩ (0..^𝑁))) = (𝐴 mod (2↑𝑁))))
1513, 8, 14sylancr 587 . . . . . . . . . . . . 13 (𝜑 → (((bits ↾ ℕ0)‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁)) → ((bits ↾ ℕ0)‘((bits‘𝐴) ∩ (0..^𝑁))) = (𝐴 mod (2↑𝑁))))
1612, 15mpd 15 . . . . . . . . . . . 12 (𝜑 → ((bits ↾ ℕ0)‘((bits‘𝐴) ∩ (0..^𝑁))) = (𝐴 mod (2↑𝑁)))
172, 16syl5eq 2845 . . . . . . . . . . 11 (𝜑 → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) = (𝐴 mod (2↑𝑁)))
1817oveq2d 7039 . . . . . . . . . 10 (𝜑 → (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) = (𝐴 − (𝐴 mod (2↑𝑁))))
1918oveq1d 7038 . . . . . . . . 9 (𝜑 → ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) / (2↑𝑁)) = ((𝐴 − (𝐴 mod (2↑𝑁))) / (2↑𝑁)))
203zred 11941 . . . . . . . . . 10 (𝜑𝐴 ∈ ℝ)
217nnrpd 12283 . . . . . . . . . 10 (𝜑 → (2↑𝑁) ∈ ℝ+)
22 moddifz 13105 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ (2↑𝑁) ∈ ℝ+) → ((𝐴 − (𝐴 mod (2↑𝑁))) / (2↑𝑁)) ∈ ℤ)
2320, 21, 22syl2anc 584 . . . . . . . . 9 (𝜑 → ((𝐴 − (𝐴 mod (2↑𝑁))) / (2↑𝑁)) ∈ ℤ)
2419, 23eqeltrd 2885 . . . . . . . 8 (𝜑 → ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ)
257nnzd 11940 . . . . . . . . 9 (𝜑 → (2↑𝑁) ∈ ℤ)
267nnne0d 11541 . . . . . . . . 9 (𝜑 → (2↑𝑁) ≠ 0)
27 inss1 4131 . . . . . . . . . . . . . 14 ((bits‘𝐴) ∩ (0..^𝑁)) ⊆ (bits‘𝐴)
28 bitsss 15612 . . . . . . . . . . . . . 14 (bits‘𝐴) ⊆ ℕ0
2927, 28sstri 3904 . . . . . . . . . . . . 13 ((bits‘𝐴) ∩ (0..^𝑁)) ⊆ ℕ0
30 fzofi 13196 . . . . . . . . . . . . . 14 (0..^𝑁) ∈ Fin
31 inss2 4132 . . . . . . . . . . . . . 14 ((bits‘𝐴) ∩ (0..^𝑁)) ⊆ (0..^𝑁)
32 ssfi 8591 . . . . . . . . . . . . . 14 (((0..^𝑁) ∈ Fin ∧ ((bits‘𝐴) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → ((bits‘𝐴) ∩ (0..^𝑁)) ∈ Fin)
3330, 31, 32mp2an 688 . . . . . . . . . . . . 13 ((bits‘𝐴) ∩ (0..^𝑁)) ∈ Fin
34 elfpw 8679 . . . . . . . . . . . . 13 (((bits‘𝐴) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) ↔ (((bits‘𝐴) ∩ (0..^𝑁)) ⊆ ℕ0 ∧ ((bits‘𝐴) ∩ (0..^𝑁)) ∈ Fin))
3529, 33, 34mpbir2an 707 . . . . . . . . . . . 12 ((bits‘𝐴) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin)
36 f1ocnv 6502 . . . . . . . . . . . . . . 15 ((bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin) → (bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0)
37 f1of 6490 . . . . . . . . . . . . . . 15 ((bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0(bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)⟶ℕ0)
3813, 36, 37mp2b 10 . . . . . . . . . . . . . 14 (bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)⟶ℕ0
391feq1i 6380 . . . . . . . . . . . . . 14 (𝐾:(𝒫 ℕ0 ∩ Fin)⟶ℕ0(bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)⟶ℕ0)
4038, 39mpbir 232 . . . . . . . . . . . . 13 𝐾:(𝒫 ℕ0 ∩ Fin)⟶ℕ0
4140ffvelrni 6722 . . . . . . . . . . . 12 (((bits‘𝐴) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) ∈ ℕ0)
4235, 41mp1i 13 . . . . . . . . . . 11 (𝜑 → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) ∈ ℕ0)
4342nn0zd 11939 . . . . . . . . . 10 (𝜑 → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) ∈ ℤ)
443, 43zsubcld 11946 . . . . . . . . 9 (𝜑 → (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ∈ ℤ)
45 dvdsval2 15447 . . . . . . . . 9 (((2↑𝑁) ∈ ℤ ∧ (2↑𝑁) ≠ 0 ∧ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ∈ ℤ) → ((2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ↔ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ))
4625, 26, 44, 45syl3anc 1364 . . . . . . . 8 (𝜑 → ((2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ↔ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ))
4724, 46mpbird 258 . . . . . . 7 (𝜑 → (2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))))
481fveq1i 6546 . . . . . . . . . . . 12 (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) = ((bits ↾ ℕ0)‘((bits‘𝐵) ∩ (0..^𝑁)))
49 sadaddlem.2 . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∈ ℤ)
5049, 7zmodcld 13114 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 mod (2↑𝑁)) ∈ ℕ0)
5150fvresd 6565 . . . . . . . . . . . . . 14 (𝜑 → ((bits ↾ ℕ0)‘(𝐵 mod (2↑𝑁))) = (bits‘(𝐵 mod (2↑𝑁))))
52 bitsmod 15622 . . . . . . . . . . . . . . 15 ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (bits‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁)))
5349, 6, 52syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (bits‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁)))
5451, 53eqtrd 2833 . . . . . . . . . . . . 13 (𝜑 → ((bits ↾ ℕ0)‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁)))
55 f1ocnvfv 6907 . . . . . . . . . . . . . 14 (((bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin) ∧ (𝐵 mod (2↑𝑁)) ∈ ℕ0) → (((bits ↾ ℕ0)‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁)) → ((bits ↾ ℕ0)‘((bits‘𝐵) ∩ (0..^𝑁))) = (𝐵 mod (2↑𝑁))))
5613, 50, 55sylancr 587 . . . . . . . . . . . . 13 (𝜑 → (((bits ↾ ℕ0)‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁)) → ((bits ↾ ℕ0)‘((bits‘𝐵) ∩ (0..^𝑁))) = (𝐵 mod (2↑𝑁))))
5754, 56mpd 15 . . . . . . . . . . . 12 (𝜑 → ((bits ↾ ℕ0)‘((bits‘𝐵) ∩ (0..^𝑁))) = (𝐵 mod (2↑𝑁)))
5848, 57syl5eq 2845 . . . . . . . . . . 11 (𝜑 → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) = (𝐵 mod (2↑𝑁)))
5958oveq2d 7039 . . . . . . . . . 10 (𝜑 → (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) = (𝐵 − (𝐵 mod (2↑𝑁))))
6059oveq1d 7038 . . . . . . . . 9 (𝜑 → ((𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) / (2↑𝑁)) = ((𝐵 − (𝐵 mod (2↑𝑁))) / (2↑𝑁)))
6149zred 11941 . . . . . . . . . 10 (𝜑𝐵 ∈ ℝ)
62 moddifz 13105 . . . . . . . . . 10 ((𝐵 ∈ ℝ ∧ (2↑𝑁) ∈ ℝ+) → ((𝐵 − (𝐵 mod (2↑𝑁))) / (2↑𝑁)) ∈ ℤ)
6361, 21, 62syl2anc 584 . . . . . . . . 9 (𝜑 → ((𝐵 − (𝐵 mod (2↑𝑁))) / (2↑𝑁)) ∈ ℤ)
6460, 63eqeltrd 2885 . . . . . . . 8 (𝜑 → ((𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ)
65 inss1 4131 . . . . . . . . . . . . . 14 ((bits‘𝐵) ∩ (0..^𝑁)) ⊆ (bits‘𝐵)
66 bitsss 15612 . . . . . . . . . . . . . 14 (bits‘𝐵) ⊆ ℕ0
6765, 66sstri 3904 . . . . . . . . . . . . 13 ((bits‘𝐵) ∩ (0..^𝑁)) ⊆ ℕ0
68 inss2 4132 . . . . . . . . . . . . . 14 ((bits‘𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁)
69 ssfi 8591 . . . . . . . . . . . . . 14 (((0..^𝑁) ∈ Fin ∧ ((bits‘𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → ((bits‘𝐵) ∩ (0..^𝑁)) ∈ Fin)
7030, 68, 69mp2an 688 . . . . . . . . . . . . 13 ((bits‘𝐵) ∩ (0..^𝑁)) ∈ Fin
71 elfpw 8679 . . . . . . . . . . . . 13 (((bits‘𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) ↔ (((bits‘𝐵) ∩ (0..^𝑁)) ⊆ ℕ0 ∧ ((bits‘𝐵) ∩ (0..^𝑁)) ∈ Fin))
7267, 70, 71mpbir2an 707 . . . . . . . . . . . 12 ((bits‘𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin)
7340ffvelrni 6722 . . . . . . . . . . . 12 (((bits‘𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) ∈ ℕ0)
7472, 73mp1i 13 . . . . . . . . . . 11 (𝜑 → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) ∈ ℕ0)
7574nn0zd 11939 . . . . . . . . . 10 (𝜑 → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) ∈ ℤ)
7649, 75zsubcld 11946 . . . . . . . . 9 (𝜑 → (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ)
77 dvdsval2 15447 . . . . . . . . 9 (((2↑𝑁) ∈ ℤ ∧ (2↑𝑁) ≠ 0 ∧ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ) → ((2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ↔ ((𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ))
7825, 26, 76, 77syl3anc 1364 . . . . . . . 8 (𝜑 → ((2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ↔ ((𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ))
7964, 78mpbird 258 . . . . . . 7 (𝜑 → (2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))))
80 dvds2add 15480 . . . . . . . 8 (((2↑𝑁) ∈ ℤ ∧ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ∈ ℤ ∧ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ) → (((2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ∧ (2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))) → (2↑𝑁) ∥ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) + (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))))))
8125, 44, 76, 80syl3anc 1364 . . . . . . 7 (𝜑 → (((2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ∧ (2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))) → (2↑𝑁) ∥ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) + (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))))))
8247, 79, 81mp2and 695 . . . . . 6 (𝜑 → (2↑𝑁) ∥ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) + (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))))
833zcnd 11942 . . . . . . 7 (𝜑𝐴 ∈ ℂ)
8449zcnd 11942 . . . . . . 7 (𝜑𝐵 ∈ ℂ)
8542nn0cnd 11811 . . . . . . 7 (𝜑 → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) ∈ ℂ)
8674nn0cnd 11811 . . . . . . 7 (𝜑 → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) ∈ ℂ)
8783, 84, 85, 86addsub4d 10898 . . . . . 6 (𝜑 → ((𝐴 + 𝐵) − ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))) = ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) + (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))))
8882, 87breqtrrd 4996 . . . . 5 (𝜑 → (2↑𝑁) ∥ ((𝐴 + 𝐵) − ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))))
893, 49zaddcld 11945 . . . . . 6 (𝜑 → (𝐴 + 𝐵) ∈ ℤ)
9043, 75zaddcld 11945 . . . . . 6 (𝜑 → ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ)
91 moddvds 15455 . . . . . 6 (((2↑𝑁) ∈ ℕ ∧ (𝐴 + 𝐵) ∈ ℤ ∧ ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ) → (((𝐴 + 𝐵) mod (2↑𝑁)) = (((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) mod (2↑𝑁)) ↔ (2↑𝑁) ∥ ((𝐴 + 𝐵) − ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))))))
927, 89, 90, 91syl3anc 1364 . . . . 5 (𝜑 → (((𝐴 + 𝐵) mod (2↑𝑁)) = (((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) mod (2↑𝑁)) ↔ (2↑𝑁) ∥ ((𝐴 + 𝐵) − ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))))))
9388, 92mpbird 258 . . . 4 (𝜑 → ((𝐴 + 𝐵) mod (2↑𝑁)) = (((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) mod (2↑𝑁)))
9428a1i 11 . . . . 5 (𝜑 → (bits‘𝐴) ⊆ ℕ0)
9566a1i 11 . . . . 5 (𝜑 → (bits‘𝐵) ⊆ ℕ0)
96 sadaddlem.c . . . . 5 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ (bits‘𝐴), 𝑚 ∈ (bits‘𝐵), ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
9794, 95, 96, 6, 1sadadd3 15647 . . . 4 (𝜑 → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) mod (2↑𝑁)) = (((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) mod (2↑𝑁)))
98 inss1 4131 . . . . . . . . 9 (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ⊆ ((bits‘𝐴) sadd (bits‘𝐵))
99 sadcl 15648 . . . . . . . . . 10 (((bits‘𝐴) ⊆ ℕ0 ∧ (bits‘𝐵) ⊆ ℕ0) → ((bits‘𝐴) sadd (bits‘𝐵)) ⊆ ℕ0)
10028, 66, 99mp2an 688 . . . . . . . . 9 ((bits‘𝐴) sadd (bits‘𝐵)) ⊆ ℕ0
10198, 100sstri 3904 . . . . . . . 8 (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ⊆ ℕ0
102 inss2 4132 . . . . . . . . 9 (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ⊆ (0..^𝑁)
103 ssfi 8591 . . . . . . . . 9 (((0..^𝑁) ∈ Fin ∧ (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ Fin)
10430, 102, 103mp2an 688 . . . . . . . 8 (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ Fin
105 elfpw 8679 . . . . . . . 8 ((((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) ↔ ((((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ⊆ ℕ0 ∧ (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ Fin))
106101, 104, 105mpbir2an 707 . . . . . . 7 (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin)
10740ffvelrni 6722 . . . . . . 7 ((((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℕ0)
108106, 107mp1i 13 . . . . . 6 (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℕ0)
109108nn0red 11810 . . . . 5 (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℝ)
110108nn0ge0d 11812 . . . . 5 (𝜑 → 0 ≤ (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))))
1111fveq1i 6546 . . . . . . . . . 10 (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) = ((bits ↾ ℕ0)‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))
112111fveq2i 6548 . . . . . . . . 9 ((bits ↾ ℕ0)‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))))
113108fvresd 6565 . . . . . . . . 9 (𝜑 → ((bits ↾ ℕ0)‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))))
114106a1i 11 . . . . . . . . . 10 (𝜑 → (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin))
115 f1ocnvfv2 6906 . . . . . . . . . 10 (((bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin) ∧ (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin)) → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))
11613, 114, 115sylancr 587 . . . . . . . . 9 (𝜑 → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))
117112, 113, 1163eqtr3a 2857 . . . . . . . 8 (𝜑 → (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))
118117, 102syl6eqss 3948 . . . . . . 7 (𝜑 → (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) ⊆ (0..^𝑁))
119108nn0zd 11939 . . . . . . . 8 (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℤ)
120 bitsfzo 15621 . . . . . . . 8 (((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
121119, 6, 120syl2anc 584 . . . . . . 7 (𝜑 → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
122118, 121mpbird 258 . . . . . 6 (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)))
123 elfzolt2 12901 . . . . . 6 ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) < (2↑𝑁))
124122, 123syl 17 . . . . 5 (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) < (2↑𝑁))
125 modid 13118 . . . . 5 ((((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℝ ∧ (2↑𝑁) ∈ ℝ+) ∧ (0 ≤ (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∧ (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) < (2↑𝑁))) → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) mod (2↑𝑁)) = (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))))
126109, 21, 110, 124, 125syl22anc 835 . . . 4 (𝜑 → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) mod (2↑𝑁)) = (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))))
12793, 97, 1263eqtr2d 2839 . . 3 (𝜑 → ((𝐴 + 𝐵) mod (2↑𝑁)) = (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))))
128127fveq2d 6549 . 2 (𝜑 → (bits‘((𝐴 + 𝐵) mod (2↑𝑁))) = (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))))
129128, 117eqtr2d 2834 1 (𝜑 → (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) = (bits‘((𝐴 + 𝐵) mod (2↑𝑁))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1525  caddwcad 1592  wcel 2083  wne 2986  cin 3864  wss 3865  c0 4217  ifcif 4387  𝒫 cpw 4459   class class class wbr 4968  cmpt 5047  ccnv 5449  cres 5452  wf 6228  1-1-ontowf1o 6231  cfv 6232  (class class class)co 7023  cmpo 7025  1oc1o 7953  2oc2o 7954  Fincfn 8364  cr 10389  0cc0 10390  1c1 10391   + caddc 10393   < clt 10528  cle 10529  cmin 10723   / cdiv 11151  cn 11492  2c2 11546  0cn0 11751  cz 11835  +crp 12243  ..^cfzo 12887   mod cmo 13091  seqcseq 13223  cexp 13283  cdvds 15444  bitscbits 15605   sadd csad 15606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-inf2 8957  ax-cnex 10446  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466  ax-pre-mulgt0 10467  ax-pre-sup 10468
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-xor 1497  df-tru 1528  df-fal 1538  df-had 1580  df-cad 1593  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-disj 4937  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-se 5410  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-isom 6241  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-om 7444  df-1st 7552  df-2nd 7553  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-2o 7961  df-oadd 7964  df-er 8146  df-map 8265  df-pm 8266  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-sup 8759  df-inf 8760  df-oi 8827  df-dju 9183  df-card 9221  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534  df-sub 10725  df-neg 10726  df-div 11152  df-nn 11493  df-2 11554  df-3 11555  df-n0 11752  df-xnn0 11822  df-z 11836  df-uz 12098  df-rp 12244  df-fz 12747  df-fzo 12888  df-fl 13016  df-mod 13092  df-seq 13224  df-exp 13284  df-hash 13545  df-cj 14296  df-re 14297  df-im 14298  df-sqrt 14432  df-abs 14433  df-clim 14683  df-sum 14881  df-dvds 15445  df-bits 15608  df-sad 15637
This theorem is referenced by:  sadadd  15653
  Copyright terms: Public domain W3C validator