Theorem eulerpartlemgs2 30442

Description: Lemma for eulerpart 30444: The 𝐺 function also preserves partition sums. (Contributed by Thierry Arnoux, 10-Sep-2017.)

Hypotheses

Ref	Expression
eulerpart.p	⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑𝑚 ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}
eulerpart.o	⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
eulerpart.d	⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}
eulerpart.j	⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
eulerpart.f	⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
eulerpart.h	⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
eulerpart.m	⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})
eulerpart.r	⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
eulerpart.t	⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑𝑚 ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}
eulerpart.g	⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
eulerpart.s	⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑𝑚 ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))

Assertion

Ref	Expression
eulerpartlemgs2	⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = (𝑆‘𝐴))

Distinct variable groups:   𝑓,𝑔,𝑘,𝑛,𝑜,𝑥,𝑦,𝑧   𝑓,𝑟,𝐴,𝑔,𝑘,𝑛,𝑜,𝑥,𝑦   𝑓,𝐺,𝑘   𝑛,𝐹,𝑜,𝑥,𝑦   𝑜,𝐻,𝑟   𝑓,𝐽,𝑛,𝑜,𝑟,𝑥,𝑦   𝑛,𝑀,𝑜,𝑟,𝑥,𝑦   𝑓,𝑁,𝑔,𝑘,𝑛,𝑥   𝑛,𝑂,𝑟,𝑥,𝑦   𝑃,𝑔,𝑘,𝑛   𝑅,𝑓,𝑘,𝑛,𝑜,𝑟,𝑥,𝑦   𝑇,𝑓,𝑘,𝑛,𝑜,𝑟,𝑥,𝑦

Allowed substitution hints:   𝐴(𝑧)   𝐷(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)   𝑃(𝑥,𝑦,𝑧,𝑓,𝑜,𝑟)   𝑅(𝑧,𝑔)   𝑆(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑜,𝑟)   𝑇(𝑧,𝑔)   𝐹(𝑧,𝑓,𝑔,𝑘,𝑟)   𝐺(𝑥,𝑦,𝑧,𝑔,𝑛,𝑜,𝑟)   𝐻(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛)   𝐽(𝑧,𝑔,𝑘)   𝑀(𝑧,𝑓,𝑔,𝑘)   𝑁(𝑦,𝑧,𝑜,𝑟)   𝑂(𝑧,𝑓,𝑔,𝑘,𝑜)

Proof of Theorem eulerpartlemgs2

