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 29762 |
. . . 4
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐺‘𝐴) = ((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))))) |
12 | 11 | fveq1d 6105 |
. . 3
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝐺‘𝐴)‘𝐵) = (((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))))‘𝐵)) |
13 | 12 | adantr 480 |
. 2
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → ((𝐺‘𝐴)‘𝐵) = (((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))))‘𝐵)) |
14 | | nnex 10903 |
. . . 4
⊢ ℕ
∈ V |
15 | 14 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → ℕ ∈
V) |
16 | | imassrn 5396 |
. . . . 5
⊢ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ⊆ ran 𝐹 |
17 | 4, 5 | oddpwdc 29743 |
. . . . . 6
⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ |
18 | | f1of 6050 |
. . . . . 6
⊢ (𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ → 𝐹:(𝐽 ×
ℕ0)⟶ℕ) |
19 | | frn 5966 |
. . . . . 6
⊢ (𝐹:(𝐽 × ℕ0)⟶ℕ
→ ran 𝐹 ⊆
ℕ) |
20 | 17, 18, 19 | mp2b 10 |
. . . . 5
⊢ ran 𝐹 ⊆
ℕ |
21 | 16, 20 | sstri 3577 |
. . . 4
⊢ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ⊆ ℕ |
22 | 21 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ⊆ ℕ) |
23 | | simpr 476 |
. . 3
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → 𝐵 ∈ ℕ) |
24 | | indfval 29406 |
. . 3
⊢ ((ℕ
∈ V ∧ (𝐹 “
(𝑀‘(bits ∘
(𝐴 ↾ 𝐽)))) ⊆ ℕ ∧ 𝐵 ∈ ℕ) →
(((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))))‘𝐵) = if(𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))), 1, 0)) |
25 | 15, 22, 23, 24 | syl3anc 1318 |
. 2
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) →
(((𝟭‘ℕ)‘(𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))))‘𝐵) = if(𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))), 1, 0)) |
26 | | ffn 5958 |
. . . . . 6
⊢ (𝐹:(𝐽 × ℕ0)⟶ℕ
→ 𝐹 Fn (𝐽 ×
ℕ0)) |
27 | 17, 18, 26 | mp2b 10 |
. . . . 5
⊢ 𝐹 Fn (𝐽 ×
ℕ0) |
28 | | inss1 3795 |
. . . . . . . 8
⊢
(𝒫 (𝐽
× ℕ0) ∩ Fin) ⊆ 𝒫 (𝐽 ×
ℕ0) |
29 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | eulerpartlemmf 29764 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (bits ∘ (𝐴 ↾ 𝐽)) ∈ 𝐻) |
30 | 1, 2, 3, 4, 5, 6, 7 | eulerpartlem1 29756 |
. . . . . . . . . . 11
⊢ 𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩
Fin) |
31 | | f1of 6050 |
. . . . . . . . . . 11
⊢ (𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
→ 𝑀:𝐻⟶(𝒫 (𝐽 × ℕ0) ∩
Fin)) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . 10
⊢ 𝑀:𝐻⟶(𝒫 (𝐽 × ℕ0) ∩
Fin) |
33 | 32 | ffvelrni 6266 |
. . . . . . . . 9
⊢ ((bits
∘ (𝐴 ↾ 𝐽)) ∈ 𝐻 → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩
Fin)) |
34 | 29, 33 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ∈ (𝒫 (𝐽 × ℕ0) ∩
Fin)) |
35 | 28, 34 | sseldi 3566 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ∈ 𝒫 (𝐽 ×
ℕ0)) |
36 | 35 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ∈ 𝒫 (𝐽 ×
ℕ0)) |
37 | 36 | elpwid 4118 |
. . . . 5
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ⊆ (𝐽 ×
ℕ0)) |
38 | | fvelimab 6163 |
. . . . 5
⊢ ((𝐹 Fn (𝐽 × ℕ0) ∧ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ⊆ (𝐽 × ℕ0)) → (𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ↔ ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵)) |
39 | 27, 37, 38 | sylancr 694 |
. . . 4
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → (𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ↔ ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵)) |
40 | | ssrab2 3650 |
. . . . . . . . . 10
⊢ {𝑧 ∈ ℕ ∣ ¬ 2
∥ 𝑧} ⊆
ℕ |
41 | 4, 40 | eqsstri 3598 |
. . . . . . . . 9
⊢ 𝐽 ⊆
ℕ |
42 | 7 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})) |
43 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 = (bits ∘ (𝐴 ↾ 𝐽)) → (𝑟‘𝑥) = ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)) |
44 | 43 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 = (bits ∘ (𝐴 ↾ 𝐽)) → (𝑦 ∈ (𝑟‘𝑥) ↔ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))) |
45 | 44 | anbi2d 736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = (bits ∘ (𝐴 ↾ 𝐽)) → ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥)) ↔ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)))) |
46 | 45 | opabbidv 4648 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = (bits ∘ (𝐴 ↾ 𝐽)) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))}) |
47 | 46 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑟 = (bits ∘ (𝐴 ↾ 𝐽))) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))}) |
48 | 14, 41 | ssexi 4731 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐽 ∈ V |
49 | | abid2 2732 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑦 ∣ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)} = ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) |
50 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((bits
∘ (𝐴 ↾ 𝐽))‘𝑥) ∈ V |
51 | 49, 50 | eqeltri 2684 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑦 ∣ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)} ∈ V |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝐽 → {𝑦 ∣ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)} ∈ V) |
53 | 48, 52 | opabex3 7038 |
. . . . . . . . . . . . . . . . 17
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))} ∈ V |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))} ∈ V) |
55 | 42, 47, 29, 54 | fvmptd 6197 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))}) |
56 | | simpl 472 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → 𝑥 = 𝑡) |
57 | 56 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → (𝑥 ∈ 𝐽 ↔ 𝑡 ∈ 𝐽)) |
58 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → 𝑦 = 𝑛) |
59 | 56 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) = ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡)) |
60 | 58, 59 | eleq12d 2682 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → (𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) ↔ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))) |
61 | 57, 60 | anbi12d 743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑛) → ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)) ↔ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡)))) |
62 | 61 | cbvopabv 4654 |
. . . . . . . . . . . . . . 15
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))} = {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))} |
63 | 55, 62 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) = {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))}) |
64 | 63 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ↔ 𝑤 ∈ {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))})) |
65 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | eulerpartlemt0 29758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0
↑𝑚 ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽)) |
66 | 65 | simp1bi 1069 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ (ℕ0
↑𝑚 ℕ)) |
67 | | nn0ex 11175 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
ℕ0 ∈ V |
68 | 67, 14 | elmap 7772 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ (ℕ0
↑𝑚 ℕ) ↔ 𝐴:ℕ⟶ℕ0) |
69 | 66, 68 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴:ℕ⟶ℕ0) |
70 | | ffun 5961 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴:ℕ⟶ℕ0 →
Fun 𝐴) |
71 | | funres 5843 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Fun
𝐴 → Fun (𝐴 ↾ 𝐽)) |
72 | 69, 70, 71 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → Fun (𝐴 ↾ 𝐽)) |
73 | 72 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ 𝐽) → Fun (𝐴 ↾ 𝐽)) |
74 | | fssres 5983 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴:ℕ⟶ℕ0 ∧
𝐽 ⊆ ℕ) →
(𝐴 ↾ 𝐽):𝐽⟶ℕ0) |
75 | 69, 41, 74 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐴 ↾ 𝐽):𝐽⟶ℕ0) |
76 | | fdm 5964 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ↾ 𝐽):𝐽⟶ℕ0 → dom
(𝐴 ↾ 𝐽) = 𝐽) |
77 | 76 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ↾ 𝐽):𝐽⟶ℕ0 → (𝑡 ∈ dom (𝐴 ↾ 𝐽) ↔ 𝑡 ∈ 𝐽)) |
78 | 75, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑡 ∈ dom (𝐴 ↾ 𝐽) ↔ 𝑡 ∈ 𝐽)) |
79 | 78 | biimpar 501 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ 𝐽) → 𝑡 ∈ dom (𝐴 ↾ 𝐽)) |
80 | | fvco 6184 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Fun
(𝐴 ↾ 𝐽) ∧ 𝑡 ∈ dom (𝐴 ↾ 𝐽)) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡) = (bits‘((𝐴 ↾ 𝐽)‘𝑡))) |
81 | 73, 79, 80 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ 𝐽) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡) = (bits‘((𝐴 ↾ 𝐽)‘𝑡))) |
82 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 ∈ 𝐽 → ((𝐴 ↾ 𝐽)‘𝑡) = (𝐴‘𝑡)) |
83 | 82 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 ∈ 𝐽 → (bits‘((𝐴 ↾ 𝐽)‘𝑡)) = (bits‘(𝐴‘𝑡))) |
84 | 83 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ 𝐽) → (bits‘((𝐴 ↾ 𝐽)‘𝑡)) = (bits‘(𝐴‘𝑡))) |
85 | 81, 84 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ 𝐽) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡) = (bits‘(𝐴‘𝑡))) |
86 | 85 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ 𝐽) → (𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡) ↔ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) |
87 | 86 | pm5.32da 671 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡)) ↔ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))))) |
88 | 87 | opabbidv 4648 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))} = {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))}) |
89 | 88 | eleq2d 2673 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑤 ∈ {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))} ↔ 𝑤 ∈ {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))})) |
90 | | elopab 4908 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))} ↔ ∃𝑡∃𝑛(𝑤 = 〈𝑡, 𝑛〉 ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))))) |
91 | 89, 90 | syl6bb 275 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑤 ∈ {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))} ↔ ∃𝑡∃𝑛(𝑤 = 〈𝑡, 𝑛〉 ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))))) |
92 | | ancom 465 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 = 〈𝑡, 𝑛〉 ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ↔ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) ∧ 𝑤 = 〈𝑡, 𝑛〉)) |
93 | | anass 679 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) ∧ 𝑤 = 〈𝑡, 𝑛〉) ↔ (𝑡 ∈ 𝐽 ∧ (𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉))) |
94 | 92, 93 | bitri 263 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 = 〈𝑡, 𝑛〉 ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ↔ (𝑡 ∈ 𝐽 ∧ (𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉))) |
95 | 94 | 2exbii 1765 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑡∃𝑛(𝑤 = 〈𝑡, 𝑛〉 ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ↔ ∃𝑡∃𝑛(𝑡 ∈ 𝐽 ∧ (𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉))) |
96 | | df-rex 2902 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑛 ∈
(bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉 ↔ ∃𝑛(𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉)) |
97 | 96 | anbi2i 726 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑡 ∈ 𝐽 ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉) ↔ (𝑡 ∈ 𝐽 ∧ ∃𝑛(𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉))) |
98 | 97 | exbii 1764 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑡(𝑡 ∈ 𝐽 ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉) ↔ ∃𝑡(𝑡 ∈ 𝐽 ∧ ∃𝑛(𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉))) |
99 | | df-rex 2902 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑡 ∈
𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉 ↔ ∃𝑡(𝑡 ∈ 𝐽 ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉)) |
100 | | exdistr 1906 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑡∃𝑛(𝑡 ∈ 𝐽 ∧ (𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉)) ↔ ∃𝑡(𝑡 ∈ 𝐽 ∧ ∃𝑛(𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉))) |
101 | 98, 99, 100 | 3bitr4i 291 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑡 ∈
𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉 ↔ ∃𝑡∃𝑛(𝑡 ∈ 𝐽 ∧ (𝑛 ∈ (bits‘(𝐴‘𝑡)) ∧ 𝑤 = 〈𝑡, 𝑛〉))) |
102 | 95, 101 | bitr4i 266 |
. . . . . . . . . . . . . 14
⊢
(∃𝑡∃𝑛(𝑤 = 〈𝑡, 𝑛〉 ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ↔ ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉) |
103 | 91, 102 | syl6bb 275 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑤 ∈ {〈𝑡, 𝑛〉 ∣ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑡))} ↔ ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉)) |
104 | 64, 103 | bitrd 267 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ↔ ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉)) |
105 | 104 | biimpa 500 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) → ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉) |
106 | 105 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) → ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉) |
107 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 〈𝑡, 𝑛〉 → (𝐹‘𝑤) = (𝐹‘〈𝑡, 𝑛〉)) |
108 | 107 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ∧ 𝑤 = 〈𝑡, 𝑛〉) → (𝐹‘𝑤) = (𝐹‘〈𝑡, 𝑛〉)) |
109 | | bitsss 14986 |
. . . . . . . . . . . . . . . . . . 19
⊢
(bits‘(𝐴‘𝑡)) ⊆
ℕ0 |
110 | 109 | sseli 3564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (bits‘(𝐴‘𝑡)) → 𝑛 ∈ ℕ0) |
111 | 110 | anim2i 591 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → (𝑡 ∈ 𝐽 ∧ 𝑛 ∈
ℕ0)) |
112 | 111 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ∧ 𝑤 = 〈𝑡, 𝑛〉) → (𝑡 ∈ 𝐽 ∧ 𝑛 ∈
ℕ0)) |
113 | | opelxp 5070 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑡, 𝑛〉 ∈ (𝐽 × ℕ0) ↔ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈
ℕ0)) |
114 | 4, 5 | oddpwdcv 29744 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑡, 𝑛〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑡, 𝑛〉) = ((2↑(2nd
‘〈𝑡, 𝑛〉)) ·
(1st ‘〈𝑡, 𝑛〉))) |
115 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑡 ∈ V |
116 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑛 ∈ V |
117 | 115, 116 | op2nd 7068 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘〈𝑡, 𝑛〉) = 𝑛 |
118 | 117 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . 19
⊢
(2↑(2nd ‘〈𝑡, 𝑛〉)) = (2↑𝑛) |
119 | 115, 116 | op1st 7067 |
. . . . . . . . . . . . . . . . . . 19
⊢
(1st ‘〈𝑡, 𝑛〉) = 𝑡 |
120 | 118, 119 | oveq12i 6561 |
. . . . . . . . . . . . . . . . . 18
⊢
((2↑(2nd ‘〈𝑡, 𝑛〉)) · (1st
‘〈𝑡, 𝑛〉)) = ((2↑𝑛) · 𝑡) |
121 | 114, 120 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑡, 𝑛〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑡, 𝑛〉) = ((2↑𝑛) · 𝑡)) |
122 | 113, 121 | sylbir 224 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0) → (𝐹‘〈𝑡, 𝑛〉) = ((2↑𝑛) · 𝑡)) |
123 | 112, 122 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ∧ 𝑤 = 〈𝑡, 𝑛〉) → (𝐹‘〈𝑡, 𝑛〉) = ((2↑𝑛) · 𝑡)) |
124 | 108, 123 | eqtr2d 2645 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) ∧ 𝑤 = 〈𝑡, 𝑛〉) → ((2↑𝑛) · 𝑡) = (𝐹‘𝑤)) |
125 | 124 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡)))) → (𝑤 = 〈𝑡, 𝑛〉 → ((2↑𝑛) · 𝑡) = (𝐹‘𝑤))) |
126 | 125 | anassrs 678 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ 𝑡 ∈ 𝐽) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → (𝑤 = 〈𝑡, 𝑛〉 → ((2↑𝑛) · 𝑡) = (𝐹‘𝑤))) |
127 | 126 | reximdva 3000 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ 𝑡 ∈ 𝐽) → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉 → ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤))) |
128 | 127 | reximdva 3000 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) → (∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑤 = 〈𝑡, 𝑛〉 → ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤))) |
129 | 106, 128 | mpd 15 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) → ∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤)) |
130 | | ssrexv 3630 |
. . . . . . . . 9
⊢ (𝐽 ⊆ ℕ →
(∃𝑡 ∈ 𝐽 ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤))) |
131 | 41, 129, 130 | mpsyl 66 |
. . . . . . . 8
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤)) |
132 | 131 | adantr 480 |
. . . . . . 7
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝐹‘𝑤) = 𝐵) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤)) |
133 | | eqeq2 2621 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑤) = 𝐵 → (((2↑𝑛) · 𝑡) = (𝐹‘𝑤) ↔ ((2↑𝑛) · 𝑡) = 𝐵)) |
134 | 133 | rexbidv 3034 |
. . . . . . . . 9
⊢ ((𝐹‘𝑤) = 𝐵 → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵)) |
135 | 134 | adantl 481 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝐹‘𝑤) = 𝐵) → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵)) |
136 | 135 | rexbidv 3034 |
. . . . . . 7
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝐹‘𝑤) = 𝐵) → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = (𝐹‘𝑤) ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵)) |
137 | 132, 136 | mpbid 221 |
. . . . . 6
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ 𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ∧ (𝐹‘𝑤) = 𝐵) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) |
138 | 137 | r19.29an 3059 |
. . . . 5
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵) → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) |
139 | | simp-5l 804 |
. . . . . . . 8
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝐴 ∈ (𝑇 ∩ 𝑅)) |
140 | | simpllr 795 |
. . . . . . . 8
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝑥 ∈ 𝐽) |
141 | | simplr 788 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝑦 ∈ (bits‘(𝐴‘𝑥))) |
142 | 72 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ 𝐽) → Fun (𝐴 ↾ 𝐽)) |
143 | 76 | eleq2d 2673 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ↾ 𝐽):𝐽⟶ℕ0 → (𝑥 ∈ dom (𝐴 ↾ 𝐽) ↔ 𝑥 ∈ 𝐽)) |
144 | 75, 143 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑥 ∈ dom (𝐴 ↾ 𝐽) ↔ 𝑥 ∈ 𝐽)) |
145 | 144 | biimpar 501 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ dom (𝐴 ↾ 𝐽)) |
146 | | fvco 6184 |
. . . . . . . . . . . 12
⊢ ((Fun
(𝐴 ↾ 𝐽) ∧ 𝑥 ∈ dom (𝐴 ↾ 𝐽)) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) = (bits‘((𝐴 ↾ 𝐽)‘𝑥))) |
147 | 142, 145,
146 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ 𝐽) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) = (bits‘((𝐴 ↾ 𝐽)‘𝑥))) |
148 | | fvres 6117 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐽 → ((𝐴 ↾ 𝐽)‘𝑥) = (𝐴‘𝑥)) |
149 | 148 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐽 → (bits‘((𝐴 ↾ 𝐽)‘𝑥)) = (bits‘(𝐴‘𝑥))) |
150 | 149 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ 𝐽) → (bits‘((𝐴 ↾ 𝐽)‘𝑥)) = (bits‘(𝐴‘𝑥))) |
151 | 147, 150 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ 𝐽) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) = (bits‘(𝐴‘𝑥))) |
152 | 139, 140,
151 | syl2anc 691 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥) = (bits‘(𝐴‘𝑥))) |
153 | 141, 152 | eleqtrrd 2691 |
. . . . . . . 8
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)) |
154 | 55 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (〈𝑥, 𝑦〉 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ↔ 〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))})) |
155 | | opabid 4907 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))} ↔ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))) |
156 | 154, 155 | syl6bb 275 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (〈𝑥, 𝑦〉 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ↔ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥)))) |
157 | 156 | biimpar 501 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ((bits ∘ (𝐴 ↾ 𝐽))‘𝑥))) → 〈𝑥, 𝑦〉 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) |
158 | 139, 140,
153, 157 | syl12anc 1316 |
. . . . . . 7
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 〈𝑥, 𝑦〉 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) |
159 | | simpr 476 |
. . . . . . . 8
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → ((2↑𝑦) · 𝑥) = 𝐵) |
160 | 37 | ad4antr 764 |
. . . . . . . . 9
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ⊆ (𝐽 ×
ℕ0)) |
161 | 160, 158 | sseldd 3569 |
. . . . . . . 8
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 〈𝑥, 𝑦〉 ∈ (𝐽 ×
ℕ0)) |
162 | | opeq1 4340 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑥 → 〈𝑡, 𝑦〉 = 〈𝑥, 𝑦〉) |
163 | 162 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑥 → (〈𝑡, 𝑦〉 ∈ (𝐽 × ℕ0) ↔
〈𝑥, 𝑦〉 ∈ (𝐽 ×
ℕ0))) |
164 | 162 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑥 → (𝐹‘〈𝑡, 𝑦〉) = (𝐹‘〈𝑥, 𝑦〉)) |
165 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑥 → ((2↑𝑦) · 𝑡) = ((2↑𝑦) · 𝑥)) |
166 | 164, 165 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑥 → ((𝐹‘〈𝑡, 𝑦〉) = ((2↑𝑦) · 𝑡) ↔ (𝐹‘〈𝑥, 𝑦〉) = ((2↑𝑦) · 𝑥))) |
167 | 163, 166 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑥 → ((〈𝑡, 𝑦〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑡, 𝑦〉) = ((2↑𝑦) · 𝑡)) ↔ (〈𝑥, 𝑦〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑥, 𝑦〉) = ((2↑𝑦) · 𝑥)))) |
168 | | opeq2 4341 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑦 → 〈𝑡, 𝑛〉 = 〈𝑡, 𝑦〉) |
169 | 168 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑦 → (〈𝑡, 𝑛〉 ∈ (𝐽 × ℕ0) ↔
〈𝑡, 𝑦〉 ∈ (𝐽 ×
ℕ0))) |
170 | 168 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑦 → (𝐹‘〈𝑡, 𝑛〉) = (𝐹‘〈𝑡, 𝑦〉)) |
171 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑦 → (2↑𝑛) = (2↑𝑦)) |
172 | 171 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑦 → ((2↑𝑛) · 𝑡) = ((2↑𝑦) · 𝑡)) |
173 | 170, 172 | eqeq12d 2625 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑦 → ((𝐹‘〈𝑡, 𝑛〉) = ((2↑𝑛) · 𝑡) ↔ (𝐹‘〈𝑡, 𝑦〉) = ((2↑𝑦) · 𝑡))) |
174 | 169, 173 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑦 → ((〈𝑡, 𝑛〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑡, 𝑛〉) = ((2↑𝑛) · 𝑡)) ↔ (〈𝑡, 𝑦〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑡, 𝑦〉) = ((2↑𝑦) · 𝑡)))) |
175 | 174, 121 | chvarv 2251 |
. . . . . . . . . 10
⊢
(〈𝑡, 𝑦〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑡, 𝑦〉) = ((2↑𝑦) · 𝑡)) |
176 | 167, 175 | chvarv 2251 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑥, 𝑦〉) = ((2↑𝑦) · 𝑥)) |
177 | | eqeq2 2621 |
. . . . . . . . . 10
⊢
(((2↑𝑦)
· 𝑥) = 𝐵 → ((𝐹‘〈𝑥, 𝑦〉) = ((2↑𝑦) · 𝑥) ↔ (𝐹‘〈𝑥, 𝑦〉) = 𝐵)) |
178 | 177 | biimpa 500 |
. . . . . . . . 9
⊢
((((2↑𝑦)
· 𝑥) = 𝐵 ∧ (𝐹‘〈𝑥, 𝑦〉) = ((2↑𝑦) · 𝑥)) → (𝐹‘〈𝑥, 𝑦〉) = 𝐵) |
179 | 176, 178 | sylan2 490 |
. . . . . . . 8
⊢
((((2↑𝑦)
· 𝑥) = 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ (𝐽 × ℕ0)) → (𝐹‘〈𝑥, 𝑦〉) = 𝐵) |
180 | 159, 161,
179 | syl2anc 691 |
. . . . . . 7
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → (𝐹‘〈𝑥, 𝑦〉) = 𝐵) |
181 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝐹‘𝑤) = (𝐹‘〈𝑥, 𝑦〉)) |
182 | 181 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ((𝐹‘𝑤) = 𝐵 ↔ (𝐹‘〈𝑥, 𝑦〉) = 𝐵)) |
183 | 182 | rspcev 3282 |
. . . . . . 7
⊢
((〈𝑥, 𝑦〉 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽))) ∧ (𝐹‘〈𝑥, 𝑦〉) = 𝐵) → ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵) |
184 | 158, 180,
183 | syl2anc 691 |
. . . . . 6
⊢
((((((𝐴 ∈
(𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵) |
185 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑥 → ((2↑𝑛) · 𝑡) = ((2↑𝑛) · 𝑥)) |
186 | 185 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑥 → (((2↑𝑛) · 𝑡) = 𝐵 ↔ ((2↑𝑛) · 𝑥) = 𝐵)) |
187 | 171 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑦 → ((2↑𝑛) · 𝑥) = ((2↑𝑦) · 𝑥)) |
188 | 187 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑦 → (((2↑𝑛) · 𝑥) = 𝐵 ↔ ((2↑𝑦) · 𝑥) = 𝐵)) |
189 | 186, 188 | sylan9bb 732 |
. . . . . . . . 9
⊢ ((𝑡 = 𝑥 ∧ 𝑛 = 𝑦) → (((2↑𝑛) · 𝑡) = 𝐵 ↔ ((2↑𝑦) · 𝑥) = 𝐵)) |
190 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑡 = 𝑥 ∧ 𝑛 = 𝑦) → 𝑡 = 𝑥) |
191 | 190 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑡 = 𝑥 ∧ 𝑛 = 𝑦) → (𝐴‘𝑡) = (𝐴‘𝑥)) |
192 | 191 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝑡 = 𝑥 ∧ 𝑛 = 𝑦) → (bits‘(𝐴‘𝑡)) = (bits‘(𝐴‘𝑥))) |
193 | 189, 192 | cbvrexdva2 3152 |
. . . . . . . 8
⊢ (𝑡 = 𝑥 → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵 ↔ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) |
194 | 193 | cbvrexv 3148 |
. . . . . . 7
⊢
(∃𝑡 ∈
ℕ ∃𝑛 ∈
(bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵 ↔ ∃𝑥 ∈ ℕ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) |
195 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦 𝐴 ∈ (𝑇 ∩ 𝑅) |
196 | | nfv 1830 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦 𝑥 ∈ ℕ |
197 | | nfre1 2988 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵 |
198 | 196, 197 | nfan 1816 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(𝑥 ∈ ℕ ∧
∃𝑦 ∈
(bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) |
199 | 195, 198 | nfan 1816 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) |
200 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → 𝑥 ∈ ℕ) |
201 | | n0i 3879 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (bits‘(𝐴‘𝑥)) → ¬ (bits‘(𝐴‘𝑥)) = ∅) |
202 | 201 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → ¬ (bits‘(𝐴‘𝑥)) = ∅) |
203 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴‘𝑥) = 0 → (bits‘(𝐴‘𝑥)) = (bits‘0)) |
204 | | 0bits 14999 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(bits‘0) = ∅ |
205 | 203, 204 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴‘𝑥) = 0 → (bits‘(𝐴‘𝑥)) = ∅) |
206 | 202, 205 | nsyl 134 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → ¬ (𝐴‘𝑥) = 0) |
207 | 69 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) → (𝐴‘𝑥) ∈
ℕ0) |
208 | 207 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → (𝐴‘𝑥) ∈
ℕ0) |
209 | | elnn0 11171 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴‘𝑥) ∈ ℕ0 ↔ ((𝐴‘𝑥) ∈ ℕ ∨ (𝐴‘𝑥) = 0)) |
210 | 208, 209 | sylib 207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → ((𝐴‘𝑥) ∈ ℕ ∨ (𝐴‘𝑥) = 0)) |
211 | 210 | orcomd 402 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → ((𝐴‘𝑥) = 0 ∨ (𝐴‘𝑥) ∈ ℕ)) |
212 | 211 | orcanai 950 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ¬ (𝐴‘𝑥) = 0) → (𝐴‘𝑥) ∈ ℕ) |
213 | 206, 212 | mpdan 699 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → (𝐴‘𝑥) ∈ ℕ) |
214 | 65 | simp3bi 1071 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (◡𝐴 “ ℕ) ⊆ 𝐽) |
215 | 214 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑛 ∈ (◡𝐴 “ ℕ)) → 𝑛 ∈ 𝐽) |
216 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = 𝑛 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑛)) |
217 | 216 | notbid 307 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = 𝑛 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑛)) |
218 | 217, 4 | elrab2 3333 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ 𝐽 ↔ (𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛)) |
219 | 218 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ 𝐽 → ¬ 2 ∥ 𝑛) |
220 | 215, 219 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑛 ∈ (◡𝐴 “ ℕ)) → ¬ 2 ∥
𝑛) |
221 | 220 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∀𝑛 ∈ (◡𝐴 “ ℕ) ¬ 2 ∥ 𝑛) |
222 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴:ℕ⟶ℕ0 →
𝐴 Fn
ℕ) |
223 | | elpreima 6245 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 Fn ℕ → (𝑛 ∈ (◡𝐴 “ ℕ) ↔ (𝑛 ∈ ℕ ∧ (𝐴‘𝑛) ∈ ℕ))) |
224 | 69, 222, 223 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑛 ∈ (◡𝐴 “ ℕ) ↔ (𝑛 ∈ ℕ ∧ (𝐴‘𝑛) ∈ ℕ))) |
225 | 224 | imbi1d 330 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝑛 ∈ (◡𝐴 “ ℕ) → ¬ 2 ∥
𝑛) ↔ ((𝑛 ∈ ℕ ∧ (𝐴‘𝑛) ∈ ℕ) → ¬ 2 ∥
𝑛))) |
226 | | impexp 461 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ℕ ∧ (𝐴‘𝑛) ∈ ℕ) → ¬ 2 ∥
𝑛) ↔ (𝑛 ∈ ℕ → ((𝐴‘𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛))) |
227 | 225, 226 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝑛 ∈ (◡𝐴 “ ℕ) → ¬ 2 ∥
𝑛) ↔ (𝑛 ∈ ℕ → ((𝐴‘𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛)))) |
228 | 227 | ralbidv2 2967 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (∀𝑛 ∈ (◡𝐴 “ ℕ) ¬ 2 ∥ 𝑛 ↔ ∀𝑛 ∈ ℕ ((𝐴‘𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛))) |
229 | 221, 228 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∀𝑛 ∈ ℕ ((𝐴‘𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛)) |
230 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑛 → (𝐴‘𝑥) = (𝐴‘𝑛)) |
231 | 230 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑛 → ((𝐴‘𝑥) ∈ ℕ ↔ (𝐴‘𝑛) ∈ ℕ)) |
232 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑛 → (2 ∥ 𝑥 ↔ 2 ∥ 𝑛)) |
233 | 232 | notbid 307 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑛 → (¬ 2 ∥ 𝑥 ↔ ¬ 2 ∥ 𝑛)) |
234 | 231, 233 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑛 → (((𝐴‘𝑥) ∈ ℕ → ¬ 2 ∥ 𝑥) ↔ ((𝐴‘𝑛) ∈ ℕ → ¬ 2 ∥ 𝑛))) |
235 | 234 | cbvralv 3147 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈
ℕ ((𝐴‘𝑥) ∈ ℕ → ¬ 2
∥ 𝑥) ↔
∀𝑛 ∈ ℕ
((𝐴‘𝑛) ∈ ℕ → ¬ 2
∥ 𝑛)) |
236 | 229, 235 | sylibr 223 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ∀𝑥 ∈ ℕ ((𝐴‘𝑥) ∈ ℕ → ¬ 2 ∥ 𝑥)) |
237 | 236 | r19.21bi 2916 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) → ((𝐴‘𝑥) ∈ ℕ → ¬ 2 ∥ 𝑥)) |
238 | 237 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ (𝐴‘𝑥) ∈ ℕ) → ¬ 2 ∥
𝑥) |
239 | 213, 238 | syldan 486 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → ¬ 2 ∥ 𝑥) |
240 | | breq2 4587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑥 → (2 ∥ 𝑧 ↔ 2 ∥ 𝑥)) |
241 | 240 | notbid 307 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑥 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑥)) |
242 | 241, 4 | elrab2 3333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝐽 ↔ (𝑥 ∈ ℕ ∧ ¬ 2 ∥ 𝑥)) |
243 | 200, 239,
242 | sylanbrc 695 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑥 ∈ ℕ) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → 𝑥 ∈ 𝐽) |
244 | 243 | adantlrr 753 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) → 𝑥 ∈ 𝐽) |
245 | 244 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) ∧ 𝑦 ∈ (bits‘(𝐴‘𝑥))) ∧ ((2↑𝑦) · 𝑥) = 𝐵) → 𝑥 ∈ 𝐽) |
246 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) → ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) |
247 | 199, 245,
246 | r19.29af 3058 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) → 𝑥 ∈ 𝐽) |
248 | 247, 246 | jca 553 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) → (𝑥 ∈ 𝐽 ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) |
249 | 248 | ex 449 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝑥 ∈ ℕ ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) → (𝑥 ∈ 𝐽 ∧ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵))) |
250 | 249 | reximdv2 2997 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (∃𝑥 ∈ ℕ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵 → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵)) |
251 | 250 | imp 444 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ ∃𝑥 ∈ ℕ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) |
252 | 251 | adantlr 747 |
. . . . . . 7
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑥 ∈ ℕ ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) |
253 | 194, 252 | sylan2b 491 |
. . . . . 6
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ (bits‘(𝐴‘𝑥))((2↑𝑦) · 𝑥) = 𝐵) |
254 | 184, 253 | r19.29vva 3062 |
. . . . 5
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵) → ∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵) |
255 | 138, 254 | impbida 873 |
. . . 4
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → (∃𝑤 ∈ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))(𝐹‘𝑤) = 𝐵 ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵)) |
256 | 39, 255 | bitrd 267 |
. . 3
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → (𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))) ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵)) |
257 | 256 | ifbid 4058 |
. 2
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → if(𝐵 ∈ (𝐹 “ (𝑀‘(bits ∘ (𝐴 ↾ 𝐽)))), 1, 0) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵, 1, 0)) |
258 | 13, 25, 257 | 3eqtrd 2648 |
1
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝐵 ∈ ℕ) → ((𝐺‘𝐴)‘𝐵) = if(∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝐵, 1, 0)) |