Step | Hyp | Ref
| Expression |
1 | | eulerpart.j |
. . . . 5
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} |
2 | | eulerpart.f |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦
((2↑𝑦) · 𝑥)) |
3 | 1, 2 | oddpwdc 30416 |
. . . 4
⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ |
4 | | f1of1 6136 |
. . . 4
⊢ (𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ → 𝐹:(𝐽 × ℕ0)–1-1→ℕ) |
5 | 3, 4 | ax-mp 5 |
. . 3
⊢ 𝐹:(𝐽 × ℕ0)–1-1→ℕ |
6 | | eulerpartlemgh.1 |
. . . 4
⊢ 𝑈 = ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) |
7 | | iunss 4561 |
. . . . 5
⊢ (∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0) ↔
∀𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) |
8 | | inss2 3834 |
. . . . . . . 8
⊢ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ 𝐽 |
9 | 8 | sseli 3599 |
. . . . . . 7
⊢ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) → 𝑡 ∈ 𝐽) |
10 | 9 | snssd 4340 |
. . . . . 6
⊢ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) → {𝑡} ⊆ 𝐽) |
11 | | bitsss 15148 |
. . . . . 6
⊢
(bits‘(𝐴‘𝑡)) ⊆
ℕ0 |
12 | | xpss12 5225 |
. . . . . 6
⊢ (({𝑡} ⊆ 𝐽 ∧ (bits‘(𝐴‘𝑡)) ⊆ ℕ0) →
({𝑡} ×
(bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) |
13 | 10, 11, 12 | sylancl 694 |
. . . . 5
⊢ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) → ({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) |
14 | 7, 13 | mprgbir 2927 |
. . . 4
⊢ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0) |
15 | 6, 14 | eqsstri 3635 |
. . 3
⊢ 𝑈 ⊆ (𝐽 ×
ℕ0) |
16 | | f1ores 6151 |
. . 3
⊢ ((𝐹:(𝐽 × ℕ0)–1-1→ℕ ∧ 𝑈 ⊆ (𝐽 × ℕ0)) → (𝐹 ↾ 𝑈):𝑈–1-1-onto→(𝐹 “ 𝑈)) |
17 | 5, 15, 16 | mp2an 708 |
. 2
⊢ (𝐹 ↾ 𝑈):𝑈–1-1-onto→(𝐹 “ 𝑈) |
18 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) ∧ ((2↑𝑛) · 𝑡) = 𝑝) → ((2↑𝑛) · 𝑡) = 𝑝) |
19 | | 2nn 11185 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → 2 ∈ ℕ) |
21 | 11 | sseli 3599 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (bits‘(𝐴‘𝑡)) → 𝑛 ∈ ℕ0) |
22 | 21 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → 𝑛 ∈ ℕ0) |
23 | 20, 22 | nnexpcld 13030 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → (2↑𝑛) ∈ ℕ) |
24 | | simplr 792 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → 𝑡 ∈ ℕ) |
25 | 23, 24 | nnmulcld 11068 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → ((2↑𝑛) · 𝑡) ∈ ℕ) |
26 | 25 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) ∧ ((2↑𝑛) · 𝑡) = 𝑝) → ((2↑𝑛) · 𝑡) ∈ ℕ) |
27 | 18, 26 | eqeltrrd 2702 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) ∧ ((2↑𝑛) · 𝑡) = 𝑝) → 𝑝 ∈ ℕ) |
28 | 27 | exp31 630 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) → (𝑛 ∈ (bits‘(𝐴‘𝑡)) → (((2↑𝑛) · 𝑡) = 𝑝 → 𝑝 ∈ ℕ))) |
29 | 28 | rexlimdv 3030 |
. . . . . . . 8
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 → 𝑝 ∈ ℕ)) |
30 | 29 | rexlimdva 3031 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 → 𝑝 ∈ ℕ)) |
31 | 30 | pm4.71rd 667 |
. . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 ↔ (𝑝 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝))) |
32 | | rex0 3938 |
. . . . . . . . . . . . . . 15
⊢ ¬
∃𝑛 ∈ ∅
((2↑𝑛) · 𝑡) = 𝑝 |
33 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → 𝑡 ∈ ℕ) |
34 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) |
35 | | eulerpart.p |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑃 = {𝑓 ∈ (ℕ0
↑𝑚 ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧
Σ𝑘 ∈ ℕ
((𝑓‘𝑘) · 𝑘) = 𝑁)} |
36 | | eulerpart.o |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛} |
37 | | eulerpart.d |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1} |
38 | | eulerpart.h |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩
Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} |
39 | | eulerpart.m |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) |
40 | | eulerpart.r |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈
Fin} |
41 | | eulerpart.t |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑇 = {𝑓 ∈ (ℕ0
↑𝑚 ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽} |
42 | 35, 36, 37, 1, 2, 38, 39, 40, 41 | eulerpartlemt0 30431 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) ↔ (𝐴 ∈ (ℕ0
↑𝑚 ℕ) ∧ (◡𝐴 “ ℕ) ∈ Fin ∧ (◡𝐴 “ ℕ) ⊆ 𝐽)) |
43 | 42 | simp1bi 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴 ∈ (ℕ0
↑𝑚 ℕ)) |
44 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ∈ (ℕ0
↑𝑚 ℕ) → 𝐴:ℕ⟶ℕ0) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → 𝐴:ℕ⟶ℕ0) |
46 | 45 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → 𝐴:ℕ⟶ℕ0) |
47 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴:ℕ⟶ℕ0 →
𝐴 Fn
ℕ) |
48 | | elpreima 6337 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 Fn ℕ → (𝑡 ∈ (◡𝐴 “ ℕ) ↔ (𝑡 ∈ ℕ ∧ (𝐴‘𝑡) ∈ ℕ))) |
49 | 46, 47, 48 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → (𝑡 ∈ (◡𝐴 “ ℕ) ↔ (𝑡 ∈ ℕ ∧ (𝐴‘𝑡) ∈ ℕ))) |
50 | 34, 49 | mtbid 314 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → ¬ (𝑡 ∈ ℕ ∧ (𝐴‘𝑡) ∈ ℕ)) |
51 | | imnan 438 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℕ → ¬
(𝐴‘𝑡) ∈ ℕ) ↔ ¬ (𝑡 ∈ ℕ ∧ (𝐴‘𝑡) ∈ ℕ)) |
52 | 50, 51 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → (𝑡 ∈ ℕ → ¬
(𝐴‘𝑡) ∈ ℕ)) |
53 | 33, 52 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → ¬ (𝐴‘𝑡) ∈ ℕ) |
54 | 46, 33 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → (𝐴‘𝑡) ∈
ℕ0) |
55 | | elnn0 11294 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴‘𝑡) ∈ ℕ0 ↔ ((𝐴‘𝑡) ∈ ℕ ∨ (𝐴‘𝑡) = 0)) |
56 | 54, 55 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → ((𝐴‘𝑡) ∈ ℕ ∨ (𝐴‘𝑡) = 0)) |
57 | | orel1 397 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
(𝐴‘𝑡) ∈ ℕ → (((𝐴‘𝑡) ∈ ℕ ∨ (𝐴‘𝑡) = 0) → (𝐴‘𝑡) = 0)) |
58 | 53, 56, 57 | sylc 65 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → (𝐴‘𝑡) = 0) |
59 | 58 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → (bits‘(𝐴‘𝑡)) = (bits‘0)) |
60 | | 0bits 15161 |
. . . . . . . . . . . . . . . . 17
⊢
(bits‘0) = ∅ |
61 | 59, 60 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → (bits‘(𝐴‘𝑡)) = ∅) |
62 | 61 | rexeqdv 3145 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 ↔ ∃𝑛 ∈ ∅ ((2↑𝑛) · 𝑡) = 𝑝)) |
63 | 32, 62 | mtbiri 317 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ (◡𝐴 “ ℕ)) → ¬ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝) |
64 | 63 | ex 450 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) → (¬ 𝑡 ∈ (◡𝐴 “ ℕ) → ¬ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) |
65 | 64 | con4d 114 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 → 𝑡 ∈ (◡𝐴 “ ℕ))) |
66 | 65 | impr 649 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ℕ ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) → 𝑡 ∈ (◡𝐴 “ ℕ)) |
67 | | eldif 3584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ (ℕ ∖ 𝐽) ↔ (𝑡 ∈ ℕ ∧ ¬ 𝑡 ∈ 𝐽)) |
68 | 35, 36, 37, 1, 2, 38, 39, 40, 41 | eulerpartlemf 30432 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ (ℕ ∖ 𝐽)) → (𝐴‘𝑡) = 0) |
69 | 67, 68 | sylan2br 493 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ℕ ∧ ¬ 𝑡 ∈ 𝐽)) → (𝐴‘𝑡) = 0) |
70 | 69 | anassrs 680 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ 𝐽) → (𝐴‘𝑡) = 0) |
71 | 70 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ 𝐽) → (bits‘(𝐴‘𝑡)) = (bits‘0)) |
72 | 71, 60 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ 𝐽) → (bits‘(𝐴‘𝑡)) = ∅) |
73 | 72 | rexeqdv 3145 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ 𝐽) → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 ↔ ∃𝑛 ∈ ∅ ((2↑𝑛) · 𝑡) = 𝑝)) |
74 | 32, 73 | mtbiri 317 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) ∧ ¬ 𝑡 ∈ 𝐽) → ¬ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝) |
75 | 74 | ex 450 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) → (¬ 𝑡 ∈ 𝐽 → ¬ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) |
76 | 75 | con4d 114 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ 𝑡 ∈ ℕ) → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 → 𝑡 ∈ 𝐽)) |
77 | 76 | impr 649 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ℕ ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) → 𝑡 ∈ 𝐽) |
78 | 66, 77 | elind 3798 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ℕ ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) → 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)) |
79 | | simprr 796 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ℕ ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) → ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝) |
80 | 78, 79 | jca 554 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝑇 ∩ 𝑅) ∧ (𝑡 ∈ ℕ ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) → (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) |
81 | 80 | ex 450 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝑡 ∈ ℕ ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝) → (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) ∧ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝))) |
82 | 81 | reximdv2 3014 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 → ∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) |
83 | | ssrab2 3687 |
. . . . . . . . . 10
⊢ {𝑧 ∈ ℕ ∣ ¬ 2
∥ 𝑧} ⊆
ℕ |
84 | 1, 83 | eqsstri 3635 |
. . . . . . . . 9
⊢ 𝐽 ⊆
ℕ |
85 | 8, 84 | sstri 3612 |
. . . . . . . 8
⊢ ((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ ℕ |
86 | | ssrexv 3667 |
. . . . . . . 8
⊢ (((◡𝐴 “ ℕ) ∩ 𝐽) ⊆ ℕ → (∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) |
87 | 85, 86 | mp1i 13 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 → ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) |
88 | 82, 87 | impbid 202 |
. . . . . 6
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝 ↔ ∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) |
89 | 31, 88 | bitr3d 270 |
. . . . 5
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝑝 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝) ↔ ∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) |
90 | | eqeq2 2633 |
. . . . . . . 8
⊢ (𝑚 = 𝑝 → (((2↑𝑛) · 𝑡) = 𝑚 ↔ ((2↑𝑛) · 𝑡) = 𝑝)) |
91 | 90 | 2rexbidv 3057 |
. . . . . . 7
⊢ (𝑚 = 𝑝 → (∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚 ↔ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) |
92 | 91 | elrab 3363 |
. . . . . 6
⊢ (𝑝 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ↔ (𝑝 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) |
93 | 92 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑝 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} ↔ (𝑝 ∈ ℕ ∧ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝))) |
94 | 6 | imaeq2i 5464 |
. . . . . . . . 9
⊢ (𝐹 “ 𝑈) = (𝐹 “ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) |
95 | | imaiun 6503 |
. . . . . . . . 9
⊢ (𝐹 “ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)({𝑡} × (bits‘(𝐴‘𝑡)))) = ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))) |
96 | 94, 95 | eqtri 2644 |
. . . . . . . 8
⊢ (𝐹 “ 𝑈) = ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))) |
97 | 96 | eleq2i 2693 |
. . . . . . 7
⊢ (𝑝 ∈ (𝐹 “ 𝑈) ↔ 𝑝 ∈ ∪
𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡))))) |
98 | | eliun 4524 |
. . . . . . 7
⊢ (𝑝 ∈ ∪ 𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)(𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))) ↔ ∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)𝑝 ∈ (𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡))))) |
99 | | f1ofn 6138 |
. . . . . . . . . . . . 13
⊢ (𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ → 𝐹 Fn (𝐽 ×
ℕ0)) |
100 | 3, 99 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 𝐹 Fn (𝐽 ×
ℕ0) |
101 | | snssi 4339 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝐽 → {𝑡} ⊆ 𝐽) |
102 | 101, 11, 12 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ 𝐽 → ({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 ×
ℕ0)) |
103 | | ovelimab 6812 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn (𝐽 × ℕ0) ∧ ({𝑡} × (bits‘(𝐴‘𝑡))) ⊆ (𝐽 × ℕ0)) → (𝑝 ∈ (𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))) ↔ ∃𝑥 ∈ {𝑡}∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑝 = (𝑥𝐹𝑛))) |
104 | 100, 102,
103 | sylancr 695 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ 𝐽 → (𝑝 ∈ (𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))) ↔ ∃𝑥 ∈ {𝑡}∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑝 = (𝑥𝐹𝑛))) |
105 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑡 ∈ V |
106 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑡 → (𝑥𝐹𝑛) = (𝑡𝐹𝑛)) |
107 | 106 | eqeq2d 2632 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑡 → (𝑝 = (𝑥𝐹𝑛) ↔ 𝑝 = (𝑡𝐹𝑛))) |
108 | 107 | rexbidv 3052 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑡 → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑝 = (𝑥𝐹𝑛) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑝 = (𝑡𝐹𝑛))) |
109 | 105, 108 | rexsn 4223 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈
{𝑡}∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑝 = (𝑥𝐹𝑛) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑝 = (𝑡𝐹𝑛)) |
110 | 104, 109 | syl6bb 276 |
. . . . . . . . . 10
⊢ (𝑡 ∈ 𝐽 → (𝑝 ∈ (𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑝 = (𝑡𝐹𝑛))) |
111 | | df-ov 6653 |
. . . . . . . . . . . . . . 15
⊢ (𝑡𝐹𝑛) = (𝐹‘〈𝑡, 𝑛〉) |
112 | 111 | eqeq1i 2627 |
. . . . . . . . . . . . . 14
⊢ ((𝑡𝐹𝑛) = 𝑝 ↔ (𝐹‘〈𝑡, 𝑛〉) = 𝑝) |
113 | | eqcom 2629 |
. . . . . . . . . . . . . 14
⊢ ((𝑡𝐹𝑛) = 𝑝 ↔ 𝑝 = (𝑡𝐹𝑛)) |
114 | 112, 113 | bitr3i 266 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘〈𝑡, 𝑛〉) = 𝑝 ↔ 𝑝 = (𝑡𝐹𝑛)) |
115 | | opelxpi 5148 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0) →
〈𝑡, 𝑛〉 ∈ (𝐽 ×
ℕ0)) |
116 | 1, 2 | oddpwdcv 30417 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑡, 𝑛〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑡, 𝑛〉) = ((2↑(2nd
‘〈𝑡, 𝑛〉)) ·
(1st ‘〈𝑡, 𝑛〉))) |
117 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑛 ∈ V |
118 | 105, 117 | op2nd 7177 |
. . . . . . . . . . . . . . . . . 18
⊢
(2nd ‘〈𝑡, 𝑛〉) = 𝑛 |
119 | 118 | oveq2i 6661 |
. . . . . . . . . . . . . . . . 17
⊢
(2↑(2nd ‘〈𝑡, 𝑛〉)) = (2↑𝑛) |
120 | 105, 117 | op1st 7176 |
. . . . . . . . . . . . . . . . 17
⊢
(1st ‘〈𝑡, 𝑛〉) = 𝑡 |
121 | 119, 120 | oveq12i 6662 |
. . . . . . . . . . . . . . . 16
⊢
((2↑(2nd ‘〈𝑡, 𝑛〉)) · (1st
‘〈𝑡, 𝑛〉)) = ((2↑𝑛) · 𝑡) |
122 | 116, 121 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑡, 𝑛〉 ∈ (𝐽 × ℕ0) → (𝐹‘〈𝑡, 𝑛〉) = ((2↑𝑛) · 𝑡)) |
123 | 115, 122 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0) → (𝐹‘〈𝑡, 𝑛〉) = ((2↑𝑛) · 𝑡)) |
124 | 123 | eqeq1d 2624 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0) → ((𝐹‘〈𝑡, 𝑛〉) = 𝑝 ↔ ((2↑𝑛) · 𝑡) = 𝑝)) |
125 | 114, 124 | syl5bbr 274 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ ℕ0) → (𝑝 = (𝑡𝐹𝑛) ↔ ((2↑𝑛) · 𝑡) = 𝑝)) |
126 | 21, 125 | sylan2 491 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ 𝐽 ∧ 𝑛 ∈ (bits‘(𝐴‘𝑡))) → (𝑝 = (𝑡𝐹𝑛) ↔ ((2↑𝑛) · 𝑡) = 𝑝)) |
127 | 126 | rexbidva 3049 |
. . . . . . . . . 10
⊢ (𝑡 ∈ 𝐽 → (∃𝑛 ∈ (bits‘(𝐴‘𝑡))𝑝 = (𝑡𝐹𝑛) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) |
128 | 110, 127 | bitrd 268 |
. . . . . . . . 9
⊢ (𝑡 ∈ 𝐽 → (𝑝 ∈ (𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) |
129 | 9, 128 | syl 17 |
. . . . . . . 8
⊢ (𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽) → (𝑝 ∈ (𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))) ↔ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) |
130 | 129 | rexbiia 3040 |
. . . . . . 7
⊢
(∃𝑡 ∈
((◡𝐴 “ ℕ) ∩ 𝐽)𝑝 ∈ (𝐹 “ ({𝑡} × (bits‘(𝐴‘𝑡)))) ↔ ∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝) |
131 | 97, 98, 130 | 3bitri 286 |
. . . . . 6
⊢ (𝑝 ∈ (𝐹 “ 𝑈) ↔ ∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝) |
132 | 131 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑝 ∈ (𝐹 “ 𝑈) ↔ ∃𝑡 ∈ ((◡𝐴 “ ℕ) ∩ 𝐽)∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑝)) |
133 | 89, 93, 132 | 3bitr4rd 301 |
. . . 4
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝑝 ∈ (𝐹 “ 𝑈) ↔ 𝑝 ∈ {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) |
134 | 133 | eqrdv 2620 |
. . 3
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐹 “ 𝑈) = {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) |
135 | | f1oeq3 6129 |
. . 3
⊢ ((𝐹 “ 𝑈) = {𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚} → ((𝐹 ↾ 𝑈):𝑈–1-1-onto→(𝐹 “ 𝑈) ↔ (𝐹 ↾ 𝑈):𝑈–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) |
136 | 134, 135 | syl 17 |
. 2
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → ((𝐹 ↾ 𝑈):𝑈–1-1-onto→(𝐹 “ 𝑈) ↔ (𝐹 ↾ 𝑈):𝑈–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚})) |
137 | 17, 136 | mpbii 223 |
1
⊢ (𝐴 ∈ (𝑇 ∩ 𝑅) → (𝐹 ↾ 𝑈):𝑈–1-1-onto→{𝑚 ∈ ℕ ∣ ∃𝑡 ∈ ℕ ∃𝑛 ∈ (bits‘(𝐴‘𝑡))((2↑𝑛) · 𝑡) = 𝑚}) |