Theorem eulerpartlemgvv 31036

Description: Lemma for eulerpart 31042: value of the function 𝐺 evaluated. (Contributed by Thierry Arnoux, 10-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 ∘ (𝑜 ↾ 𝐽))))))

Assertion

Ref	Expression
eulerpartlemgvv	⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → ((𝐺‘𝐴)‘𝐵) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵, 1, 0))

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

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

Proof of Theorem eulerpartlemgvv

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eulerpart.p	. . . . 5 ⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑𝑚 ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}
2		eulerpart.o	. . . . 5 ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
3		eulerpart.d	. . . . 5 ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}
4		eulerpart.j	. . . . 5 ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
5		eulerpart.f	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
6		eulerpart.h	. . . . 5 ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
7		eulerpart.m	. . . . 5 ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})
8		eulerpart.r	. . . . 5 ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
9		eulerpart.t	. . . . 5 ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑𝑚 ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}
10		eulerpart.g	. . . . 5 ⊢ 𝐺 = (𝑜 ∈ (𝑇 ∩ 𝑅) ↦ ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝑜 ↾ 𝐽))))))
11	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	eulerpartlemgv 31033	. . . 4 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))))))
12	11	fveq1d 6448	. . 3 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝐺‘𝐴)‘𝐵) = (((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))))‘𝐵))
13	12	adantr 474	. 2 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → ((𝐺‘𝐴)‘𝐵) = (((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))))‘𝐵))
14		nnex 11381	. . 3 ⊢ ℕ ∈ V
15		imassrn 5731	. . . 4 ⊢ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ⊆ ran 𝐹
16	4, 5	oddpwdc 31014	. . . . 5 ⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
17		f1of 6391	. . . . 5 ⊢ (𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ → 𝐹:(𝐽 × ℕ0)⟶ℕ)
18		frn 6297	. . . . 5 ⊢ (𝐹:(𝐽 × ℕ0)⟶ℕ → ran 𝐹 ⊆ ℕ)
19	16, 17, 18	mp2b 10	. . . 4 ⊢ ran 𝐹 ⊆ ℕ
20	15, 19	sstri 3830	. . 3 ⊢ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ⊆ ℕ
21		simpr 479	. . 3 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → 𝐵 ∈ ℕ)
22		indfval 30676	. . 3 ⊢ ((ℕ ∈ V ∧ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ⊆ ℕ ∧ 𝐵 ∈ ℕ) → (((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))))‘𝐵) = if(𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))), 1, 0))
23	14, 20, 21, 22	mp3an12i 1538	. 2 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → (((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))))‘𝐵) = if(𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))), 1, 0))
24		ffn 6291	. . . . . 6 ⊢ (𝐹:(𝐽 × ℕ0)⟶ℕ → 𝐹 Fn (𝐽 × ℕ0))
25	16, 17, 24	mp2b 10	. . . . 5 ⊢ 𝐹 Fn (𝐽 × ℕ0)
26	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	eulerpartlemmf 31035	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (bits ∘ (𝐴 ↾ 𝐽)) ∈ 𝐻)
27	1, 2, 3, 4, 5, 6, 7	eulerpartlem1 31027	. . . . . . . . . . 11 ⊢ 𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
28		f1of 6391	. . . . . . . . . . 11 ⊢ (𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) → 𝑀:𝐻⟶(𝒫 (𝐽 × ℕ0) ∩ Fin))
29	27, 28	ax-mp 5	. . . . . . . . . 10 ⊢ 𝑀:𝐻⟶(𝒫 (𝐽 × ℕ0) ∩ Fin)
30	29	ffvelrni 6622	. . . . . . . . 9 ⊢ ((bits ∘ (𝐴 ↾ 𝐽)) ∈ 𝐻 → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
31	26, 30	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩ Fin))
32	31	elin1d 4025	. . . . . . 7 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ∈ 𝒫 (𝐽 × ℕ0))
33	32	adantr 474	. . . . . 6 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ∈ 𝒫 (𝐽 × ℕ0))
34	33	elpwid 4391	. . . . 5 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ⊆ (𝐽 × ℕ0))
35		fvelimab 6513	. . . . 5 ⊢ ((𝐹 Fn (𝐽 × ℕ0) ∧ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ⊆ (𝐽 × ℕ0)) → (𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ↔ ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵))
36	25, 34, 35	sylancr 581	. . . 4 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → (𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ↔ ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵))
37	4	ssrab3 3909	. . . . . . . . 9 ⊢ 𝐽 ⊆ ℕ
38		fveq1 6445	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = (bits ∘ (𝐴 ↾ 𝐽)) → (𝑟‘𝑥) = ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))
39	38	eleq2d 2845	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = (bits ∘ (𝐴 ↾ 𝐽)) → (𝑦 ∈ (𝑟‘𝑥) ↔ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)))
40	39	anbi2d 622	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = (bits ∘ (𝐴 ↾ 𝐽)) → ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥)) ↔ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))))
41	40	opabbidv 4952	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = (bits ∘ (𝐴 ↾ 𝐽)) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))})
42	14, 37	ssexi 5040	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐽 ∈ V
43		abid2 2912	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑦 ∣ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)} = ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)
44	43	fvexi 6460	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∣ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)} ∈ V
45	44	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐽 → {𝑦 ∣ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)} ∈ V)
46	42, 45	opabex3 7424	. . . . . . . . . . . . . . . . 17 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))} ∈ V
47	46	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))} ∈ V)
48	7, 41, 26, 47	fvmptd3 6564	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))})
49		simpl 476	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → 𝑥 = 𝑡)
50	49	eleq1d 2844	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → (𝑥 ∈ 𝐽 ↔ 𝑡 ∈ 𝐽))
51		simpr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → 𝑦 = 𝑛)
52	49	fveq2d 6450	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) = ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))
53	51, 52	eleq12d 2853	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → (𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) ↔ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡)))
54	50, 53	anbi12d 624	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)) ↔ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))))
55	54	cbvopabv 4958	. . . . . . . . . . . . . . 15 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))} = {⟨𝑡, 𝑛⟩ ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))}
56	48, 55	syl6eq 2830	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) = {⟨𝑡, 𝑛⟩ ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))})
57	56	eleq2d 2845	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ↔ 𝑤 ∈ {⟨𝑡, 𝑛⟩ ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))}))
58	1, 2, 3, 4, 5, 6, 7, 8, 9	eulerpartlemt0 31029	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0 ↑𝑚 ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽))
59	58	simp1bi 1136	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ (ℕ0 ↑𝑚 ℕ))
60		nn0ex 11649	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℕ0 ∈ V
61	60, 14	elmap 8169	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴 ∈ (ℕ0 ↑𝑚 ℕ) ↔ 𝐴:ℕ⟶ℕ0)
62	59, 61	sylib 210	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴:ℕ⟶ℕ0)
63		ffun 6294	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴:ℕ⟶ℕ0 → Fun 𝐴)
64		funres 6177	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Fun 𝐴 → Fun (𝐴 ↾ 𝐽))
65	62, 63, 64	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Fun (𝐴 ↾ 𝐽))
66		fssres 6320	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴:ℕ⟶ℕ0 ∧ 𝐽 ⊆ ℕ) → (𝐴 ↾ 𝐽):𝐽⟶ℕ0)
67	62, 37, 66	sylancl 580	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐴 ↾ 𝐽):𝐽⟶ℕ0)
68		fdm 6299	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ↾ 𝐽):𝐽⟶ℕ0 → dom (𝐴 ↾ 𝐽) = 𝐽)
69	68	eleq2d 2845	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ↾ 𝐽):𝐽⟶ℕ0 → (𝑡 ∈ dom (𝐴 ↾ 𝐽) ↔ 𝑡 ∈ 𝐽))
70	67, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑡 ∈ dom (𝐴 ↾ 𝐽) ↔ 𝑡 ∈ 𝐽))
71	70	biimpar 471	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ 𝐽) → 𝑡 ∈ dom (𝐴 ↾ 𝐽))
72		fvco 6534	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Fun (𝐴 ↾ 𝐽) ∧ 𝑡 ∈ dom (𝐴 ↾ 𝐽)) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡) = (bits‘((𝐴 ↾ 𝐽)‘𝑡)))
73	65, 71, 72	syl2an2r 675	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ 𝐽) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡) = (bits‘((𝐴 ↾ 𝐽)‘𝑡)))
74		fvres 6465	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ 𝐽 → ((𝐴 ↾ 𝐽)‘𝑡) = (𝐴‘𝑡))
75	74	fveq2d 6450	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ 𝐽 → (bits‘((𝐴 ↾ 𝐽)‘𝑡)) = (bits‘(𝐴‘𝑡)))
76	75	adantl 475	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ 𝐽) → (bits‘((𝐴 ↾ 𝐽)‘𝑡)) = (bits‘(𝐴‘𝑡)))
77	73, 76	eqtrd 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ 𝐽) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡) = (bits‘(𝐴‘𝑡)))
78	77	eleq2d 2845	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ 𝐽) → (𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡) ↔ 𝑛 ∈ (bits‘(𝐴‘𝑡))))
79	78	pm5.32da 574	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡)) ↔ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))))
80	79	opabbidv 4952	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → {⟨𝑡, 𝑛⟩ ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))} = {⟨𝑡, 𝑛⟩ ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))})
81	80	eleq2d 2845	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑤 ∈ {⟨𝑡, 𝑛⟩ ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))} ↔ 𝑤 ∈ {⟨𝑡, 𝑛⟩ ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))}))
82		elopab 5220	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ {⟨𝑡, 𝑛⟩ ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))} ↔ ∃𝑡∃𝑛(𝑤 = ⟨𝑡, 𝑛⟩ ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))))
83	81, 82	syl6bb 279	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑤 ∈ {⟨𝑡, 𝑛⟩ ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))} ↔ ∃𝑡∃𝑛(𝑤 = ⟨𝑡, 𝑛⟩ ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))))))
84		ancom 454	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 = ⟨𝑡, 𝑛⟩ ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ↔ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) ∧ 𝑤 = ⟨𝑡, 𝑛⟩))
85		anass 462	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) ∧ 𝑤 = ⟨𝑡, 𝑛⟩) ↔ (𝑡 ∈ 𝐽 ∧ (𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩)))
86	84, 85	bitri 267	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 = ⟨𝑡, 𝑛⟩ ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ↔ (𝑡 ∈ 𝐽 ∧ (𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩)))
87	86	2exbii 1893	. . . . . . . . . . . . . . 15 ⊢ (∃𝑡∃𝑛(𝑤 = ⟨𝑡, 𝑛⟩ ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ↔ ∃𝑡∃𝑛(𝑡 ∈ 𝐽 ∧ (𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩)))
88		df-rex 3096	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = ⟨𝑡, 𝑛⟩ ↔ ∃𝑛(𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩))
89	88	anbi2i 616	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ∈ 𝐽 ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = ⟨𝑡, 𝑛⟩) ↔ (𝑡 ∈ 𝐽 ∧ ∃𝑛(𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩)))
90	89	exbii 1892	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑡(𝑡 ∈ 𝐽 ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = ⟨𝑡, 𝑛⟩) ↔ ∃𝑡(𝑡 ∈ 𝐽 ∧ ∃𝑛(𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩)))
91		df-rex 3096	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = ⟨𝑡, 𝑛⟩ ↔ ∃𝑡(𝑡 ∈ 𝐽 ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = ⟨𝑡, 𝑛⟩))
92		exdistr 1997	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑡∃𝑛(𝑡 ∈ 𝐽 ∧ (𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩)) ↔ ∃𝑡(𝑡 ∈ 𝐽 ∧ ∃𝑛(𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩)))
93	90, 91, 92	3bitr4i 295	. . . . . . . . . . . . . . 15 ⊢ (∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = ⟨𝑡, 𝑛⟩ ↔ ∃𝑡∃𝑛(𝑡 ∈ 𝐽 ∧ (𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = ⟨𝑡, 𝑛⟩)))
94	87, 93	bitr4i 270	. . . . . . . . . . . . . 14 ⊢ (∃𝑡∃𝑛(𝑤 = ⟨𝑡, 𝑛⟩ ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ↔ ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = ⟨𝑡, 𝑛⟩)
95	83, 94	syl6bb 279	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑤 ∈ {⟨𝑡, 𝑛⟩ ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))} ↔ ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = ⟨𝑡, 𝑛⟩))
96	57, 95	bitrd 271	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ↔ ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = ⟨𝑡, 𝑛⟩))
97	96	biimpa 470	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) → ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = ⟨𝑡, 𝑛⟩)
98	97	adantlr 705	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) → ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = ⟨𝑡, 𝑛⟩)
99		fveq2 6446	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ⟨𝑡, 𝑛⟩ → (𝐹‘𝑤) = (𝐹‘⟨𝑡, 𝑛⟩))
100	99	adantl 475	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ∧ 𝑤 = ⟨𝑡, 𝑛⟩) → (𝐹‘𝑤) = (𝐹‘⟨𝑡, 𝑛⟩))
101		bitsss 15554	. . . . . . . . . . . . . . . . 17 ⊢ (bits‘(𝐴‘𝑡)) ⊆ ℕ0
102	101	sseli 3817	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (bits‘(𝐴‘𝑡)) → 𝑛 ∈ ℕ0)
103	102	anim2i 610	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0))
104	103	ad2antlr 717	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ∧ 𝑤 = ⟨𝑡, 𝑛⟩) → (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0))
105		opelxp 5391	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑡, 𝑛⟩ ∈ (𝐽 × ℕ0) ↔ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0))
106	4, 5	oddpwdcv 31015	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑡, 𝑛⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑡, 𝑛⟩) = ((2↑(2nd ‘⟨𝑡, 𝑛⟩)) · (1st ‘⟨𝑡, 𝑛⟩)))
107		vex 3401	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑡 ∈ V
108		vex 3401	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑛 ∈ V
109	107, 108	op2nd 7454	. . . . . . . . . . . . . . . . . 18 ⊢ (2nd ‘⟨𝑡, 𝑛⟩) = 𝑛
110	109	oveq2i 6933	. . . . . . . . . . . . . . . . 17 ⊢ (2↑(2nd ‘⟨𝑡, 𝑛⟩)) = (2↑𝑛)
111	107, 108	op1st 7453	. . . . . . . . . . . . . . . . 17 ⊢ (1st ‘⟨𝑡, 𝑛⟩) = 𝑡
112	110, 111	oveq12i 6934	. . . . . . . . . . . . . . . 16 ⊢ ((2↑(2nd ‘⟨𝑡, 𝑛⟩)) · (1st ‘⟨𝑡, 𝑛⟩)) = ((2↑𝑛) · 𝑡)
113	106, 112	syl6eq 2830	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑡, 𝑛⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑡, 𝑛⟩) = ((2↑𝑛) · 𝑡))
114	105, 113	sylbir 227	. . . . . . . . . . . . . 14 ⊢ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0) → (𝐹‘⟨𝑡, 𝑛⟩) = ((2↑𝑛) · 𝑡))
115	104, 114	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ∧ 𝑤 = ⟨𝑡, 𝑛⟩) → (𝐹‘⟨𝑡, 𝑛⟩) = ((2↑𝑛) · 𝑡))
116	100, 115	eqtr2d 2815	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ∧ 𝑤 = ⟨𝑡, 𝑛⟩) → ((2↑𝑛) · 𝑡) = (𝐹‘𝑤))
117	116	ex 403	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → (𝑤 = ⟨𝑡, 𝑛⟩ → ((2↑𝑛) · 𝑡) = (𝐹‘𝑤)))
118	117	reximdvva 3201	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) → (∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = ⟨𝑡, 𝑛⟩ → ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤)))
119	98, 118	mpd 15	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) → ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤))
120		ssrexv 3886	. . . . . . . . 9 ⊢ (𝐽 ⊆ ℕ → (∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤)))
121	37, 119, 120	mpsyl 68	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤))
122	121	adantr 474	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝐹‘𝑤) = 𝐵) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤))
123		eqeq2 2789	. . . . . . . . . 10 ⊢ ((𝐹‘𝑤) = 𝐵 → (((2↑𝑛) · 𝑡) = (𝐹‘𝑤) ↔ ((2↑𝑛) · 𝑡) = 𝐵))
124	123	rexbidv 3237	. . . . . . . . 9 ⊢ ((𝐹‘𝑤) = 𝐵 → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵))
125	124	adantl 475	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝐹‘𝑤) = 𝐵) → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵))
126	125	rexbidv 3237	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝐹‘𝑤) = 𝐵) → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤) ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵))
127	122, 126	mpbid 224	. . . . . 6 ⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝐹‘𝑤) = 𝐵) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵)
128	127	r19.29an 3263	. . . . 5 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵)
129		simp-5l 775	. . . . . . . 8 ⊢ ((((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝐴 ∈ (𝑇 ∩ 𝑅))
130		simpllr 766	. . . . . . . 8 ⊢ ((((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝑥 ∈ 𝐽)
131		simplr 759	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝑦 ∈ (bits‘(𝐴‘𝑥)))
132	68	eleq2d 2845	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ↾ 𝐽):𝐽⟶ℕ0 → (𝑥 ∈ dom (𝐴 ↾ 𝐽) ↔ 𝑥 ∈ 𝐽))
133	67, 132	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑥 ∈ dom (𝐴 ↾ 𝐽) ↔ 𝑥 ∈ 𝐽))
134	133	biimpar 471	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ dom (𝐴 ↾ 𝐽))
135		fvco 6534	. . . . . . . . . . . 12 ⊢ ((Fun (𝐴 ↾ 𝐽) ∧ 𝑥 ∈ dom (𝐴 ↾ 𝐽)) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) = (bits‘((𝐴 ↾ 𝐽)‘𝑥)))
136	65, 134, 135	syl2an2r 675	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ 𝐽) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) = (bits‘((𝐴 ↾ 𝐽)‘𝑥)))
137		fvres 6465	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐽 → ((𝐴 ↾ 𝐽)‘𝑥) = (𝐴‘𝑥))
138	137	fveq2d 6450	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐽 → (bits‘((𝐴 ↾ 𝐽)‘𝑥)) = (bits‘(𝐴‘𝑥)))
139	138	adantl 475	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ 𝐽) → (bits‘((𝐴 ↾ 𝐽)‘𝑥)) = (bits‘(𝐴‘𝑥)))
140	136, 139	eqtrd 2814	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ 𝐽) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) = (bits‘(𝐴‘𝑥)))
141	129, 130, 140	syl2anc 579	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) = (bits‘(𝐴‘𝑥)))
142	131, 141	eleqtrrd 2862	. . . . . . . 8 ⊢ ((((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))
143	48	eleq2d 2845	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (⟨𝑥, 𝑦⟩ ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))}))
144		opabid 5219	. . . . . . . . . 10 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))} ↔ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)))
145	143, 144	syl6bb 279	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (⟨𝑥, 𝑦⟩ ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ↔ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))))
146	145	biimpar 471	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))) → ⟨𝑥, 𝑦⟩ ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))))
147	129, 130, 142, 146	syl12anc 827	. . . . . . 7 ⊢ ((((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → ⟨𝑥, 𝑦⟩ ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))))
148		simpr 479	. . . . . . . 8 ⊢ ((((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → ((2↑𝑦) · 𝑥) = 𝐵)
149	34	ad4antr 722	. . . . . . . . 9 ⊢ ((((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ⊆ (𝐽 × ℕ0))
150	149, 147	sseldd 3822	. . . . . . . 8 ⊢ ((((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → ⟨𝑥, 𝑦⟩ ∈ (𝐽 × ℕ0))
151		opeq1 4636	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑥 → ⟨𝑡, 𝑦⟩ = ⟨𝑥, 𝑦⟩)
152	151	eleq1d 2844	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑥 → (⟨𝑡, 𝑦⟩ ∈ (𝐽 × ℕ0) ↔ ⟨𝑥, 𝑦⟩ ∈ (𝐽 × ℕ0)))
153	151	fveq2d 6450	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑥 → (𝐹‘⟨𝑡, 𝑦⟩) = (𝐹‘⟨𝑥, 𝑦⟩))
154		oveq2 6930	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑥 → ((2↑𝑦) · 𝑡) = ((2↑𝑦) · 𝑥))
155	153, 154	eqeq12d 2793	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑥 → ((𝐹‘⟨𝑡, 𝑦⟩) = ((2↑𝑦) · 𝑡) ↔ (𝐹‘⟨𝑥, 𝑦⟩) = ((2↑𝑦) · 𝑥)))
156	152, 155	imbi12d 336	. . . . . . . . . 10 ⊢ (𝑡 = 𝑥 → ((⟨𝑡, 𝑦⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑡, 𝑦⟩) = ((2↑𝑦) · 𝑡)) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑥, 𝑦⟩) = ((2↑𝑦) · 𝑥))))
157		opeq2 4637	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑦 → ⟨𝑡, 𝑛⟩ = ⟨𝑡, 𝑦⟩)
158	157	eleq1d 2844	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑦 → (⟨𝑡, 𝑛⟩ ∈ (𝐽 × ℕ0) ↔ ⟨𝑡, 𝑦⟩ ∈ (𝐽 × ℕ0)))
159	157	fveq2d 6450	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑦 → (𝐹‘⟨𝑡, 𝑛⟩) = (𝐹‘⟨𝑡, 𝑦⟩))
160		oveq2 6930	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑦 → (2↑𝑛) = (2↑𝑦))
161	160	oveq1d 6937	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑦 → ((2↑𝑛) · 𝑡) = ((2↑𝑦) · 𝑡))
162	159, 161	eqeq12d 2793	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑦 → ((𝐹‘⟨𝑡, 𝑛⟩) = ((2↑𝑛) · 𝑡) ↔ (𝐹‘⟨𝑡, 𝑦⟩) = ((2↑𝑦) · 𝑡)))
163	158, 162	imbi12d 336	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑦 → ((⟨𝑡, 𝑛⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑡, 𝑛⟩) = ((2↑𝑛) · 𝑡)) ↔ (⟨𝑡, 𝑦⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑡, 𝑦⟩) = ((2↑𝑦) · 𝑡))))
164	163, 113	chvarv 2361	. . . . . . . . . 10 ⊢ (⟨𝑡, 𝑦⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑡, 𝑦⟩) = ((2↑𝑦) · 𝑡))
165	156, 164	chvarv 2361	. . . . . . . . 9 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐽 × ℕ0) → (𝐹‘⟨𝑥, 𝑦⟩) = ((2↑𝑦) · 𝑥))
166		eqeq2 2789	. . . . . . . . . 10 ⊢ (((2↑𝑦) · 𝑥) = 𝐵 → ((𝐹‘⟨𝑥, 𝑦⟩) = ((2↑𝑦) · 𝑥) ↔ (𝐹‘⟨𝑥, 𝑦⟩) = 𝐵))
167	166	biimpa 470	. . . . . . . . 9 ⊢ ((((2↑𝑦) · 𝑥) = 𝐵 ∧ (𝐹‘⟨𝑥, 𝑦⟩) = ((2↑𝑦) · 𝑥)) → (𝐹‘⟨𝑥, 𝑦⟩) = 𝐵)
168	165, 167	sylan2 586	. . . . . . . 8 ⊢ ((((2↑𝑦) · 𝑥) = 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐽 × ℕ0)) → (𝐹‘⟨𝑥, 𝑦⟩) = 𝐵)
169	148, 150, 168	syl2anc 579	. . . . . . 7 ⊢ ((((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → (𝐹‘⟨𝑥, 𝑦⟩) = 𝐵)
170		fveqeq2 6455	. . . . . . . 8 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((𝐹‘𝑤) = 𝐵 ↔ (𝐹‘⟨𝑥, 𝑦⟩) = 𝐵))
171	170	rspcev 3511	. . . . . . 7 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ∧ (𝐹‘⟨𝑥, 𝑦⟩) = 𝐵) → ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵)
172	147, 169, 171	syl2anc 579	. . . . . 6 ⊢ ((((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵)
173		oveq2 6930	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑥 → ((2↑𝑛) · 𝑡) = ((2↑𝑛) · 𝑥))
174	173	eqeq1d 2780	. . . . . . . . . 10 ⊢ (𝑡 = 𝑥 → (((2↑𝑛) · 𝑡) = 𝐵 ↔ ((2↑𝑛) · 𝑥) = 𝐵))
175	160	oveq1d 6937	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑦 → ((2↑𝑛) · 𝑥) = ((2↑𝑦) · 𝑥))
176	175	eqeq1d 2780	. . . . . . . . . 10 ⊢ (𝑛 = 𝑦 → (((2↑𝑛) · 𝑥) = 𝐵 ↔ ((2↑𝑦) · 𝑥) = 𝐵))
177	174, 176	sylan9bb 505	. . . . . . . . 9 ⊢ ((𝑡 = 𝑥 ∧ 𝑛 = 𝑦) → (((2↑𝑛) · 𝑡) = 𝐵 ↔ ((2↑𝑦) · 𝑥) = 𝐵))
178		simpl 476	. . . . . . . . . . 11 ⊢ ((𝑡 = 𝑥 ∧ 𝑛 = 𝑦) → 𝑡 = 𝑥)
179	178	fveq2d 6450	. . . . . . . . . 10 ⊢ ((𝑡 = 𝑥 ∧ 𝑛 = 𝑦) → (𝐴‘𝑡) = (𝐴‘𝑥))
180	179	fveq2d 6450	. . . . . . . . 9 ⊢ ((𝑡 = 𝑥 ∧ 𝑛 = 𝑦) → (bits‘(𝐴‘𝑡)) = (bits‘(𝐴‘𝑥)))
181	177, 180	cbvrexdva2 3372	. . . . . . . 8 ⊢ (𝑡 = 𝑥 → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵 ↔ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵))
182	181	cbvrexv 3368	. . . . . . 7 ⊢ (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵 ↔ ∃𝑥 ∈ ℕ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)
183		nfv 1957	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 𝐴 ∈ (𝑇 ∩ 𝑅)
184		nfv 1957	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑥 ∈ ℕ
185		nfre1 3186	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵
186	184, 185	nfan 1946	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)
187	183, 186	nfan 1946	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵))
188		simplr 759	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → 𝑥 ∈ ℕ)
189		n0i 4148	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (bits‘(𝐴‘𝑥)) → ¬ (bits‘(𝐴‘𝑥)) = ∅)
190	189	adantl 475	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → ¬ (bits‘(𝐴‘𝑥)) = ∅)
191		fveq2 6446	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴‘𝑥) = 0 → (bits‘(𝐴‘𝑥)) = (bits‘0))
192		0bits 15567	. . . . . . . . . . . . . . . . . . . 20 ⊢ (bits‘0) = ∅
193	191, 192	syl6eq 2830	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴‘𝑥) = 0 → (bits‘(𝐴‘𝑥)) = ∅)
194	190, 193	nsyl 138	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → ¬ (𝐴‘𝑥) = 0)
195	62	ffvelrnda 6623	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) → (𝐴‘𝑥) ∈ ℕ0)
196	195	adantr 474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → (𝐴‘𝑥) ∈ ℕ0)
197		elnn0 11644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴‘𝑥) ∈ ℕ0 ↔ ((𝐴‘𝑥) ∈ ℕ ∨ (𝐴‘𝑥) = 0))
198	196, 197	sylib 210	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → ((𝐴‘𝑥) ∈ ℕ ∨ (𝐴‘𝑥) = 0))
199	198	orcomd 860	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → ((𝐴‘𝑥) = 0 ∨ (𝐴‘𝑥) ∈ ℕ))
200	199	orcanai 988	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ¬ (𝐴‘𝑥) = 0) → (𝐴‘𝑥) ∈ ℕ)
201	194, 200	mpdan 677	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → (𝐴‘𝑥) ∈ ℕ)
202	58	simp3bi 1138	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆ 𝐽)
203	202	sselda 3821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑛 ∈ (◡𝐴 “ ℕ)) → 𝑛 ∈ 𝐽)
204		breq2 4890	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = 𝑛 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑛))
205	204	notbid 310	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 = 𝑛 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑛))
206	205, 4	elrab2 3576	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ 𝐽 ↔ (𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛))
207	206	simprbi 492	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ 𝐽 → ¬ 2 ∥ 𝑛)
208	203, 207	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑛 ∈ (◡𝐴 “ ℕ)) → ¬ 2 ∥ 𝑛)
209	208	ralrimiva 3148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∀𝑛 ∈ (◡𝐴 “ ℕ) ¬ 2 ∥ 𝑛)
210		ffn 6291	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴:ℕ⟶ℕ0 → 𝐴 Fn ℕ)
211		elpreima 6600	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 Fn ℕ → (𝑛 ∈ (◡𝐴 “ ℕ) ↔ (𝑛 ∈ ℕ ∧ (𝐴‘𝑛) ∈ ℕ)))
212	62, 210, 211	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑛 ∈ (◡𝐴 “ ℕ) ↔ (𝑛 ∈ ℕ ∧ (𝐴‘𝑛) ∈ ℕ)))
213	212	imbi1d 333	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝑛 ∈ (◡𝐴 “ ℕ) → ¬ 2 ∥ 𝑛) ↔ ((𝑛 ∈ ℕ ∧ (𝐴‘𝑛) ∈ ℕ) → ¬ 2 ∥ 𝑛)))
214		impexp 443	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 ∈ ℕ ∧ (𝐴‘𝑛) ∈ ℕ) → ¬ 2 ∥ 𝑛) ↔ (𝑛 ∈ ℕ → ((𝐴‘𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛)))
215	213, 214	syl6bb 279	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝑛 ∈ (◡𝐴 “ ℕ) → ¬ 2 ∥ 𝑛) ↔ (𝑛 ∈ ℕ → ((𝐴‘𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛))))
216	215	ralbidv2 3166	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (∀𝑛 ∈ (◡𝐴 “ ℕ) ¬ 2 ∥ 𝑛 ↔ ∀𝑛 ∈ ℕ ((𝐴‘𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛)))
217	209, 216	mpbid 224	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∀𝑛 ∈ ℕ ((𝐴‘𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛))
218		fveq2 6446	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑛 → (𝐴‘𝑥) = (𝐴‘𝑛))
219	218	eleq1d 2844	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑛 → ((𝐴‘𝑥) ∈ ℕ ↔ (𝐴‘𝑛) ∈ ℕ))
220		breq2 4890	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑛 → (2 ∥ 𝑥 ↔ 2 ∥ 𝑛))
221	220	notbid 310	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑛 → (¬ 2 ∥ 𝑥 ↔ ¬ 2 ∥ 𝑛))
222	219, 221	imbi12d 336	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑛 → (((𝐴‘𝑥) ∈ ℕ → ¬ 2 ∥ 𝑥) ↔ ((𝐴‘𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛)))
223	222	cbvralv 3367	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑥 ∈ ℕ ((𝐴‘𝑥) ∈ ℕ → ¬ 2 ∥ 𝑥) ↔ ∀𝑛 ∈ ℕ ((𝐴‘𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛))
224	217, 223	sylibr 226	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∀𝑥 ∈ ℕ ((𝐴‘𝑥) ∈ ℕ → ¬ 2 ∥ 𝑥))
225	224	r19.21bi 3114	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) → ((𝐴‘𝑥) ∈ ℕ → ¬ 2 ∥ 𝑥))
226	225	imp 397	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ (𝐴‘𝑥) ∈ ℕ) → ¬ 2 ∥ 𝑥)
227	201, 226	syldan 585	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → ¬ 2 ∥ 𝑥)
228		breq2 4890	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑥 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑥))
229	228	notbid 310	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑥 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑥))
230	229, 4	elrab2 3576	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐽 ↔ (𝑥 ∈ ℕ ∧ ¬ 2 ∥ 𝑥))
231	188, 227, 230	sylanbrc 578	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → 𝑥 ∈ 𝐽)
232	231	adantlrr 711	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → 𝑥 ∈ 𝐽)
233	232	adantr 474	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝑥 ∈ 𝐽)
234		simprr 763	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) → ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)
235	187, 233, 234	r19.29af 3262	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) → 𝑥 ∈ 𝐽)
236	235, 234	jca 507	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) → (𝑥 ∈ 𝐽 ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵))
237	236	ex 403	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) → (𝑥 ∈ 𝐽 ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)))
238	237	reximdv2 3195	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (∃𝑥 ∈ ℕ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵 → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵))
239	238	imp 397	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ ∃𝑥 ∈ ℕ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)
240	239	adantlr 705	. . . . . . 7 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑥 ∈ ℕ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)
241	182, 240	sylan2b 587	. . . . . 6 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)
242	172, 241	r19.29vva 3267	. . . . 5 ⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) → ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵)
243	128, 242	impbida 791	. . . 4 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → (∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵 ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵))
244	36, 243	bitrd 271	. . 3 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → (𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵))
245	244	ifbid 4329	. 2 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → if(𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))), 1, 0) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵, 1, 0))
246	13, 23, 245	3eqtrd 2818	1 ⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → ((𝐺‘𝐴)‘𝐵) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵, 1, 0))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 836   = wceq 1601  ∃wex 1823   ∈ wcel 2107  {cab 2763  ∀wral 3090  ∃wrex 3091  {crab 3094  Vcvv 3398   ∩ cin 3791   ⊆ wss 3792  ∅c0 4141  ifcif 4307  𝒫 cpw 4379  ⟨cop 4404   class class class wbr 4886  {copab 4948   ↦ cmpt 4965   × cxp 5353  ^◡ccnv 5354  dom cdm 5355  ran crn 5356   ↾ cres 5357   “ cima 5358   ∘ ccom 5359  Fun wfun 6129   Fn wfn 6130  ⟶wf 6131  –1-1-onto→wf1o 6134  ‘cfv 6135  (class class class)co 6922   ↦ cmpt2 6924  1^st c1st 7443  2^nd c2nd 7444   supp csupp 7576   ↑_𝑚 cmap 8140  Fincfn 8241  0cc0 10272  1c1 10273   · cmul 10277   ≤ cle 10412  ℕcn 11374  2c2 11430  ℕ₀cn0 11642  ↑cexp 13178  Σcsu 14824   ∥ cdvds 15387  bitscbits 15547  𝟭cind 30670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-ac2 9620  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-disj 4855  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-supp 7577  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-2o 7844  df-oadd 7847  df-er 8026  df-map 8142  df-pm 8143  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-acn 9101  df-ac 9272  df-cda 9325  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-n0 11643  df-xnn0 11715  df-z 11729  df-uz 11993  df-rp 12138  df-fz 12644  df-fzo 12785  df-fl 12912  df-mod 12988  df-seq 13120  df-exp 13179  df-hash 13436  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-clim 14627  df-sum 14825  df-dvds 15388  df-bits 15550  df-ind 30671

This theorem is referenced by:  eulerpartlemgs2  31040