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 30435 |
. . . 4
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))))) |
12 | 11 | fveq1d 6193 |
. . 3
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝐺‘𝐴)‘𝐵) = (((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))))‘𝐵)) |
13 | 12 | adantr 481 |
. 2
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → ((𝐺‘𝐴)‘𝐵) = (((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))))‘𝐵)) |
14 | | nnex 11026 |
. . 3
⊢ ℕ
∈ V |
15 | | imassrn 5477 |
. . . 4
⊢ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ⊆ ran 𝐹 |
16 | 4, 5 | oddpwdc 30416 |
. . . . 5
⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ |
17 | | f1of 6137 |
. . . . 5
⊢ (𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ → 𝐹:(𝐽 ×
ℕ0)⟶ℕ) |
18 | | frn 6053 |
. . . . 5
⊢ (𝐹:(𝐽 × ℕ0)⟶ℕ
→ ran 𝐹 ⊆
ℕ) |
19 | 16, 17, 18 | mp2b 10 |
. . . 4
⊢ ran 𝐹 ⊆
ℕ |
20 | 15, 19 | sstri 3612 |
. . 3
⊢ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ⊆ ℕ |
21 | | simpr 477 |
. . 3
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → 𝐵 ∈ ℕ) |
22 | | indfval 30078 |
. . 3
⊢ ((ℕ
∈ V ∧ (𝐹 “
(𝑀‘(bits ∘
(𝐴 ↾ 𝐽)))) ⊆ ℕ ∧ 𝐵 ∈ ℕ) →
(((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))))‘𝐵) = if(𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))), 1, 0)) |
23 | 14, 20, 21, 22 | mp3an12i 1428 |
. 2
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) →
(((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))))‘𝐵) = if(𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))), 1, 0)) |
24 | | ffn 6045 |
. . . . . 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 30437 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (bits ∘ (𝐴 ↾ 𝐽)) ∈ 𝐻) |
27 | 1, 2, 3, 4, 5, 6, 7 | eulerpartlem1 30429 |
. . . . . . . . . . 11
⊢ 𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩
Fin) |
28 | | f1of 6137 |
. . . . . . . . . . 11
⊢ (𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
→ 𝑀:𝐻⟶(𝒫 (𝐽 × ℕ0) ∩
Fin)) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . 10
⊢ 𝑀:𝐻⟶(𝒫 (𝐽 × ℕ0) ∩
Fin) |
30 | 29 | ffvelrni 6358 |
. . . . . . . . 9
⊢ ((bits
∘ (𝐴 ↾ 𝐽)) ∈ 𝐻 → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩
Fin)) |
31 | 26, 30 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩
Fin)) |
32 | 31 | elin1d 3802 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ∈ 𝒫 (𝐽 ×
ℕ0)) |
33 | 32 | adantr 481 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ∈ 𝒫 (𝐽 ×
ℕ0)) |
34 | 33 | elpwid 4170 |
. . . . 5
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ⊆ (𝐽 ×
ℕ0)) |
35 | | fvelimab 6253 |
. . . . 5
⊢ ((𝐹 Fn (𝐽 × ℕ0) ∧ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ⊆ (𝐽 × ℕ0)) → (𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ↔ ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵)) |
36 | 25, 34, 35 | sylancr 695 |
. . . 4
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → (𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ↔ ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵)) |
37 | 4 | ssrab3 3688 |
. . . . . . . . 9
⊢ 𝐽 ⊆
ℕ |
38 | 7 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})) |
39 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 = (bits ∘ (𝐴 ↾ 𝐽)) → (𝑟‘𝑥) = ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)) |
40 | 39 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 = (bits ∘ (𝐴 ↾ 𝐽)) → (𝑦 ∈ (𝑟‘𝑥) ↔ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))) |
41 | 40 | anbi2d 740 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = (bits ∘ (𝐴 ↾ 𝐽)) → ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥)) ↔ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)))) |
42 | 41 | opabbidv 4716 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = (bits ∘ (𝐴 ↾ 𝐽)) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))}) |
43 | 42 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑟 = (bits ∘ (𝐴 ↾ 𝐽))) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))}) |
44 | 14, 37 | ssexi 4803 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐽 ∈ V |
45 | | abid2 2745 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑦 ∣ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)} = ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) |
46 | 45 | fvexi 6202 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑦 ∣ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)} ∈ V |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝐽 → {𝑦 ∣ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)} ∈ V) |
48 | 44, 47 | opabex3 7146 |
. . . . . . . . . . . . . . . . 17
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))} ∈ V |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))} ∈ V) |
50 | 38, 43, 26, 49 | fvmptd 6288 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))}) |
51 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → 𝑥 = 𝑡) |
52 | 51 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → (𝑥 ∈ 𝐽 ↔ 𝑡 ∈ 𝐽)) |
53 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → 𝑦 = 𝑛) |
54 | 51 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) = ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡)) |
55 | 53, 54 | eleq12d 2695 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → (𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) ↔ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))) |
56 | 52, 55 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)) ↔ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡)))) |
57 | 56 | cbvopabv 4722 |
. . . . . . . . . . . . . . 15
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))} = {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))} |
58 | 50, 57 | syl6eq 2672 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) = {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))}) |
59 | 58 | eleq2d 2687 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ↔ 𝑤 ∈ {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))})) |
60 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | eulerpartlemt0 30431 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0
↑𝑚 ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽)) |
61 | 60 | simp1bi 1076 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ (ℕ0
↑𝑚 ℕ)) |
62 | | nn0ex 11298 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
ℕ0 ∈ V |
63 | 62, 14 | elmap 7886 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∈ (ℕ0
↑𝑚 ℕ) ↔ 𝐴:ℕ⟶ℕ0) |
64 | 61, 63 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴:ℕ⟶ℕ0) |
65 | | ffun 6048 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴:ℕ⟶ℕ0 →
Fun 𝐴) |
66 | | funres 5929 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Fun
𝐴 → Fun (𝐴 ↾ 𝐽)) |
67 | 64, 65, 66 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Fun (𝐴 ↾ 𝐽)) |
68 | | fssres 6070 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝐽 ⊆ ℕ) →
(𝐴 ↾ 𝐽):𝐽⟶ℕ0) |
69 | 64, 37, 68 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐴 ↾ 𝐽):𝐽⟶ℕ0) |
70 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ↾ 𝐽):𝐽⟶ℕ0 → dom
(𝐴 ↾ 𝐽) = 𝐽) |
71 | 70 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ↾ 𝐽):𝐽⟶ℕ0 → (𝑡 ∈ dom (𝐴 ↾ 𝐽) ↔ 𝑡 ∈ 𝐽)) |
72 | 69, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑡 ∈ dom (𝐴 ↾ 𝐽) ↔ 𝑡 ∈ 𝐽)) |
73 | 72 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ 𝐽) → 𝑡 ∈ dom (𝐴 ↾ 𝐽)) |
74 | | fvco 6274 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Fun
(𝐴 ↾ 𝐽) ∧ 𝑡 ∈ dom (𝐴 ↾ 𝐽)) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡) = (bits‘((𝐴 ↾ 𝐽)‘𝑡))) |
75 | 67, 73, 74 | syl2an2r 876 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ 𝐽) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡) = (bits‘((𝐴 ↾ 𝐽)‘𝑡))) |
76 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 ∈ 𝐽 → ((𝐴 ↾ 𝐽)‘𝑡) = (𝐴‘𝑡)) |
77 | 76 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 ∈ 𝐽 → (bits‘((𝐴 ↾ 𝐽)‘𝑡)) = (bits‘(𝐴‘𝑡))) |
78 | 77 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ 𝐽) → (bits‘((𝐴 ↾ 𝐽)‘𝑡)) = (bits‘(𝐴‘𝑡))) |
79 | 75, 78 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ 𝐽) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡) = (bits‘(𝐴‘𝑡))) |
80 | 79 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ 𝐽) → (𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡) ↔ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) |
81 | 80 | pm5.32da 673 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡)) ↔ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))))) |
82 | 81 | opabbidv 4716 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))} = {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))}) |
83 | 82 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑤 ∈ {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))} ↔ 𝑤 ∈ {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))})) |
84 | | elopab 4983 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))} ↔ ∃𝑡∃𝑛(𝑤 = 〈𝑡, 𝑛〉 ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))))) |
85 | 83, 84 | syl6bb 276 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑤 ∈ {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))} ↔ ∃𝑡∃𝑛(𝑤 = 〈𝑡, 𝑛〉 ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))))) |
86 | | ancom 466 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 = 〈𝑡, 𝑛〉 ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ↔ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) ∧ 𝑤 = 〈𝑡, 𝑛〉)) |
87 | | anass 681 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) ∧ 𝑤 = 〈𝑡, 𝑛〉) ↔ (𝑡 ∈ 𝐽 ∧ (𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉))) |
88 | 86, 87 | bitri 264 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 = 〈𝑡, 𝑛〉 ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ↔ (𝑡 ∈ 𝐽 ∧ (𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉))) |
89 | 88 | 2exbii 1775 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑡∃𝑛(𝑤 = 〈𝑡, 𝑛〉 ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ↔ ∃𝑡∃𝑛(𝑡 ∈ 𝐽 ∧ (𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉))) |
90 | | df-rex 2918 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑛 ∈
(bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉 ↔ ∃𝑛(𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉)) |
91 | 90 | anbi2i 730 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑡 ∈ 𝐽 ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉) ↔ (𝑡 ∈ 𝐽 ∧ ∃𝑛(𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉))) |
92 | 91 | exbii 1774 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑡(𝑡 ∈ 𝐽 ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉) ↔ ∃𝑡(𝑡 ∈ 𝐽 ∧ ∃𝑛(𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉))) |
93 | | df-rex 2918 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑡 ∈
𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉 ↔ ∃𝑡(𝑡 ∈ 𝐽 ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉)) |
94 | | exdistr 1919 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑡∃𝑛(𝑡 ∈ 𝐽 ∧ (𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉)) ↔ ∃𝑡(𝑡 ∈ 𝐽 ∧ ∃𝑛(𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉))) |
95 | 92, 93, 94 | 3bitr4i 292 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑡 ∈
𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉 ↔ ∃𝑡∃𝑛(𝑡 ∈ 𝐽 ∧ (𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉))) |
96 | 89, 95 | bitr4i 267 |
. . . . . . . . . . . . . 14
⊢
(∃𝑡∃𝑛(𝑤 = 〈𝑡, 𝑛〉 ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ↔ ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉) |
97 | 85, 96 | syl6bb 276 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑤 ∈ {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))} ↔ ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉)) |
98 | 59, 97 | bitrd 268 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ↔ ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉)) |
99 | 98 | biimpa 501 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) → ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉) |
100 | 99 | adantlr 751 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) → ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉) |
101 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 〈𝑡, 𝑛〉 → (𝐹‘𝑤) = (𝐹‘〈𝑡, 𝑛〉)) |
102 | 101 | adantl 482 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ∧ 𝑤 = 〈𝑡, 𝑛〉) → (𝐹‘𝑤) = (𝐹‘〈𝑡, 𝑛〉)) |
103 | | bitsss 15148 |
. . . . . . . . . . . . . . . . 17
⊢
(bits‘(𝐴‘𝑡)) ⊆
ℕ0 |
104 | 103 | sseli 3599 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (bits‘(𝐴‘𝑡)) → 𝑛 ∈ ℕ0) |
105 | 104 | anim2i 593 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → (𝑡 ∈ 𝐽 ∧ 𝑛 ∈
ℕ0)) |
106 | 105 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ∧ 𝑤 = 〈𝑡, 𝑛〉) → (𝑡 ∈ 𝐽 ∧ 𝑛 ∈
ℕ0)) |
107 | | opelxp 5146 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑡, 𝑛〉 ∈ (𝐽 × ℕ0) ↔ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈
ℕ0)) |
108 | 4, 5 | oddpwdcv 30417 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑡, 𝑛〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑡, 𝑛〉) = ((2↑(2nd
‘〈𝑡, 𝑛〉)) ·
(1st ‘〈𝑡, 𝑛〉))) |
109 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑡 ∈ V |
110 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑛 ∈ V |
111 | 109, 110 | op2nd 7177 |
. . . . . . . . . . . . . . . . . 18
⊢
(2nd ‘〈𝑡, 𝑛〉) = 𝑛 |
112 | 111 | oveq2i 6661 |
. . . . . . . . . . . . . . . . 17
⊢
(2↑(2nd ‘〈𝑡, 𝑛〉)) = (2↑𝑛) |
113 | 109, 110 | op1st 7176 |
. . . . . . . . . . . . . . . . 17
⊢
(1st ‘〈𝑡, 𝑛〉) = 𝑡 |
114 | 112, 113 | oveq12i 6662 |
. . . . . . . . . . . . . . . 16
⊢
((2↑(2nd ‘〈𝑡, 𝑛〉)) · (1st
‘〈𝑡, 𝑛〉)) = ((2↑𝑛) · 𝑡) |
115 | 108, 114 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑡, 𝑛〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑡, 𝑛〉) = ((2↑𝑛) · 𝑡)) |
116 | 107, 115 | sylbir 225 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0) → (𝐹‘〈𝑡, 𝑛〉) = ((2↑𝑛) · 𝑡)) |
117 | 106, 116 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ∧ 𝑤 = 〈𝑡, 𝑛〉) → (𝐹‘〈𝑡, 𝑛〉) = ((2↑𝑛) · 𝑡)) |
118 | 102, 117 | eqtr2d 2657 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ∧ 𝑤 = 〈𝑡, 𝑛〉) → ((2↑𝑛) · 𝑡) = (𝐹‘𝑤)) |
119 | 118 | ex 450 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → (𝑤 = 〈𝑡, 𝑛〉 → ((2↑𝑛) · 𝑡) = (𝐹‘𝑤))) |
120 | 119 | reximdvva 3019 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) → (∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉 → ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤))) |
121 | 100, 120 | mpd 15 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) → ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤)) |
122 | | ssrexv 3667 |
. . . . . . . . 9
⊢ (𝐽 ⊆ ℕ →
(∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤))) |
123 | 37, 121, 122 | mpsyl 68 |
. . . . . . . 8
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤)) |
124 | 123 | adantr 481 |
. . . . . . 7
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝐹‘𝑤) = 𝐵) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤)) |
125 | | eqeq2 2633 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑤) = 𝐵 → (((2↑𝑛) · 𝑡) = (𝐹‘𝑤) ↔ ((2↑𝑛) · 𝑡) = 𝐵)) |
126 | 125 | rexbidv 3052 |
. . . . . . . . 9
⊢ ((𝐹‘𝑤) = 𝐵 → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵)) |
127 | 126 | adantl 482 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝐹‘𝑤) = 𝐵) → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵)) |
128 | 127 | rexbidv 3052 |
. . . . . . 7
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝐹‘𝑤) = 𝐵) → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤) ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵)) |
129 | 124, 128 | mpbid 222 |
. . . . . 6
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝐹‘𝑤) = 𝐵) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) |
130 | 129 | r19.29an 3077 |
. . . . 5
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) |
131 | | simp-5l 808 |
. . . . . . . 8
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝐴 ∈ (𝑇 ∩ 𝑅)) |
132 | | simpllr 799 |
. . . . . . . 8
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝑥 ∈ 𝐽) |
133 | | simplr 792 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝑦 ∈ (bits‘(𝐴‘𝑥))) |
134 | 70 | eleq2d 2687 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ↾ 𝐽):𝐽⟶ℕ0 → (𝑥 ∈ dom (𝐴 ↾ 𝐽) ↔ 𝑥 ∈ 𝐽)) |
135 | 69, 134 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑥 ∈ dom (𝐴 ↾ 𝐽) ↔ 𝑥 ∈ 𝐽)) |
136 | 135 | biimpar 502 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ dom (𝐴 ↾ 𝐽)) |
137 | | fvco 6274 |
. . . . . . . . . . . 12
⊢ ((Fun
(𝐴 ↾ 𝐽) ∧ 𝑥 ∈ dom (𝐴 ↾ 𝐽)) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) = (bits‘((𝐴 ↾ 𝐽)‘𝑥))) |
138 | 67, 136, 137 | syl2an2r 876 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ 𝐽) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) = (bits‘((𝐴 ↾ 𝐽)‘𝑥))) |
139 | | fvres 6207 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐽 → ((𝐴 ↾ 𝐽)‘𝑥) = (𝐴‘𝑥)) |
140 | 139 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐽 → (bits‘((𝐴 ↾ 𝐽)‘𝑥)) = (bits‘(𝐴‘𝑥))) |
141 | 140 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ 𝐽) → (bits‘((𝐴 ↾ 𝐽)‘𝑥)) = (bits‘(𝐴‘𝑥))) |
142 | 138, 141 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ 𝐽) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) = (bits‘(𝐴‘𝑥))) |
143 | 131, 132,
142 | syl2anc 693 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) = (bits‘(𝐴‘𝑥))) |
144 | 133, 143 | eleqtrrd 2704 |
. . . . . . . 8
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)) |
145 | 50 | eleq2d 2687 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (〈𝑥, 𝑦〉 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ↔ 〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))})) |
146 | | opabid 4982 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))} ↔ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))) |
147 | 145, 146 | syl6bb 276 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (〈𝑥, 𝑦〉 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ↔ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)))) |
148 | 147 | biimpar 502 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))) → 〈𝑥, 𝑦〉 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) |
149 | 131, 132,
144, 148 | syl12anc 1324 |
. . . . . . 7
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 〈𝑥, 𝑦〉 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) |
150 | | simpr 477 |
. . . . . . . 8
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → ((2↑𝑦) · 𝑥) = 𝐵) |
151 | 34 | ad4antr 768 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ⊆ (𝐽 ×
ℕ0)) |
152 | 151, 149 | sseldd 3604 |
. . . . . . . 8
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 〈𝑥, 𝑦〉 ∈ (𝐽 ×
ℕ0)) |
153 | | opeq1 4402 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑥 → 〈𝑡, 𝑦〉 = 〈𝑥, 𝑦〉) |
154 | 153 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑥 → (〈𝑡, 𝑦〉 ∈ (𝐽 × ℕ0) ↔
〈𝑥, 𝑦〉 ∈ (𝐽 ×
ℕ0))) |
155 | 153 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑥 → (𝐹‘〈𝑡, 𝑦〉) = (𝐹‘〈𝑥, 𝑦〉)) |
156 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑥 → ((2↑𝑦) · 𝑡) = ((2↑𝑦) · 𝑥)) |
157 | 155, 156 | eqeq12d 2637 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑥 → ((𝐹‘〈𝑡, 𝑦〉) = ((2↑𝑦) · 𝑡) ↔ (𝐹‘〈𝑥, 𝑦〉) = ((2↑𝑦) · 𝑥))) |
158 | 154, 157 | imbi12d 334 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑥 → ((〈𝑡, 𝑦〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑡, 𝑦〉) = ((2↑𝑦) · 𝑡)) ↔ (〈𝑥, 𝑦〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑥, 𝑦〉) = ((2↑𝑦) · 𝑥)))) |
159 | | opeq2 4403 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑦 → 〈𝑡, 𝑛〉 = 〈𝑡, 𝑦〉) |
160 | 159 | eleq1d 2686 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑦 → (〈𝑡, 𝑛〉 ∈ (𝐽 × ℕ0) ↔
〈𝑡, 𝑦〉 ∈ (𝐽 ×
ℕ0))) |
161 | 159 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑦 → (𝐹‘〈𝑡, 𝑛〉) = (𝐹‘〈𝑡, 𝑦〉)) |
162 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑦 → (2↑𝑛) = (2↑𝑦)) |
163 | 162 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑦 → ((2↑𝑛) · 𝑡) = ((2↑𝑦) · 𝑡)) |
164 | 161, 163 | eqeq12d 2637 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑦 → ((𝐹‘〈𝑡, 𝑛〉) = ((2↑𝑛) · 𝑡) ↔ (𝐹‘〈𝑡, 𝑦〉) = ((2↑𝑦) · 𝑡))) |
165 | 160, 164 | imbi12d 334 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑦 → ((〈𝑡, 𝑛〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑡, 𝑛〉) = ((2↑𝑛) · 𝑡)) ↔ (〈𝑡, 𝑦〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑡, 𝑦〉) = ((2↑𝑦) · 𝑡)))) |
166 | 165, 115 | chvarv 2263 |
. . . . . . . . . 10
⊢
(〈𝑡, 𝑦〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑡, 𝑦〉) = ((2↑𝑦) · 𝑡)) |
167 | 158, 166 | chvarv 2263 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑥, 𝑦〉) = ((2↑𝑦) · 𝑥)) |
168 | | eqeq2 2633 |
. . . . . . . . . 10
⊢
(((2↑𝑦)
· 𝑥) = 𝐵 → ((𝐹‘〈𝑥, 𝑦〉) = ((2↑𝑦) · 𝑥) ↔ (𝐹‘〈𝑥, 𝑦〉) = 𝐵)) |
169 | 168 | biimpa 501 |
. . . . . . . . 9
⊢
((((2↑𝑦)
· 𝑥) = 𝐵 ∧ (𝐹‘〈𝑥, 𝑦〉) = ((2↑𝑦) · 𝑥)) → (𝐹‘〈𝑥, 𝑦〉) = 𝐵) |
170 | 167, 169 | sylan2 491 |
. . . . . . . 8
⊢
((((2↑𝑦)
· 𝑥) = 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ (𝐽 × ℕ0)) → (𝐹‘〈𝑥, 𝑦〉) = 𝐵) |
171 | 150, 152,
170 | syl2anc 693 |
. . . . . . 7
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → (𝐹‘〈𝑥, 𝑦〉) = 𝐵) |
172 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝐹‘𝑤) = (𝐹‘〈𝑥, 𝑦〉)) |
173 | 172 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ((𝐹‘𝑤) = 𝐵 ↔ (𝐹‘〈𝑥, 𝑦〉) = 𝐵)) |
174 | 173 | rspcev 3309 |
. . . . . . 7
⊢
((〈𝑥, 𝑦〉 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝐵) → ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵) |
175 | 149, 171,
174 | syl2anc 693 |
. . . . . 6
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵) |
176 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑥 → ((2↑𝑛) · 𝑡) = ((2↑𝑛) · 𝑥)) |
177 | 176 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑥 → (((2↑𝑛) · 𝑡) = 𝐵 ↔ ((2↑𝑛) · 𝑥) = 𝐵)) |
178 | 162 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑦 → ((2↑𝑛) · 𝑥) = ((2↑𝑦) · 𝑥)) |
179 | 178 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑦 → (((2↑𝑛) · 𝑥) = 𝐵 ↔ ((2↑𝑦) · 𝑥) = 𝐵)) |
180 | 177, 179 | sylan9bb 736 |
. . . . . . . . 9
⊢ ((𝑡 = 𝑥 ∧ 𝑛 = 𝑦) → (((2↑𝑛) · 𝑡) = 𝐵 ↔ ((2↑𝑦) · 𝑥) = 𝐵)) |
181 | | simpl 473 |
. . . . . . . . . . 11
⊢ ((𝑡 = 𝑥 ∧ 𝑛 = 𝑦) → 𝑡 = 𝑥) |
182 | 181 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝑡 = 𝑥 ∧ 𝑛 = 𝑦) → (𝐴‘𝑡) = (𝐴‘𝑥)) |
183 | 182 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝑡 = 𝑥 ∧ 𝑛 = 𝑦) → (bits‘(𝐴‘𝑡)) = (bits‘(𝐴‘𝑥))) |
184 | 180, 183 | cbvrexdva2 3176 |
. . . . . . . 8
⊢ (𝑡 = 𝑥 → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵 ↔ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) |
185 | 184 | cbvrexv 3172 |
. . . . . . 7
⊢
(∃𝑡 ∈
ℕ ∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵 ↔ ∃𝑥 ∈ ℕ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) |
186 | | nfv 1843 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦 𝐴 ∈ (𝑇 ∩ 𝑅) |
187 | | nfv 1843 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦 𝑥 ∈ ℕ |
188 | | nfre1 3005 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵 |
189 | 187, 188 | nfan 1828 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(𝑥 ∈ ℕ ∧
∃𝑦 ∈
(bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) |
190 | 186, 189 | nfan 1828 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) |
191 | | simplr 792 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → 𝑥 ∈ ℕ) |
192 | | n0i 3920 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (bits‘(𝐴‘𝑥)) → ¬ (bits‘(𝐴‘𝑥)) = ∅) |
193 | 192 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → ¬ (bits‘(𝐴‘𝑥)) = ∅) |
194 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴‘𝑥) = 0 → (bits‘(𝐴‘𝑥)) = (bits‘0)) |
195 | | 0bits 15161 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(bits‘0) = ∅ |
196 | 194, 195 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴‘𝑥) = 0 → (bits‘(𝐴‘𝑥)) = ∅) |
197 | 193, 196 | nsyl 135 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → ¬ (𝐴‘𝑥) = 0) |
198 | 64 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) → (𝐴‘𝑥) ∈
ℕ0) |
199 | 198 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → (𝐴‘𝑥) ∈
ℕ0) |
200 | | elnn0 11294 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴‘𝑥) ∈ ℕ0 ↔ ((𝐴‘𝑥) ∈ ℕ ∨ (𝐴‘𝑥) = 0)) |
201 | 199, 200 | sylib 208 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → ((𝐴‘𝑥) ∈ ℕ ∨ (𝐴‘𝑥) = 0)) |
202 | 201 | orcomd 403 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → ((𝐴‘𝑥) = 0 ∨ (𝐴‘𝑥) ∈ ℕ)) |
203 | 202 | orcanai 952 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ¬ (𝐴‘𝑥) = 0) → (𝐴‘𝑥) ∈ ℕ) |
204 | 197, 203 | mpdan 702 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → (𝐴‘𝑥) ∈ ℕ) |
205 | 60 | simp3bi 1078 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆ 𝐽) |
206 | 205 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑛 ∈ (◡𝐴 “ ℕ)) → 𝑛 ∈ 𝐽) |
207 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = 𝑛 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑛)) |
208 | 207 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = 𝑛 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑛)) |
209 | 208, 4 | elrab2 3366 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ 𝐽 ↔ (𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛)) |
210 | 209 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ 𝐽 → ¬ 2 ∥ 𝑛) |
211 | 206, 210 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑛 ∈ (◡𝐴 “ ℕ)) → ¬ 2 ∥
𝑛) |
212 | 211 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∀𝑛 ∈ (◡𝐴 “ ℕ) ¬ 2 ∥ 𝑛) |
213 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴:ℕ⟶ℕ0 →
𝐴 Fn
ℕ) |
214 | | elpreima 6337 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 Fn ℕ → (𝑛 ∈ (◡𝐴 “ ℕ) ↔ (𝑛 ∈ ℕ ∧ (𝐴‘𝑛) ∈ ℕ))) |
215 | 64, 213, 214 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑛 ∈ (◡𝐴 “ ℕ) ↔ (𝑛 ∈ ℕ ∧ (𝐴‘𝑛) ∈ ℕ))) |
216 | 215 | imbi1d 331 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝑛 ∈ (◡𝐴 “ ℕ) → ¬ 2 ∥
𝑛) ↔ ((𝑛 ∈ ℕ ∧ (𝐴‘𝑛) ∈ ℕ) → ¬ 2 ∥
𝑛))) |
217 | | impexp 462 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ℕ ∧ (𝐴‘𝑛) ∈ ℕ) → ¬ 2 ∥
𝑛) ↔ (𝑛 ∈ ℕ → ((𝐴‘𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛))) |
218 | 216, 217 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝑛 ∈ (◡𝐴 “ ℕ) → ¬ 2 ∥
𝑛) ↔ (𝑛 ∈ ℕ → ((𝐴‘𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛)))) |
219 | 218 | ralbidv2 2984 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (∀𝑛 ∈ (◡𝐴 “ ℕ) ¬ 2 ∥ 𝑛 ↔ ∀𝑛 ∈ ℕ ((𝐴‘𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛))) |
220 | 212, 219 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∀𝑛 ∈ ℕ ((𝐴‘𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛)) |
221 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑛 → (𝐴‘𝑥) = (𝐴‘𝑛)) |
222 | 221 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑛 → ((𝐴‘𝑥) ∈ ℕ ↔ (𝐴‘𝑛) ∈ ℕ)) |
223 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑛 → (2 ∥ 𝑥 ↔ 2 ∥ 𝑛)) |
224 | 223 | notbid 308 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑛 → (¬ 2 ∥ 𝑥 ↔ ¬ 2 ∥ 𝑛)) |
225 | 222, 224 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑛 → (((𝐴‘𝑥) ∈ ℕ → ¬ 2 ∥ 𝑥) ↔ ((𝐴‘𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛))) |
226 | 225 | cbvralv 3171 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈
ℕ ((𝐴‘𝑥) ∈ ℕ → ¬ 2
∥ 𝑥) ↔
∀𝑛 ∈ ℕ
((𝐴‘𝑛) ∈ ℕ → ¬ 2
∥ 𝑛)) |
227 | 220, 226 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∀𝑥 ∈ ℕ ((𝐴‘𝑥) ∈ ℕ → ¬ 2 ∥ 𝑥)) |
228 | 227 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) → ((𝐴‘𝑥) ∈ ℕ → ¬ 2 ∥ 𝑥)) |
229 | 228 | imp 445 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ (𝐴‘𝑥) ∈ ℕ) → ¬ 2 ∥
𝑥) |
230 | 204, 229 | syldan 487 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → ¬ 2 ∥ 𝑥) |
231 | | breq2 4657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑥 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑥)) |
232 | 231 | notbid 308 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑥 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑥)) |
233 | 232, 4 | elrab2 3366 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝐽 ↔ (𝑥 ∈ ℕ ∧ ¬ 2 ∥ 𝑥)) |
234 | 191, 230,
233 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → 𝑥 ∈ 𝐽) |
235 | 234 | adantlrr 757 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → 𝑥 ∈ 𝐽) |
236 | 235 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝑥 ∈ 𝐽) |
237 | | simprr 796 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) → ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) |
238 | 190, 236,
237 | r19.29af 3076 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) → 𝑥 ∈ 𝐽) |
239 | 238, 237 | jca 554 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) → (𝑥 ∈ 𝐽 ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) |
240 | 239 | ex 450 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) → (𝑥 ∈ 𝐽 ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵))) |
241 | 240 | reximdv2 3014 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (∃𝑥 ∈ ℕ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵 → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) |
242 | 241 | imp 445 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ ∃𝑥 ∈ ℕ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) |
243 | 242 | adantlr 751 |
. . . . . . 7
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑥 ∈ ℕ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) |
244 | 185, 243 | sylan2b 492 |
. . . . . 6
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) |
245 | 175, 244 | r19.29vva 3081 |
. . . . 5
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) → ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵) |
246 | 130, 245 | impbida 877 |
. . . 4
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → (∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵 ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵)) |
247 | 36, 246 | bitrd 268 |
. . 3
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → (𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵)) |
248 | 247 | ifbid 4108 |
. 2
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → if(𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))), 1, 0) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵, 1, 0)) |
249 | 13, 23, 248 | 3eqtrd 2660 |
1
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → ((𝐺‘𝐴)‘𝐵) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵, 1, 0)) |