sadasslem - Metamath Proof Explorer

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

Theorem sadasslem 15192

Description: Lemma for sadass 15193. (Contributed by Mario Carneiro, 9-Sep-2016.)

**Hypotheses**
Ref	Expression
sadasslem.1	⊢ (𝜑 → 𝐴 ⊆ ℕ₀)
sadasslem.2	⊢ (𝜑 → 𝐵 ⊆ ℕ₀)
sadasslem.3	⊢ (𝜑 → 𝐶 ⊆ ℕ₀)
sadasslem.4	⊢ (𝜑 → 𝑁 ∈ ℕ₀)

**Assertion**
Ref	Expression
sadasslem	⊢ (𝜑 → (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) = ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)))

Proof of Theorem sadasslem Dummy variables 𝑐 𝑚 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss1 3833	. . . . . . . . . . 11 ⊢ (𝐴 ∩ (0..^𝑁)) ⊆ 𝐴
2		sadasslem.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ⊆ ℕ₀)
3	1, 2	syl5ss 3614	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∩ (0..^𝑁)) ⊆ ℕ₀)
4		fzofi 12773	. . . . . . . . . . . 12 ⊢ (0..^𝑁) ∈ Fin
5	4	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (0..^𝑁) ∈ Fin)
6		inss2 3834	. . . . . . . . . . 11 ⊢ (𝐴 ∩ (0..^𝑁)) ⊆ (0..^𝑁)
7		ssfi 8180	. . . . . . . . . . 11 ⊢ (((0..^𝑁) ∈ Fin ∧ (𝐴 ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (𝐴 ∩ (0..^𝑁)) ∈ Fin)
8	5, 6, 7	sylancl 694	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∩ (0..^𝑁)) ∈ Fin)
9		elfpw 8268	. . . . . . . . . 10 ⊢ ((𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin) ↔ ((𝐴 ∩ (0..^𝑁)) ⊆ ℕ₀ ∧ (𝐴 ∩ (0..^𝑁)) ∈ Fin))
10	3, 8, 9	sylanbrc 698	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin))
11		bitsf1o 15167	. . . . . . . . . . 11 ⊢ (bits ↾ ℕ₀):ℕ₀–1-1-onto→(𝒫 ℕ₀ ∩ Fin)
12		f1ocnv 6149	. . . . . . . . . . 11 ⊢ ((bits ↾ ℕ₀):ℕ₀–1-1-onto→(𝒫 ℕ₀ ∩ Fin) → ^◡(bits ↾ ℕ₀):(𝒫 ℕ₀ ∩ Fin)–1-1-onto→ℕ₀)
13		f1of 6137	. . . . . . . . . . 11 ⊢ (^◡(bits ↾ ℕ₀):(𝒫 ℕ₀ ∩ Fin)–1-1-onto→ℕ₀ → ^◡(bits ↾ ℕ₀):(𝒫 ℕ₀ ∩ Fin)⟶ℕ₀)
14	11, 12, 13	mp2b 10	. . . . . . . . . 10 ⊢ ^◡(bits ↾ ℕ₀):(𝒫 ℕ₀ ∩ Fin)⟶ℕ₀
15	14	ffvelrni 6358	. . . . . . . . 9 ⊢ ((𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin) → (^◡(bits ↾ ℕ₀)‘(𝐴 ∩ (0..^𝑁))) ∈ ℕ₀)
16	10, 15	syl 17	. . . . . . . 8 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘(𝐴 ∩ (0..^𝑁))) ∈ ℕ₀)
17	16	nn0cnd 11353	. . . . . . 7 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘(𝐴 ∩ (0..^𝑁))) ∈ ℂ)
18		inss1 3833	. . . . . . . . . . 11 ⊢ (𝐵 ∩ (0..^𝑁)) ⊆ 𝐵
19		sadasslem.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ⊆ ℕ₀)
20	18, 19	syl5ss 3614	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 ∩ (0..^𝑁)) ⊆ ℕ₀)
21		inss2 3834	. . . . . . . . . . 11 ⊢ (𝐵 ∩ (0..^𝑁)) ⊆ (0..^𝑁)
22		ssfi 8180	. . . . . . . . . . 11 ⊢ (((0..^𝑁) ∈ Fin ∧ (𝐵 ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (𝐵 ∩ (0..^𝑁)) ∈ Fin)
23	5, 21, 22	sylancl 694	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 ∩ (0..^𝑁)) ∈ Fin)
24		elfpw 8268	. . . . . . . . . 10 ⊢ ((𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin) ↔ ((𝐵 ∩ (0..^𝑁)) ⊆ ℕ₀ ∧ (𝐵 ∩ (0..^𝑁)) ∈ Fin))
25	20, 23, 24	sylanbrc 698	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin))
26	14	ffvelrni 6358	. . . . . . . . 9 ⊢ ((𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin) → (^◡(bits ↾ ℕ₀)‘(𝐵 ∩ (0..^𝑁))) ∈ ℕ₀)
27	25, 26	syl 17	. . . . . . . 8 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘(𝐵 ∩ (0..^𝑁))) ∈ ℕ₀)
28	27	nn0cnd 11353	. . . . . . 7 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘(𝐵 ∩ (0..^𝑁))) ∈ ℂ)
29		inss1 3833	. . . . . . . . . . 11 ⊢ (𝐶 ∩ (0..^𝑁)) ⊆ 𝐶
30		sadasslem.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ⊆ ℕ₀)
31	29, 30	syl5ss 3614	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 ∩ (0..^𝑁)) ⊆ ℕ₀)
32		inss2 3834	. . . . . . . . . . 11 ⊢ (𝐶 ∩ (0..^𝑁)) ⊆ (0..^𝑁)
33		ssfi 8180	. . . . . . . . . . 11 ⊢ (((0..^𝑁) ∈ Fin ∧ (𝐶 ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (𝐶 ∩ (0..^𝑁)) ∈ Fin)
34	5, 32, 33	sylancl 694	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 ∩ (0..^𝑁)) ∈ Fin)
35		elfpw 8268	. . . . . . . . . 10 ⊢ ((𝐶 ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin) ↔ ((𝐶 ∩ (0..^𝑁)) ⊆ ℕ₀ ∧ (𝐶 ∩ (0..^𝑁)) ∈ Fin))
36	31, 34, 35	sylanbrc 698	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin))
37	14	ffvelrni 6358	. . . . . . . . 9 ⊢ ((𝐶 ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin) → (^◡(bits ↾ ℕ₀)‘(𝐶 ∩ (0..^𝑁))) ∈ ℕ₀)
38	36, 37	syl 17	. . . . . . . 8 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘(𝐶 ∩ (0..^𝑁))) ∈ ℕ₀)
39	38	nn0cnd 11353	. . . . . . 7 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘(𝐶 ∩ (0..^𝑁))) ∈ ℂ)
40	17, 28, 39	addassd 10062	. . . . . 6 ⊢ (𝜑 → (((^◡(bits ↾ ℕ₀)‘(𝐴 ∩ (0..^𝑁))) + (^◡(bits ↾ ℕ₀)‘(𝐵 ∩ (0..^𝑁)))) + (^◡(bits ↾ ℕ₀)‘(𝐶 ∩ (0..^𝑁)))) = ((^◡(bits ↾ ℕ₀)‘(𝐴 ∩ (0..^𝑁))) + ((^◡(bits ↾ ℕ₀)‘(𝐵 ∩ (0..^𝑁))) + (^◡(bits ↾ ℕ₀)‘(𝐶 ∩ (0..^𝑁))))))
41	40	oveq1d 6665	. . . . 5 ⊢ (𝜑 → ((((^◡(bits ↾ ℕ₀)‘(𝐴 ∩ (0..^𝑁))) + (^◡(bits ↾ ℕ₀)‘(𝐵 ∩ (0..^𝑁)))) + (^◡(bits ↾ ℕ₀)‘(𝐶 ∩ (0..^𝑁)))) mod (2↑𝑁)) = (((^◡(bits ↾ ℕ₀)‘(𝐴 ∩ (0..^𝑁))) + ((^◡(bits ↾ ℕ₀)‘(𝐵 ∩ (0..^𝑁))) + (^◡(bits ↾ ℕ₀)‘(𝐶 ∩ (0..^𝑁))))) mod (2↑𝑁)))
42		inss1 3833	. . . . . . . . . 10 ⊢ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (𝐴 sadd 𝐵)
43		sadcl 15184	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ ℕ₀ ∧ 𝐵 ⊆ ℕ₀) → (𝐴 sadd 𝐵) ⊆ ℕ₀)
44	2, 19, 43	syl2anc 693	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 sadd 𝐵) ⊆ ℕ₀)
45	42, 44	syl5ss 3614	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ ℕ₀)
46		inss2 3834	. . . . . . . . . 10 ⊢ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁)
47		ssfi 8180	. . . . . . . . . 10 ⊢ (((0..^𝑁) ∈ Fin ∧ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin)
48	5, 46, 47	sylancl 694	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin)
49		elfpw 8268	. . . . . . . . 9 ⊢ (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin) ↔ (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ⊆ ℕ₀ ∧ ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ Fin))
50	45, 48, 49	sylanbrc 698	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin))
51	14	ffvelrni 6358	. . . . . . . 8 ⊢ (((𝐴 sadd 𝐵) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin) → (^◡(bits ↾ ℕ₀)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℕ₀)
52	50, 51	syl 17	. . . . . . 7 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℕ₀)
53	52	nn0red 11352	. . . . . 6 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) ∈ ℝ)
54	16	nn0red 11352	. . . . . . 7 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘(𝐴 ∩ (0..^𝑁))) ∈ ℝ)
55	27	nn0red 11352	. . . . . . 7 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘(𝐵 ∩ (0..^𝑁))) ∈ ℝ)
56	54, 55	readdcld 10069	. . . . . 6 ⊢ (𝜑 → ((^◡(bits ↾ ℕ₀)‘(𝐴 ∩ (0..^𝑁))) + (^◡(bits ↾ ℕ₀)‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ)
57	38	nn0red 11352	. . . . . 6 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘(𝐶 ∩ (0..^𝑁))) ∈ ℝ)
58		2rp 11837	. . . . . . . 8 ⊢ 2 ∈ ℝ⁺
59	58	a1i 11	. . . . . . 7 ⊢ (𝜑 → 2 ∈ ℝ⁺)
60		sadasslem.4	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
61	60	nn0zd 11480	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℤ)
62	59, 61	rpexpcld 13032	. . . . . 6 ⊢ (𝜑 → (2↑𝑁) ∈ ℝ⁺)
63		eqid 2622	. . . . . . 7 ⊢ seq0((𝑐 ∈ 2_𝑜, 𝑚 ∈ ℕ₀ ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1_𝑜, ∅)), (𝑛 ∈ ℕ₀ ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) = seq0((𝑐 ∈ 2_𝑜, 𝑚 ∈ ℕ₀ ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1_𝑜, ∅)), (𝑛 ∈ ℕ₀ ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
64		eqid 2622	. . . . . . 7 ⊢ ^◡(bits ↾ ℕ₀) = ^◡(bits ↾ ℕ₀)
65	2, 19, 63, 60, 64	sadadd3 15183	. . . . . 6 ⊢ (𝜑 → ((^◡(bits ↾ ℕ₀)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)) = (((^◡(bits ↾ ℕ₀)‘(𝐴 ∩ (0..^𝑁))) + (^◡(bits ↾ ℕ₀)‘(𝐵 ∩ (0..^𝑁)))) mod (2↑𝑁)))
66		eqidd 2623	. . . . . 6 ⊢ (𝜑 → ((^◡(bits ↾ ℕ₀)‘(𝐶 ∩ (0..^𝑁))) mod (2↑𝑁)) = ((^◡(bits ↾ ℕ₀)‘(𝐶 ∩ (0..^𝑁))) mod (2↑𝑁)))
67	53, 56, 57, 57, 62, 65, 66	modadd12d 12726	. . . . 5 ⊢ (𝜑 → (((^◡(bits ↾ ℕ₀)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + (^◡(bits ↾ ℕ₀)‘(𝐶 ∩ (0..^𝑁)))) mod (2↑𝑁)) = ((((^◡(bits ↾ ℕ₀)‘(𝐴 ∩ (0..^𝑁))) + (^◡(bits ↾ ℕ₀)‘(𝐵 ∩ (0..^𝑁)))) + (^◡(bits ↾ ℕ₀)‘(𝐶 ∩ (0..^𝑁)))) mod (2↑𝑁)))
68		inss1 3833	. . . . . . . . . 10 ⊢ ((𝐵 sadd 𝐶) ∩ (0..^𝑁)) ⊆ (𝐵 sadd 𝐶)
69		sadcl 15184	. . . . . . . . . . 11 ⊢ ((𝐵 ⊆ ℕ₀ ∧ 𝐶 ⊆ ℕ₀) → (𝐵 sadd 𝐶) ⊆ ℕ₀)
70	19, 30, 69	syl2anc 693	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 sadd 𝐶) ⊆ ℕ₀)
71	68, 70	syl5ss 3614	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 sadd 𝐶) ∩ (0..^𝑁)) ⊆ ℕ₀)
72		inss2 3834	. . . . . . . . . 10 ⊢ ((𝐵 sadd 𝐶) ∩ (0..^𝑁)) ⊆ (0..^𝑁)
73		ssfi 8180	. . . . . . . . . 10 ⊢ (((0..^𝑁) ∈ Fin ∧ ((𝐵 sadd 𝐶) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → ((𝐵 sadd 𝐶) ∩ (0..^𝑁)) ∈ Fin)
74	5, 72, 73	sylancl 694	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 sadd 𝐶) ∩ (0..^𝑁)) ∈ Fin)
75		elfpw 8268	. . . . . . . . 9 ⊢ (((𝐵 sadd 𝐶) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin) ↔ (((𝐵 sadd 𝐶) ∩ (0..^𝑁)) ⊆ ℕ₀ ∧ ((𝐵 sadd 𝐶) ∩ (0..^𝑁)) ∈ Fin))
76	71, 74, 75	sylanbrc 698	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 sadd 𝐶) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin))
77	14	ffvelrni 6358	. . . . . . . 8 ⊢ (((𝐵 sadd 𝐶) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin) → (^◡(bits ↾ ℕ₀)‘((𝐵 sadd 𝐶) ∩ (0..^𝑁))) ∈ ℕ₀)
78	76, 77	syl 17	. . . . . . 7 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘((𝐵 sadd 𝐶) ∩ (0..^𝑁))) ∈ ℕ₀)
79	78	nn0red 11352	. . . . . 6 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘((𝐵 sadd 𝐶) ∩ (0..^𝑁))) ∈ ℝ)
80	55, 57	readdcld 10069	. . . . . 6 ⊢ (𝜑 → ((^◡(bits ↾ ℕ₀)‘(𝐵 ∩ (0..^𝑁))) + (^◡(bits ↾ ℕ₀)‘(𝐶 ∩ (0..^𝑁)))) ∈ ℝ)
81		eqidd 2623	. . . . . 6 ⊢ (𝜑 → ((^◡(bits ↾ ℕ₀)‘(𝐴 ∩ (0..^𝑁))) mod (2↑𝑁)) = ((^◡(bits ↾ ℕ₀)‘(𝐴 ∩ (0..^𝑁))) mod (2↑𝑁)))
82		eqid 2622	. . . . . . 7 ⊢ seq0((𝑐 ∈ 2_𝑜, 𝑚 ∈ ℕ₀ ↦ if(cadd(𝑚 ∈ 𝐵, 𝑚 ∈ 𝐶, ∅ ∈ 𝑐), 1_𝑜, ∅)), (𝑛 ∈ ℕ₀ ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) = seq0((𝑐 ∈ 2_𝑜, 𝑚 ∈ ℕ₀ ↦ if(cadd(𝑚 ∈ 𝐵, 𝑚 ∈ 𝐶, ∅ ∈ 𝑐), 1_𝑜, ∅)), (𝑛 ∈ ℕ₀ ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
83	19, 30, 82, 60, 64	sadadd3 15183	. . . . . 6 ⊢ (𝜑 → ((^◡(bits ↾ ℕ₀)‘((𝐵 sadd 𝐶) ∩ (0..^𝑁))) mod (2↑𝑁)) = (((^◡(bits ↾ ℕ₀)‘(𝐵 ∩ (0..^𝑁))) + (^◡(bits ↾ ℕ₀)‘(𝐶 ∩ (0..^𝑁)))) mod (2↑𝑁)))
84	54, 54, 79, 80, 62, 81, 83	modadd12d 12726	. . . . 5 ⊢ (𝜑 → (((^◡(bits ↾ ℕ₀)‘(𝐴 ∩ (0..^𝑁))) + (^◡(bits ↾ ℕ₀)‘((𝐵 sadd 𝐶) ∩ (0..^𝑁)))) mod (2↑𝑁)) = (((^◡(bits ↾ ℕ₀)‘(𝐴 ∩ (0..^𝑁))) + ((^◡(bits ↾ ℕ₀)‘(𝐵 ∩ (0..^𝑁))) + (^◡(bits ↾ ℕ₀)‘(𝐶 ∩ (0..^𝑁))))) mod (2↑𝑁)))
85	41, 67, 84	3eqtr4d 2666	. . . 4 ⊢ (𝜑 → (((^◡(bits ↾ ℕ₀)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + (^◡(bits ↾ ℕ₀)‘(𝐶 ∩ (0..^𝑁)))) mod (2↑𝑁)) = (((^◡(bits ↾ ℕ₀)‘(𝐴 ∩ (0..^𝑁))) + (^◡(bits ↾ ℕ₀)‘((𝐵 sadd 𝐶) ∩ (0..^𝑁)))) mod (2↑𝑁)))
86		eqid 2622	. . . . 5 ⊢ seq0((𝑐 ∈ 2_𝑜, 𝑚 ∈ ℕ₀ ↦ if(cadd(𝑚 ∈ (𝐴 sadd 𝐵), 𝑚 ∈ 𝐶, ∅ ∈ 𝑐), 1_𝑜, ∅)), (𝑛 ∈ ℕ₀ ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) = seq0((𝑐 ∈ 2_𝑜, 𝑚 ∈ ℕ₀ ↦ if(cadd(𝑚 ∈ (𝐴 sadd 𝐵), 𝑚 ∈ 𝐶, ∅ ∈ 𝑐), 1_𝑜, ∅)), (𝑛 ∈ ℕ₀ ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
87	44, 30, 86, 60, 64	sadadd3 15183	. . . 4 ⊢ (𝜑 → ((^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) mod (2↑𝑁)) = (((^◡(bits ↾ ℕ₀)‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + (^◡(bits ↾ ℕ₀)‘(𝐶 ∩ (0..^𝑁)))) mod (2↑𝑁)))
88		eqid 2622	. . . . 5 ⊢ seq0((𝑐 ∈ 2_𝑜, 𝑚 ∈ ℕ₀ ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ (𝐵 sadd 𝐶), ∅ ∈ 𝑐), 1_𝑜, ∅)), (𝑛 ∈ ℕ₀ ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) = seq0((𝑐 ∈ 2_𝑜, 𝑚 ∈ ℕ₀ ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ (𝐵 sadd 𝐶), ∅ ∈ 𝑐), 1_𝑜, ∅)), (𝑛 ∈ ℕ₀ ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
89	2, 70, 88, 60, 64	sadadd3 15183	. . . 4 ⊢ (𝜑 → ((^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) mod (2↑𝑁)) = (((^◡(bits ↾ ℕ₀)‘(𝐴 ∩ (0..^𝑁))) + (^◡(bits ↾ ℕ₀)‘((𝐵 sadd 𝐶) ∩ (0..^𝑁)))) mod (2↑𝑁)))
90	85, 87, 89	3eqtr4d 2666	. . 3 ⊢ (𝜑 → ((^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) mod (2↑𝑁)) = ((^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) mod (2↑𝑁)))
91		inss1 3833	. . . . . . . 8 ⊢ (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) ⊆ ((𝐴 sadd 𝐵) sadd 𝐶)
92		sadcl 15184	. . . . . . . . 9 ⊢ (((𝐴 sadd 𝐵) ⊆ ℕ₀ ∧ 𝐶 ⊆ ℕ₀) → ((𝐴 sadd 𝐵) sadd 𝐶) ⊆ ℕ₀)
93	44, 30, 92	syl2anc 693	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 sadd 𝐵) sadd 𝐶) ⊆ ℕ₀)
94	91, 93	syl5ss 3614	. . . . . . 7 ⊢ (𝜑 → (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) ⊆ ℕ₀)
95		inss2 3834	. . . . . . . 8 ⊢ (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) ⊆ (0..^𝑁)
96		ssfi 8180	. . . . . . . 8 ⊢ (((0..^𝑁) ∈ Fin ∧ (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) ∈ Fin)
97	5, 95, 96	sylancl 694	. . . . . . 7 ⊢ (𝜑 → (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) ∈ Fin)
98		elfpw 8268	. . . . . . 7 ⊢ ((((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin) ↔ ((((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) ⊆ ℕ₀ ∧ (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) ∈ Fin))
99	94, 97, 98	sylanbrc 698	. . . . . 6 ⊢ (𝜑 → (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin))
100	14	ffvelrni 6358	. . . . . 6 ⊢ ((((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin) → (^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) ∈ ℕ₀)
101	99, 100	syl 17	. . . . 5 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) ∈ ℕ₀)
102	101	nn0red 11352	. . . 4 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) ∈ ℝ)
103	101	nn0ge0d 11354	. . . 4 ⊢ (𝜑 → 0 ≤ (^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))))
104		fvres 6207	. . . . . . . . 9 ⊢ ((^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) ∈ ℕ₀ → ((bits ↾ ℕ₀)‘(^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)))) = (bits‘(^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)))))
105	101, 104	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((bits ↾ ℕ₀)‘(^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)))) = (bits‘(^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)))))
106		f1ocnvfv2 6533	. . . . . . . . 9 ⊢ (((bits ↾ ℕ₀):ℕ₀–1-1-onto→(𝒫 ℕ₀ ∩ Fin) ∧ (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin)) → ((bits ↾ ℕ₀)‘(^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)))) = (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)))
107	11, 99, 106	sylancr 695	. . . . . . . 8 ⊢ (𝜑 → ((bits ↾ ℕ₀)‘(^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)))) = (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)))
108	105, 107	eqtr3d 2658	. . . . . . 7 ⊢ (𝜑 → (bits‘(^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)))) = (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)))
109	108, 95	syl6eqss 3655	. . . . . 6 ⊢ (𝜑 → (bits‘(^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)))) ⊆ (0..^𝑁))
110	101	nn0zd 11480	. . . . . . 7 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) ∈ ℤ)
111		bitsfzo 15157	. . . . . . 7 ⊢ (((^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ₀) → ((^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
112	110, 60, 111	syl2anc 693	. . . . . 6 ⊢ (𝜑 → ((^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
113	109, 112	mpbird 247	. . . . 5 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)))
114		elfzolt2 12479	. . . . 5 ⊢ ((^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → (^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) < (2↑𝑁))
115	113, 114	syl 17	. . . 4 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) < (2↑𝑁))
116		modid 12695	. . . 4 ⊢ ((((^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) ∈ ℝ ∧ (2↑𝑁) ∈ ℝ⁺) ∧ (0 ≤ (^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) ∧ (^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) < (2↑𝑁))) → ((^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) mod (2↑𝑁)) = (^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))))
117	102, 62, 103, 115, 116	syl22anc 1327	. . 3 ⊢ (𝜑 → ((^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) mod (2↑𝑁)) = (^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))))
118		inss1 3833	. . . . . . . 8 ⊢ ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)) ⊆ (𝐴 sadd (𝐵 sadd 𝐶))
119		sadcl 15184	. . . . . . . . 9 ⊢ ((𝐴 ⊆ ℕ₀ ∧ (𝐵 sadd 𝐶) ⊆ ℕ₀) → (𝐴 sadd (𝐵 sadd 𝐶)) ⊆ ℕ₀)
120	2, 70, 119	syl2anc 693	. . . . . . . 8 ⊢ (𝜑 → (𝐴 sadd (𝐵 sadd 𝐶)) ⊆ ℕ₀)
121	118, 120	syl5ss 3614	. . . . . . 7 ⊢ (𝜑 → ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)) ⊆ ℕ₀)
122		inss2 3834	. . . . . . . 8 ⊢ ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)) ⊆ (0..^𝑁)
123		ssfi 8180	. . . . . . . 8 ⊢ (((0..^𝑁) ∈ Fin ∧ ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)) ∈ Fin)
124	5, 122, 123	sylancl 694	. . . . . . 7 ⊢ (𝜑 → ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)) ∈ Fin)
125		elfpw 8268	. . . . . . 7 ⊢ (((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin) ↔ (((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)) ⊆ ℕ₀ ∧ ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)) ∈ Fin))
126	121, 124, 125	sylanbrc 698	. . . . . 6 ⊢ (𝜑 → ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin))
127	14	ffvelrni 6358	. . . . . 6 ⊢ (((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin) → (^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) ∈ ℕ₀)
128	126, 127	syl 17	. . . . 5 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) ∈ ℕ₀)
129	128	nn0red 11352	. . . 4 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) ∈ ℝ)
130		2nn 11185	. . . . . . 7 ⊢ 2 ∈ ℕ
131	130	a1i 11	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℕ)
132	131, 60	nnexpcld 13030	. . . . 5 ⊢ (𝜑 → (2↑𝑁) ∈ ℕ)
133	132	nnrpd 11870	. . . 4 ⊢ (𝜑 → (2↑𝑁) ∈ ℝ⁺)
134	128	nn0ge0d 11354	. . . 4 ⊢ (𝜑 → 0 ≤ (^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))))
135		fvres 6207	. . . . . . . . 9 ⊢ ((^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) ∈ ℕ₀ → ((bits ↾ ℕ₀)‘(^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)))) = (bits‘(^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)))))
136	128, 135	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((bits ↾ ℕ₀)‘(^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)))) = (bits‘(^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)))))
137		f1ocnvfv2 6533	. . . . . . . . 9 ⊢ (((bits ↾ ℕ₀):ℕ₀–1-1-onto→(𝒫 ℕ₀ ∩ Fin) ∧ ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin)) → ((bits ↾ ℕ₀)‘(^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)))) = ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)))
138	11, 126, 137	sylancr 695	. . . . . . . 8 ⊢ (𝜑 → ((bits ↾ ℕ₀)‘(^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)))) = ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)))
139	136, 138	eqtr3d 2658	. . . . . . 7 ⊢ (𝜑 → (bits‘(^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)))) = ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)))
140	139, 122	syl6eqss 3655	. . . . . 6 ⊢ (𝜑 → (bits‘(^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)))) ⊆ (0..^𝑁))
141	128	nn0zd 11480	. . . . . . 7 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) ∈ ℤ)
142		bitsfzo 15157	. . . . . . 7 ⊢ (((^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ₀) → ((^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
143	141, 60, 142	syl2anc 693	. . . . . 6 ⊢ (𝜑 → ((^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
144	140, 143	mpbird 247	. . . . 5 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)))
145		elfzolt2 12479	. . . . 5 ⊢ ((^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → (^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) < (2↑𝑁))
146	144, 145	syl 17	. . . 4 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) < (2↑𝑁))
147		modid 12695	. . . 4 ⊢ ((((^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) ∈ ℝ ∧ (2↑𝑁) ∈ ℝ⁺) ∧ (0 ≤ (^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) ∧ (^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) < (2↑𝑁))) → ((^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) mod (2↑𝑁)) = (^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))))
148	129, 133, 134, 146, 147	syl22anc 1327	. . 3 ⊢ (𝜑 → ((^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) mod (2↑𝑁)) = (^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))))
149	90, 117, 148	3eqtr3d 2664	. 2 ⊢ (𝜑 → (^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) = (^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))))
150		f1of1 6136	. . . . 5 ⊢ (^◡(bits ↾ ℕ₀):(𝒫 ℕ₀ ∩ Fin)–1-1-onto→ℕ₀ → ^◡(bits ↾ ℕ₀):(𝒫 ℕ₀ ∩ Fin)–1-1→ℕ₀)
151	11, 12, 150	mp2b 10	. . . 4 ⊢ ^◡(bits ↾ ℕ₀):(𝒫 ℕ₀ ∩ Fin)–1-1→ℕ₀
152		f1fveq 6519	. . . 4 ⊢ ((^◡(bits ↾ ℕ₀):(𝒫 ℕ₀ ∩ Fin)–1-1→ℕ₀ ∧ ((((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin) ∧ ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin))) → ((^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) = (^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) ↔ (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) = ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))))
153	151, 152	mpan 706	. . 3 ⊢ (((((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin) ∧ ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)) ∈ (𝒫 ℕ₀ ∩ Fin)) → ((^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) = (^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) ↔ (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) = ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))))
154	99, 126, 153	syl2anc 693	. 2 ⊢ (𝜑 → ((^◡(bits ↾ ℕ₀)‘(((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁))) = (^◡(bits ↾ ℕ₀)‘((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) ↔ (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) = ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))))
155	149, 154	mpbid 222	1 ⊢ (𝜑 → (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) = ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 caddwcad 1545 ∈ wcel 1990 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 ifcif 4086 𝒫 cpw 4158 class class class wbr 4653 ↦ cmpt 4729 ^◡ccnv 5113 ↾ cres 5116 ⟶wf 5884 –1-1→wf1 5885 –1-1-onto→wf1o 5887 ‘cfv 5888 (class class class)co 6650 ↦ cmpt2 6652 1_𝑜c1o 7553 2_𝑜c2o 7554 Fincfn 7955 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 < clt 10074 ≤ cle 10075 − cmin 10266 ℕcn 11020 2c2 11070 ℕ₀cn0 11292 ℤcz 11377 ℝ⁺crp 11832 ..^cfzo 12465 mod cmo 12668 seqcseq 12801 ↑cexp 12860 bitscbits 15141 sadd csad 15142

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-xor 1465 df-tru 1486 df-fal 1489 df-had 1533 df-cad 1546 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-disj 4621 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-rp 11833 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417 df-dvds 14984 df-bits 15144 df-sad 15173

This theorem is referenced by: sadass 15193

W3C validator