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

Theorem sadaddlem 16503
Description: Lemma for sadadd 16504. (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 2nn 12339 . . . . . . . . . 10 2 ∈ ℕ
21a1i 11 . . . . . . . . 9 (𝜑 → 2 ∈ ℕ)
3 sadaddlem.3 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ0)
42, 3nnexpcld 14284 . . . . . . . 8 (𝜑 → (2↑𝑁) ∈ ℕ)
54nnzd 12640 . . . . . . 7 (𝜑 → (2↑𝑁) ∈ ℤ)
6 sadaddlem.1 . . . . . . . 8 (𝜑𝐴 ∈ ℤ)
7 inss1 4237 . . . . . . . . . . . 12 ((bits‘𝐴) ∩ (0..^𝑁)) ⊆ (bits‘𝐴)
8 bitsss 16463 . . . . . . . . . . . 12 (bits‘𝐴) ⊆ ℕ0
97, 8sstri 3993 . . . . . . . . . . 11 ((bits‘𝐴) ∩ (0..^𝑁)) ⊆ ℕ0
10 fzofi 14015 . . . . . . . . . . . 12 (0..^𝑁) ∈ Fin
11 inss2 4238 . . . . . . . . . . . 12 ((bits‘𝐴) ∩ (0..^𝑁)) ⊆ (0..^𝑁)
12 ssfi 9213 . . . . . . . . . . . 12 (((0..^𝑁) ∈ Fin ∧ ((bits‘𝐴) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → ((bits‘𝐴) ∩ (0..^𝑁)) ∈ Fin)
1310, 11, 12mp2an 692 . . . . . . . . . . 11 ((bits‘𝐴) ∩ (0..^𝑁)) ∈ Fin
14 elfpw 9394 . . . . . . . . . . 11 (((bits‘𝐴) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) ↔ (((bits‘𝐴) ∩ (0..^𝑁)) ⊆ ℕ0 ∧ ((bits‘𝐴) ∩ (0..^𝑁)) ∈ Fin))
159, 13, 14mpbir2an 711 . . . . . . . . . 10 ((bits‘𝐴) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin)
16 bitsf1o 16482 . . . . . . . . . . . . 13 (bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin)
17 f1ocnv 6860 . . . . . . . . . . . . 13 ((bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin) → (bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0)
18 f1of 6848 . . . . . . . . . . . . 13 ((bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0(bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)⟶ℕ0)
1916, 17, 18mp2b 10 . . . . . . . . . . . 12 (bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)⟶ℕ0
20 sadaddlem.k . . . . . . . . . . . . 13 𝐾 = (bits ↾ ℕ0)
2120feq1i 6727 . . . . . . . . . . . 12 (𝐾:(𝒫 ℕ0 ∩ Fin)⟶ℕ0(bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)⟶ℕ0)
2219, 21mpbir 231 . . . . . . . . . . 11 𝐾:(𝒫 ℕ0 ∩ Fin)⟶ℕ0
2322ffvelcdmi 7103 . . . . . . . . . 10 (((bits‘𝐴) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) ∈ ℕ0)
2415, 23mp1i 13 . . . . . . . . 9 (𝜑 → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) ∈ ℕ0)
2524nn0zd 12639 . . . . . . . 8 (𝜑 → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) ∈ ℤ)
266, 25zsubcld 12727 . . . . . . 7 (𝜑 → (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ∈ ℤ)
27 sadaddlem.2 . . . . . . . 8 (𝜑𝐵 ∈ ℤ)
28 inss1 4237 . . . . . . . . . . . 12 ((bits‘𝐵) ∩ (0..^𝑁)) ⊆ (bits‘𝐵)
29 bitsss 16463 . . . . . . . . . . . 12 (bits‘𝐵) ⊆ ℕ0
3028, 29sstri 3993 . . . . . . . . . . 11 ((bits‘𝐵) ∩ (0..^𝑁)) ⊆ ℕ0
31 inss2 4238 . . . . . . . . . . . 12 ((bits‘𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁)
32 ssfi 9213 . . . . . . . . . . . 12 (((0..^𝑁) ∈ Fin ∧ ((bits‘𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → ((bits‘𝐵) ∩ (0..^𝑁)) ∈ Fin)
3310, 31, 32mp2an 692 . . . . . . . . . . 11 ((bits‘𝐵) ∩ (0..^𝑁)) ∈ Fin
34 elfpw 9394 . . . . . . . . . . 11 (((bits‘𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) ↔ (((bits‘𝐵) ∩ (0..^𝑁)) ⊆ ℕ0 ∧ ((bits‘𝐵) ∩ (0..^𝑁)) ∈ Fin))
3530, 33, 34mpbir2an 711 . . . . . . . . . 10 ((bits‘𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin)
3622ffvelcdmi 7103 . . . . . . . . . 10 (((bits‘𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) ∈ ℕ0)
3735, 36mp1i 13 . . . . . . . . 9 (𝜑 → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) ∈ ℕ0)
3837nn0zd 12639 . . . . . . . 8 (𝜑 → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) ∈ ℤ)
3927, 38zsubcld 12727 . . . . . . 7 (𝜑 → (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ)
4020fveq1i 6907 . . . . . . . . . . . 12 (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) = ((bits ↾ ℕ0)‘((bits‘𝐴) ∩ (0..^𝑁)))
416, 4zmodcld 13932 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 mod (2↑𝑁)) ∈ ℕ0)
4241fvresd 6926 . . . . . . . . . . . . . 14 (𝜑 → ((bits ↾ ℕ0)‘(𝐴 mod (2↑𝑁))) = (bits‘(𝐴 mod (2↑𝑁))))
43 bitsmod 16473 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (bits‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁)))
446, 3, 43syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (bits‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁)))
4542, 44eqtrd 2777 . . . . . . . . . . . . 13 (𝜑 → ((bits ↾ ℕ0)‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁)))
46 f1ocnvfv 7298 . . . . . . . . . . . . . 14 (((bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin) ∧ (𝐴 mod (2↑𝑁)) ∈ ℕ0) → (((bits ↾ ℕ0)‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁)) → ((bits ↾ ℕ0)‘((bits‘𝐴) ∩ (0..^𝑁))) = (𝐴 mod (2↑𝑁))))
4716, 41, 46sylancr 587 . . . . . . . . . . . . 13 (𝜑 → (((bits ↾ ℕ0)‘(𝐴 mod (2↑𝑁))) = ((bits‘𝐴) ∩ (0..^𝑁)) → ((bits ↾ ℕ0)‘((bits‘𝐴) ∩ (0..^𝑁))) = (𝐴 mod (2↑𝑁))))
4845, 47mpd 15 . . . . . . . . . . . 12 (𝜑 → ((bits ↾ ℕ0)‘((bits‘𝐴) ∩ (0..^𝑁))) = (𝐴 mod (2↑𝑁)))
4940, 48eqtrid 2789 . . . . . . . . . . 11 (𝜑 → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) = (𝐴 mod (2↑𝑁)))
5049oveq2d 7447 . . . . . . . . . 10 (𝜑 → (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) = (𝐴 − (𝐴 mod (2↑𝑁))))
5150oveq1d 7446 . . . . . . . . 9 (𝜑 → ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) / (2↑𝑁)) = ((𝐴 − (𝐴 mod (2↑𝑁))) / (2↑𝑁)))
526zred 12722 . . . . . . . . . 10 (𝜑𝐴 ∈ ℝ)
534nnrpd 13075 . . . . . . . . . 10 (𝜑 → (2↑𝑁) ∈ ℝ+)
54 moddifz 13923 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ (2↑𝑁) ∈ ℝ+) → ((𝐴 − (𝐴 mod (2↑𝑁))) / (2↑𝑁)) ∈ ℤ)
5552, 53, 54syl2anc 584 . . . . . . . . 9 (𝜑 → ((𝐴 − (𝐴 mod (2↑𝑁))) / (2↑𝑁)) ∈ ℤ)
5651, 55eqeltrd 2841 . . . . . . . 8 (𝜑 → ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ)
574nnne0d 12316 . . . . . . . . 9 (𝜑 → (2↑𝑁) ≠ 0)
58 dvdsval2 16293 . . . . . . . . 9 (((2↑𝑁) ∈ ℤ ∧ (2↑𝑁) ≠ 0 ∧ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ∈ ℤ) → ((2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ↔ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ))
595, 57, 26, 58syl3anc 1373 . . . . . . . 8 (𝜑 → ((2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) ↔ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ))
6056, 59mpbird 257 . . . . . . 7 (𝜑 → (2↑𝑁) ∥ (𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))))
6120fveq1i 6907 . . . . . . . . . . . 12 (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) = ((bits ↾ ℕ0)‘((bits‘𝐵) ∩ (0..^𝑁)))
6227, 4zmodcld 13932 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 mod (2↑𝑁)) ∈ ℕ0)
6362fvresd 6926 . . . . . . . . . . . . . 14 (𝜑 → ((bits ↾ ℕ0)‘(𝐵 mod (2↑𝑁))) = (bits‘(𝐵 mod (2↑𝑁))))
64 bitsmod 16473 . . . . . . . . . . . . . . 15 ((𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (bits‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁)))
6527, 3, 64syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (bits‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁)))
6663, 65eqtrd 2777 . . . . . . . . . . . . 13 (𝜑 → ((bits ↾ ℕ0)‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁)))
67 f1ocnvfv 7298 . . . . . . . . . . . . . 14 (((bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin) ∧ (𝐵 mod (2↑𝑁)) ∈ ℕ0) → (((bits ↾ ℕ0)‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁)) → ((bits ↾ ℕ0)‘((bits‘𝐵) ∩ (0..^𝑁))) = (𝐵 mod (2↑𝑁))))
6816, 62, 67sylancr 587 . . . . . . . . . . . . 13 (𝜑 → (((bits ↾ ℕ0)‘(𝐵 mod (2↑𝑁))) = ((bits‘𝐵) ∩ (0..^𝑁)) → ((bits ↾ ℕ0)‘((bits‘𝐵) ∩ (0..^𝑁))) = (𝐵 mod (2↑𝑁))))
6966, 68mpd 15 . . . . . . . . . . . 12 (𝜑 → ((bits ↾ ℕ0)‘((bits‘𝐵) ∩ (0..^𝑁))) = (𝐵 mod (2↑𝑁)))
7061, 69eqtrid 2789 . . . . . . . . . . 11 (𝜑 → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) = (𝐵 mod (2↑𝑁)))
7170oveq2d 7447 . . . . . . . . . 10 (𝜑 → (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) = (𝐵 − (𝐵 mod (2↑𝑁))))
7271oveq1d 7446 . . . . . . . . 9 (𝜑 → ((𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) / (2↑𝑁)) = ((𝐵 − (𝐵 mod (2↑𝑁))) / (2↑𝑁)))
7327zred 12722 . . . . . . . . . 10 (𝜑𝐵 ∈ ℝ)
74 moddifz 13923 . . . . . . . . . 10 ((𝐵 ∈ ℝ ∧ (2↑𝑁) ∈ ℝ+) → ((𝐵 − (𝐵 mod (2↑𝑁))) / (2↑𝑁)) ∈ ℤ)
7573, 53, 74syl2anc 584 . . . . . . . . 9 (𝜑 → ((𝐵 − (𝐵 mod (2↑𝑁))) / (2↑𝑁)) ∈ ℤ)
7672, 75eqeltrd 2841 . . . . . . . 8 (𝜑 → ((𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ)
77 dvdsval2 16293 . . . . . . . . 9 (((2↑𝑁) ∈ ℤ ∧ (2↑𝑁) ≠ 0 ∧ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ) → ((2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ↔ ((𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ))
785, 57, 39, 77syl3anc 1373 . . . . . . . 8 (𝜑 → ((2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ↔ ((𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) / (2↑𝑁)) ∈ ℤ))
7976, 78mpbird 257 . . . . . . 7 (𝜑 → (2↑𝑁) ∥ (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))))
805, 26, 39, 60, 79dvds2addd 16329 . . . . . 6 (𝜑 → (2↑𝑁) ∥ ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) + (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))))
816zcnd 12723 . . . . . . 7 (𝜑𝐴 ∈ ℂ)
8227zcnd 12723 . . . . . . 7 (𝜑𝐵 ∈ ℂ)
8324nn0cnd 12589 . . . . . . 7 (𝜑 → (𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) ∈ ℂ)
8437nn0cnd 12589 . . . . . . 7 (𝜑 → (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))) ∈ ℂ)
8581, 82, 83, 84addsub4d 11667 . . . . . 6 (𝜑 → ((𝐴 + 𝐵) − ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))) = ((𝐴 − (𝐾‘((bits‘𝐴) ∩ (0..^𝑁)))) + (𝐵 − (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))))
8680, 85breqtrrd 5171 . . . . 5 (𝜑 → (2↑𝑁) ∥ ((𝐴 + 𝐵) − ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁))))))
876, 27zaddcld 12726 . . . . . 6 (𝜑 → (𝐴 + 𝐵) ∈ ℤ)
8825, 38zaddcld 12726 . . . . . 6 (𝜑 → ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ)
89 moddvds 16301 . . . . . 6 (((2↑𝑁) ∈ ℕ ∧ (𝐴 + 𝐵) ∈ ℤ ∧ ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) ∈ ℤ) → (((𝐴 + 𝐵) mod (2↑𝑁)) = (((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) mod (2↑𝑁)) ↔ (2↑𝑁) ∥ ((𝐴 + 𝐵) − ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))))))
904, 87, 88, 89syl3anc 1373 . . . . 5 (𝜑 → (((𝐴 + 𝐵) mod (2↑𝑁)) = (((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) mod (2↑𝑁)) ↔ (2↑𝑁) ∥ ((𝐴 + 𝐵) − ((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))))))
9186, 90mpbird 257 . . . 4 (𝜑 → ((𝐴 + 𝐵) mod (2↑𝑁)) = (((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) mod (2↑𝑁)))
928a1i 11 . . . . 5 (𝜑 → (bits‘𝐴) ⊆ ℕ0)
9329a1i 11 . . . . 5 (𝜑 → (bits‘𝐵) ⊆ ℕ0)
94 sadaddlem.c . . . . 5 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ (bits‘𝐴), 𝑚 ∈ (bits‘𝐵), ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
9592, 93, 94, 3, 20sadadd3 16498 . . . 4 (𝜑 → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) mod (2↑𝑁)) = (((𝐾‘((bits‘𝐴) ∩ (0..^𝑁))) + (𝐾‘((bits‘𝐵) ∩ (0..^𝑁)))) mod (2↑𝑁)))
96 inss1 4237 . . . . . . . . 9 (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ⊆ ((bits‘𝐴) sadd (bits‘𝐵))
97 sadcl 16499 . . . . . . . . . 10 (((bits‘𝐴) ⊆ ℕ0 ∧ (bits‘𝐵) ⊆ ℕ0) → ((bits‘𝐴) sadd (bits‘𝐵)) ⊆ ℕ0)
988, 29, 97mp2an 692 . . . . . . . . 9 ((bits‘𝐴) sadd (bits‘𝐵)) ⊆ ℕ0
9996, 98sstri 3993 . . . . . . . 8 (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ⊆ ℕ0
100 inss2 4238 . . . . . . . . 9 (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ⊆ (0..^𝑁)
101 ssfi 9213 . . . . . . . . 9 (((0..^𝑁) ∈ Fin ∧ (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ Fin)
10210, 100, 101mp2an 692 . . . . . . . 8 (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ Fin
103 elfpw 9394 . . . . . . . 8 ((((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) ↔ ((((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ⊆ ℕ0 ∧ (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ Fin))
10499, 102, 103mpbir2an 711 . . . . . . 7 (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin)
10522ffvelcdmi 7103 . . . . . . 7 ((((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℕ0)
106104, 105mp1i 13 . . . . . 6 (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℕ0)
107106nn0red 12588 . . . . 5 (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℝ)
108106nn0ge0d 12590 . . . . 5 (𝜑 → 0 ≤ (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))))
10920fveq1i 6907 . . . . . . . . . 10 (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) = ((bits ↾ ℕ0)‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))
110109fveq2i 6909 . . . . . . . . 9 ((bits ↾ ℕ0)‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))))
111106fvresd 6926 . . . . . . . . 9 (𝜑 → ((bits ↾ ℕ0)‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))))
112104a1i 11 . . . . . . . . . 10 (𝜑 → (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin))
113 f1ocnvfv2 7297 . . . . . . . . . 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..^𝑁)))
11416, 112, 113sylancr 587 . . . . . . . . 9 (𝜑 → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))
115110, 111, 1143eqtr3a 2801 . . . . . . . 8 (𝜑 → (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) = (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))
116115, 100eqsstrdi 4028 . . . . . . 7 (𝜑 → (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) ⊆ (0..^𝑁))
117106nn0zd 12639 . . . . . . . 8 (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℤ)
118 bitsfzo 16472 . . . . . . . 8 (((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
119117, 3, 118syl2anc 584 . . . . . . 7 (𝜑 → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
120116, 119mpbird 257 . . . . . 6 (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)))
121 elfzolt2 13708 . . . . . 6 ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) < (2↑𝑁))
122120, 121syl 17 . . . . 5 (𝜑 → (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) < (2↑𝑁))
123 modid 13936 . . . . 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..^𝑁))))
124107, 53, 108, 122, 123syl22anc 839 . . . 4 (𝜑 → ((𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))) mod (2↑𝑁)) = (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))))
12591, 95, 1243eqtr2d 2783 . . 3 (𝜑 → ((𝐴 + 𝐵) mod (2↑𝑁)) = (𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁))))
126125fveq2d 6910 . 2 (𝜑 → (bits‘((𝐴 + 𝐵) mod (2↑𝑁))) = (bits‘(𝐾‘(((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)))))
127126, 115eqtr2d 2778 1 (𝜑 → (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) = (bits‘((𝐴 + 𝐵) mod (2↑𝑁))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1540  caddwcad 1606  wcel 2108  wne 2940  cin 3950  wss 3951  c0 4333  ifcif 4525  𝒫 cpw 4600   class class class wbr 5143  cmpt 5225  ccnv 5684  cres 5687  wf 6557  1-1-ontowf1o 6560  cfv 6561  (class class class)co 7431  cmpo 7433  1oc1o 8499  2oc2o 8500  Fincfn 8985  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   < clt 11295  cle 11296  cmin 11492   / cdiv 11920  cn 12266  2c2 12321  0cn0 12526  cz 12613  +crp 13034  ..^cfzo 13694   mod cmo 13909  seqcseq 14042  cexp 14102  cdvds 16290  bitscbits 16456   sadd csad 16457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-xor 1512  df-tru 1543  df-fal 1553  df-had 1594  df-cad 1607  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-disj 5111  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-map 8868  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-xnn0 12600  df-z 12614  df-uz 12879  df-rp 13035  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723  df-dvds 16291  df-bits 16459  df-sad 16488
This theorem is referenced by:  sadadd  16504
  Copyright terms: Public domain W3C validator