Theorem eulerpartlemgh 30908

Description: Lemma for eulerpart 30912: The 𝐹 function is a bijection on the 𝑈 subsets. (Contributed by Thierry Arnoux, 15-Aug-2018.)

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 ∘ (𝑜 ↾ 𝐽))))))
eulerpartlemgh.1	⊢ 𝑈 = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))

Assertion

Ref	Expression
eulerpartlemgh	⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐹 ↾ 𝑈):𝑈–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})

Distinct variable groups:   𝑧,𝑡   𝑓,𝑔,𝑘,𝑛,𝑡,𝐴   𝑓,𝐽,𝑛,𝑡   𝑓,𝑁,𝑘,𝑛,𝑡   𝑛,𝑂,𝑡   𝑃,𝑔,𝑘   𝑅,𝑓,𝑘,𝑛,𝑡   𝑇,𝑛,𝑡   𝑥,𝑡,𝑦,𝑧   𝑓,𝑚,𝑥,𝑔,𝑘,𝑛,𝑡,𝐴   𝑛,𝐹,𝑡,𝑥   𝑦,𝑓,𝑛   𝑥,𝐽,𝑦   𝑡,𝑃

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

Proof of Theorem eulerpartlemgh

Dummy variable 𝑝 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eulerpart.j	. . . . 5 ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
2		eulerpart.f	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
3	1, 2	oddpwdc 30884	. . . 4 ⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
4		f1of1 6323	. . . 4 ⊢ (𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ → 𝐹:(𝐽 × ℕ0)–1-1→ℕ)
5	3, 4	ax-mp 5	. . 3 ⊢ 𝐹:(𝐽 × ℕ0)–1-1→ℕ
6		eulerpartlemgh.1	. . . 4 ⊢ 𝑈 = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))
7		iunss 4719	. . . . 5 ⊢ (∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0) ↔ ∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0))
8		inss2 3995	. . . . . . . 8 ⊢ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ 𝐽
9	8	sseli 3759	. . . . . . 7 ⊢ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) → 𝑡 ∈ 𝐽)
10	9	snssd 4496	. . . . . 6 ⊢ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) → {𝑡} ⊆ 𝐽)
11		bitsss 15443	. . . . . 6 ⊢ (bits‘(𝐴‘𝑡)) ⊆ ℕ0
12		xpss12 5294	. . . . . 6 ⊢ (({𝑡} ⊆ 𝐽 ∧ (bits‘(𝐴‘𝑡)) ⊆ ℕ0) → ({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0))
13	10, 11, 12	sylancl 580	. . . . 5 ⊢ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) → ({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0))
14	7, 13	mprgbir 3074	. . . 4 ⊢ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0)
15	6, 14	eqsstri 3797	. . 3 ⊢ 𝑈 ⊆ (𝐽 × ℕ0)
16		f1ores 6338	. . 3 ⊢ ((𝐹:(𝐽 × ℕ0)–1-1→ℕ ∧ 𝑈 ⊆ (𝐽 × ℕ0)) → (𝐹 ↾ 𝑈):𝑈–1-1-onto→(𝐹 “ 𝑈))
17	5, 15, 16	mp2an 683	. 2 ⊢ (𝐹 ↾ 𝑈):𝑈–1-1-onto→(𝐹 “ 𝑈)
18		simpr 477	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) ∧ ((2↑𝑛) · 𝑡) = 𝑝) → ((2↑𝑛) · 𝑡) = 𝑝)
19		2nn 11349	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℕ
20	19	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → 2 ∈ ℕ)
21	11	sseli 3759	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (bits‘(𝐴‘𝑡)) → 𝑛 ∈ ℕ0)
22	21	adantl 473	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → 𝑛 ∈ ℕ0)
23	20, 22	nnexpcld 13242	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → (2↑𝑛) ∈ ℕ)
24		simplr 785	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → 𝑡 ∈ ℕ)
25	23, 24	nnmulcld 11329	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → ((2↑𝑛) · 𝑡) ∈ ℕ)
26	25	adantr 472	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) ∧ ((2↑𝑛) · 𝑡) = 𝑝) → ((2↑𝑛) · 𝑡) ∈ ℕ)
27	18, 26	eqeltrrd 2845	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) ∧ ((2↑𝑛) · 𝑡) = 𝑝) → 𝑝 ∈ ℕ)
28	27	exp31 410	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) → (𝑛 ∈ (bits‘(𝐴‘𝑡)) → (((2↑𝑛) · 𝑡) = 𝑝 → 𝑝 ∈ ℕ)))
29	28	rexlimdv 3177	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 → 𝑝 ∈ ℕ))
30	29	rexlimdva 3178	. . . . . . 7 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 → 𝑝 ∈ ℕ))
31	30	pm4.71rd 558	. . . . . 6 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 ↔ (𝑝 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)))
32		rex0 4104	. . . . . . . . . . . . . . 15 ⊢ ¬ ∃𝑛 ∈ ∅ ((2↑𝑛) · 𝑡) = 𝑝
33		simplr 785	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → 𝑡 ∈ ℕ)
34		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → ¬ 𝑡 ∈ (◡𝐴 “ ℕ))
35		eulerpart.p	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑𝑚 ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}
36		eulerpart.o	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
37		eulerpart.d	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}
38		eulerpart.h	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
39		eulerpart.m	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})
40		eulerpart.r	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
41		eulerpart.t	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑𝑚 ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}
42	35, 36, 37, 1, 2, 38, 39, 40, 41	eulerpartlemt0 30899	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0 ↑𝑚 ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽))
43	42	simp1bi 1175	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ (ℕ0 ↑𝑚 ℕ))
44		elmapi 8086	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∈ (ℕ0 ↑𝑚 ℕ) → 𝐴:ℕ⟶ℕ0)
45	43, 44	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴:ℕ⟶ℕ0)
46	45	ad2antrr 717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → 𝐴:ℕ⟶ℕ0)
47		ffn 6225	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴:ℕ⟶ℕ0 → 𝐴 Fn ℕ)
48		elpreima 6531	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴 Fn ℕ → (𝑡 ∈ (◡𝐴 “ ℕ) ↔ (𝑡 ∈ ℕ ∧ (𝐴‘𝑡) ∈ ℕ)))
49	46, 47, 48	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → (𝑡 ∈ (◡𝐴 “ ℕ) ↔ (𝑡 ∈ ℕ ∧ (𝐴‘𝑡) ∈ ℕ)))
50	34, 49	mtbid 315	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → ¬ (𝑡 ∈ ℕ ∧ (𝐴‘𝑡) ∈ ℕ))
51		imnan 388	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℕ → ¬ (𝐴‘𝑡) ∈ ℕ) ↔ ¬ (𝑡 ∈ ℕ ∧ (𝐴‘𝑡) ∈ ℕ))
52	50, 51	sylibr 225	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → (𝑡 ∈ ℕ → ¬ (𝐴‘𝑡) ∈ ℕ))
53	33, 52	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → ¬ (𝐴‘𝑡) ∈ ℕ)
54	46, 33	ffvelrnd 6554	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → (𝐴‘𝑡) ∈ ℕ0)
55		elnn0 11544	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴‘𝑡) ∈ ℕ0 ↔ ((𝐴‘𝑡) ∈ ℕ ∨ (𝐴‘𝑡) = 0))
56	54, 55	sylib 209	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → ((𝐴‘𝑡) ∈ ℕ ∨ (𝐴‘𝑡) = 0))
57		orel1 912	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ (𝐴‘𝑡) ∈ ℕ → (((𝐴‘𝑡) ∈ ℕ ∨ (𝐴‘𝑡) = 0) → (𝐴‘𝑡) = 0))
58	53, 56, 57	sylc 65	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → (𝐴‘𝑡) = 0)
59	58	fveq2d 6383	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → (bits‘(𝐴‘𝑡)) = (bits‘0))
60		0bits 15456	. . . . . . . . . . . . . . . . 17 ⊢ (bits‘0) = ∅
61	59, 60	syl6eq 2815	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → (bits‘(𝐴‘𝑡)) = ∅)
62	61	rexeqdv 3293	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 ↔ ∃𝑛 ∈ ∅ ((2↑𝑛) · 𝑡) = 𝑝))
63	32, 62	mtbiri 318	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → ¬ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)
64	63	ex 401	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) → (¬ 𝑡 ∈ (◡𝐴 “ ℕ) → ¬ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝))
65	64	con4d 115	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 → 𝑡 ∈ (◡𝐴 “ ℕ)))
66	65	impr 446	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ℕ ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) → 𝑡 ∈ (◡𝐴 “ ℕ))
67		eldif 3744	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (ℕ ∖ 𝐽) ↔ (𝑡 ∈ ℕ ∧ ¬ 𝑡 ∈ 𝐽))
68	35, 36, 37, 1, 2, 38, 39, 40, 41	eulerpartlemf 30900	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → (𝐴‘𝑡) = 0)
69	67, 68	sylan2br 588	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ℕ ∧ ¬ 𝑡 ∈ 𝐽)) → (𝐴‘𝑡) = 0)
70	69	anassrs 459	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ 𝐽) → (𝐴‘𝑡) = 0)
71	70	fveq2d 6383	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ 𝐽) → (bits‘(𝐴‘𝑡)) = (bits‘0))
72	71, 60	syl6eq 2815	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ 𝐽) → (bits‘(𝐴‘𝑡)) = ∅)
73	72	rexeqdv 3293	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ 𝐽) → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 ↔ ∃𝑛 ∈ ∅ ((2↑𝑛) · 𝑡) = 𝑝))
74	32, 73	mtbiri 318	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ 𝐽) → ¬ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)
75	74	ex 401	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) → (¬ 𝑡 ∈ 𝐽 → ¬ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝))
76	75	con4d 115	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 → 𝑡 ∈ 𝐽))
77	76	impr 446	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ℕ ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) → 𝑡 ∈ 𝐽)
78	66, 77	elind 3962	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ℕ ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) → 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽))
79		simprr 789	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ℕ ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) → ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)
80	78, 79	jca 507	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ℕ ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) → (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝))
81	80	ex 401	. . . . . . . 8 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝑡 ∈ ℕ ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝) → (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)))
82	81	reximdv2 3160	. . . . . . 7 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 → ∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝))
83		ssrab2 3849	. . . . . . . . . 10 ⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
84	1, 83	eqsstri 3797	. . . . . . . . 9 ⊢ 𝐽 ⊆ ℕ
85	8, 84	sstri 3772	. . . . . . . 8 ⊢ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ ℕ
86		ssrexv 3829	. . . . . . . 8 ⊢ (((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ ℕ → (∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝))
87	85, 86	mp1i 13	. . . . . . 7 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝))
88	82, 87	impbid 203	. . . . . 6 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 ↔ ∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝))
89	31, 88	bitr3d 272	. . . . 5 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝑝 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝) ↔ ∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝))
90		eqeq2 2776	. . . . . . . 8 ⊢ (𝑚 = 𝑝 → (((2↑𝑛) · 𝑡) = 𝑚 ↔ ((2↑𝑛) · 𝑡) = 𝑝))
91	90	2rexbidv 3204	. . . . . . 7 ⊢ (𝑚 = 𝑝 → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚 ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝))
92	91	elrab 3521	. . . . . 6 ⊢ (𝑝 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ↔ (𝑝 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝))
93	92	a1i 11	. . . . 5 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑝 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ↔ (𝑝 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)))
94	6	imaeq2i 5648	. . . . . . . . 9 ⊢ (𝐹 “ 𝑈) = (𝐹 “ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))))
95		imaiun 6699	. . . . . . . . 9 ⊢ (𝐹 “ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡))))
96	94, 95	eqtri 2787	. . . . . . . 8 ⊢ (𝐹 “ 𝑈) = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡))))
97	96	eleq2i 2836	. . . . . . 7 ⊢ (𝑝 ∈ (𝐹 “ 𝑈) ↔ 𝑝 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))))
98		eliun 4682	. . . . . . 7 ⊢ (𝑝 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))) ↔ ∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)𝑝 ∈ (𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))))
99		f1ofn 6325	. . . . . . . . . . . . 13 ⊢ (𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ → 𝐹 Fn (𝐽 × ℕ0))
100	3, 99	ax-mp 5	. . . . . . . . . . . 12 ⊢ 𝐹 Fn (𝐽 × ℕ0)
101		snssi 4495	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝐽 → {𝑡} ⊆ 𝐽)
102	101, 11, 12	sylancl 580	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝐽 → ({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0))
103		ovelimab 7014	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn (𝐽 × ℕ0) ∧ ({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0)) → (𝑝 ∈ (𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))) ↔ ∃𝑥 ∈ {𝑡}∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑝 = (𝑥𝐹𝑛)))
104	100, 102, 103	sylancr 581	. . . . . . . . . . 11 ⊢ (𝑡 ∈ 𝐽 → (𝑝 ∈ (𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))) ↔ ∃𝑥 ∈ {𝑡}∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑝 = (𝑥𝐹𝑛)))
105		vex 3353	. . . . . . . . . . . 12 ⊢ 𝑡 ∈ V
106		oveq1 6853	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑡 → (𝑥𝐹𝑛) = (𝑡𝐹𝑛))
107	106	eqeq2d 2775	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑡 → (𝑝 = (𝑥𝐹𝑛) ↔ 𝑝 = (𝑡𝐹𝑛)))
108	107	rexbidv 3199	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑝 = (𝑥𝐹𝑛) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑝 = (𝑡𝐹𝑛)))
109	105, 108	rexsn 4382	. . . . . . . . . . 11 ⊢ (∃𝑥 ∈ {𝑡}∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑝 = (𝑥𝐹𝑛) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑝 = (𝑡𝐹𝑛))
110	104, 109	syl6bb 278	. . . . . . . . . 10 ⊢ (𝑡 ∈ 𝐽 → (𝑝 ∈ (𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑝 = (𝑡𝐹𝑛)))
111		df-ov 6849	. . . . . . . . . . . . . . 15 ⊢ (𝑡𝐹𝑛) = (𝐹‘⟨𝑡, 𝑛⟩)
112	111	eqeq1i 2770	. . . . . . . . . . . . . 14 ⊢ ((𝑡𝐹𝑛) = 𝑝 ↔ (𝐹‘⟨𝑡, 𝑛⟩) = 𝑝)
113		eqcom 2772	. . . . . . . . . . . . . 14 ⊢ ((𝑡𝐹𝑛) = 𝑝 ↔ 𝑝 = (𝑡𝐹𝑛))
114	112, 113	bitr3i 268	. . . . . . . . . . . . 13 ⊢ ((𝐹‘⟨𝑡, 𝑛⟩) = 𝑝 ↔ 𝑝 = (𝑡𝐹𝑛))
115		opelxpi 5316	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0) → ⟨𝑡, 𝑛⟩ ∈ (𝐽 × ℕ0))
116	1, 2	oddpwdcv 30885	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑡, 𝑛⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑡, 𝑛⟩) = ((2↑(2nd ‘⟨𝑡, 𝑛⟩)) · (1st ‘⟨𝑡, 𝑛⟩)))
117		vex 3353	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑛 ∈ V
118	105, 117	op2nd 7379	. . . . . . . . . . . . . . . . . 18 ⊢ (2nd ‘⟨𝑡, 𝑛⟩) = 𝑛
119	118	oveq2i 6857	. . . . . . . . . . . . . . . . 17 ⊢ (2↑(2nd ‘⟨𝑡, 𝑛⟩)) = (2↑𝑛)
120	105, 117	op1st 7378	. . . . . . . . . . . . . . . . 17 ⊢ (1st ‘⟨𝑡, 𝑛⟩) = 𝑡
121	119, 120	oveq12i 6858	. . . . . . . . . . . . . . . 16 ⊢ ((2↑(2nd ‘⟨𝑡, 𝑛⟩)) · (1st ‘⟨𝑡, 𝑛⟩)) = ((2↑𝑛) · 𝑡)
122	116, 121	syl6eq 2815	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑡, 𝑛⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑡, 𝑛⟩) = ((2↑𝑛) · 𝑡))
123	115, 122	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0) → (𝐹‘⟨𝑡, 𝑛⟩) = ((2↑𝑛) · 𝑡))
124	123	eqeq1d 2767	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0) → ((𝐹‘⟨𝑡, 𝑛⟩) = 𝑝 ↔ ((2↑𝑛) · 𝑡) = 𝑝))
125	114, 124	syl5bbr 276	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0) → (𝑝 = (𝑡𝐹𝑛) ↔ ((2↑𝑛) · 𝑡) = 𝑝))
126	21, 125	sylan2 586	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → (𝑝 = (𝑡𝐹𝑛) ↔ ((2↑𝑛) · 𝑡) = 𝑝))
127	126	rexbidva 3196	. . . . . . . . . 10 ⊢ (𝑡 ∈ 𝐽 → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑝 = (𝑡𝐹𝑛) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝))
128	110, 127	bitrd 270	. . . . . . . . 9 ⊢ (𝑡 ∈ 𝐽 → (𝑝 ∈ (𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝))
129	9, 128	syl 17	. . . . . . . 8 ⊢ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) → (𝑝 ∈ (𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝))
130	129	rexbiia 3187	. . . . . . 7 ⊢ (∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)𝑝 ∈ (𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))) ↔ ∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)
131	97, 98, 130	3bitri 288	. . . . . 6 ⊢ (𝑝 ∈ (𝐹 “ 𝑈) ↔ ∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)
132	131	a1i 11	. . . . 5 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑝 ∈ (𝐹 “ 𝑈) ↔ ∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝))
133	89, 93, 132	3bitr4rd 303	. . . 4 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑝 ∈ (𝐹 “ 𝑈) ↔ 𝑝 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}))
134	133	eqrdv 2763	. . 3 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐹 “ 𝑈) = {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})
135		f1oeq3 6316	. . 3 ⊢ ((𝐹 “ 𝑈) = {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → ((𝐹 ↾ 𝑈):𝑈–1-1-onto→(𝐹 “ 𝑈) ↔ (𝐹 ↾ 𝑈):𝑈–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}))
136	134, 135	syl 17	. 2 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝐹 ↾ 𝑈):𝑈–1-1-onto→(𝐹 “ 𝑈) ↔ (𝐹 ↾ 𝑈):𝑈–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}))
137	17, 136	mpbii 224	1 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐹 ↾ 𝑈):𝑈–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 197   ∧ wa 384   ∨ wo 873   = wceq 1652   ∈ wcel 2155  {cab 2751  ∀wral 3055  ∃wrex 3056  {crab 3059   ∖ cdif 3731   ∩ cin 3733   ⊆ wss 3734  ∅c0 4081  𝒫 cpw 4317  {csn 4336  ⟨cop 4342  ∪ ciun 4678   class class class wbr 4811  {copab 4873   ↦ cmpt 4890   × cxp 5277  ^◡ccnv 5278   ↾ cres 5281   “ cima 5282   ∘ ccom 5283   Fn wfn 6065  ⟶wf 6066  –1-1→wf1 6067  –1-1-onto→wf1o 6069  ‘cfv 6070  (class class class)co 6846   ↦ cmpt2 6848  1^st c1st 7368  2^nd c2nd 7369   supp csupp 7501   ↑_𝑚 cmap 8064  Fincfn 8164  0cc0 10193  1c1 10194   · cmul 10198   ≤ cle 10333  ℕcn 11278  2c2 11331  ℕ₀cn0 11542  ↑cexp 13072  Σcsu 14715   ∥ cdvds 15279  bitscbits 15436  𝟭cind 30540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270  ax-pre-sup 10271

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-om 7268  df-1st 7370  df-2nd 7371  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-1o 7768  df-er 7951  df-map 8066  df-en 8165  df-dom 8166  df-sdom 8167  df-fin 8168  df-sup 8559  df-inf 8560  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10526  df-neg 10527  df-div 10943  df-nn 11279  df-2 11339  df-n0 11543  df-z 11629  df-uz 11892  df-rp 12034  df-fz 12539  df-fzo 12679  df-fl 12806  df-seq 13014  df-exp 13073  df-dvds 15280  df-bits 15439

This theorem is referenced by:  eulerpartlemgs2  30910