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)) |