Theorem eulerpartlemgs2 34679

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

Hypotheses

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

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 6071	. . . . . . . 8 ⊢ (◡(𝐺‘𝐴) “ ℕ) ⊆ dom (𝐺‘𝐴)
2		eulerpart.p	. . . . . . . . . . . . . 14 ⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ 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) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
8		eulerpart.m	. . . . . . . . . . . . . 14 ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})
9		eulerpart.r	. . . . . . . . . . . . . 14 ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
10		eulerpart.t	. . . . . . . . . . . . . 14 ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}
11		eulerpart.g	. . . . . . . . . . . . . 14 ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
12	2, 3, 4, 5, 6, 7, 8, 9, 10, 11	eulerpartgbij 34671	. . . . . . . . . . . . 13 ⊢ 𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅)
13		f1of 6806	. . . . . . . . . . . . 13 ⊢ (𝐺:(𝑇 ∩ 𝑅)–1-1-onto→(({0, 1} ↑m ℕ) ∩ 𝑅) → 𝐺:(𝑇 ∩ 𝑅)⟶(({0, 1} ↑m ℕ) ∩ 𝑅))
14	12, 13	ax-mp 5	. . . . . . . . . . . 12 ⊢ 𝐺:(𝑇 ∩ 𝑅)⟶(({0, 1} ↑m ℕ) ∩ 𝑅)
15	14	ffvelcdmi 7064	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) ∈ (({0, 1} ↑m ℕ) ∩ 𝑅))
16		elin 3921	. . . . . . . . . . 11 ⊢ ((𝐺‘𝐴) ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) ↔ ((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ) ∧ (𝐺‘𝐴) ∈ 𝑅))
17	15, 16	sylib 220	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ) ∧ (𝐺‘𝐴) ∈ 𝑅))
18	17	simpld 498	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ))
19		elmapi 8830	. . . . . . . . 9 ⊢ ((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ) → (𝐺‘𝐴):ℕ⟶{0, 1})
20		fdm 6701	. . . . . . . . 9 ⊢ ((𝐺‘𝐴):ℕ⟶{0, 1} → dom (𝐺‘𝐴) = ℕ)
21	18, 19, 20	3syl 18	. . . . . . . 8 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → dom (𝐺‘𝐴) = ℕ)
22	1, 21	sseqtrid 3979	. . . . . . 7 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡(𝐺‘𝐴) “ ℕ) ⊆ ℕ)
23	22	sselda 3937	. . . . . 6 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)) → 𝑘 ∈ ℕ)
24	2, 3, 4, 5, 6, 7, 8, 9, 10, 11	eulerpartlemgvv 34675	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ℕ) → ((𝐺‘𝐴)‘𝑘) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0))
25	24	oveq1d 7411	. . . . . 6 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ℕ) → (((𝐺‘𝐴)‘𝑘) · 𝑘) = (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘))
26	23, 25	syldan 600	. . . . 5 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)) → (((𝐺‘𝐴)‘𝑘) · 𝑘) = (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘))
27	26	sumeq2dv 15739	. . . 4 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘))
28		eqeq2 2775	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑘 → (((2↑𝑛) · 𝑡) = 𝑚 ↔ ((2↑𝑛) · 𝑡) = 𝑘))
29	28	2rexbidv 3228	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑘 → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚 ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘))
30	29	elrab 3651	. . . . . . . . . . 11 ⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ↔ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘))
31	30	simprbi 501	. . . . . . . . . 10 ⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)
32	31	iftrued 4489	. . . . . . . . 9 ⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 1)
33	32	oveq1d 7411	. . . . . . . 8 ⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = (1 · 𝑘))
34		elrabi 3647	. . . . . . . . . 10 ⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ ℕ)
35	34	nncnd 12236	. . . . . . . . 9 ⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ ℂ)
36	35	mullidd 11211	. . . . . . . 8 ⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (1 · 𝑘) = 𝑘)
37	33, 36	eqtrd 2798	. . . . . . 7 ⊢ (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = 𝑘)
38	37	sumeq2i 15735	. . . . . 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 34678	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡(𝐺‘𝐴) “ ℕ) ∈ Fin)
41	34	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℕ)
42	41, 24	syldan 600	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺‘𝐴)‘𝑘) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0))
43	31	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)
44	43	iftrued 4489	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 1)
45	42, 44	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺‘𝐴)‘𝑘) = 1)
46		1nn 12231	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ
47	45, 46	eqeltrdi 2871	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ((𝐺‘𝐴)‘𝑘) ∈ ℕ)
48		ffn 6691	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝐴):ℕ⟶{0, 1} → (𝐺‘𝐴) Fn ℕ)
49		elpreima 7039	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝐴) Fn ℕ → (𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺‘𝐴)‘𝑘) ∈ ℕ)))
50	18, 19, 48, 49	4syl 19	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺‘𝐴)‘𝑘) ∈ ℕ)))
51	50	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → (𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ) ↔ (𝑘 ∈ ℕ ∧ ((𝐺‘𝐴)‘𝑘) ∈ ℕ)))
52	41, 47, 51	mpbir2and 723	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ))
53	52	ex 416	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → 𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)))
54	53	ssrdv 3943	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ (◡(𝐺‘𝐴) “ ℕ))
55		ssfi 9141	. . . . . . . . 9 ⊢ (((◡(𝐺‘𝐴) “ ℕ) ∈ Fin ∧ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ (◡(𝐺‘𝐴) “ ℕ)) → {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin)
56	40, 54, 55	syl2anc 593	. . . . . . . 8 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin)
57		cnvexg 7905	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ◡𝐴 ∈ V)
58		imaexg 7894	. . . . . . . . . . 11 ⊢ (◡𝐴 ∈ V → (◡𝐴 “ ℕ) ∈ V)
59		inex1g 5276	. . . . . . . . . . 11 ⊢ ((◡𝐴 “ ℕ) ∈ V → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ V)
60	57, 58, 59	3syl 18	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ V)
61		vsnex 5393	. . . . . . . . . . . 12 ⊢ {𝑡} ∈ V
62		fvex 6880	. . . . . . . . . . . 12 ⊢ (bits‘(𝐴‘𝑡)) ∈ V
63	61, 62	xpex 7736	. . . . . . . . . . 11 ⊢ ({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V
64	63	rgenw 3081	. . . . . . . . . 10 ⊢ ∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V
65		iunexg 7944	. . . . . . . . . 10 ⊢ ((((◡𝐴 “ ℕ) ∩ 𝐽) ∈ V ∧ ∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V)
66	60, 64, 65	sylancl 595	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V)
67		eqid 2763	. . . . . . . . . 10 ⊢ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))
68	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 67	eulerpartlemgh 34677	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐹 ↾ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))):∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})
69		f1oeng 8951	. . . . . . . . 9 ⊢ ((∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ V ∧ (𝐹 ↾ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))):∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ≈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})
70	66, 68, 69	syl2anc 593	. . . . . . . 8 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ≈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})
71		enfii 9154	. . . . . . . 8 ⊢ (({𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ∈ Fin ∧ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ≈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ Fin)
72	56, 70, 71	syl2anc 593	. . . . . . 7 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ∈ Fin)
73		fvres 6886	. . . . . . . . 9 ⊢ (𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) → ((𝐹 ↾ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))))‘𝑤) = (𝐹‘𝑤))
74	73	adantl 485	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → ((𝐹 ↾ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))))‘𝑤) = (𝐹‘𝑤))
75		inss2 4190	. . . . . . . . . . . . . . 15 ⊢ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ 𝐽
76		simpr 488	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽))
77	75, 76	sselid 3935	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ 𝐽)
78	77	snssd 4746	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → {𝑡} ⊆ 𝐽)
79		bitsss 16470	. . . . . . . . . . . . 13 ⊢ (bits‘(𝐴‘𝑡)) ⊆ ℕ0
80		xpss12 5663	. . . . . . . . . . . . 13 ⊢ (({𝑡} ⊆ 𝐽 ∧ (bits‘(𝐴‘𝑡)) ⊆ ℕ0) → ({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0))
81	78, 79, 80	sylancl 595	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → ({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0))
82	81	ralrimiva 3155	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0))
83		iunss 5003	. . . . . . . . . . 11 ⊢ (∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0) ↔ ∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0))
84	82, 83	sylibr 236	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0))
85	84	sselda 3937	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → 𝑤 ∈ (𝐽 × ℕ0))
86	5, 6	oddpwdcv 34654	. . . . . . . . 9 ⊢ (𝑤 ∈ (𝐽 × ℕ0) → (𝐹‘𝑤) = ((2↑(2nd ‘𝑤)) · (1st ‘𝑤)))
87	85, 86	syl 17	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → (𝐹‘𝑤) = ((2↑(2nd ‘𝑤)) · (1st ‘𝑤)))
88	74, 87	eqtrd 2798	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) → ((𝐹 ↾ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))))‘𝑤) = ((2↑(2nd ‘𝑤)) · (1st ‘𝑤)))
89	41	nncnd 12236	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℂ)
90	39, 72, 68, 88, 89	fsumf1o 15760	. . . . . 6 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}𝑘 = Σ𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st ‘𝑤)))
91	38, 90	eqtrid 2810	. . . . 5 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = Σ𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st ‘𝑤)))
92		ax-1cn 11142	. . . . . . . . 9 ⊢ 1 ∈ ℂ
93		0cn 11182	. . . . . . . . 9 ⊢ 0 ∈ ℂ
94	92, 93	ifcli 4529	. . . . . . . 8 ⊢ if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) ∈ ℂ
95	94	a1i 11	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) ∈ ℂ)
96		ssrab2 4034	. . . . . . . . 9 ⊢ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ⊆ ℕ
97		simpr 488	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})
98	96, 97	sselid 3935	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℕ)
99	98	nncnd 12236	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → 𝑘 ∈ ℂ)
100	95, 99	mulcld 11213	. . . . . 6 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) ∈ ℂ)
101		simpr 488	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}))
102	101	eldifbd 3918	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → ¬ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})
103	22	ssdifssd 4101	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) ⊆ ℕ)
104	103	sselda 3937	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ ℕ)
105	30	notbii 322	. . . . . . . . . . 11 ⊢ (¬ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ↔ ¬ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘))
106		imnan 403	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ → ¬ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘) ↔ ¬ (𝑘 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘))
107	105, 106	sylbb2 240	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → (𝑘 ∈ ℕ → ¬ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘))
108	102, 104, 107	sylc 65	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → ¬ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘)
109	108	iffalsed 4492	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) = 0)
110	109	oveq1d 7411	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = (0 · 𝑘))
111		nnsscn 12225	. . . . . . . . . 10 ⊢ ℕ ⊆ ℂ
112	103, 111	sstrdi 3949	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) ⊆ ℂ)
113	112	sselda 3937	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → 𝑘 ∈ ℂ)
114	113	mul02d 11392	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (0 · 𝑘) = 0)
115	110, 114	eqtrd 2798	. . . . . 6 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑘 ∈ ((◡(𝐺‘𝐴) “ ℕ) ∖ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) → (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = 0)
116	54, 100, 115, 40	fsumss 15762	. . . . 5 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} (if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘))
117	91, 116	eqtr3d 2800	. . . 4 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st ‘𝑤)) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑘, 1, 0) · 𝑘))
118	2, 3, 4, 5, 6, 7, 8, 9, 10	eulerpartlemt0 34668	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0 ↑m ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽))
119	118	simp1bi 1159	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ (ℕ0 ↑m ℕ))
120		elmapi 8830	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (ℕ0 ↑m ℕ) → 𝐴:ℕ⟶ℕ0)
121	119, 120	syl 17	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴:ℕ⟶ℕ0)
122	121	adantr 484	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝐴:ℕ⟶ℕ0)
123		cnvimass 6071	. . . . . . . . . . . . 13 ⊢ (◡𝐴 “ ℕ) ⊆ dom 𝐴
124	123, 121	fssdm 6711	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆ ℕ)
125	124	adantr 484	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (◡𝐴 “ ℕ) ⊆ ℕ)
126		inss1 4189	. . . . . . . . . . . 12 ⊢ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ (◡𝐴 “ ℕ)
127	126, 76	sselid 3935	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ (◡𝐴 “ ℕ))
128	125, 127	sseldd 3938	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ℕ)
129	122, 128	ffvelcdmd 7066	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (𝐴‘𝑡) ∈ ℕ0)
130		bitsfi 16481	. . . . . . . . 9 ⊢ ((𝐴‘𝑡) ∈ ℕ0 → (bits‘(𝐴‘𝑡)) ∈ Fin)
131	129, 130	syl 17	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (bits‘(𝐴‘𝑡)) ∈ Fin)
132	128	nncnd 12236	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → 𝑡 ∈ ℂ)
133		2cnd 12306	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 2 ∈ ℂ)
134		simprr 782	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 𝑛 ∈ (bits‘(𝐴‘𝑡)))
135	79, 134	sselid 3935	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 𝑛 ∈ ℕ0)
136	133, 135	expcld 14169	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → (2↑𝑛) ∈ ℂ)
137	136	anassrs 471	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → (2↑𝑛) ∈ ℂ)
138	131, 132, 137	fsummulc1 15822	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = Σ𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡))
139	138	sumeq2dv 15739	. . . . . 6 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)Σ𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡))
140		bitsinv1 16486	. . . . . . . . 9 ⊢ ((𝐴‘𝑡) ∈ ℕ0 → Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) = (𝐴‘𝑡))
141	140	oveq1d 7411	. . . . . . . 8 ⊢ ((𝐴‘𝑡) ∈ ℕ0 → (Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = ((𝐴‘𝑡) · 𝑡))
142	129, 141	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) → (Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = ((𝐴‘𝑡) · 𝑡))
143	142	sumeq2dv 15739	. . . . . 6 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(Σ𝑛 ∈ (bits‘(𝐴‘𝑡))(2↑𝑛) · 𝑡) = Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)((𝐴‘𝑡) · 𝑡))
144		vex 3459	. . . . . . . . . 10 ⊢ 𝑡 ∈ V
145		vex 3459	. . . . . . . . . 10 ⊢ 𝑛 ∈ V
146	144, 145	op2ndd 7981	. . . . . . . . 9 ⊢ (𝑤 = ⟨𝑡, 𝑛⟩ → (2nd ‘𝑤) = 𝑛)
147	146	oveq2d 7412	. . . . . . . 8 ⊢ (𝑤 = ⟨𝑡, 𝑛⟩ → (2↑(2nd ‘𝑤)) = (2↑𝑛))
148	144, 145	op1std 7980	. . . . . . . 8 ⊢ (𝑤 = ⟨𝑡, 𝑛⟩ → (1st ‘𝑤) = 𝑡)
149	147, 148	oveq12d 7414	. . . . . . 7 ⊢ (𝑤 = ⟨𝑡, 𝑛⟩ → ((2↑(2nd ‘𝑤)) · (1st ‘𝑤)) = ((2↑𝑛) · 𝑡))
150		inss2 4190	. . . . . . . . . 10 ⊢ (𝑇 ∩ 𝑅) ⊆ 𝑅
151	150	sseli 3933	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ 𝑅)
152		cnveq 5846	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐴 → ◡𝑓 = ◡𝐴)
153	152	imaeq1d 6048	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐴 → (◡𝑓 “ ℕ) = (◡𝐴 “ ℕ))
154	153	eleq1d 2848	. . . . . . . . . 10 ⊢ (𝑓 = 𝐴 → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝐴 “ ℕ) ∈ Fin))
155	154, 9	elab2g 3640	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐴 ∈ 𝑅 ↔ (◡𝐴 “ ℕ) ∈ Fin))
156	151, 155	mpbid 234	. . . . . . . 8 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ∈ Fin)
157		ssfi 9141	. . . . . . . 8 ⊢ (((◡𝐴 “ ℕ) ∈ Fin ∧ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ (◡𝐴 “ ℕ)) → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ Fin)
158	156, 126, 157	sylancl 595	. . . . . . 7 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) ∈ Fin)
159	132	adantrr 727	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → 𝑡 ∈ ℂ)
160	136, 159	mulcld 11213	. . . . . . 7 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → ((2↑𝑛) · 𝑡) ∈ ℂ)
161	149, 158, 131, 160	fsum2d 15808	. . . . . 6 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)Σ𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = Σ𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st ‘𝑤)))
162	139, 143, 161	3eqtr3d 2806	. . . . 5 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)((𝐴‘𝑡) · 𝑡) = Σ𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st ‘𝑤)))
163		inss1 4189	. . . . . . . . 9 ⊢ (𝑇 ∩ 𝑅) ⊆ 𝑇
164	163	sseli 3933	. . . . . . . 8 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ 𝑇)
165	153	sseq1d 3968	. . . . . . . . . 10 ⊢ (𝑓 = 𝐴 → ((◡𝑓 “ ℕ) ⊆ 𝐽 ↔ (◡𝐴 “ ℕ) ⊆ 𝐽))
166	165, 10	elrab2 3655	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑇 ↔ (𝐴 ∈ (ℕ0 ↑m ℕ) ∧ (◡𝐴 “ ℕ) ⊆ 𝐽))
167	166	simprbi 501	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑇 → (◡𝐴 “ ℕ) ⊆ 𝐽)
168	164, 167	syl 17	. . . . . . 7 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆ 𝐽)
169		dfss2 3923	. . . . . . 7 ⊢ ((◡𝐴 “ ℕ) ⊆ 𝐽 ↔ ((◡𝐴 “ ℕ) ∩ 𝐽) = (◡𝐴 “ ℕ))
170	168, 169	sylib 220	. . . . . 6 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((◡𝐴 “ ℕ) ∩ 𝐽) = (◡𝐴 “ ℕ))
171	170	sumeq1d 15737	. . . . 5 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)((𝐴‘𝑡) · 𝑡) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡))
172	162, 171	eqtr3d 2800	. . . 4 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑤 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))((2↑(2nd ‘𝑤)) · (1st ‘𝑤)) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡))
173	27, 117, 172	3eqtr2d 2804	. . 3 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡))
174		fveq2 6867	. . . . 5 ⊢ (𝑘 = 𝑡 → (𝐴‘𝑘) = (𝐴‘𝑡))
175		id 22	. . . . 5 ⊢ (𝑘 = 𝑡 → 𝑘 = 𝑡)
176	174, 175	oveq12d 7414	. . . 4 ⊢ (𝑘 = 𝑡 → ((𝐴‘𝑘) · 𝑘) = ((𝐴‘𝑡) · 𝑡))
177	176	cbvsumv 15733	. . 3 ⊢ Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘) = Σ𝑡 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑡) · 𝑡)
178	173, 177	eqtr4di 2816	. 2 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘))
179		0nn0 12506	. . . . . . . 8 ⊢ 0 ∈ ℕ0
180		1nn0 12507	. . . . . . . 8 ⊢ 1 ∈ ℕ0
181		prssi 4780	. . . . . . . 8 ⊢ ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1} ⊆ ℕ0)
182	179, 180, 181	mp2an 702	. . . . . . 7 ⊢ {0, 1} ⊆ ℕ0
183		fss 6708	. . . . . . 7 ⊢ (((𝐺‘𝐴):ℕ⟶{0, 1} ∧ {0, 1} ⊆ ℕ0) → (𝐺‘𝐴):ℕ⟶ℕ0)
184	182, 183	mpan2 701	. . . . . 6 ⊢ ((𝐺‘𝐴):ℕ⟶{0, 1} → (𝐺‘𝐴):ℕ⟶ℕ0)
185		nn0ex 12497	. . . . . . . 8 ⊢ ℕ0 ∈ V
186		nnex 12226	. . . . . . . 8 ⊢ ℕ ∈ V
187	185, 186	elmap 8853	. . . . . . 7 ⊢ ((𝐺‘𝐴) ∈ (ℕ0 ↑m ℕ) ↔ (𝐺‘𝐴):ℕ⟶ℕ0)
188	187	biimpri 230	. . . . . 6 ⊢ ((𝐺‘𝐴):ℕ⟶ℕ0 → (𝐺‘𝐴) ∈ (ℕ0 ↑m ℕ))
189	19, 184, 188	3syl 18	. . . . 5 ⊢ ((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ) → (𝐺‘𝐴) ∈ (ℕ0 ↑m ℕ))
190	189	anim1i 624	. . . 4 ⊢ (((𝐺‘𝐴) ∈ ({0, 1} ↑m ℕ) ∧ (𝐺‘𝐴) ∈ 𝑅) → ((𝐺‘𝐴) ∈ (ℕ0 ↑m ℕ) ∧ (𝐺‘𝐴) ∈ 𝑅))
191		elin 3921	. . . 4 ⊢ ((𝐺‘𝐴) ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↔ ((𝐺‘𝐴) ∈ (ℕ0 ↑m ℕ) ∧ (𝐺‘𝐴) ∈ 𝑅))
192	190, 16, 191	3imtr4i 294	. . 3 ⊢ ((𝐺‘𝐴) ∈ (({0, 1} ↑m ℕ) ∩ 𝑅) → (𝐺‘𝐴) ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅))
193		eulerpart.s	. . . 4 ⊢ 𝑆 = (𝑓 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) ↦ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘))
194	9, 193	eulerpartlemsv2 34657	. . 3 ⊢ ((𝐺‘𝐴) ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘))
195	15, 192, 194	3syl 18	. 2 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = Σ𝑘 ∈ (◡(𝐺‘𝐴) “ ℕ)(((𝐺‘𝐴)‘𝑘) · 𝑘))
196	119, 151	elind 4153	. . 3 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅))
197	9, 193	eulerpartlemsv2 34657	. . 3 ⊢ (𝐴 ∈ ((ℕ0 ↑m ℕ) ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘))
198	196, 197	syl 17	. 2 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘𝐴) = Σ𝑘 ∈ (◡𝐴 “ ℕ)((𝐴‘𝑘) · 𝑘))
199	178, 195, 198	3eqtr4d 2808	1 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑆‘(𝐺‘𝐴)) = (𝑆‘𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1561   ∈ wcel 2143  {cab 2741  ∀wral 3077  ∃wrex 3087  {crab 3415  Vcvv 3455   ∖ cdif 3902   ∩ cin 3904   ⊆ wss 3905  ∅c0 4286  ifcif 4481  𝒫 cpw 4556  {csn 4583  {cpr 4585  ⟨cop 4589  ∪ ciun 4950   class class class wbr 5101  {copab 5163   ↦ cmpt 5182   × cxp 5646  ^◡ccnv 5647  dom cdm 5648   ↾ cres 5650   “ cima 5651   ∘ ccom 5652   Fn wfn 6516  ⟶wf 6517  –1-1-onto→wf1o 6520  ‘cfv 6521  (class class class)co 7396   ∈ cmpo 7398  1^st c1st 7968  2^nd c2nd 7969   supp csupp 8140   ↑_m cmap 8808   ≈ cen 8924  Fincfn 8927  ℂcc 11082  0cc0 11084  1c1 11085   · cmul 11089   ≤ cle 11228  𝟭cind 12205  ℕcn 12220  2c2 12282  ℕ₀cn0 12491  ↑cexp 14084  Σcsu 15723   ∥ cdvds 16296  bitscbits 16463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5228  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7718  ax-inf2 9594  ax-ac2 10431  ax-cnex 11140  ax-resscn 11141  ax-1cn 11142  ax-icn 11143  ax-addcl 11144  ax-addrcl 11145  ax-mulcl 11146  ax-mulrcl 11147  ax-mulcom 11148  ax-addass 11149  ax-mulass 11150  ax-distr 11151  ax-i2m1 11152  ax-1ne0 11153  ax-1rid 11154  ax-rnegex 11155  ax-rrecex 11156  ax-cnre 11157  ax-pre-lttri 11158  ax-pre-lttrn 11159  ax-pre-ltadd 11160  ax-pre-mulgt0 11161  ax-pre-sup 11162

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-disj 5069  df-br 5102  df-opab 5164  df-mpt 5183  df-tr 5209  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-se 5602  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-isom 6530  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-1st 7970  df-2nd 7971  df-supp 8141  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-1o 8437  df-2o 8438  df-oadd 8441  df-er 8678  df-map 8810  df-pm 8811  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-fsupp 9306  df-sup 9386  df-inf 9387  df-oi 9456  df-dju 9871  df-card 9909  df-acn 9912  df-ac 10084  df-pnf 11229  df-mnf 11230  df-xr 11231  df-ltxr 11232  df-le 11233  df-sub 11427  df-neg 11428  df-div 11856  df-ind 12206  df-nn 12221  df-2 12290  df-3 12291  df-n0 12492  df-xnn0 12565  df-z 12579  df-uz 12850  df-rp 13004  df-fz 13523  df-fzo 13670  df-fl 13812  df-mod 13890  df-seq 14025  df-exp 14085  df-hash 14354  df-cj 15136  df-re 15137  df-im 15138  df-sqrt 15272  df-abs 15273  df-clim 15525  df-sum 15724  df-dvds 16297  df-bits 16466

This theorem is referenced by:  eulerpartlemn  34680