Dummy variables 𝑡 𝑚 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnvimass 5485	. . . . . . . 8 ⊢ (◡(𝐺‘𝐴) “ ℕ) ⊆ dom (𝐺‘𝐴)
2		eulerpart.p	. . . . . . . . . . . . . 14 ⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑𝑚 ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}
3		eulerpart.o	. . . . . . . . . . . . . 14 ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
4		eulerpart.d	. . . . . . . . . . . . . 14 ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}
5		eulerpart.j	. . . . . . . . . . . . . 14 ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
6		eulerpart.f	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
7		eulerpart.h	. . . . . . . . . . . . . 14 ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
8		eulerpart.m	. . . . . . . . . . . . . 14 ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})
9		eulerpart.r	. . . . . . . . . . . . . 14 ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
10		eulerpart.t	. . . . . . . . . . . . . 14 ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑𝑚 ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}
11		eulerpart.g	. . . . . . . . . . . . . 14 ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
12	2, 3, 4, 5, 6, 7, 8, 9, 10, 11	eulerpartgbij 30434	. . . . . . . . . . . . 13 ⊢ 𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
13		f1of 6137	. . . . . . . . . . . . 13 ⊢ (𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑𝑚 ℕ) ∩ 𝑅) → 𝐺:(𝑇 ∩ 𝑅)⟶(({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
14	12, 13	ax-mp 5	. . . . . . . . . . . 12 ⊢ 𝐺:(𝑇 ∩ 𝑅)⟶(({0, 1} ↑𝑚 ℕ) ∩ 𝑅)
15	14	ffvelrni 6358	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅))
16		elin 3796	. . . . . . . . . . 11 ⊢ ((𝐺‘𝐴) ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) ↔ ((𝐺‘𝐴) ∈ ({0, 1} ↑𝑚 ℕ) ∧ (𝐺‘𝐴) ∈ 𝑅))
17	15, 16	sylib 208	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝐺‘𝐴) ∈ ({0, 1} ↑𝑚 ℕ) ∧ (𝐺‘𝐴) ∈ 𝑅))
18	17	simpld 475	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) ∈ ({0, 1} ↑𝑚 ℕ))
19		elmapi 7879	. . . . . . . . 9 ⊢ ((𝐺‘𝐴) ∈ ({0, 1} ↑𝑚 ℕ) → (𝐺‘𝐴):ℕ⟶{0, 1})
20		fdm 6051	. . . . . . . . 9 ⊢ ((𝐺‘𝐴):ℕ⟶{0, 1} → dom (𝐺‘𝐴) = ℕ)
21	18, 19, 20	3syl 18	. . . . . . . 8 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → dom (𝐺‘𝐴) = ℕ)
22	1, 21	syl5sseq 3653	. . . . . . 7 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡(𝐺‘𝐴) “ ℕ) ⊆ ℕ)
23	22	sselda 3603	. . . . . 6 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)) → 𝑘 ∈ ℕ)
24	2, 3, 4, 5, 6, 7, 8, 9, 10, 11	eulerpartlemgvv 30438	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ℕ) → ((𝐺‘𝐴)‘𝑘) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0))
25	24	oveq1d 6665	. . . . . 6 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ℕ) → (((𝐺‘𝐴)‘𝑘) · 𝑘) = (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘))
26	23, 25	syldan 487	. . . . 5 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)) → (((𝐺‘𝐴)‘𝑘) · 𝑘) = (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘))
27	26	sumeq2dv 14433	. . . 4 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘))
28		eqeq2 2633	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑘 → (((2↑𝑛) · 𝑡) = 𝑚 ↔ ((2↑𝑛) · 𝑡) = 𝑘))
29	28	2rexbidv 3057	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑘 → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚 ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘))
30	29	elrab 3363	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ↔ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘))
31	30	simprbi 480	. . . . . . . . . 10 ⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)
32	31	iftrued 4094	. . . . . . . . 9 ⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 1)
33	32	oveq1d 6665	. . . . . . . 8 ⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = (1 · 𝑘))
34		elrabi 3359	. . . . . . . . . 10 ⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ ℕ)
35	34	nncnd 11036	. . . . . . . . 9 ⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ ℂ)
36	35	mulid2d 10058	. . . . . . . 8 ⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (1 · 𝑘) = 𝑘)
37	33, 36	eqtrd 2656	. . . . . . 7 ⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = 𝑘)
38	37	sumeq2i 14429	. . . . . 6 ⊢ Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}𝑘
39		id 22	. . . . . . 7 ⊢ (𝑘 = ((2↑(2nd ‘𝑤)) · (1st ‘𝑤)) → 𝑘 = ((2↑(2nd ‘𝑤)) · (1st ‘𝑤)))
40	2, 3, 4, 5, 6, 7, 8, 9, 10, 11	eulerpartlemgf 30441	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡(𝐺‘𝐴) “ ℕ) ∈ Fin)
41	34	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℕ)
42	41, 24	syldan 487	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺‘𝐴)‘𝑘) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0))
43	31	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)
44	43	iftrued 4094	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 1)
45	42, 44	eqtrd 2656	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺‘𝐴)‘𝑘) = 1)
46		1nn 11031	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ
47	45, 46	syl6eqel 2709	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺‘𝐴)‘𝑘) ∈ ℕ)
48	18, 19	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴):ℕ⟶{0, 1})
49		ffn 6045	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝐴):ℕ⟶{0, 1} → (𝐺‘𝐴) Fn ℕ)
50		elpreima 6337	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝐴) Fn ℕ → (𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺‘𝐴)‘𝑘) ∈ ℕ)))
51	48, 49, 50	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺‘𝐴)‘𝑘) ∈ ℕ)))
52	51	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → (𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺‘𝐴)‘𝑘) ∈ ℕ)))
53	41, 47, 52	mpbir2and 957	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ))
54	53	ex 450	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)))
55	54	ssrdv 3609	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ (◡(𝐺‘𝐴) “ ℕ))
56		ssfi 8180	. . . . . . . . 9 ⊢ (((◡(𝐺‘𝐴) “ ℕ) ∈ Fin ∧ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ (◡(𝐺‘𝐴) “ ℕ)) → {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin)
57	40, 55, 56	syl2anc 693	. . . . . . . 8 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin)
58		cnvexg 7112	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ◡𝐴 ∈ V)
59		imaexg 7103	. . . . . . . . . . 11 ⊢ (◡𝐴 ∈ V → (◡𝐴 “ ℕ) ∈ V)
60		inex1g 4801	. . . . . . . . . . 11 ⊢ ((◡𝐴 “ ℕ) ∈ V → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ V)
61	58, 59, 60	3syl 18	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ V)
62		snex 4908	. . . . . . . . . . . 12 ⊢ {𝑡} ∈ V
63		fvex 6201	. . . . . . . . . . . 12 ⊢ (bits‘(𝐴‘𝑡)) ∈ V
64	62, 63	xpex 6962	. . . . . . . . . . 11 ⊢ ({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V
65	64	rgenw 2924	. . . . . . . . . 10 ⊢ ∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V
66		iunexg 7143	. . . . . . . . . 10 ⊢ ((((◡𝐴 “ ℕ) ∩ 𝐽) ∈ V ∧ ∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V)
67	61, 65, 66	sylancl 694	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V)
68		eqid 2622	. . . . . . . . . 10 ⊢ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))
69	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 68	eulerpartlemgh 30440	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐹 ↾ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))):∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})
70		f1oeng 7974	. . . . . . . . 9 ⊢ ((∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V ∧ (𝐹 ↾ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))):∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ≈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})
71	67, 69, 70	syl2anc 693	. . . . . . . 8 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ≈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})
72		enfii 8177	. . . . . . . 8 ⊢ (({𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin ∧ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ≈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ Fin)
73	57, 71, 72	syl2anc 693	. . . . . . 7 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ Fin)
74		fvres 6207	. . . . . . . . 9 ⊢ (𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) → ((𝐹 ↾ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))))‘𝑤) = (𝐹‘𝑤))
75	74	adantl 482	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → ((𝐹 ↾ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))))‘𝑤) = (𝐹‘𝑤))
76		inss2 3834	. . . . . . . . . . . . . . 15 ⊢ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ 𝐽
77		simpr 477	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽))
78	76, 77	sseldi 3601	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ 𝐽)
79	78	snssd 4340	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → {𝑡} ⊆ 𝐽)
80		bitsss 15148	. . . . . . . . . . . . 13 ⊢ (bits‘(𝐴‘𝑡)) ⊆ ℕ0
81		xpss12 5225	. . . . . . . . . . . . 13 ⊢ (({𝑡} ⊆ 𝐽 ∧ (bits‘(𝐴‘𝑡)) ⊆ ℕ0) → ({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0))
82	79, 80, 81	sylancl 694	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → ({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0))
83	82	ralrimiva 2966	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0))
84		iunss 4561	. . . . . . . . . . 11 ⊢ (∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0) ↔ ∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0))
85	83, 84	sylibr 224	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0))
86	85	sselda 3603	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → 𝑤 ∈ (𝐽 × ℕ0))
87	5, 6	oddpwdcv 30417	. . . . . . . . 9 ⊢ (𝑤 ∈ (𝐽 × ℕ0) → (𝐹‘𝑤) = ((2↑(2nd ‘𝑤)) · (1st ‘𝑤)))
88	86, 87	syl 17	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → (𝐹‘𝑤) = ((2↑(2nd ‘𝑤)) · (1st ‘𝑤)))
89	75, 88	eqtrd 2656	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → ((𝐹 ↾ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))))‘𝑤) = ((2↑(2nd ‘𝑤)) · (1st ‘𝑤)))
90	41	nncnd 11036	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℂ)
91	39, 73, 69, 89, 90	fsumf1o 14454	. . . . . 6 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}𝑘 = Σ𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st ‘𝑤)))
92	38, 91	syl5eq 2668	. . . . 5 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = Σ𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st ‘𝑤)))
93		ax-1cn 9994	. . . . . . . . 9 ⊢ 1 ∈ ℂ
94		0cn 10032	. . . . . . . . 9 ⊢ 0 ∈ ℂ
95	93, 94	keepel 4155	. . . . . . . 8 ⊢ if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) ∈ ℂ
96	95	a1i 11	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) ∈ ℂ)
97		ssrab2 3687	. . . . . . . . 9 ⊢ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ ℕ
98		simpr 477	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})
99	97, 98	sseldi 3601	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℕ)
100	99	nncnd 11036	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℂ)
101	96, 100	mulcld 10060	. . . . . 6 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) ∈ ℂ)
102		simpr 477	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}))
103	102	eldifbd 3587	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → ¬ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})
104	22	ssdifssd 3748	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) ⊆ ℕ)
105	104	sselda 3603	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ ℕ)
106	30	notbii 310	. . . . . . . . . . 11 ⊢ (¬ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ↔ ¬ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘))
107		imnan 438	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ → ¬ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘) ↔ ¬ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘))
108	106, 107	sylbb2 228	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (𝑘 ∈ ℕ → ¬ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘))
109	103, 105, 108	sylc 65	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → ¬ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)
110	109	iffalsed 4097	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 0)
111	110	oveq1d 6665	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = (0 · 𝑘))
112		nnsscn 11025	. . . . . . . . . 10 ⊢ ℕ ⊆ ℂ
113	104, 112	syl6ss 3615	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) ⊆ ℂ)
114	113	sselda 3603	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ ℂ)
115	114	mul02d 10234	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (0 · 𝑘) = 0)
116	111, 115	eqtrd 2656	. . . . . 6 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = 0)
117	55, 101, 116, 40	fsumss 14456	. . . . 5 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘))
118	92, 117	eqtr3d 2658	. . . 4 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st ‘𝑤)) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘))
119	2, 3, 4, 5, 6, 7, 8, 9, 10	eulerpartlemt0 30431	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0 ↑𝑚 ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽))
120	119	simp1bi 1076	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ (ℕ0 ↑𝑚 ℕ))
121		elmapi 7879	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (ℕ0 ↑𝑚 ℕ) → 𝐴:ℕ⟶ℕ0)
122	120, 121	syl 17	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴:ℕ⟶ℕ0)
123	122	adantr 481	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝐴:ℕ⟶ℕ0)
124		cnvimass 5485	. . . . . . . . . . . . 13 ⊢ (◡𝐴 “ ℕ) ⊆ dom 𝐴
125		fdm 6051	. . . . . . . . . . . . . 14 ⊢ (𝐴:ℕ⟶ℕ0 → dom 𝐴 = ℕ)
126	122, 125	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → dom 𝐴 = ℕ)
127	124, 126	syl5sseq 3653	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆ ℕ)
128	127	adantr 481	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (◡𝐴 “ ℕ) ⊆ ℕ)
129		inss1 3833	. . . . . . . . . . . 12 ⊢ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ (◡𝐴 “ ℕ)
130	129, 77	sseldi 3601	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ (◡𝐴 “ ℕ))
131	128, 130	sseldd 3604	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ℕ)
132	123, 131	ffvelrnd 6360	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (𝐴‘𝑡) ∈ ℕ0)
133		bitsfi 15159	. . . . . . . . 9 ⊢ ((𝐴‘𝑡) ∈ ℕ0 → (bits‘(𝐴‘𝑡)) ∈ Fin)
134	132, 133	syl 17	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (bits‘(𝐴‘𝑡)) ∈ Fin)
135	131	nncnd 11036	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ℂ)
136		2cnd 11093	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 2 ∈ ℂ)
137		simprr 796	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 𝑛 ∈ (bits‘(𝐴‘𝑡)))
138	80, 137	sseldi 3601	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 𝑛 ∈ ℕ0)
139	136, 138	expcld 13008	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → (2↑𝑛) ∈ ℂ)
140	139	anassrs 680	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → (2↑𝑛) ∈ ℂ)
141	134, 135, 140	fsummulc1 14517	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = Σ𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡))
142	141	sumeq2dv 14433	. . . . . 6 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)Σ𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡))
143		bitsinv1 15164	. . . . . . . . 9 ⊢ ((𝐴‘𝑡) ∈ ℕ0 → Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) = (𝐴‘𝑡))
144	143	oveq1d 6665	. . . . . . . 8 ⊢ ((𝐴‘𝑡) ∈ ℕ0 → (Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = ((𝐴‘𝑡) · 𝑡))
145	132, 144	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = ((𝐴‘𝑡) · 𝑡))
146	145	sumeq2dv 14433	. . . . . 6 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)((𝐴‘𝑡) · 𝑡))
147		vex 3203	. . . . . . . . . 10 ⊢ 𝑡 ∈ V
148		vex 3203	. . . . . . . . . 10 ⊢ 𝑛 ∈ V
149	147, 148	op2ndd 7179	. . . . . . . . 9 ⊢ (𝑤 = ⟨𝑡, 𝑛⟩ → (2nd ‘𝑤) = 𝑛)
150	149	oveq2d 6666	. . . . . . . 8 ⊢ (𝑤 = ⟨𝑡, 𝑛⟩ → (2↑(2nd ‘𝑤)) = (2↑𝑛))
151	147, 148	op1std 7178	. . . . . . . 8 ⊢ (𝑤 = ⟨𝑡, 𝑛⟩ → (1st ‘𝑤) = 𝑡)
152	150, 151	oveq12d 6668	. . . . . . 7 ⊢ (𝑤 = ⟨𝑡, 𝑛⟩ → ((2↑(2nd ‘𝑤)) · (1st ‘𝑤)) = ((2↑𝑛) · 𝑡))
153		inss2 3834	. . . . . . . . . 10 ⊢ (𝑇 ∩ 𝑅) ⊆ 𝑅
154	153	sseli 3599	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ 𝑅)
155		cnveq 5296	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐴 → ◡𝑓 = ◡𝐴)
156	155	imaeq1d 5465	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐴 → (◡𝑓 “ ℕ) = (◡𝐴 “ ℕ))
157	156	eleq1d 2686	. . . . . . . . . 10 ⊢ (𝑓 = 𝐴 → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝐴 “ ℕ) ∈ Fin))
158	157, 9	elab2g 3353	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐴 ∈ 𝑅 ↔ (◡𝐴 “ ℕ) ∈ Fin))
159	154, 158	mpbid 222	. . . . . . . 8 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ∈ Fin)
160		ssfi 8180	. . . . . . . 8 ⊢ (((◡𝐴 “ ℕ) ∈ Fin ∧ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ (◡𝐴 “ ℕ)) → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ Fin)
161	159, 129, 160	sylancl 694	. . . . . . 7 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ Fin)
162	135	adantrr 753	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 𝑡 ∈ ℂ)
163	139, 162	mulcld 10060	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → ((2↑𝑛) · 𝑡) ∈ ℂ)
164	152, 161, 134, 163	fsum2d 14502	. . . . . 6 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)Σ𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = Σ𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st ‘𝑤)))
165	142, 146, 164	3eqtr3d 2664	. . . . 5 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)((𝐴‘𝑡) · 𝑡) = Σ𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st ‘𝑤)))
166		inss1 3833	. . . . . . . . 9 ⊢ (𝑇 ∩ 𝑅) ⊆ 𝑇
167	166	sseli 3599	. . . . . . . 8 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ 𝑇)
168	156	sseq1d 3632	. . . . . . . . . 10 ⊢ (𝑓 = 𝐴 → ((◡𝑓 “ ℕ) ⊆ 𝐽 ↔ (◡𝐴 “ ℕ) ⊆ 𝐽))
169	168, 10	elrab2 3366	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑇 ↔ (𝐴 ∈ (ℕ0 ↑𝑚 ℕ) ∧ (◡𝐴 “ ℕ) ⊆ 𝐽))
170	169	simprbi 480	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑇 → (◡𝐴 “ ℕ) ⊆ 𝐽)
171	167, 170	syl 17	. . . . . . 7 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆ 𝐽)
172		df-ss 3588	. . . . . . 7 ⊢ ((◡𝐴 “ ℕ) ⊆ 𝐽 ↔ ((◡𝐴 “ ℕ) ∩ 𝐽) = (◡𝐴 “ ℕ))
173	171, 172	sylib 208	. . . . . 6 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) = (◡𝐴 “ ℕ))
174	173	sumeq1d 14431	. . . . 5 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)((𝐴‘𝑡) · 𝑡) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡))
175	165, 174	eqtr3d 2658	. . . 4 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st ‘𝑤)) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡))
176	27, 118, 175	3eqtr2d 2662	. . 3 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡))
177		fveq2 6191	. . . . 5 ⊢ (𝑘 = 𝑡 → (𝐴‘𝑘) = (𝐴‘𝑡))
178		id 22	. . . . 5 ⊢ (𝑘 = 𝑡 → 𝑘 = 𝑡)
179	177, 178	oveq12d 6668	. . . 4 ⊢ (𝑘 = 𝑡 → ((𝐴‘𝑘) · 𝑘) = ((𝐴‘𝑡) · 𝑡))
180	179	cbvsumv 14426	. . 3 ⊢ Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡)
181	176, 180	syl6eqr 2674	. 2 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘))
182		0nn0 11307	. . . . . . . 8 ⊢ 0 ∈ ℕ0
183		1nn0 11308	. . . . . . . 8 ⊢ 1 ∈ ℕ0
184		prssi 4353	. . . . . . . 8 ⊢ ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
185	182, 183, 184	mp2an 708	. . . . . . 7 ⊢ {0, 1} ⊆ ℕ0
186		fss 6056	. . . . . . 7 ⊢ (((𝐺‘𝐴):ℕ⟶{0, 1} ∧ {0, 1} ⊆ ℕ0) → (𝐺‘𝐴):ℕ⟶ℕ0)
187	185, 186	mpan2 707	. . . . . 6 ⊢ ((𝐺‘𝐴):ℕ⟶{0, 1} → (𝐺‘𝐴):ℕ⟶ℕ0)
188		nn0ex 11298	. . . . . . . 8 ⊢ ℕ0 ∈ V
189		nnex 11026	. . . . . . . 8 ⊢ ℕ ∈ V
190	188, 189	elmap 7886	. . . . . . 7 ⊢ ((𝐺‘𝐴) ∈ (ℕ0 ↑𝑚 ℕ) ↔ (𝐺‘𝐴):ℕ⟶ℕ0)
191	190	biimpri 218	. . . . . 6 ⊢ ((𝐺‘𝐴):ℕ⟶ℕ0 → (𝐺‘𝐴) ∈ (ℕ0 ↑𝑚 ℕ))
192	19, 187, 191	3syl 18	. . . . 5 ⊢ ((𝐺‘𝐴) ∈ ({0, 1} ↑𝑚 ℕ) → (𝐺‘𝐴) ∈ (ℕ0 ↑𝑚 ℕ))
193	192	anim1i 592	. . . 4 ⊢ (((𝐺‘𝐴) ∈ ({0, 1} ↑𝑚 ℕ) ∧ (𝐺‘𝐴) ∈ 𝑅) → ((𝐺‘𝐴) ∈ (ℕ0 ↑𝑚 ℕ) ∧ (𝐺‘𝐴) ∈ 𝑅))
194		elin 3796	. . . 4 ⊢ ((𝐺‘𝐴) ∈ ((ℕ0 ↑𝑚 ℕ) ∩ 𝑅) ↔ ((𝐺‘𝐴) ∈ (ℕ0 ↑𝑚 ℕ) ∧ (𝐺‘𝐴) ∈ 𝑅))
195	193, 16, 194	3imtr4i 281	. . 3 ⊢ ((𝐺‘𝐴) ∈ (({0, 1} ↑𝑚 ℕ) ∩ 𝑅) → (𝐺‘𝐴) ∈ ((ℕ0 ↑𝑚 ℕ) ∩ 𝑅))
196		eulerpart.s	. . . 4 ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑𝑚 ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))
197	9, 196	eulerpartlemsv2 30420	. . 3 ⊢ ((𝐺‘𝐴) ∈ ((ℕ0 ↑𝑚 ℕ) ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘))
198	15, 195, 197	3syl 18	. 2 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘))
199	120, 154	elind 3798	. . 3 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ ((ℕ0 ↑𝑚 ℕ) ∩ 𝑅))
200	9, 196	eulerpartlemsv2 30420	. . 3 ⊢ (𝐴 ∈ ((ℕ0 ↑𝑚 ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘))
201	199, 200	syl 17	. 2 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘))
202	181, 198, 201	3eqtr4d 2666	1 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = (𝑆‘𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990  {cab 2608  ∀wral 2912  ∃wrex 2913  {crab 2916  Vcvv 3200   ∖ cdif 3571   ∩ cin 3573   ⊆ wss 3574  ∅c0 3915  ifcif 4086  𝒫 cpw 4158  {csn 4177  {cpr 4179  ⟨cop 4183  ∪ ciun 4520   class class class wbr 4653  {copab 4712   ↦ cmpt 4729   × cxp 5112  ^◡ccnv 5113  dom cdm 5114   ↾ cres 5116   “ cima 5117   ∘ ccom 5118   Fn wfn 5883  ⟶wf 5884  –1-1-onto→wf1o 5887  ‘cfv 5888  (class class class)co 6650   ↦ cmpt2 6652  1^st c1st 7166  2^nd c2nd 7167   supp csupp 7295   ↑_𝑚 cmap 7857   ≈ cen 7952  Fincfn 7955  ℂcc 9934  0cc0 9936  1c1 9937   · cmul 9941   ≤ cle 10075  ℕcn 11020  2c2 11070  ℕ₀cn0 11292  ↑cexp 12860  Σcsu 14416   ∥ cdvds 14983  bitscbits 15141  𝟭cind 30072

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-ac2 9285  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-tru 1486  df-fal 1489  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-supp 7296  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-fsupp 8276  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-acn 8768  df-ac 8939  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-ind 30073

This theorem is referenced by:  eulerpartlemn  30443